Hello again,
I have used your advice to further develop my invariant over the course of the last month and I have checked that this new invariant is an inductive invariant -- at least under a state constraint that caps an unbounded integer (with a reasonably high limit).
This new invariant seems much stronger than my initial attempt, but is nonetheless unable to be proven by TLAPS. Specifically, my new invariant is constituted of the conjunction of 9 invariants and type-correctness -- and TLAPS is unable to prove for two conjuncts (specifically Inv0 and Inv2) that assuming the entire invariant is correct for a step, that they hold in a subsequent state. Given that the invariant I am working with seems to be inductive after model checking, and that the algorithm seems straightforward to prove via behavioral reasoning, I am very curious as to what I may be missing in order to complete an inductive proof.
The specification containing the algorithm and my attempted proof is as follows:
---------------------------- MODULE AndersonMutex ---------------------------
EXTENDS Integers, TLAPS, FiniteSets
CONSTANT N, Limit
ASSUME NneqNULL == N \in Nat \ {0, 1}
ASSUME LimitDef == Limit \in Nat \ {0} /\ (Limit > N)
VARIABLES pc, L, flag, ticket
vars == <<pc, L, flag, ticket>>
ProcSet == 1..N
Lines == {"dw", "wr", "ex1", "ex2"}
\* L = N + 1
\* Flag[0] = TRUE
\* Flag[i] = FALSE, i != 0
\* Ticket_p = p
\*
\* dw: ticket[p] <- FetchAndAdd(L)
\* wr: await flag[ticket[p] % N]
\* ex1: flag[ticket[p] % N] <- FALSE
\* ex2: flag[(ticket[p] + 1) % N] <- TRUE
Init == /\ pc = [p \in ProcSet |-> "dw"]
/\ L = 0
/\ flag = [i \in 0..N-1 |-> IF i = 0 THEN TRUE ELSE FALSE]
/\ ticket = [p \in ProcSet |-> 0]
dw(p) == /\ pc[p] = "dw"
/\ pc' = [pc EXCEPT ![p] = "wr"]
/\ L' = L + 1
/\ ticket' = [ticket EXCEPT ![p] = L]
/\ UNCHANGED flag
wr(p) == /\ pc[p] = "wr"
/\ flag[ticket[p] % N]
/\ pc' = [pc EXCEPT ![p] = "ex1"]
/\ UNCHANGED <<L, flag, ticket>>
ex1(p) == /\ pc[p] = "ex1"
/\ pc' = [pc EXCEPT ![p] = "ex2"]
/\ flag' = [flag EXCEPT ![ticket[p] % N] = FALSE]
/\ UNCHANGED <<L, ticket>>
ex2(p) == /\ pc[p] = "ex2"
/\ pc' = [pc EXCEPT ![p] = "dw"]
/\ flag' = [flag EXCEPT ![(ticket[p] + 1) % N] = TRUE]
/\ UNCHANGED <<L, ticket>>
Step(p) == \/ dw(p)
\/ wr(p)
\/ ex1(p)
\/ ex2(p)
Next == \E p \in ProcSet : Step(p)
Spec == /\ Init
/\ [][Next]_vars
\* Limit state space by capping L
LStep(p) == Step(p) /\ (L < Limit)
LNext == \E p \in ProcSet : LStep(p)
LSpec == /\ Init
/\ [][LNext]_vars
\* Define type correctness, limited type correctness and mutual exclusion
TypeOK == /\ pc \in [ProcSet -> Lines]
/\ L \in Nat
/\ flag \in [0..(N-1) -> BOOLEAN]
/\ ticket \in [ProcSet -> Nat]
LTypeOK == /\ pc \in [ProcSet -> Lines]
/\ L \in 0..Limit
/\ flag \in [0..(N-1) -> BOOLEAN]
/\ ticket \in [ProcSet -> 0..Limit]
MutualExclusion ==
\A i, j \in ProcSet : i /= j => ~(pc[i] = "ex1" /\ pc[j] = "ex1")
\* Invariants
\* It is either the case that:
\* 1. L's flag is TRUE and all processes are in remainder.
\* 2. L's flag is TRUE and all processes are active, and the ticket of some active process is L's predecessor.
\* ---> Inv0
\* 3. L's flag is FALSE and the ticket of some active process is L's predecessor.
\* ---> Inv1
Inv0 == flag[L % N] => (\/ (\A p \in ProcSet : pc[p] = "dw")
\/ ((\A p \in ProcSet : pc[p] /= "dw") /\ (\E p \in ProcSet : ticket[p] = L - 1)))
Inv1 == (~flag[L % N]) => (\E p \in ProcSet : (pc[p] /= "dw" /\ ticket[p] = L - 1))
\* Any two distinct active processes wait on different flags.
Inv2 == \A p, q \in ProcSet : ((p /= q /\ pc[p] /= "dw" /\ pc[q] /= "dw") => (ticket[p] % N /= ticket[q] % N))
\* If a waiting process has FALSE flag, then there must be an active process with the predecessor ticket.
Inv3 == \A p \in ProcSet : ((pc[p] = "wr" /\ ~flag[ticket[p] % N])
=> (\E q \in ProcSet : pc[q] /= "dw" /\ ticket[q] = ticket[p] - 1))
\* If a process is in CS, then its flag is TRUE.
Inv4 == \A p \in ProcSet : pc[p] = "ex1" => flag[ticket[p] % N]
\* If a process is at E2, then there is no TRUE flag.
Inv5 == \A p \in ProcSet : pc[p] = "ex2" => (\A i \in DOMAIN flag : ~flag[i])
\* No two distinct flags are TRUE.
Inv6 == \A i, j \in DOMAIN flag : ~(i /= j /\ flag[i] /\ flag[j])
\* Any active ticket is lower than L, as its acquisition incremented L.
Inv7 == \A p \in ProcSet : pc[p] /= "dw" => ticket[p] < L
\*Inv7 == \A p \in ProcSet : ticket[p] < L
\* If no process is at E2, there is some TRUE flag.
Inv8 == (\A p \in ProcSet : pc[p] /= "ex2") => (\E i \in DOMAIN flag : flag[i])
\* No two distinct processes can be at E2, as no TRUE would be written yet.
Inv9 == \A p, q \in ProcSet : ~(p /= q /\ pc[p] = "ex2" /\ pc[q] = "ex2")
\* Inductive invariant
Inv == /\ TypeOK
/\ Inv0
/\ Inv1
/\ Inv2
/\ Inv3
/\ Inv4
/\ Inv5
/\ Inv6
/\ Inv7
/\ Inv8
/\ Inv9
ISpec == /\ Inv
/\ [][Next]_vars
\* Inductive invariant for limited state space, model checked for two and three processes for Limit = 17.
LInv == /\ LTypeOK
/\ Inv0
/\ Inv1
/\ Inv2
/\ Inv3
/\ Inv4
/\ Inv5
/\ Inv6
/\ Inv7
/\ Inv8
/\ Inv9
LISpec == /\ LInv
/\ [][LNext]_vars
\* Proofs
LEMMA InvMutexLemma == Inv => MutualExclusion
<1> USE NneqNULL DEF MutualExclusion, Inv, TypeOK, Inv2, Inv4, Inv6
<1>1. QED
PROOF OBVIOUS
\* PROOF: Successful
THEOREM TypeCorrectness == Spec => []TypeOK
<1> USE NneqNULL DEFS ProcSet, Lines, TypeOK
<1>1. Init => TypeOK
PROOF BY DEF Init
<1>2. TypeOK /\ [Next]_vars => TypeOK'
<2> SUFFICES ASSUME TypeOK,
[Next]_vars
PROVE TypeOK'
OBVIOUS
<2>1. (pc \in [ProcSet -> Lines])'
PROOF BY DEF Next, vars, Step, dw, wr, ex1, ex2
<2>2. (L \in Nat)'
PROOF BY DEF Next, vars, Step, dw, wr, ex1, ex2
<2>3. (flag \in [0..(N-1) -> BOOLEAN])'
PROOF BY DEF Next, vars, Step, dw, wr, ex1, ex2
<2>4. (ticket \in [ProcSet -> Nat])'
PROOF BY DEF Next, vars, Step, dw, wr, ex1, ex2
<2>5. QED
BY <2>1, <2>2, <2>3, <2>4 DEF TypeOK
<1>3. QED
PROOF BY <1>1, <1>2, PTL DEF Spec
\* PROOF: Successful
THEOREM Spec => []Inv
<1> USE NneqNULL DEFS ProcSet, Lines, Inv, Step, dw, wr, ex1, ex2
<1>1. Init => Inv
PROOF BY DEF Init, Inv0, Inv1, Inv2, Inv3, Inv4, Inv5, Inv6, Inv7, Inv8, Inv9, TypeOK
<1>2. Inv /\ [Next]_vars => Inv'
<2> SUFFICES ASSUME Inv /\ [Next]_vars
PROVE Inv'
OBVIOUS
<2>1. TypeOK'
PROOF BY DEF Next, vars, TypeOK
<2>2. Inv0'
PROOF OMITTED
\* PROOF BY DEF Next, vars, TypeOK, Inv0, Inv1, Inv2, Inv3, Inv4, Inv5, Inv6, Inv7, Inv8, Inv9, TypeOK
<2>3. Inv1'
PROOF BY DEF Next, vars, TypeOK, Inv0, Inv1
<2>4. Inv2'
PROOF OMITTED
\* PROOF BY DEF Next, vars, TypeOK, Inv0, Inv1, Inv2, Inv3, Inv4, Inv5, Inv6, Inv7, Inv8, Inv9, TypeOK
<2>5. Inv3'
PROOF BY DEF Next, vars, TypeOK, Inv0, Inv1, Inv2, Inv3
<2>6. Inv4'
PROOF BY DEF Next, vars, TypeOK, Inv2, Inv4
<2>7. Inv5'
PROOF BY DEF Next, vars, TypeOK, Inv4, Inv5, Inv6, Inv9
<2>8. Inv6'
PROOF BY DEF Next, vars, TypeOK, Inv5, Inv6
<2>9. Inv7'
PROOF BY DEF Next, vars, TypeOK, Inv7
<2>10. Inv8'
PROOF BY DEF Next, vars, TypeOK, Inv8
<2>11. Inv9'
PROOF BY DEF Next, vars, TypeOK, Inv4, Inv5, Inv9
<2>12. QED
BY <2>1, <2>10, <2>11, <2>2, <2>3, <2>4, <2>5, <2>6, <2>7, <2>8, <2>9 DEF Inv
<1>3. QED
PROOF BY <1>1, <1>2, PTL DEF Spec
\* PROOF: Failed, specifically <2>2 and <2>4
=============================================================================
I am fairly new to TLA+, and I would appreciate anybody's input on my improved proof attempt of the algorithm using TLAPS. Thank you very much for your suggestions.
Best regards,
Ugur Yavuz