[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

# Re: [tlaplus] Proving Mutual Exclusion of a simple algorithm using TLAPS

 Hello,you did the right thing when you used TLC to get confident that your invariant is indeed inductive. However, even if you have an inductive invariant, there is no guarantee that the prover will be able to show automatically that it is preserved by the next-state relation. If it isn't, you have to decompose the proof and find out what is needed.I did this for one of the conjuncts whose preservation is not proved automatically (Inv0') and found that the automatic proof fails for two actions. I then looked at one of those actions (ex2) and tried to understand why the invariant is preserved. Without knowing the algorithm or its pencil-and-paper proof, this took me quite a while even on paper. The essence is a counting argument, and if there is any automatic theorem prover that can find this proof, I'd like to hear about it.Attached is the TLAPS proof of that particular step. (It could probably be shortened somewhat.) The proof uses two unproved lemmas:- The first one asserts the existence of a minimal element in any set of natural numbers. This is fairly easy to prove from the theorems in the library module NaturalsInduction, and should indeed be provided by this module.- The second one asserts that for two positive natural numbers m and M such that m \in M-N+1 .. M-1 (where N is the constant from the specification), one cannot have m % N = M % N. Unfortunately, Z3 does not seem to know this (modulus arithmetic is not part of the decision procedure underlying Z3 but is handled heuristically).I don't know if the remaining steps are equally hard, you may want to give it a try if you are interested.Regards,Stephan -- 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.

Attachment: AndersonMutex.tla
Description: Binary data

 On 17 Feb 2021, at 02:45, Ugur Yagmur Yavuz wrote: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, FiniteSetsCONSTANT N, LimitASSUME NneqNULL == N \in Nat \ {0, 1} ASSUME LimitDef == Limit \in Nat \ {0} /\ (Limit > N)VARIABLES pc, L, flag, ticketvars == <>ProcSet == 1..NLines == {"dw", "wr", "ex1", "ex2"}\* L = N + 1\* Flag = 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 <>            ex1(p) == /\ pc[p] = "ex1"          /\ pc' = [pc EXCEPT ![p] = "ex2"]          /\ flag' = [flag EXCEPT ![ticket[p] % N] = FALSE]          /\ UNCHANGED <>             ex2(p) == /\ pc[p] = "ex2"          /\ pc' = [pc EXCEPT ![p] = "dw"]          /\ flag' = [flag EXCEPT ![(ticket[p] + 1) % N] = TRUE]          /\ UNCHANGED <>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 LLStep(p) == Step(p) /\ (L < Limit)LNext == \E p \in ProcSet : LStep(p) LSpec == /\ Init         /\ [][LNext]_vars\* Define type correctness, limited type correctness and mutual exclusionTypeOK == /\ 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 invariantInv  == /\ 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         \* ProofsLEMMA InvMutexLemma == Inv => MutualExclusion<1> USE NneqNULL DEF MutualExclusion, Inv, TypeOK, Inv2, Inv4, Inv6<1>1. QED  PROOF OBVIOUS\* PROOF: SuccessfulTHEOREM 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: SuccessfulTHEOREM 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 YavuzOn 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 => []TypeOKSuppose 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 SpecThis 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,StephanOn 8 Jan 2021, at 19:48, Leslie Lamport wrote:The first thing to do is check that your inductive invariant really is inductive.  Read this to find out how: LeslieOn 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, FiniteSetsCONSTANT NASSUME NneqNULL == N \in Nat \ {0}Procs == 1..NVARIABLES L, flag, pc, ticketvars == << 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' = flagwaiting(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))\* ShorthandsInRemainder(i) == pc[i] = "remainder"Trying(i) == pc[i] \in {"doorway", "waiting"}Waiting(i) == pc[i] = "waiting"InCS(i) == pc[i] = "cs"\* Type correctnessTypeOK == /\ 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 SpecThis 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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a2c3a96f-bc21-4be2-8bc9-11fd7b4cc0ean%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/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.