Analysis of a PlusCal algorithm is sensitive to placement of labels

[Georgios Kafanas (gkaf)]

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.

[Paul Eipper]

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.

--
Paul Eipper

--
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/59e2207e-e272-4eaa-868c-a5d5c0b944ebn%40googlegroups.com.

[Felipe Oliveira Carvalho]

> I would expect that the presence of labels would not affect liveness properties. Am I missing something, or is this a bug?

The placement of labels very much affects liveness properties. In
PlusCal, every basic block is assumed to run atomically -- no
preemption is possible at positions that don't have a label. You can
think of labels as points where a lock is released-acquire on the pc
(program counter).

So in PlusCal preemption is much more coarse-grained than in x86
assembly. You have to go as granular as possible to get closer to what
a CPU does: able to preempt after any instruction, but if you go too
granular the state space explodes combinatorially. So placing the
labels is a very important aspect of using PlusCal.

And even though structured programming (avoiding gotos) simplifies
proof of sequential programs, it can make the proof of concurrent
programs harder because it obscures the mutations to the pc done by
your program and the CPU scheduling system (when it decides to put a
thread to sleep and resume execution of another).

--
Felipe

On Tue, Mar 26, 2024 at 8:33 AM Georgios Kafanas (gkaf)
<kafanas...@gmail.com> wrote:
>