46 lines
No EOL
1.2 KiB
Text
46 lines
No EOL
1.2 KiB
Text
---- MODULE mutex ----
|
|
EXTENDS Integers
|
|
VARIABLES
|
|
flag, \* Array of flags, one per process
|
|
turn \* Who's turn is it to enter critical section
|
|
|
|
Proc == 1..2 \* Two processes
|
|
|
|
vars == <<flag, turn>>
|
|
|
|
Init ==
|
|
/\ flag = [i \in Proc |-> FALSE] \* No one wants to enter initially
|
|
/\ turn = 1 \* Process 1 goes first
|
|
|
|
Try(i) == \* Process i wants to enter critical section
|
|
/\ flag' = [flag EXCEPT ![i] = TRUE]
|
|
/\ UNCHANGED turn
|
|
|
|
Give(i) == \* Process i gives turn to other process
|
|
/\ flag[i] = TRUE
|
|
/\ turn' = 3 - i \* Switch between 1 and 2
|
|
/\ UNCHANGED flag
|
|
|
|
Enter(i) == \* Process i enters critical section if it's their turn
|
|
/\ flag[i] = TRUE
|
|
/\ turn = i
|
|
/\ ~flag[3-i] \* Other process doesn't want to enter
|
|
/\ UNCHANGED vars
|
|
|
|
Exit(i) == \* Process i leaves critical section
|
|
/\ flag' = [flag EXCEPT ![i] = FALSE]
|
|
/\ UNCHANGED turn
|
|
|
|
Next ==
|
|
\E i \in Proc : Try(i) \/ Give(i) \/ Enter(i) \/ Exit(i)
|
|
|
|
Spec == Init /\ [][Next]_vars
|
|
|
|
\* Type correctness invariant
|
|
TypeOK ==
|
|
/\ flag \in [Proc -> BOOLEAN]
|
|
/\ turn \in Proc
|
|
|
|
\* Safety: No two processes in critical section simultaneously
|
|
Mutex == [][\A i,j \in Proc : i # j => ~(Enter(i) /\ Enter(j))]_vars
|
|
==== |