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
On Saturday, 9 January 2021 at 14:04:11 UTC+3 Stephan Merz wrote:
Following up on Leslie's advice, here is a hint: your invariant doesn't refer at all to the variable L, so it would seem that L plays no role in the correctness argument. Do you really believe that this is the case? Also, it looks like you need to gather more information about values of tickets that different processes hold.
One bit of advice on the structure of the proof itself: since you've already proved that TypeOK is an invariant, you probably want to use it in the remainder of the proof. So let's give that theorem a name:
THEOREM TypeCorrect == Spec => []TypeOK
Suppose now that you want to prove that CSisFlag is an invariant, assuming type correctness. You can set up that proof as follows:
THEOREM FlagCondition == Spec => []CSisFlag <1>1. Init => CSisFlag <1>2. TypeOK /\ CSisFlag /\ [Next]_vars => CSisFlag' <1>. QED BY <1>1, <1>2, TypeCorrect, PTL DEF Spec
This proof should be accepted by TLAPS (of course you're still left with proving <1>1 and <1>2). Note that we simply introduce TypeOK as an additional hypothesis in step <1>2 and justify this in the QED step by appealing to the previous theorem. You could also use TypeOK in step <1>1 but it's certainly not needed there.
Hope this helps, Stephan The first thing to do is check that your inductive invariant really is inductive. Read this to find out how:
Leslie
On Friday, January 8, 2021 at 8:47:42 AM UTC-8 uguryag...@ gmail.com wrote: 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 :)
-- 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/1c9424ed-1eb5-449b-99fd-064987e317f2n%40googlegroups.com.
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/2BB6CDD6-7E28-4680-848A-8F49479372E7%40gmail.com.
|