Proving Mutual Exclusion of a simple algorithm using TLAPS

139 views
Skip to first unread message

Ugur Yagmur Yavuz

unread,
Jan 8, 2021, 11:47:42 AM1/8/21
to tlaplus
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 :)

Leslie Lamport

unread,
Jan 8, 2021, 1:48:25 PM1/8/21
to tlaplus
The first thing to do is check that your inductive invariant really is inductive.  Read this to find out how:

 
Leslie

Stephan Merz

unread,
Jan 9, 2021, 6:04:11 AM1/9/21
to tla...@googlegroups.com
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


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

Ugur Yagmur Yavuz

unread,
Feb 16, 2021, 8:45:09 PM2/16/21
to tlaplus
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

Stephan Merz

unread,
Feb 26, 2021, 11:37:48 AM2/26/21
to tla...@googlegroups.com
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

AndersonMutex.tla
Reply all
Reply to author
Forward
0 new messages