Labels in TLA+/pluscal and mutexes

[Dana Kaban]

Hello,

  

I have read some 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:

Q1: 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.  

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

Q2: I want to be able to loop in an atomic fashion, but it appears that the label applies to a single iteration of the while loop. Is that correct? why? 
I discovered that by having the processes add tuples of {value, pc} to some shared sequence, where the value incremented from 1 to some n. and I saw interleaving writes of processes. adding mutex allows for one process to finish adding variables before another one begins.  

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

       

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 do:
L_Invalidate:
       if some other condition:
            entity_lock();
            cache_lock();
            call invalidate(verGentime); \* inside this procedure cache_unclock(); is called


            L_Gen_Version:
                   \* do something
                  entity_unlock();


       end if;

end while;

I was sure that it will never execute  L_Gen_Version without first executing L_Invalidate 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.

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

[Stephan Merz]

Hello Dana,

the precise rules on where labels can and cannot be placed are given in the PlusCal manual (section 3.7, with a summary in section 2.7). Although as you say, the idea of labels is to identify units of atomic execution, there are some constraints, essentially to ensure that the translation from PlusCal to TLA+ remains simple. Ultimately, the semantics of a PlusCal algorithm is given by its TLA+ translation. My answers to your individual questions are below.

On 15 Jun 2019, at 01:13, Dana Kaban <dana7...@gmail.com> 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+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
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.