--------------------------------- MODULE UM ---------------------------------
(***************************************************************************)
(* This file contains the abstract program UM whose safety part is in      *)
(* Figure 4.2 of Section 4.2.2.1 of the book "A Science of Concurrent      *)
(* Programs" by Leslie Lamport.                                            *)
(*                                                                         *)
(* The atomic action that describes execution of one step of process p     *)
(* beginning with control at a label such as `wait' is represented by the  *)
(* action wait(p).  The value of pc(p) indicating control is at `wait' is  *)
(* written as the string "wait" in the TLA+ version.  (We could declare    *)
(* `wait' to be a constant and give anther name to the action wait(p), but *)
(* it's more convenient to use strings so we don't have to add assumptions *)
(* such as that `wait' doesn't equal `ncs'.                                *)
(*                                                                         *)
(* As usual, Init and Next are the initial-state predicate and step        *)
(* predicate of the program.                                               *)
(***************************************************************************)

EXTENDS Integers

VARIABLES x, pc
v == << x, pc >>

Procs == {0,1}

Init == /\ x = [p \in {0,1} |-> FALSE]
        /\ pc = [p \in Procs |-> "ncs"]

ncs(p) == /\ pc[p] = "ncs"
          /\ TRUE
          /\ pc' = [pc EXCEPT ![p] = "wait"]
          /\ x' = x

wait(p) == /\ pc[p] = "wait"
           /\ x' = [x EXCEPT ![p] = TRUE]
           /\ pc' = [pc EXCEPT ![p] = "w2"]

w2(p) == /\ pc[p] = "w2"
         /\ ~x[1-p]
         /\ pc' = [pc EXCEPT ![p] = "cs"]
         /\ x' = x

cs(p) == /\ pc[p] = "cs"
         /\ pc' = [pc EXCEPT ![p] = "exit"]
         /\ x' = x

exit(p) == /\ pc[p] = "exit"
           /\ x' = [x EXCEPT ![p] = FALSE]
           /\ pc' = [pc EXCEPT ![p] = "ncs"]

PNext(p) == ncs(p) \/ wait(p) \/ w2(p) \/ cs(p) \/ exit(p)

Next == \E p \in Procs : PNext(p)

UMSafe == Init /\ [][Next]_v

(***************************************************************************)
(* Here are the definitions of TypeOK and the inductive invariant of UM    *)
(* given in the book, which we give the name Inv.                          *)
(***************************************************************************)
TypeOK == /\ x \in [{0,1} -> BOOLEAN]
          /\ pc \in [{0,1} -> {"ncs", "wait", "w2", "cs", "exit"}]
          
Inv == /\ TypeOK
       /\ \A p \in {0,1} : /\ (pc[p] \in {"w2", "cs"}) => x[p]
                           /\ (pc[p] = "cs") => (pc[1-p] # "cs")
                           
(***************************************************************************)
(* We define Mutex to be formula (4.5) of the book, which is given there   *)
(* as the definition of mutual exclusion.  More precisely, the algorithm   *)
(* UM satisfies mutual exclusion iff Mutex is an invariant of UM.          *)
(***************************************************************************)
Mutex == \A p, q \in {0,1} : (p # q) => ({pc[p], pc[q]} # {"cs"})

(***************************************************************************)
(* TLAPS, the TLA+ proof checker, easily checks that Inv implies Mutex, so *)
(* the invariance of Inv implies that UM satisfies mutual exclusion.  The  *)
(* module TLAPS must be imported to use TLAPS.                             *)
(***************************************************************************)
INSTANCE TLAPS

THEOREM Inv => Mutex
BY DEF TypeOK, Inv, Mutex
----------------------------------------------------------------------------
(***************************************************************************)
(* The book defines UMLive to be formula (4.4), which is:                  *)
(*                                                                         *)
(*    (ENABLED <<PNext(p)>>_v) ~> <<PNext(p)>>_v                           *)
(*                                                                         *)
(* However, the TLA+ grammar allows the TLA formula F ~> G only if F and G *)
(* are both TLA+ temporal formula, which <<PNext(p)>>_v isn't.  So to      *)
(* write it, we must expand the definition of ~> .                         *)
(***************************************************************************)
UMLive == \A p \in Procs : []((ENABLED <<PNext(p)>>_v) => <><<PNext(p)>>_v) 

(***************************************************************************)
(* The abstract program UM with its liveness property is described by the  *)
(* TLA+ formula UMSafe /\ UMLive is deadlock free, meaning that it         *)
(* satisfies this property:                                                *)
(***************************************************************************)
DeadlockFree == (\E p \in Procs : pc[p] = "wait") 
                      ~> (\E p \in Procs : pc[p] = "cs")
                      
(***************************************************************************)
(* However, TLC cannot check if UMSafe /\ UMLive satisfies property        *)
(* DeadlockFree because it cannot check any liveness properties of a       *)
(* program with a liveness property of the form [](F => <><<A>>_v).  (As   *)
(* explained in the book, we don't write programs with such a liveness     *)
(* property.)                                                              *)
(***************************************************************************)                      

=============================================================================
\* Modification History
\* Last modified Fri Oct 11 13:20:53 CEST 2024 by lamport
\* Last modified Fri Oct 11 11:46:42 CEST 2024 by lblam
\* Created Sun Nov 05 10:32:54 CET 2023 by lamport
