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 :)