-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathTwoPhase.tla
211 lines (193 loc) · 11.2 KB
/
TwoPhase.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
------------------------------ MODULE TwoPhase ------------------------------
(***************************************************************************)
(* This specification is discussed in "Two-Phase Commit", Lecture 6 of the *)
(* TLA+ Video Course. It describes the Two-Phase Commit protocol, in *)
(* which a transaction manager (TM) coordinates the resource managers *)
(* (RMs) to implement the Transaction Commit specification of module *)
(* TCommit. In this specification, RMs spontaneously issue Prepared *)
(* messages. We ignore the Prepare messages that the TM can send to the *)
(* RMs. *)
(* *)
(* For simplicity, we also eliminate Abort messages sent by an RM when it *)
(* decides to abort. Such a message would cause the TM to abort the *)
(* transaction, an event represented here by the TM spontaneously deciding *)
(* to abort. *)
(***************************************************************************)
CONSTANT RM \* The set of resource managers
VARIABLES
rmState, \* rmState[r] is the state of resource manager r.
tmState, \* The state of the transaction manager.
tmPrepared, \* The set of RMs from which the TM has received "Prepared"
\* messages.
msgs
(***********************************************************************)
(* In the protocol, processes communicate with one another by sending *)
(* messages. For simplicity, we represent message passing with the *)
(* variable msgs whose value is the set of all messages that have been *)
(* sent. A message is sent by adding it to the set msgs. An action *)
(* that, in an implementation, would be enabled by the receipt of a *)
(* certain message is here enabled by the presence of that message in *)
(* msgs. For simplicity, messages are never removed from msgs. This *)
(* allows a single message to be received by multiple receivers. *)
(* Receipt of the same message twice is therefore allowed; but in this *)
(* particular protocol, that's not a problem. *)
(***********************************************************************)
Messages ==
(*************************************************************************)
(* The set of all possible messages. Messages of type "Prepared" are *)
(* sent from the RM indicated by the message's rm field to the TM. *)
(* Messages of type "Commit" and "Abort" are broadcast by the TM, to be *)
(* received by all RMs. The set msgs contains just a single copy of *)
(* such a message. *)
(*************************************************************************)
[type : {"Prepared"}, rm : RM] \cup [type : {"Commit", "Abort"}]
TPTypeOK ==
(*************************************************************************)
(* The type-correctness invariant *)
(*************************************************************************)
/\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
/\ tmState \in {"init", "done"}
/\ tmPrepared \subseteq RM
/\ msgs \subseteq Messages
TPInit ==
(*************************************************************************)
(* The initial predicate. *)
(*************************************************************************)
/\ rmState = [r \in RM |-> "working"]
/\ tmState = "init"
/\ tmPrepared = {}
/\ msgs = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the processes, first *)
(* the TM's actions, then the RMs' actions. *)
(***************************************************************************)
TMRcvPrepared(r) ==
(*************************************************************************)
(* The TM receives a "Prepared" message from resource manager r. We *)
(* could add the additional enabling condition r \notin tmPrepared, *)
(* which disables the action if the TM has already received this *)
(* message. But there is no need, because in that case the action has *)
(* no effect; it leaves the state unchanged. *)
(*************************************************************************)
/\ tmState = "init"
/\ [type |-> "Prepared", rm |-> r] \in msgs
/\ tmPrepared' = tmPrepared \union {r}
/\ UNCHANGED <<rmState, tmState, msgs>>
\*TMCommit == /\ tmState = "init"
\* /\ tmPrepared = RM
\* /\ tmState' = "done"
\* /\ msgs' = msgs \union {[type |-> "Commit"]}
\* /\ UNCHANGED <<rmState, tmPrepared>>
\*
\*TMAbort == /\ tmState = "init"
\* /\ msgs' = msgs \union {[type |-> "Abort"]}
\* /\ tmState' = "done"
\* /\ UNCHANGED <<rmState, tmPrepared>>
\*
\*RMPrepare(r) == /\ rmState[r] = "working"
\* /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
\* /\ msgs' = msgs \union {[type |-> "Prepared", rm |-> r]}
\* /\ UNCHANGED <<tmPrepared, tmState>>
\*
\*RMChooseToAbort(r) == /\ rmState[r] = "working"
\* /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
\* /\ UNCHANGED <<tmPrepared, tmState, msgs>>
\*
\*RMRcvCommitMsg(r) == /\ [type |-> "Commit"] \in msgs
\* /\ rmState' = [rmState EXCEPT ![r] = "committed"]
\* /\ UNCHANGED <<tmPrepared, tmState, msgs>>
\*
\*RMRcvAbortMsg(r) == /\ [type |-> "Abort"] \in msgs
\* /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
\* /\ UNCHANGED <<tmPrepared, tmState, msgs>>
TMCommit ==
(*************************************************************************)
(* The TM commits the transaction; enabled iff the TM is in its initial *)
(* state and every RM has sent a "Prepared" message. *)
(*************************************************************************)
/\ tmState = "init"
/\ tmPrepared = RM
/\ tmState' = "done"
/\ msgs' = msgs \cup {[type |-> "Commit"]}
/\ UNCHANGED <<rmState, tmPrepared>>
TMAbort ==
(*************************************************************************)
(* The TM spontaneously aborts the transaction. *)
(*************************************************************************)
/\ tmState = "init"
/\ tmState' = "done"
/\ msgs' = msgs \cup {[type |-> "Abort"]}
/\ UNCHANGED <<rmState, tmPrepared>>
RMPrepare(r) ==
(*************************************************************************)
(* Resource manager r prepares. *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
/\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}
/\ UNCHANGED <<tmState, tmPrepared>>
RMChooseToAbort(r) ==
(*************************************************************************)
(* Resource manager r spontaneously decides to abort. As noted above, r *)
(* does not send any message in our simplified spec. *)
(*************************************************************************)
/\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
RMRcvCommitMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to commit. *)
(*************************************************************************)
/\ [type |-> "Commit"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
RMRcvAbortMsg(r) ==
(*************************************************************************)
(* Resource manager r is told by the TM to abort. *)
(*************************************************************************)
/\ [type |-> "Abort"] \in msgs
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
/\ UNCHANGED <<tmState, tmPrepared, msgs>>
TPNext ==
\/ TMCommit \/ TMAbort
\/ \E r \in RM :
TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r)
\/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r)
-----------------------------------------------------------------------------
(***************************************************************************)
(* The material below this point is not discussed in Video Lecture 6. It *)
(* will be explained in Video Lecture 8. *)
(***************************************************************************)
TPSpec == TPInit /\ [][TPNext]_<<rmState, tmState, tmPrepared, msgs>>
(*************************************************************************)
(* The complete spec of the Two-Phase Commit protocol. *)
(*************************************************************************)
THEOREM TPSpec => []TPTypeOK
(*************************************************************************)
(* This theorem asserts that the type-correctness predicate TPTypeOK is *)
(* an invariant of the specification. *)
(*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now assert that the Two-Phase Commit protocol implements the *)
(* Transaction Commit protocol of module TCommit. The following statement *)
(* imports all the definitions from module TCommit into the current *)
(* module. *)
(***************************************************************************)
INSTANCE TCommit
THEOREM TPSpec => TCSpec
(*************************************************************************)
(* This theorem asserts that the specification TPSpec of the Two-Phase *)
(* Commit protocol implements the specification TCSpec of the *)
(* Transaction Commit protocol. *)
(*************************************************************************)
(***************************************************************************)
(* The two theorems in this module have been checked with TLC for six *)
(* RMs, a configuration with 50816 reachable states, in a little over a *)
(* minute on a 1 GHz PC. *)
(***************************************************************************)
=============================================================================
\* Modification History
\* Last modified Mon Oct 23 22:04:39 CDT 2017 by chris
\* Created Mon Oct 23 15:59:46 CDT 2017 by chris