/
LamportMutex.tla
184 lines (159 loc) · 8.71 KB
/
LamportMutex.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
--------------------------- MODULE LamportMutex ----------------------------
(***************************************************************************)
(* TLA+ specification of Lamport's distributed mutual-exclusion algorithm *)
(* that appeared as an example in *)
(* L. Lamport: Time, Clocks and the Ordering of Events in a Distributed *)
(* System. CACM 21(7):558-565, 1978. *)
(***************************************************************************)
EXTENDS Naturals, Sequences
(***************************************************************************)
(* The parameter N represents the number of processes. *)
(* The parameter maxClock is used only for model checking in order to *)
(* keep the state space finite. *)
(***************************************************************************)
CONSTANT N, maxClock
ASSUME NType == N \in Nat
ASSUME maxClockType == maxClock \in Nat
Proc == 1 .. N
Clock == Nat \ {0}
(***************************************************************************)
(* For model checking, add ClockConstraint as a state constraint to ensure *)
(* a finite state space and override the definition of Clock by *)
(* 1 .. maxClock+1 so that TLC can evaluate the definition of Message. *)
(***************************************************************************)
VARIABLES
clock, \* local clock of each process
req, \* requests received from processes (clock transmitted with request)
ack, \* acknowledgements received from processes
network, \* messages sent but not yet received
crit \* set of processes in critical section
(***************************************************************************)
(* Messages used in the algorithm. *)
(***************************************************************************)
ReqMessage(c) == [type |-> "req", clock |-> c]
AckMessage == [type |-> "ack", clock |-> 0]
RelMessage == [type |-> "rel", clock |-> 0]
Message == {AckMessage, RelMessage} \union {ReqMessage(c) : c \in Clock}
(***************************************************************************)
(* The type correctness predicate. *)
(***************************************************************************)
TypeOK ==
(* clock[p] is the local clock of process p *)
/\ clock \in [Proc -> Clock]
(* req[p][q] stores the clock associated with request from q received by p, 0 if none *)
/\ req \in [Proc -> [Proc -> Nat]]
(* ack[p] stores the processes that have ack'ed p's request *)
/\ ack \in [Proc -> SUBSET Proc]
(* network[p][q]: queue of messages from p to q -- pairwise FIFO communication *)
/\ network \in [Proc -> [Proc -> Seq(Message)]]
(* set of processes in critical section: should be empty or singleton *)
/\ crit \in SUBSET Proc
(***************************************************************************)
(* The initial state predicate. *)
(***************************************************************************)
Init ==
/\ clock = [p \in Proc |-> 1]
/\ req = [p \in Proc |-> [q \in Proc |-> 0]]
/\ ack = [p \in Proc |-> {}]
/\ network = [p \in Proc |-> [q \in Proc |-> <<>> ]]
/\ crit = {}
(***************************************************************************)
(* beats(p,q) is true if process p believes that its request has higher *)
(* priority than q's request. This is true if either p has not received a *)
(* request from q or p's request has a smaller clock value than q's. *)
(* If there is a tie, the numerical process ID decides. *)
(***************************************************************************)
beats(p,q) ==
\/ req[p][q] = 0
\/ req[p][p] < req[p][q]
\/ req[p][p] = req[p][q] /\ p < q
(***************************************************************************)
(* Broadcast a message: send it to all processes except the sender. *)
(***************************************************************************)
Broadcast(s, m) ==
[r \in Proc |-> IF s=r THEN network[s][r] ELSE Append(network[s][r], m)]
(***************************************************************************)
(* Process p requests access to critical section. *)
(***************************************************************************)
Request(p) ==
/\ req[p][p] = 0
/\ req'= [req EXCEPT ![p][p] = clock[p]]
/\ network' = [network EXCEPT ![p] = Broadcast(p, ReqMessage(clock[p]))]
/\ ack' = [ack EXCEPT ![p] = {p}]
/\ UNCHANGED <<clock, crit>>
(***************************************************************************)
(* Process p receives a request from q and acknowledges it. *)
(***************************************************************************)
ReceiveRequest(p,q) ==
/\ network[q][p] # << >>
/\ LET m == Head(network[q][p])
c == m.clock
IN /\ m.type = "req"
/\ req' = [req EXCEPT ![p][q] = c]
/\ clock' = [clock EXCEPT ![p] = IF c > clock[p] THEN c + 1 ELSE @ + 1]
/\ network' = [network EXCEPT ![q][p] = Tail(@),
![p][q] = Append(@, AckMessage)]
/\ UNCHANGED <<ack, crit>>
(***************************************************************************)
(* Process p receives an acknowledgement from q. *)
(***************************************************************************)
ReceiveAck(p,q) ==
/\ network[q][p] # << >>
/\ LET m == Head(network[q][p])
IN /\ m.type = "ack"
/\ ack' = [ack EXCEPT ![p] = @ \union {q}]
/\ network' = [network EXCEPT ![q][p] = Tail(@)]
/\ UNCHANGED <<clock, req, crit>>
(**************************************************************************)
(* Process p enters the critical section. *)
(**************************************************************************)
Enter(p) ==
/\ ack[p] = Proc
/\ \A q \in Proc \ {p} : beats(p,q)
/\ crit' = crit \union {p}
/\ UNCHANGED <<clock, req, ack, network>>
(***************************************************************************)
(* Process p exits the critical section and notifies other processes. *)
(***************************************************************************)
Exit(p) ==
/\ p \in crit
/\ crit' = crit \ {p}
/\ network' = [network EXCEPT ![p] = Broadcast(p, RelMessage)]
/\ req' = [req EXCEPT ![p][p] = 0]
/\ ack' = [ack EXCEPT ![p] = {}]
/\ UNCHANGED clock
(***************************************************************************)
(* Process p receives a release notification from q. *)
(***************************************************************************)
ReceiveRelease(p,q) ==
/\ network[q][p] # << >>
/\ LET m == Head(network[q][p])
IN /\ m.type = "rel"
/\ req' = [req EXCEPT ![p][q] = 0]
/\ network' = [network EXCEPT ![q][p] = Tail(@)]
/\ UNCHANGED <<clock, ack, crit>>
(***************************************************************************)
(* Next-state relation. *)
(***************************************************************************)
Next ==
\/ \E p \in Proc : Request(p) \/ Enter(p) \/ Exit(p)
\/ \E p \in Proc : \E q \in Proc \ {p} :
ReceiveRequest(p,q) \/ ReceiveAck(p,q) \/ ReceiveRelease(p,q)
vars == <<req, network, clock, ack, crit>>
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
(***************************************************************************)
(* A state constraint that is useful for validating the specification *)
(* using finite-state model checking. *)
(***************************************************************************)
ClockConstraint == \A p \in Proc : clock[p] <= maxClock
(***************************************************************************)
(* No channel ever contains more than three messages. In fact, no channel *)
(* ever contains more than one message of the same type, as proved below. *)
(***************************************************************************)
BoundedNetwork == \A p,q \in Proc : Len(network[p][q]) <= 3
(***************************************************************************)
(* The main safety property of mutual exclusion. *)
(***************************************************************************)
Mutex == \A p,q \in crit : p = q
==============================================================================