50 lines
No EOL
1.4 KiB
Text
50 lines
No EOL
1.4 KiB
Text
---- MODULE mutex_sweeping_badcfg ----
|
|
EXTENDS Integers, FiniteSets
|
|
CONSTANT N \* Number of processes
|
|
ASSUME N \in Nat \* N must be a natural number
|
|
ASSUME N > 1 \* Need at least 2 processes
|
|
|
|
VARIABLES
|
|
flag, \* Array of flags, one per process
|
|
turn \* Who's turn is it to enter critical section
|
|
|
|
Proc == 1..N \* N 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
|
|
/\ \E j \in Proc \ {i} : turn' = j \* Give turn to any other process
|
|
/\ UNCHANGED flag
|
|
|
|
Enter(i) == \* Process i enters critical section if it's their turn
|
|
/\ flag[i] = TRUE
|
|
/\ turn = i
|
|
/\ \A j \in Proc \ {i} : ~flag[j] \* No other process wants 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
|
|
==== |