[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Labels in TLA+/pluscal and mutexes

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?

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? 

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

while some condition:
if some condition:
            call invalidate

\* do something

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.

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;
:= 1;
end macro;
macro cache_unlock
() begin
:= 0;
end macro;


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.