[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Analysis of a PlusCal algorithm is sensitive to placement of labels
Indeed, the deadlock is related to `can_enter_critical_region`. Without the `e5` label, the following formula is produced:
```
e4(self) == /\ pc[self] = "e4"
/\ can_enter_critical_region' = [can_enter_critical_region EXCEPT ![self] = FALSE]
/\ higher_priority' = [higher_priority EXCEPT ![self] = { i \in Procs : i < self }]
/\ ~ can_enter_critical_region'[proc[self]]
/\ pc' = [pc EXCEPT ![self] = "e1"]
/\ UNCHANGED << lower_priority, proc >>
```
This formula causes the deadlock because of the condition on the next state `~ can_enter_critical_region'[proc[self]]`: the term does not allow the next state to change independently from `proc[self]` which awaits the change in `e9`.
This is expected expected behavior. From the PlusCal user’s Manual (v1.8):
PlusCal uses labels to describe the algorithm’s steps. However, you can omit the labels and let the PlusCal translator add them as necessary. You are likely to do this only for uniprocess (sequential) algorithms, where the partitioning of the computation into steps does not affect
the values computed [...] For multiprocess (concurrent) algorithms, you will probably want to specify the grain of atomicity explicitly.
On Thursday, March 28, 2024 at 9:14:57 AM UTC+1 Paul Eipper wrote:
Did you check the generated TLA+ code? I assume it has something to do with the "can_enter_critical_region" using the primed vs not primed output.
I am trying to implement the 1BitNProcMutex from the PlusCal tutorial session 8, without using a goto statement. However, the resulting algorithm is very sensitive to the labeling of the statements.
This is the module I am using:
```
----------------------------- MODULE OneBitNProcMutex -----------------------------
EXTENDS Integers, TLC
CONSTANT N
ASSUME N \in Nat
Procs == 0..(N-1)
(*
--algorithm 1BitNProcMutex {
variables can_enter_critical_region = [i \in Procs |-> FALSE] ;
process (P \in Procs)
variable higher_priority = {}; lower_priority = {}; proc = self;
{ ncs: while (TRUE) {
skip ;
enter: while ( ~ can_enter_critical_region[self] ) {
can_enter_critical_region[self] := TRUE ;
higher_priority := { i \in Procs : i < self } ;
e1: while ( higher_priority /= {} /\ can_enter_critical_region[self] ) {
e2: with ( q \in higher_priority ) {
proc := q;
};
e3: if ( can_enter_critical_region[proc] ) {
e4: can_enter_critical_region[self] := FALSE ;
e5: higher_priority := { i \in Procs : i < self } ;
await ~ can_enter_critical_region[proc] ;
} else e6: {
higher_priority := higher_priority \ {proc} ;
} ;
};
} ;
lower_priority := { i \in Procs : i > self } ;
e7: while ( lower_priority /= {} ) {
e8: with ( q \in lower_priority ) {
proc := q ;
} ;
e9: await ~ can_enter_critical_region[proc] ;
lower_priority := lower_priority \ {proc};
} ;
cs: skip ;
exit: can_enter_critical_region[self] := FALSE ;
}
}
}
*)
MutualExclusion == \A i, j \in Procs : (i /= j) => ~ ((pc[i] = "cs") /\ (pc[j] = "cs"))
=============================================================================
```
The model is tested with N=2 and MutualExclusion added to the list of invariant properties. When removing the label e5, the TLA+ toolbox reports a deadlock.
I would expect that the presence of labels would not affect liveness properties. Am I missing something, or is this a bug?
The version of the TLA+ Toolbox used is 1.7.1.
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9820668f-3175-4a9b-b63d-ea2ffcb0eca5n%40googlegroups.com.