-
Notifications
You must be signed in to change notification settings - Fork 2
/
ClientCentric2PLBug.tla
243 lines (204 loc) · 10 KB
/
ClientCentric2PLBug.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
-------------------------- MODULE ClientCentric2PLBug --------------------------
EXTENDS Naturals, TLC, Sequences, FiniteSets, Util
CONSTANTS transactions, resources
(*
2PL/2PC where processes interleave
Assumes that no messages are lost, but can be received out of order.
2PC for atomicity.
2PL for isolation => serializability
No deadlock, because TM is allowed to abort
*)
\* Client Centric instance for checking consistency levels
CC == INSTANCE ClientCentric WITH Keys <- resources, Values <- 0..10 \* Nat doesn't work for some reason
w(k,v) == CC!w(k,v)
r(k,v) == CC!r(k,v)
(* --algorithm 2pl
variables
\* append send in the system
msgs = {},
\* reads and writes per transaction id
operations = [ tId \in transactions |-> <<>> ]
;
define
InitialState == [k \in resources |-> 0]
end define;
macro sendMessage(msg) begin
msgs := msgs \union {msg};
end macro
fair process tm \in transactions
begin
INIT: sendMessage([id |-> self, type |-> "VoteRequest"]);
WAIT: either \* receive commit votes
await \A rm \in resources: [id |-> self, type |-> "VoteCommit", rm |-> rm] \in msgs;
sendMessage( [id |-> self, type |-> "GlobalCommit"]);
goto COMMIT;
or \* receive at least 1 abort votes
await \E rm \in resources: [id |-> self, type |-> "VoteAbort", rm |-> rm] \in msgs;
sendMessage([id |-> self, type |-> "GlobalAbort"]);
goto ABORT;
or \* or timeout, solves deadlock when two transactions lock each others resources
sendMessage([id |-> self, type |-> "GlobalAbort"]);
goto ABORT;
end either;
ABORT: goto Done;
COMMIT: goto Done;
end process
fair process tr \in resources
variables maxTxs = 5,
voted = {}, committed = {}, aborted = {},
state = 0;
begin TR_INIT:
while maxTxs >= 0 do
either skip; \* skip to not deadlock
or \* Wait on VoteRequest
with tId \in transactions \ voted do
await [id |-> tId, type |-> "VoteRequest"] \in msgs;
either \* If preconditions hold, VoteCommit, else VoteAbort
sendMessage([id |-> tId, type |-> "VoteCommit", rm |-> self]);
voted := voted \union {tId};
or
sendMessage([id |-> tId, type |-> "VoteAbort", rm |-> self]);
voted := voted \union {tId};
aborted := aborted \union {tId};
goto STEP;
end either;
end with;
READY: \* Wait on Commit/Abort
either \* receive GlobalAbort
with tId \in transactions \ committed do
await [id |-> tId, type |-> "GlobalCommit"] \in msgs;
committed := committed \union {tId};
\* Add read and write operations of local values to the relevant transaction's operations
operations[tId] := operations[tId] \o << r(self, state), w(self, state+1) >>;
state := state + 1;
end with;
or \* receive GlobalCommit
with tId \in transactions \ aborted do
await [id |-> tId, type |-> "GlobalAbort"] \in msgs;
aborted := aborted \union {tId};
end with;
end either;
end either;
STEP: maxTxs := maxTxs - 1;
end while;
end process;
end algorithm *)
\* BEGIN TRANSLATION - the hash of the PCal code: PCal-e937946e98c89eb514a3196c7c0ea29d
VARIABLES msgs, operations, pc
(* define statement *)
InitialState == [k \in resources |-> 0]
VARIABLES maxTxs, voted, committed, aborted, state
vars == << msgs, operations, pc, maxTxs, voted, committed, aborted, state >>
ProcSet == (transactions) \cup (resources)
Init == (* Global variables *)
/\ msgs = {}
/\ operations = [ tId \in transactions |-> <<>> ]
(* Process tr *)
/\ maxTxs = [self \in resources |-> 5]
/\ voted = [self \in resources |-> {}]
/\ committed = [self \in resources |-> {}]
/\ aborted = [self \in resources |-> {}]
/\ state = [self \in resources |-> 0]
/\ pc = [self \in ProcSet |-> CASE self \in transactions -> "INIT"
[] self \in resources -> "TR_INIT"]
INIT(self) == /\ pc[self] = "INIT"
/\ msgs' = (msgs \union {([id |-> self, type |-> "VoteRequest"])})
/\ pc' = [pc EXCEPT ![self] = "WAIT"]
/\ UNCHANGED << operations, maxTxs, voted, committed, aborted,
state >>
WAIT(self) == /\ pc[self] = "WAIT"
/\ \/ /\ \A rm \in resources: [id |-> self, type |-> "VoteCommit", rm |-> rm] \in msgs
/\ msgs' = (msgs \union {([id |-> self, type |-> "GlobalCommit"])})
/\ pc' = [pc EXCEPT ![self] = "COMMIT"]
\/ /\ \E rm \in resources: [id |-> self, type |-> "VoteAbort", rm |-> rm] \in msgs
/\ msgs' = (msgs \union {([id |-> self, type |-> "GlobalAbort"])})
/\ pc' = [pc EXCEPT ![self] = "ABORT"]
\/ /\ msgs' = (msgs \union {([id |-> self, type |-> "GlobalAbort"])})
/\ pc' = [pc EXCEPT ![self] = "ABORT"]
/\ UNCHANGED << operations, maxTxs, voted, committed, aborted,
state >>
ABORT(self) == /\ pc[self] = "ABORT"
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << msgs, operations, maxTxs, voted, committed,
aborted, state >>
COMMIT(self) == /\ pc[self] = "COMMIT"
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << msgs, operations, maxTxs, voted, committed,
aborted, state >>
tm(self) == INIT(self) \/ WAIT(self) \/ ABORT(self) \/ COMMIT(self)
TR_INIT(self) == /\ pc[self] = "TR_INIT"
/\ IF maxTxs[self] >= 0
THEN /\ \/ /\ TRUE
/\ pc' = [pc EXCEPT ![self] = "STEP"]
/\ UNCHANGED <<msgs, voted, aborted>>
\/ /\ \E tId \in transactions \ voted[self]:
/\ [id |-> tId, type |-> "VoteRequest"] \in msgs
/\ \/ /\ msgs' = (msgs \union {([id |-> tId, type |-> "VoteCommit", rm |-> self])})
/\ voted' = [voted EXCEPT ![self] = voted[self] \union {tId}]
/\ pc' = [pc EXCEPT ![self] = "READY"]
/\ UNCHANGED aborted
\/ /\ msgs' = (msgs \union {([id |-> tId, type |-> "VoteAbort", rm |-> self])})
/\ voted' = [voted EXCEPT ![self] = voted[self] \union {tId}]
/\ aborted' = [aborted EXCEPT ![self] = aborted[self] \union {tId}]
/\ pc' = [pc EXCEPT ![self] = "STEP"]
ELSE /\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << msgs, voted, aborted >>
/\ UNCHANGED << operations, maxTxs, committed, state >>
STEP(self) == /\ pc[self] = "STEP"
/\ maxTxs' = [maxTxs EXCEPT ![self] = maxTxs[self] - 1]
/\ pc' = [pc EXCEPT ![self] = "TR_INIT"]
/\ UNCHANGED << msgs, operations, voted, committed, aborted,
state >>
READY(self) == /\ pc[self] = "READY"
/\ \/ /\ \E tId \in transactions \ committed[self]:
/\ [id |-> tId, type |-> "GlobalCommit"] \in msgs
/\ committed' = [committed EXCEPT ![self] = committed[self] \union {tId}]
/\ operations' = [operations EXCEPT ![tId] = operations[tId] \o << r(self, state[self]), w(self, state[self]+1) >>]
/\ state' = [state EXCEPT ![self] = state[self] + 1]
/\ UNCHANGED aborted
\/ /\ \E tId \in transactions \ aborted[self]:
/\ [id |-> tId, type |-> "GlobalAbort"] \in msgs
/\ aborted' = [aborted EXCEPT ![self] = aborted[self] \union {tId}]
/\ UNCHANGED <<operations, committed, state>>
/\ pc' = [pc EXCEPT ![self] = "STEP"]
/\ UNCHANGED << msgs, maxTxs, voted >>
tr(self) == TR_INIT(self) \/ STEP(self) \/ READY(self)
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == (\E self \in transactions: tm(self))
\/ (\E self \in resources: tr(self))
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ \A self \in transactions : WF_vars(tm(self))
/\ \A self \in resources : WF_vars(tr(self))
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-ae86c4994dcf7791fb3f7e6903f8d16f
Message == [id: transactions, type: {"VoteRequest", "GlobalCommit", "GlobalAbort"}] \union
[id: transactions, type: {"VoteAbort", "VoteCommit"}, rm: resources]
TypeOK == /\ msgs \subseteq Message
/\ \A res \in resources:
/\ committed[res] \in SUBSET transactions
/\ aborted[res] \in SUBSET transactions
/\ voted[res] \in SUBSET transactions
Atomicity ==
\* When resource are done
\A id \in transactions: pc[id]="Done" =>
\A a1,a2 \in resources:
\* no participants differ from result aborted or committed
~ /\ id \in aborted[a1]
/\ id \in committed[a2]
AllTransactionsFinish == <>(\A t \in transactions: pc[t] = "Done")
ccTransactions == Range(operations)
CCTypeOK == CC!TypeOKT(ccTransactions)
Serializable ==
\* PrintT(<<"InitialState", InitialState>>) /\
\* PrintT(<<"ccTransactions2", ccTransactions2>>) /\
CC!Serializability(InitialState, ccTransactions)
SnapshotIsolation == CC!SnapshotIsolation(InitialState, ccTransactions)
ReadCommitted == CC!ReadCommitted(InitialState, ccTransactions)
ReadUncommitted == CC!ReadUncommitted(InitialState, ccTransactions)
=============================================================================
\* Modification History
\* Last modified Wed Jun 24 13:52:10 CEST 2020 by tim
\* Created Tue Apr 28 16:41:42 CEST 2020 by tim