Re: [tlaplus] Labels in TLA+/pluscal and mutexes

On 15 Jun 2019, at 01:13, Dana Kaban <dana7kaban7@xxxxxxxxx> wrote:

Hello,

I have read a lot of documentation and ran experiments in the TLA+ toolbox to test how labels work.
I know that it meant to identify units of atomic execution, but I discovered that it doesn't work entirely as I expect.

Here are a few cases I would like to understand:

Assume I have two fair processes A and B, and that I have a globally defined seq cache = <<>>.
Each process has label_1 that performs an operation on the cache.

Q1: what does atomicity mean in this case? can both processes access the cache at the same time?

Parallel processes execute in interleaved fashion so their steps will never occur simultaneously.

Q2: I want to be able to loop in an atomic fashion, why does the label apply to a single iteration of the while loop?

The labeling rules require the while statement to be labeled: the translation corresponds to inserting a jump back to the test of the while loop at the end of the loop body. Some loops may be sufficiently simple that you may want to consider them to be performed atomically at a high level of abstraction, such as broadcasting a message to a set of destination processes. In these cases, it is often possible (and easier) to use TLA+ expressions instead of loops, i.e. write something like

network := [ p,q \in Procs |->

IF p = self /\ q \in destinations

THEN Append(network[p,q], msg)

ELSE network[p,q] ]

rather than

bcast:

while (destinations # {}) {

with (d \in destinations) {

destinations := destinations \ {d};

network[self,d] := Append(@, msg)

}

In particular, the TLA+ version generates only one successor state whereas the PlusCal version generates many, so model checking is much quicker with the TLA+ version. But you should be careful about what the right unit of atomicity is for your level of abstraction.

Q3: If a process contains for example 3 labels, lb1, lb2, lb3, will that process attempt to execute them sequentially?

Control flow within a process is sequential (ignoring jumps and loops) so if the three labels occur in that order then they will be executed one after another. Check the TLA+ generated from the PlusCal algorithm to understand how control flow is represented.

I implemented mutex to lock resources with the intent that I can lock a resource in one label and release in the next label (to mimic a prepare phase on an entity), but I discovered that sometimes the process skips the first label and goes directly to the second label. For example:

process A variables ... While_label: while some condition: L_Invalidate: if some condition: entity_lock(); cache_lock(); call invalidate(verGentime); L_Gen_Version: \* do something cache_unlock(); entity_unlock(); end if;

I was sure that it will never skip to L_Gen_Version since it is defined within the if statement. However, I saw that the process translated to TLA+ as follow: A = While_label \/ L_Gen_Version, and sometimes when the condition of the if is not satisfied it jumps to L_Gen_Version.
I am very confused by this behavior.

Since there is no statement between `While_label' and `L_Invalidate' the second label is ignored. If you really want to insert a yield point after the test of the while loop, insert a skip statement in front of the second label. Again, look at the TLA+ translation: you'll see that control flow doesn't "jump" from the check of the while loop to label `L_Gen_Version' but that the PlusCal code between `L_Invalidate' and `L_Gen_Version' is represented in the TLA+ action called While_label.

Regards,

Stephan

Clarification of the labels behavior will be greatly appreciated.

If it is important I implemented mutex as following:

macro cache_lock() begin await c_lock = 0; c_lock := 1; end macro; macro cache_unlock() begin c_lock := 0; end macro;

Thanks,
Dana

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/3a3f76a2-b21d-4ff1-97bf-21e7449d8107%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.