Hello everyone, I am fairly new to TLA+ and TLAPS, and I have been trying to improve my proficiency in both by proving the mutual exclusion property of a simple algorithm, Anderson's algorithm, using TLAPS.

The algorithm is as follows in PlusCal (please excuse the non-monospaced font):

(***

--algorithm Anderson

{ variables L = 0, flag = [i \in 0..N-1 |-> IF i = 0 THEN TRUE ELSE FALSE] ;

fair process (p \in Procs)

variables ticket = 0 ;

{ remainder:- while (TRUE)

{ doorway: ticket := L;

L := (L + 1) % N;

waiting: await flag[ticket % N] = TRUE;

cs: skip;

exit1: flag[ticket % N] := FALSE;

exit2: flag[(ticket + 1) % N] := TRUE;

}

}

}

***)

And it is translated into TLA+ as follows, with additional expressions about the section of the algorithm which the process is in and a type correctness formula at the very end:

EXTENDS Integers, TLC, TLAPS, FiniteSets

CONSTANT N

ASSUME NneqNULL == N \in Nat \ {0}

Procs == 1..N

VARIABLES L, flag, pc, ticket

vars == << L, flag, pc, ticket >>

ProcSet == (Procs)

Init == (* Global variables *)

/\ L = 0

/\ flag = [i \in 0..N-1 |-> IF i = 0 THEN TRUE ELSE FALSE]

(* Process p *)

/\ ticket = [self \in Procs |-> 0]

/\ pc = [self \in ProcSet |-> "remainder"]

remainder(self) == /\ pc[self] = "remainder"

/\ pc' = [pc EXCEPT ![self] = "doorway"]

/\ UNCHANGED << L, flag, ticket >>

doorway(self) == /\ pc[self] = "doorway"

/\ ticket' = [ticket EXCEPT ![self] = L]

/\ L' = (L + 1) % N

/\ pc' = [pc EXCEPT ![self] = "waiting"]

/\ flag' = flag

waiting(self) == /\ pc[self] = "waiting"

/\ flag[ticket[self] % N] = TRUE

/\ pc' = [pc EXCEPT ![self] = "cs"]

/\ UNCHANGED << L, flag, ticket >>

cs(self) == /\ pc[self] = "cs"

/\ TRUE

/\ pc' = [pc EXCEPT ![self] = "exit1"]

/\ UNCHANGED << L, flag, ticket >>

exit1(self) == /\ pc[self] = "exit1"

/\ flag' = [flag EXCEPT ![ticket[self] % N] = FALSE]

/\ pc' = [pc EXCEPT ![self] = "exit2"]

/\ UNCHANGED << L, ticket >>

exit2(self) == /\ pc[self] = "exit2"

/\ flag' = [flag EXCEPT ![(ticket[self] + 1) % N] = TRUE]

/\ pc' = [pc EXCEPT ![self] = "remainder"]

/\ UNCHANGED << L, ticket >>

p(self) == remainder(self) \/ doorway(self) \/ waiting(self) \/ cs(self)

\/ exit1(self) \/ exit2(self)

Next == (\E self \in Procs: p(self))

Spec == /\ Init /\ [][Next]_vars

/\ \A self \in Procs : WF_vars((pc[self] # "remainder") /\ p(self))

\* Shorthands

InRemainder(i) == pc[i] = "remainder"

Trying(i) == pc[i] \in {"doorway", "waiting"}

Waiting(i) == pc[i] = "waiting"

InCS(i) == pc[i] = "cs"

\* Type correctness

TypeOK == /\ L \in 0..(N-1)

/\ flag \in [0..(N-1) -> BOOLEAN]

/\ ticket \in [Procs -> 0..(N-1)]

/\ pc \in [Procs -> {"remainder", "doorway", "waiting", "cs",

"exit1", "exit2"}]

And finally, mutual exclusion can then be expressed as follows:

MutualExclusion == \A i, j \in Procs : ( i # j ) => ~ ( /\ InCS(i)

/\ InCS(j) )

Normally, I would personally prove that this algorithm respects mutual exclusion by proving that 1) being in the CS implies that the flag indexed at the ticket corresponding to the process is True, and 2) that at most one flag is true at any given time. These two can be translated into the two following formulae in TLA+:

CSisFlag == \A i \in Procs : InCS(i) => (flag[ticket[i] % N] = TRUE)

MaxOneFlag == \A x, y \in 0..(N-1) : (/\ flag[x] = TRUE

/\ flag[y] = TRUE) => (x = y)

Having read the hyperbook, I am aware that the way to prove a desired property (i.e. THEOREM Spec => Property) is by finding an invariant Inv, then proving that: Init => Inv; Inv /\ [Next]_vars => Inv'; Inv => Property. Given how I would personally prove the property, I thought that setting **Inv == TypeOK /\ CSisFlag /\ MaxOneFlag**, would be sufficient. This was not the case, as the proof failed. Then I tried to break this invariant into its three pieces, and then to prove them separately. For instance, gradually decomposing the proof, I was able to prove TypeOK correct as follows:

THEOREM Spec => []TypeOK

<1> USE NneqNULL DEFS Procs, ProcSet

<1>1 Init => TypeOK

PROOF BY DEF Init, TypeOK

<1>2 TypeOK /\ [Next]_vars => TypeOK'

<2> SUFFICES ASSUME TypeOK,

[Next]_vars

PROVE TypeOK'

OBVIOUS

<2>1. ASSUME NEW self \in Procs,

remainder(self)

PROVE TypeOK'

PROOF BY <2>1 DEF Next, p, TypeOK, remainder

<2>2. ASSUME NEW self \in Procs,

doorway(self)

PROVE TypeOK'

PROOF BY <2>2 DEF Next, p, TypeOK, doorway

<2>3. ASSUME NEW self \in Procs,

waiting(self)

PROVE TypeOK'

PROOF BY <2>3 DEF Next, p, TypeOK, waiting

<2>4. ASSUME NEW self \in Procs,

cs(self)

PROVE TypeOK'

PROOF BY <2>4 DEF Next, p, TypeOK, cs

<2>5. ASSUME NEW self \in Procs,

exit1(self)

PROVE TypeOK'

PROOF BY <2>5 DEF Next, p, TypeOK, exit1

<2>6. ASSUME NEW self \in Procs,

exit2(self)

PROVE TypeOK'

PROOF BY <2>6 DEF Next, p, TypeOK, exit2

<2>7. CASE UNCHANGED vars

PROOF BY <2>7 DEF Next, p, TypeOK, vars

<2>8. QED

BY <2>1, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7 DEF Next, p

<1>3 QED

PROOF BY <1>1, <1>2, PTL DEF Spec

This led me to believe that I would be able to prove CSisFlag and MaxOneFlag very similarly, but they fail at <2>5 and <2>6 respectively (with all other parts working smoothly). I was unable to figure out what is missing, and I would appreciate others' inputs regarding the proofs of these invariants, and of mutual exclusion. Apologies for the lengthy post and thank you for any assistance :)