-
Notifications
You must be signed in to change notification settings - Fork 0
/
paxoscommit.tla
284 lines (269 loc) · 16.3 KB
/
paxoscommit.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
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
----------------------------- MODULE paxoscommit ----------------------------
(***************************************************************************)
(* This specification is discussed in "Paxos Commit", Lecture 6 of the *)
(* TLA+ Video Course. *)
(* *)
(* This module specifies the Paxos Commit algorithm. We specify only *)
(* safety properties, not liveness properties. We simplify the *)
(* specification in the following ways. *)
(* *)
(* - As in the specification of module TwoPhase, and for the same *)
(* reasons, we let the variable msgs be the set of all messages that *)
(* have ever been sent. If a message is sent to a set of recipients, *)
(* only one copy of the message appears in msgs. *)
(* *)
(* - We do not explicitly model the receipt of messages. If an *)
(* operation can be performed when a process has received a certain set *)
(* of messages, then the operation is represented by an action that is *)
(* enabled when those messages are in the set msgs of sent messages. *)
(* (We are specifying only safety properties, which assert what events *)
(* can occur, and the operation can occur if the messages that enable *)
(* it have been sent.) *)
(* *)
(* - We do not model leader selection. We define actions that the *)
(* current leader may perform, but do not specify who performs them. *)
(* *)
(* As in the specification of Two-Phase commit in module TwoPhase, we have *)
(* RMs spontaneously issue Prepared messages and we ignore Prepare *)
(* messages. *)
(***************************************************************************)
EXTENDS Integers
Maximum(S) ==
(*************************************************************************)
(* If S is a set of numbers, then this define Maximum(S) to be the *)
(* maximum of those numbers, or -1 if S is empty. *)
(*************************************************************************)
IF S = {} THEN -1
ELSE CHOOSE n \in S : \A m \in S : n \geq m
CONSTANT RM, \* The set of resource managers.
Acceptor, \* The set of acceptors.
Majority, \* The set of majorities of acceptors
Ballot \* The set of ballot numbers
(***************************************************************************)
(* We assume the following properties of the declared constants. *)
(***************************************************************************)
ASSUME
/\ Ballot \subseteq Nat
/\ 0 \in Ballot
/\ Majority \subseteq SUBSET Acceptor
/\ \A MS1, MS2 \in Majority : MS1 \cap MS2 # {}
(********************************************************************)
(* All we assume about the set Majority of majorities is that any *)
(* two majorities have non-empty intersection. *)
(********************************************************************)
Messages ==
(*************************************************************************)
(* The set of all possible messages. There are messages of type *)
(* "Commit" and "Abort" to announce the decision, as well as messages *)
(* for each phase of each instance of ins of the Paxos consensus *)
(* algorithm. The acc field indicates the sender of a message from an *)
(* acceptor to the leader; messages from a leader are broadcast to all *)
(* acceptors. *)
(*************************************************************************)
[type : {"phase1a"}, ins : RM, bal : Ballot \ {0}]
\cup
[type : {"phase1b"}, ins : RM, mbal : Ballot, bal : Ballot \cup {-1},
val : {"prepared", "aborted", "none"}, acc : Acceptor]
\cup
[type : {"phase2a"}, ins : RM, bal : Ballot, val : {"prepared", "aborted"}]
\cup
[type : {"phase2b"}, acc : Acceptor, ins : RM, bal : Ballot,
val : {"prepared", "aborted"}]
\cup
[type : {"Commit", "Abort"}]
-----------------------------------------------------------------------------
VARIABLES
rmState, \* rmState[r] is the state of resource manager r.
aState, \* aState[ins][ac] is the state of acceptor ac for instance
\* ins of the Paxos algorithm.
msgs \* The set of all messages ever sent.
PCTypeOK ==
(*************************************************************************)
(* The type-correctness invariant. Each acceptor maintains the values *)
(* mbal, bal, and val for each instance of the Paxos consensus *)
(* algorithm. *)
(*************************************************************************)
/\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
/\ aState \in [RM -> [Acceptor -> [mbal : Ballot,
bal : Ballot \cup {-1},
val : {"prepared", "aborted", "none"}]]]
/\ msgs \subseteq Messages
PCInit == \* The initial predicate.
/\ rmState = [r \in RM |-> "working"]
/\ aState = [r \in RM |->
[ac \in Acceptor
|-> [mbal |-> 0, bal |-> -1, val |-> "none"]]]
/\ msgs = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* THE ACTIONS *)
(***************************************************************************)
Send(m) == msgs' = msgs \cup {m}
(*************************************************************************)
(* An action expression that describes the sending of message m. *)
(*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* RM ACTIONS *)
(***************************************************************************)
RMPrepare(r) ==
(*************************************************************************)
(* Resource manager r prepares by sending a phase 2a message for ballot *)
(* number 0 with value "prepared". *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
/\ Send([type |-> "phase2a", ins |-> r, bal |-> 0, val |-> "prepared"])
/\ UNCHANGED aState
RMChooseToAbort(r) ==
(*************************************************************************)
(* Resource manager r spontaneously decides to abort. It may (but need *)
(* not) send a phase 2a message for ballot number 0 with value *)
(* "aborted". *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ Send([type |-> "phase2a", ins |-> r, bal |-> 0, val |-> "aborted"])
/\ UNCHANGED aState
RMRcvCommitMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the leader to commit. When this action *)
(* is enabled, rmState[r] must equal either "prepared" or "committed". *)
(* In the latter case, the action leaves the state unchanged (it is a *)
(* ``stuttering step''). *)
(*************************************************************************)
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<aState, msgs>>
RMRcvAbortMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the leader to abort. It could be in *)
(* any state except "committed". *)
(*************************************************************************)
/\ [type |-> "Abort"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ UNCHANGED <<aState, msgs>>
-----------------------------------------------------------------------------
(***************************************************************************)
(* LEADER ACTIONS *)
(* *)
(* The following actions are performed by any process that believes itself *)
(* to be the current leader. Since leader selection is not assumed to be *)
(* reliable, multiple processes could simultaneously consider themselves *)
(* to be the leader. *)
(***************************************************************************)
Phase1a(bal, r) ==
(*************************************************************************)
(* If the leader times out without learning that a decision has been *)
(* reached on resource manager r's prepare/abort decision, it can *)
(* perform this action to initiate a new ballot bal. (Sending duplicate *)
(* phase 1a messages is harmless.) *)
(*************************************************************************)
/\ Send([type |-> "phase1a", ins |-> r, bal |-> bal])
/\ UNCHANGED <<rmState, aState>>
Phase2a(bal, r) ==
(*************************************************************************)
(* The action in which a leader sends a phase 2a message with ballot *)
(* bal > 0 in instance r, if it has received phase 1b messages for *)
(* ballot number bal from a majority of acceptors. If the leader *)
(* received a phase 1b message from some acceptor that had sent a phase *)
(* 2b message for this instance, then maxbal \geq 0 and the value val *)
(* the leader sends is determined by the phase 1b messages. (If *)
(* val = "prepared", then r must have prepared.) Otherwise, maxbal = -1 *)
(* and the leader sends the value "aborted". *)
(* *)
(* The first conjunct asserts that the action is disabled if any commit *)
(* leader has already sent a phase 2a message with ballot number bal. *)
(* In practice, this is implemented by having ballot numbers partitioned *)
(* among potential leaders, and having a leader record in stable storage *)
(* the largest ballot number for which it sent a phase 2a message. *)
(*************************************************************************)
/\ ~\E m \in msgs : /\ m.type = "phase2a"
/\ m.bal = bal
/\ m.ins = r
/\ \E MS \in Majority :
LET mset == {m \in msgs : /\ m.type = "phase1b"
/\ m.ins = r
/\ m.mbal = bal
/\ m.acc \in MS}
maxbal == Maximum({m.bal : m \in mset})
val == IF maxbal = -1
THEN "aborted"
ELSE (CHOOSE m \in mset : m.bal = maxbal).val
IN /\ \A ac \in MS : \E m \in mset : m.acc = ac
/\ Send([type |-> "phase2a", ins |-> r, bal |-> bal, val |-> val])
/\ UNCHANGED <<rmState, aState>>
PCDecide ==
(*************************************************************************)
(* A leader can decide that Paxos Commit has reached a result and send a *)
(* message announcing the result if it has received the necessary phase *)
(* 2b messages. *)
(*************************************************************************)
/\ LET Decided(r, v) ==
(****************************************************************)
(* True iff instance r of the Paxos consensus algorithm has *)
(* chosen the value v. *)
(****************************************************************)
\E b \in Ballot, MS \in Majority :
\A ac \in MS : [type |-> "phase2b", ins |-> r,
bal |-> b, val |-> v, acc |-> ac ] \in msgs
IN \/ /\ \A r \in RM : Decided(r, "prepared")
/\ Send([type |-> "Commit"])
\/ /\ \E r \in RM : Decided(r, "aborted")
/\ Send([type |-> "Abort"])
/\ UNCHANGED <<rmState, aState>>
-----------------------------------------------------------------------------
(***************************************************************************)
(* ACCEPTOR ACTIONS *)
(***************************************************************************)
Phase1b(acc) ==
\E m \in msgs :
/\ m.type = "phase1a"
/\ aState[m.ins][acc].mbal < m.bal
/\ aState' = [aState EXCEPT ![m.ins][acc].mbal = m.bal]
/\ Send([type |-> "phase1b",
ins |-> m.ins,
mbal |-> m.bal,
bal |-> aState[m.ins][acc].bal,
val |-> aState[m.ins][acc].val,
acc |-> acc])
/\ UNCHANGED rmState
Phase2b(acc) ==
/\ \E m \in msgs :
/\ m.type = "phase2a"
/\ aState[m.ins][acc].mbal \leq m.bal
/\ aState' = [aState EXCEPT ![m.ins][acc].mbal = m.bal,
![m.ins][acc].bal = m.bal,
![m.ins][acc].val = m.val]
/\ Send([type |-> "phase2b", ins |-> m.ins, bal |-> m.bal,
val |-> m.val, acc |-> acc])
/\ UNCHANGED rmState
-----------------------------------------------------------------------------
PCNext == \* The next-state action
\/ \E r \in RM : \/ RMPrepare(r)
\/ RMChooseToAbort(r)
\/ RMRcvCommitMsg(r)
\/ RMRcvAbortMsg(r)
\/ \E bal \in Ballot \ {0}, r \in RM : Phase1a(bal, r) \/ Phase2a(bal, r)
\/ PCDecide
\/ \E acc \in Acceptor : Phase1b(acc) \/ Phase2b(acc)
-----------------------------------------------------------------------------
(***************************************************************************)
(* The following part of the spec is not covered in Lecture 7. It will be *)
(* explained in Lecture 8. *)
(***************************************************************************)
PCSpec == PCInit /\ [][PCNext]_<<rmState, aState, msgs>>
(*************************************************************************)
(* The complete spec of the Paxos Commit protocol. *)
(*************************************************************************)
THEOREM PCSpec => []PCTypeOK
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now assert that the Paxos Commit protocol implements the transaction *)
(* commit protocol of module TCommit. The following statement imports *)
(* into the current module the definitions from module TCommit, including *)
(* the definition of TCSpec. *)
(***************************************************************************)
INSTANCE TCommitOriginal
THEOREM PCSpec => TCSpec
=============================================================================