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

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

=============================================================================

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

On 8 Jan 2021, at 19:48, Leslie Lamport <tlapl...@xxxxxxxxx> wrote:

The first thing to do is check that your inductive invariant really is inductive. Read this to find out how:

https://lamport.azurewebsites.net/tla/inductive-invariant.pdf

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+u...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a2c3a96f-bc21-4be2-8bc9-11fd7b4cc0ean%40googlegroups.com.