Project P119
Two-phase commit
A coordinator and its participants as state machines, the coordinator crashing after any step: wait, ask peers, presume abort and presume commit at every crash point, with the time each participant's data stays locked in doubt.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-16
Every screen below was recorded under CPython. When this page was built, the EML interpreter replayed each session from the same input and printed the same bytes.
About
A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes is in doubt, its data locked, until it hears. The coordinator can crash after any step.
main.eml- the menu, the transaction, one run tick by tick, every crash point under four strategies, and the votes and timingtwopc.eml- the coordinator and the participants, one coordinator step a tick, the four strategies, the outcome of a run, and the count over every pattern of votes
How each part works:
- The coordinator's steps: prepare each participant in turn (a yes locks its data, a no aborts at once and ends the asking), log the decision, tell each participant that voted yes. A coordinator that comes back with no decision logged decides abort; with one logged, it tells everyone again.
- A participant in doubt for the timeout acts on its strategy: - wait keeps waiting for the coordinator; - ask peers asks the coordinator if it is up, else the others: one that has committed or aborted settles it, and one never asked aborts on its own, and so does the one that asked; - presume abort and presume commit decide on their own.
- A run is wrong when it splits, goes against the coordinator's log, or commits though someone never voted yes. As in the corpus case
two-phase-commit-window, with three yes votes, a timeout of 5 ticks and the coordinator back after 10: - wait and ask peers are never wrong, and hold the data for up to 17 and 14 ticks; - presume abort is wrong at 3 of the 9 crash points, and presume commit at 3. - If the coordinator never comes back, wait is left in doubt at 6 crash points, and ask peers only at 2: after every participant voted yes and before any heard the decision. That window is where two-phase commit blocks.
- A timeout of 3 ticks makes presume abort wrong with no crash at all: each participant is in doubt for 4 ticks before it hears.
What is checked: menu choices 1 to 6; one of the four strategies; a crash point from 0 to the last step, or none; 2 to 4 votes of yes or no; a timeout from 1 to 9 ticks; the coordinator back after 1 to 30 ticks, or never. An empty answer cancels.
Sessions: sessions/basic.in gives: - the transaction and every crash point; - runs: wait after step 3, presume abort after step 4 (it aborts what the coordinator committed), ask peers after steps 2 and 4; - the coordinator never back: every crash point, and ask peers after step 3, left in doubt; - the votes yes, no, yes and yes, presume commit after step 1, and every crash point; - three yes votes again with a timeout of 3, every crash point, and presume abort with no crash.
sessions/bad-input.in gives: - menu choices 0 and x; - runs: a cancel, the strategy fast, then crash points of a cancel, 8, x and -1; - votes: a cancel, one vote, five votes, yes maybe, and YES yes; - timing: a cancel, 0, 10 and x, then 5 with a cancel, 0, 31 and sometime.
Built on the verified corpus case two-phase-commit-window (a coordinator crash leaves participants in doubt, and presuming an outcome trades the blocking for a split).
Recorded sessions
What the screen shows while someone uses the program. Each typed line appears after its prompt, the way a terminal shows it.
bad-input
interpreter: byte-equal== Two-phase commit ==
A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 0
Pick a number from 1 to 6.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> x
Pick a number from 1 to 6.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)>
Cancelled.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> fast
Type wait, ask peers, presume abort or presume commit.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)>
Cancelled.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> 8
Type a step from 0 to 7, or none.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> x
Type a step from 0 to 7, or none.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> -1
Type a step from 0 to 7, or none.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)>
Cancelled.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes
Type 2 to 4 votes, each yes or no.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes yes yes yes yes
Type 2 to 4 votes, each yes or no.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes maybe
Type 2 to 4 votes, each yes or no.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> YES yes
Type 2 to 4 votes, each yes or no.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)>
Cancelled.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 0
Type a whole number from 1 to 9.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 10
Type a whole number from 1 to 9.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> x
Type a whole number from 1 to 9.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)>
Cancelled.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> 0
Type a whole number from 1 to 30, or never.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> 31
Type a whole number from 1 to 30, or never.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> sometime
Type a whole number from 1 to 30, or never.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 6
Bye.
What was typed (49 lines)
0
x
2
2
fast
2
wait
2
wait
8
2
wait
x
2
wait
-1
4
4
yes
4
yes yes yes yes yes
4
yes maybe
4
YES yes
5
5
0
5
10
5
x
5
5
5
5
0
5
5
31
5
5
sometime
6
basic
interpreter: byte-equal== Two-phase commit ==
A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 1
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator is back after 10 ticks.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 5 ticks; the coordinator is back after 10 ticks:
crash after wait ask peers presume abort presume commit
none c c c c c c c c c c c c
0 before any step - - - - - - - - - - - -
1 prepare P1 a - - a a - a - - c - - !
2 prepare P2 a a - a a a a a - c c - !
3 prepare P3 a a a a a a a a a c c c !
4 log commit c c c c c c a a a ! c c c
5 tell P1 c c c c c c c a a ! c c c
6 tell P2 c c c c c c c c a ! c c c
7 tell P3 c c c c c c c c c c c c
c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
wait: wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 17 ticks.
ask peers: wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 14 ticks.
presume abort: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
presume commit: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
Every pattern of 3 votes, each with every crash point and none:
strategy runs wrong in doubt at the end most ticks locked
wait 45 0 0 17
ask peers 45 0 0 14
presume abort 45 3 0 5
presume commit 45 14 0 5
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> 3
wait, the coordinator crashing after step 3 (it is back after 10 ticks):
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 3 prepare P3: it votes yes and locks its data
tick 3 the coordinator crashes
tick 6 P1 in doubt: waits, its data locked
tick 7 P2 in doubt: waits, its data locked
tick 8 P3 in doubt: waits, its data locked
tick 14 the coordinator is back; with no decision logged, it decides abort
tick 15 tell P1 abort: it aborts and unlocks
tick 16 tell P2 abort: it aborts and unlocks
tick 17 tell P3 abort: it aborts and unlocks
P1 aborted at tick 15, its data locked for 14 ticks.
P2 aborted at tick 16, its data locked for 14 ticks.
P3 aborted at tick 17, its data locked for 14 ticks.
Atomic: everyone who finished aborted, as the coordinator logged.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume abort
crash after step (0 to 7, or none)> 4
presume abort, the coordinator crashing after step 4 (it is back after 10 ticks):
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 3 prepare P3: it votes yes and locks its data
tick 4 the coordinator logs commit
tick 4 the coordinator crashes
tick 6 P1 in doubt: presumes abort and unlocks
tick 7 P2 in doubt: presumes abort and unlocks
tick 8 P3 in doubt: presumes abort and unlocks
tick 15 the coordinator is back with commit logged, and tells everyone again
tick 16 tell P1 commit: but it had already aborted
tick 17 tell P2 commit: but it had already aborted
tick 18 tell P3 commit: but it had already aborted
P1 aborted at tick 6, its data locked for 5 ticks.
P2 aborted at tick 7, its data locked for 5 ticks.
P3 aborted at tick 8, its data locked for 5 ticks.
Against the coordinator, which logged commit: P1, P2 and P3 aborted.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 2
ask peers, the coordinator crashing after step 2 (it is back after 10 ticks):
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 2 the coordinator crashes
tick 6 P3, never asked, aborts on its own
tick 6 P1 in doubt: asks P3, and aborts too
tick 7 P2 in doubt: asks P1, which has aborted, and aborts too
tick 13 the coordinator is back; with no decision logged, it decides abort
tick 14 tell P1 abort: it had already aborted
tick 15 tell P2 abort: it had already aborted
P1 aborted at tick 6, its data locked for 5 ticks.
P2 aborted at tick 7, its data locked for 5 ticks.
P3 aborted at tick 6, never locked.
Atomic: everyone who finished aborted, as the coordinator logged.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 4
ask peers, the coordinator crashing after step 4 (it is back after 10 ticks):
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 3 prepare P3: it votes yes and locks its data
tick 4 the coordinator logs commit
tick 4 the coordinator crashes
tick 6 P1 in doubt: asks the others, all in doubt too, so it waits, its data locked
tick 7 P2 in doubt: asks the others, all in doubt too, so it waits, its data locked
tick 8 P3 in doubt: asks the others, all in doubt too, so it waits, its data locked
tick 15 the coordinator is back with commit logged, and tells everyone again
tick 15 P1 in doubt: asks the coordinator: commit
tick 15 P2 in doubt: asks the coordinator: commit
tick 15 P3 in doubt: asks the coordinator: commit
tick 16 tell P1 commit: it had already committed
tick 17 tell P2 commit: it had already committed
tick 18 tell P3 commit: it had already committed
P1 committed at tick 15, its data locked for 14 ticks.
P2 committed at tick 15, its data locked for 13 ticks.
P3 committed at tick 15, its data locked for 12 ticks.
Atomic: everyone who finished committed, as the coordinator logged.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> never
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 5 ticks; the coordinator never comes back:
crash after wait ask peers presume abort presume commit
none c c c c c c c c c c c c
0 before any step - - - - - - - - - - - -
1 prepare P1 ? - - a a - a - - c - - !
2 prepare P2 ? ? - a a a a a - c c - !
3 prepare P3 ? ? ? ? ? ? a a a c c c
4 log commit ? ? ? ? ? ? a a a ! c c c
5 tell P1 c ? ? c c c c a a ! c c c
6 tell P2 c c ? c c c c c a ! c c c
7 tell P3 c c c c c c c c c c c c
c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
wait: wrong at 0 of 9 crash points, still in doubt at 6, data locked at most 39 ticks.
ask peers: wrong at 0 of 9 crash points, still in doubt at 2, data locked at most 39 ticks.
presume abort: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
presume commit: wrong at 2 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
Ask peers is still in doubt only at crash points 3 and 4: every participant had voted yes, and none had heard the decision.
Every pattern of 3 votes, each with every crash point and none:
strategy runs wrong in doubt at the end most ticks locked
wait 45 0 17 39
ask peers 45 0 2 39
presume abort 45 3 0 5
presume commit 45 13 0 5
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 3
ask peers, the coordinator crashing after step 3 (it never comes back):
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 3 prepare P3: it votes yes and locks its data
tick 3 the coordinator crashes
tick 6 P1 in doubt: asks the others, all in doubt too, so it waits, its data locked
tick 7 P2 in doubt: asks the others, all in doubt too, so it waits, its data locked
tick 8 P3 in doubt: asks the others, all in doubt too, so it waits, its data locked
P1 still in doubt at tick 40, its data locked for 39 ticks.
P2 still in doubt at tick 40, its data locked for 38 ticks.
P3 still in doubt at tick 40, its data locked for 37 ticks.
Still in doubt at tick 40, data locked: P1, P2 and P3.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes no yes yes
Participants P1, P2, P3 and P4 vote yes, no, yes and yes.
With no crash, the coordinator takes 4 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 log abort, 4 tell P1.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume commit
crash after step (0 to 4, or none)> 1
presume commit, the coordinator crashing after step 1 (it never comes back):
tick 1 prepare P1: it votes yes and locks its data
tick 1 the coordinator crashes
tick 6 P1 in doubt: presumes commit and unlocks
P1 committed at tick 6, its data locked for 5 ticks.
P2 was never asked.
P3 was never asked.
P4 was never asked.
Committed without every yes: P1 committed, though P2, P3 and P4 never voted yes.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 3
Every crash point, votes yes, no, yes and yes; a participant in doubt acts after 5 ticks; the coordinator never comes back:
crash after wait ask peers presume abort presume commit
none a a - - a a - - a a - - a a - -
0 before any step - - - - - - - - - - - - - - - -
1 prepare P1 ? - - - a a - - a - - - c - - - !
2 prepare P2 ? a - - a a - - a a - - c a - - !
3 log abort ? a - - a a - - a a - - c a - - !
4 tell P1 a a - - a a - - a a - - a a - -
c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
wait: wrong at 0 of 6 crash points, still in doubt at 3, data locked at most 39 ticks.
ask peers: wrong at 0 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
presume abort: wrong at 0 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
presume commit: wrong at 3 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
Every pattern of 4 votes, each with every crash point and none:
strategy runs wrong in doubt at the end most ticks locked
wait 93 0 37 39
ask peers 93 0 2 39
presume abort 93 4 0 5
presume commit 93 32 0 5
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes yes yes
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 3
coordinator back after (1 to 30 ticks, or never)> 10
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 3 ticks acts on its strategy; a crashed coordinator is back after 10 ticks.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 3 ticks; the coordinator is back after 10 ticks:
crash after wait ask peers presume abort presume commit
none c c c c c c a a a ! c c c
0 before any step - - - - - - - - - - - -
1 prepare P1 a - - a a - a - - c - - !
2 prepare P2 a a - a a a a a - c c - !
3 prepare P3 a a a a a a a a a c c c !
4 log commit c c c c c c a a a ! c c c
5 tell P1 c c c c c c a a a ! c c c
6 tell P2 c c c c c c a a a ! c c c
7 tell P3 c c c c c c a a a ! c c c
c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
wait: wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 17 ticks.
ask peers: wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 14 ticks.
presume abort: wrong at 5 of 9 crash points, still in doubt at 0, data locked at most 3 ticks.
presume commit: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 3 ticks.
Every pattern of 3 votes, each with every crash point and none:
strategy runs wrong in doubt at the end most ticks locked
wait 45 0 0 17
ask peers 45 0 0 14
presume abort 45 5 0 3
presume commit 45 16 0 3
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume abort
crash after step (0 to 7, or none)> none
presume abort, no crash:
tick 1 prepare P1: it votes yes and locks its data
tick 2 prepare P2: it votes yes and locks its data
tick 3 prepare P3: it votes yes and locks its data
tick 4 the coordinator logs commit
tick 4 P1 in doubt: presumes abort and unlocks
tick 5 tell P1 commit: but it had already aborted
tick 5 P2 in doubt: presumes abort and unlocks
tick 6 tell P2 commit: but it had already aborted
tick 6 P3 in doubt: presumes abort and unlocks
tick 7 tell P3 commit: but it had already aborted
P1 aborted at tick 4, its data locked for 3 ticks.
P2 aborted at tick 5, its data locked for 3 ticks.
P3 aborted at tick 6, its data locked for 3 ticks.
Against the coordinator, which logged commit: P1, P2 and P3 aborted.
1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit
choice> 6
Bye.
What was typed (37 lines)
1
3
2
wait
3
2
presume abort
4
2
ask peers
2
2
ask peers
4
5
5
never
3
2
ask peers
3
4
yes no yes yes
2
presume commit
1
3
4
yes yes yes
5
3
10
3
2
presume abort
none
6
Modules
The program as written, entry module first. Each module transpiles to its own Python file, which is what eml project run executes.
main.eml(entry)
eml# P119 two-phase commit: one run tick by tick with the coordinator crashing
# after a chosen step, every crash point under four strategies for a
# participant in doubt, and every pattern of votes counted.
import twopc
def plain(s):
0 => i
len(s) => j
while i < j and s[i] == " ":
i + 1 => i
while j > i and s[j - 1] == " ":
j - 1 => j
return s[i:j]
def pad(s, n):
s => out
while len(out) < n:
out + " " => out
return out
def lpad(s, n):
s => out
while len(out) < n:
" " + out => out
return out
def is_digits(s):
if len(s) == 0:
return False
for c in s:
if c < "0" or c > "9":
return False
return True
def ticks_text(n):
if n == 1:
return "1 tick"
return str(n) + " ticks"
def names_text(ns):
"" => out
for i in [0:len(ns) - 1]:
if i > 0 and i == len(ns) - 1:
out + " and " => out
elif i > 0:
out + ", " => out
out + ns[i] => out
return out
def votes_text(votes):
[] => out
for v in votes:
if v:
out + ["yes"] => out
else:
out + ["no"] => out
return out
def back_text(back):
if back == 0:
return "never comes back"
return "is back after " + ticks_text(back)
def show(votes, timeout, back):
[] => ps
for i in [0:len(votes) - 1]:
ps + [twopc.name(i)] => ps
("Participants " + names_text(ps) + " vote " + names_text(votes_text(votes)) + ".") ^0
twopc.run(votes, "wait", timeout, back, 0 - 1, 40) => r
"" => line
for k in [0:len(r[7]) - 1]:
if line != "":
line + ", " => line
line + str(k + 1) + " " + r[7][k] => line
("With no crash, the coordinator takes " + str(r[5]) + " steps, one a tick: " + line + ".") ^0
("A participant in doubt for " + ticks_text(timeout) + " acts on its strategy; a crashed coordinator " + back_text(back) + ".") ^0
def ask_strategy():
plain(input("strategy (wait, ask peers, presume abort or presume commit)> ")) => s
if s == "":
"Cancelled." ^0
return ""
for x in twopc.strategies():
if x == s:
return s
"Type wait, ask peers, presume abort or presume commit." ^0
return ""
def verdict(r):
twopc.outcome(r) => o
[] => c
[] => a
[] => d
for i in [0:len(r[1]) - 1]:
if r[1][i] == "committed":
c + [twopc.name(i)] => c
elif r[1][i] == "aborted":
a + [twopc.name(i)] => a
elif r[1][i] == "prepared":
d + [twopc.name(i)] => d
if o[0]:
("Split: " + names_text(c) + " committed, and " + names_text(a) + " aborted.") ^0
if o[1]:
[] => wrong
for i in [0:len(r[1]) - 1]:
if (r[1][i] == "committed" or r[1][i] == "aborted") and r[1][i] != twopc.past(r[4]):
wrong + [twopc.name(i)] => wrong
("Against the coordinator, which logged " + r[4] + ": " + names_text(wrong) + " " + opposite(r[4]) + ".") ^0
if o[3]:
[] => never
for i in [0:len(r[1]) - 1]:
if r[8][i] < 0:
never + [twopc.name(i)] => never
("Committed without every yes: " + names_text(c) + " committed, though " + names_text(never) + " never voted yes.") ^0
if o[2]:
("Still in doubt at tick 40, data locked: " + names_text(d) + ".") ^0
if len(c) == 0 and len(a) == 0 and len(d) == 0:
if r[4] == "":
"No participant was asked, and the coordinator never logged a decision." ^0
else:
("No participant was asked; the coordinator logged " + r[4] + ".") ^0
elif not twopc.wrong(o) and not o[2]:
"aborted" => common
if len(c) > 0:
"committed" => common
if r[4] == "":
("Atomic: everyone who finished " + common + ", and the coordinator never logged a decision.") ^0
else:
("Atomic: everyone who finished " + common + ", as the coordinator logged.") ^0
def opposite(d):
if d == "commit":
return "aborted"
return "committed"
def one_run(votes, timeout, back):
ask_strategy() => s
if s == "":
return
twopc.crash_points(votes, timeout, back, 40) => n
plain(input("crash after step (0 to " + str(n) + ", or none)> ")) => t
if t == "":
"Cancelled." ^0
return
0 - 1 => crash
if t != "none":
if not is_digits(t) or len(t) > 2 or int(t) > n:
("Type a step from 0 to " + str(n) + ", or none.") ^0
return
int(t) => crash
twopc.run(votes, s, timeout, back, crash, 40) => r
if crash < 0:
(s + ", no crash:") ^0
else:
(s + ", the coordinator crashing after step " + str(crash) + " (it " + back_text(back) + "):") ^0
for e in r[0]:
(" tick " + lpad(str(e[0]), 2) + " " + e[1]) ^0
for i in [0:len(votes) - 1]:
twopc.name(i) => p
r[1][i] => st
if st == "prepared":
(" " + p + " still in doubt at tick 40, its data locked for " + ticks_text(r[2][i]) + ".") ^0
elif st == "idle":
(" " + p + " was never asked.") ^0
elif r[2][i] == 0:
(" " + p + " " + st + " at tick " + str(r[6][i]) + ", never locked.") ^0
else:
(" " + p + " " + st + " at tick " + str(r[6][i]) + ", its data locked for " + ticks_text(r[2][i]) + ".") ^0
verdict(r)
def every(votes, timeout, back):
twopc.crash_points(votes, timeout, back, 40) => n
twopc.run(votes, "wait", timeout, back, 0 - 1, 40)[7] => labels
("Every crash point, votes " + names_text(votes_text(votes)) + "; a participant in doubt acts after " + ticks_text(timeout) + "; the coordinator " + back_text(back) + ":") ^0
[9, 9, 13, 14] => widths
" " + pad("crash after", 26) => head
for k in [0:3]:
head + " " + pad(twopc.strategies()[k], widths[k]) => head
rstrip(head) ^0
[0, 0, 0, 0] => wrong
[0, 0, 0, 0] => doubt
[0, 0, 0, 0] => most
[] => stuck
for c in [0 - 1:n]:
"none" => label
if c == 0:
"0 before any step" => label
elif c > 0:
str(c) + " " + labels[c - 1] => label
" " + pad(label, 26) => line
for k in [0:3]:
twopc.run(votes, twopc.strategies()[k], timeout, back, c, 40) => r
twopc.outcome(r) => o
twopc.letters(r) => cell
if twopc.wrong(o):
cell + " !" => cell
wrong[k] + 1 => wrong[k]
if o[2]:
doubt[k] + 1 => doubt[k]
if k == 1:
stuck + [str(c)] => stuck
for x in r[2]:
if x > most[k]:
x => most[k]
line + " " + pad(cell, widths[k]) => line
rstrip(line) ^0
" c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes." ^0
for k in [0:3]:
(" " + pad(twopc.strategies()[k] + ":", 16) + "wrong at " + str(wrong[k]) + " of " + str(n + 2) + " crash points, still in doubt at " + str(doubt[k]) + ", data locked at most " + ticks_text(most[k]) + ".") ^0
if len(stuck) == 1:
("Ask peers is still in doubt only at crash point " + stuck[0] + ": every participant had voted yes, and none had heard the decision.") ^0
elif len(stuck) > 1:
("Ask peers is still in doubt only at crash points " + names_text(stuck) + ": every participant had voted yes, and none had heard the decision.") ^0
("Every pattern of " + str(len(votes)) + " votes, each with every crash point and none:") ^0
" strategy runs wrong in doubt at the end most ticks locked" ^0
for s in twopc.strategies():
twopc.census(len(votes), s, timeout, back, 40) => x
(" " + pad(s, 14) + lpad(str(x[0]), 8) + lpad(str(x[1]), 7) + lpad(str(x[2]), 21) + lpad(str(x[3]), 19)) ^0
def rstrip(s):
len(s) => j
while j > 0 and s[j - 1] == " ":
j - 1 => j
return s[0:j]
def ask_votes():
plain(input("votes (2 to 4 of yes or no, such as yes yes no)> ")) => t
if t == "":
"Cancelled." ^0
return []
[] => out
"" => w
for c in t + " ":
if c == " ":
if w == "yes":
out + [True] => out
elif w == "no":
out + [False] => out
elif w != "":
"Type 2 to 4 votes, each yes or no." ^0
return []
"" => w
else:
w + c => w
if len(out) < 2 or len(out) > 4:
"Type 2 to 4 votes, each yes or no." ^0
return []
return out
def ask_timing(timeout, back):
plain(input("in doubt for how long before acting (1 to 9 ticks)> ")) => t
if t == "":
"Cancelled." ^0
return []
if len(t) != 1 or t < "1" or t > "9":
"Type a whole number from 1 to 9." ^0
return []
plain(input("coordinator back after (1 to 30 ticks, or never)> ")) => b
if b == "":
"Cancelled." ^0
return []
0 => nb
if b != "never":
if not is_digits(b) or len(b) > 2 or int(b) < 1 or int(b) > 30:
"Type a whole number from 1 to 30, or never." ^0
return []
int(b) => nb
return [int(t), nb]
[True, True, True] => votes
5 => timeout
10 => back
"== Two-phase commit ==" ^0
"A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears." ^0
True => running
while running:
"" ^0
"1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
show(votes, timeout, back)
elif choice == "2":
one_run(votes, timeout, back)
elif choice == "3":
every(votes, timeout, back)
elif choice == "4":
ask_votes() => v
if len(v) > 0:
v => votes
show(votes, timeout, back)
elif choice == "5":
ask_timing(timeout, back) => x
if len(x) > 0:
x[0] => timeout
x[1] => back
show(votes, timeout, back)
elif choice == "6":
False => running
else:
"Pick a number from 1 to 6." ^0
"Bye." ^0
Python projection (main.py)
import twopc
def plain(s):
i = 0
j = len(s)
while i < j and s[i] == " ":
i = i + 1
while j > i and s[j - 1] == " ":
j = j - 1
return s[i:j]
def pad(s, n):
out = s
while len(out) < n:
out = out + " "
return out
def lpad(s, n):
out = s
while len(out) < n:
out = " " + out
return out
def is_digits(s):
if len(s) == 0:
return False
for c in s:
if c < "0" or c > "9":
return False
return True
def ticks_text(n):
if n == 1:
return "1 tick"
return str(n) + " ticks"
def names_text(ns):
out = ""
for i in range(0, len(ns)):
if i > 0 and i == len(ns) - 1:
out = out + " and "
elif i > 0:
out = out + ", "
out = out + ns[i]
return out
def votes_text(votes):
out = []
for v in votes:
if v:
out = out + ["yes"]
else:
out = out + ["no"]
return out
def back_text(back):
if back == 0:
return "never comes back"
return "is back after " + ticks_text(back)
def show(votes, timeout, back):
ps = []
for i in range(0, len(votes)):
ps = ps + [twopc.name(i)]
print("Participants " + names_text(ps) + " vote " + names_text(votes_text(votes)) + ".")
r = twopc.run(votes, "wait", timeout, back, 0 - 1, 40)
line = ""
for k in range(0, len(r[7])):
if line != "":
line = line + ", "
line = line + str(k + 1) + " " + r[7][k]
print("With no crash, the coordinator takes " + str(r[5]) + " steps, one a tick: " + line + ".")
print("A participant in doubt for " + ticks_text(timeout) + " acts on its strategy; a crashed coordinator " + back_text(back) + ".")
def ask_strategy():
s = plain(input("strategy (wait, ask peers, presume abort or presume commit)> "))
if s == "":
print("Cancelled.")
return ""
for x in twopc.strategies():
if x == s:
return s
print("Type wait, ask peers, presume abort or presume commit.")
return ""
def verdict(r):
o = twopc.outcome(r)
c = []
a = []
d = []
for i in range(0, len(r[1])):
if r[1][i] == "committed":
c = c + [twopc.name(i)]
elif r[1][i] == "aborted":
a = a + [twopc.name(i)]
elif r[1][i] == "prepared":
d = d + [twopc.name(i)]
if o[0]:
print("Split: " + names_text(c) + " committed, and " + names_text(a) + " aborted.")
if o[1]:
wrong = []
for i in range(0, len(r[1])):
if (r[1][i] == "committed" or r[1][i] == "aborted") and r[1][i] != twopc.past(r[4]):
wrong = wrong + [twopc.name(i)]
print("Against the coordinator, which logged " + r[4] + ": " + names_text(wrong) + " " + opposite(r[4]) + ".")
if o[3]:
never = []
for i in range(0, len(r[1])):
if r[8][i] < 0:
never = never + [twopc.name(i)]
print("Committed without every yes: " + names_text(c) + " committed, though " + names_text(never) + " never voted yes.")
if o[2]:
print("Still in doubt at tick 40, data locked: " + names_text(d) + ".")
if len(c) == 0 and len(a) == 0 and len(d) == 0:
if r[4] == "":
print("No participant was asked, and the coordinator never logged a decision.")
else:
print("No participant was asked; the coordinator logged " + r[4] + ".")
elif not twopc.wrong(o) and not o[2]:
common = "aborted"
if len(c) > 0:
common = "committed"
if r[4] == "":
print("Atomic: everyone who finished " + common + ", and the coordinator never logged a decision.")
else:
print("Atomic: everyone who finished " + common + ", as the coordinator logged.")
def opposite(d):
if d == "commit":
return "aborted"
return "committed"
def one_run(votes, timeout, back):
s = ask_strategy()
if s == "":
return
n = twopc.crash_points(votes, timeout, back, 40)
t = plain(input("crash after step (0 to " + str(n) + ", or none)> "))
if t == "":
print("Cancelled.")
return
crash = 0 - 1
if t != "none":
if not is_digits(t) or len(t) > 2 or int(t) > n:
print("Type a step from 0 to " + str(n) + ", or none.")
return
crash = int(t)
r = twopc.run(votes, s, timeout, back, crash, 40)
if crash < 0:
print(s + ", no crash:")
else:
print(s + ", the coordinator crashing after step " + str(crash) + " (it " + back_text(back) + "):")
for e in r[0]:
print(" tick " + lpad(str(e[0]), 2) + " " + e[1])
for i in range(0, len(votes)):
p = twopc.name(i)
st = r[1][i]
if st == "prepared":
print(" " + p + " still in doubt at tick 40, its data locked for " + ticks_text(r[2][i]) + ".")
elif st == "idle":
print(" " + p + " was never asked.")
elif r[2][i] == 0:
print(" " + p + " " + st + " at tick " + str(r[6][i]) + ", never locked.")
else:
print(" " + p + " " + st + " at tick " + str(r[6][i]) + ", its data locked for " + ticks_text(r[2][i]) + ".")
verdict(r)
def every(votes, timeout, back):
n = twopc.crash_points(votes, timeout, back, 40)
labels = twopc.run(votes, "wait", timeout, back, 0 - 1, 40)[7]
print("Every crash point, votes " + names_text(votes_text(votes)) + "; a participant in doubt acts after " + ticks_text(timeout) + "; the coordinator " + back_text(back) + ":")
widths = [9, 9, 13, 14]
head = " " + pad("crash after", 26)
for k in range(0, 4):
head = head + " " + pad(twopc.strategies()[k], widths[k])
print(rstrip(head))
wrong = [0, 0, 0, 0]
doubt = [0, 0, 0, 0]
most = [0, 0, 0, 0]
stuck = []
for c in range(0 - 1, n+1):
label = "none"
if c == 0:
label = "0 before any step"
elif c > 0:
label = str(c) + " " + labels[c - 1]
line = " " + pad(label, 26)
for k in range(0, 4):
r = twopc.run(votes, twopc.strategies()[k], timeout, back, c, 40)
o = twopc.outcome(r)
cell = twopc.letters(r)
if twopc.wrong(o):
cell = cell + " !"
wrong[k] = wrong[k] + 1
if o[2]:
doubt[k] = doubt[k] + 1
if k == 1:
stuck = stuck + [str(c)]
for x in r[2]:
if x > most[k]:
most[k] = x
line = line + " " + pad(cell, widths[k])
print(rstrip(line))
print(" c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.")
for k in range(0, 4):
print(" " + pad(twopc.strategies()[k] + ":", 16) + "wrong at " + str(wrong[k]) + " of " + str(n + 2) + " crash points, still in doubt at " + str(doubt[k]) + ", data locked at most " + ticks_text(most[k]) + ".")
if len(stuck) == 1:
print("Ask peers is still in doubt only at crash point " + stuck[0] + ": every participant had voted yes, and none had heard the decision.")
elif len(stuck) > 1:
print("Ask peers is still in doubt only at crash points " + names_text(stuck) + ": every participant had voted yes, and none had heard the decision.")
print("Every pattern of " + str(len(votes)) + " votes, each with every crash point and none:")
print(" strategy runs wrong in doubt at the end most ticks locked")
for s in twopc.strategies():
x = twopc.census(len(votes), s, timeout, back, 40)
print(" " + pad(s, 14) + lpad(str(x[0]), 8) + lpad(str(x[1]), 7) + lpad(str(x[2]), 21) + lpad(str(x[3]), 19))
def rstrip(s):
j = len(s)
while j > 0 and s[j - 1] == " ":
j = j - 1
return s[0:j]
def ask_votes():
t = plain(input("votes (2 to 4 of yes or no, such as yes yes no)> "))
if t == "":
print("Cancelled.")
return []
out = []
w = ""
for c in t + " ":
if c == " ":
if w == "yes":
out = out + [True]
elif w == "no":
out = out + [False]
elif w != "":
print("Type 2 to 4 votes, each yes or no.")
return []
w = ""
else:
w = w + c
if len(out) < 2 or len(out) > 4:
print("Type 2 to 4 votes, each yes or no.")
return []
return out
def ask_timing(timeout, back):
t = plain(input("in doubt for how long before acting (1 to 9 ticks)> "))
if t == "":
print("Cancelled.")
return []
if len(t) != 1 or t < "1" or t > "9":
print("Type a whole number from 1 to 9.")
return []
b = plain(input("coordinator back after (1 to 30 ticks, or never)> "))
if b == "":
print("Cancelled.")
return []
nb = 0
if b != "never":
if not is_digits(b) or len(b) > 2 or int(b) < 1 or int(b) > 30:
print("Type a whole number from 1 to 30, or never.")
return []
nb = int(b)
return [int(t), nb]
votes = [True, True, True]
timeout = 5
back = 10
print("== Two-phase commit ==")
print("A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.")
running = True
while running:
print("")
print("1) the transaction 2) one run 3) every crash point 4) votes 5) timing 6) quit")
choice = plain(input("choice> "))
if choice == "1":
show(votes, timeout, back)
elif choice == "2":
one_run(votes, timeout, back)
elif choice == "3":
every(votes, timeout, back)
elif choice == "4":
v = ask_votes()
if len(v) > 0:
votes = v
show(votes, timeout, back)
elif choice == "5":
x = ask_timing(timeout, back)
if len(x) > 0:
timeout = x[0]
back = x[1]
show(votes, timeout, back)
elif choice == "6":
running = False
else:
print("Pick a number from 1 to 6.")
print("Bye.")
twopc.eml
eml# P119 two-phase commit - a coordinator and its participants as state
# machines, one coordinator step a tick: prepare each participant (it votes,
# and a yes locks its data), log the decision, tell each participant that
# voted yes. A crash of the coordinator after any step leaves participants
# that voted yes in doubt, their data locked. As in the corpus case
# two-phase-commit-window, what a participant does then decides between
# blocking and a split outcome:
# wait keeps waiting for the coordinator;
# ask peers asks the coordinator if it is up, else the other
# participants: one that knows the outcome, or one never
# asked (which then aborts on its own), settles it;
# presume abort aborts once the timeout has passed;
# presume commit commits once the timeout has passed.
# A coordinator that comes back with no decision logged decides abort.
def strategies():
return ["wait", "ask peers", "presume abort", "presume commit"]
def name(i):
return "P" + str(i + 1)
def run(votes, strategy, timeout, back, crash, horizon):
# votes: a yes or no per participant; back: ticks the coordinator stays
# down after a crash (0: it never comes back); crash: the number of
# steps after which it crashes (-1: none).
# [events as [tick, text], final states, ticks locked, still locked,
# the coordinator's logged decision ("" if none), steps taken, the
# tick each participant finished (-1 if not), a label per step, the
# tick each voted yes (-1 if it never did)]
len(votes) => n
[] => state
[] => since
[] => until
[] => noted
for v in votes:
state + ["idle"] => state
since + [0 - 1] => since
until + [0 - 1] => until
noted + [""] => noted
[] => events
[] => labels
"prepare" => phase
0 => nxt
"" => decision
False => logged
[] => told
0 => tell_at
False => done
0 => steps
False => down
False => crashed_once
0 - 1 => up_at
if crash == 0:
True => down
True => crashed_once
events + [[0, "the coordinator crashes before its first step"]] => events
if back > 0:
back + 1 => up_at
for t in [1:horizon]:
if down and up_at == t:
False => down
"tell" => phase
0 => tell_at
if not logged:
events + [[t, "the coordinator is back; with no decision logged, it decides abort"]] => events
"abort" => decision
True => logged
steps + 1 => steps
labels + ["decide abort on its return"] => labels
else:
events + [[t, "the coordinator is back with " + decision + " logged, and tells everyone again"]] => events
elif not down and not done:
steps + 1 => steps
if phase == "prepare":
nxt => i
nxt + 1 => nxt
labels + ["prepare " + name(i)] => labels
if state[i] == "idle" and votes[i]:
"prepared" => state[i]
t => since[i]
told + [i] => told
events + [[t, "prepare " + name(i) + ": it votes yes and locks its data"]] => events
if nxt == n:
"decide" => phase
else:
if state[i] == "idle":
"aborted" => state[i]
t => until[i]
events + [[t, "prepare " + name(i) + ": it votes no"]] => events
"decide" => phase
"abort" => decision
elif phase == "decide":
if decision == "":
"commit" => decision
True => logged
labels + ["log " + decision] => labels
events + [[t, "the coordinator logs " + decision]] => events
"tell" => phase
0 => tell_at
else:
told[tell_at] => i
tell_at + 1 => tell_at
labels + ["tell " + name(i)] => labels
if state[i] == "prepared":
past(decision) => state[i]
t => until[i]
events + [[t, "tell " + name(i) + " " + decision + ": it " + verb(decision) + " and unlocks"]] => events
elif state[i] == past(decision):
events + [[t, "tell " + name(i) + " " + decision + ": it had already " + past(decision)]] => events
else:
events + [[t, "tell " + name(i) + " " + decision + ": but it had already " + state[i]]] => events
if crash > 0 and steps == crash and not crashed_once:
True => down
True => crashed_once
events + [[t, "the coordinator crashes"]] => events
if back > 0:
t + back + 1 => up_at
if not down and phase == "tell" and tell_at >= len(told):
True => done
"" => known
if logged:
decision => known
for i in [0:n - 1]:
if state[i] == "prepared" and t - since[i] >= timeout:
learn(state, votes, i, strategy, down, known, n) => r
if r[0] != "":
r[0] => state[i]
t => until[i]
if r[1] >= 0:
"aborted" => state[r[1]]
t => until[r[1]]
events + [[t, name(r[1]) + ", never asked, aborts on its own"]] => events
events + [[t, name(i) + " in doubt: " + r[2]]] => events
elif noted[i] != r[2]:
r[2] => noted[i]
events + [[t, name(i) + " in doubt: " + r[2]]] => events
[] => locked
[] => still
for i in [0:n - 1]:
if since[i] < 0:
locked + [0] => locked
still + [False] => still
elif until[i] < 0:
locked + [horizon - since[i]] => locked
still + [True] => still
else:
locked + [until[i] - since[i]] => locked
still + [False] => still
"" => final
if logged:
decision => final
return [events, state, locked, still, final, steps, until, labels, since]
def verb(d):
if d == "commit":
return "commits"
return "aborts"
def past(d):
if d == "commit":
return "committed"
return "aborted"
def learn(state, votes, i, strategy, down, decision, n):
# what participant i in doubt does now: [new state or "", a participant
# never asked that aborts on its own or -1, what it says]
if strategy == "presume abort":
return ["aborted", 0 - 1, "presumes abort and unlocks"]
if strategy == "presume commit":
return ["committed", 0 - 1, "presumes commit and unlocks"]
if strategy == "wait":
return ["", 0 - 1, "waits, its data locked"]
if not down:
if decision != "":
return [past(decision), 0 - 1, "asks the coordinator: " + decision]
return ["", 0 - 1, "asks the coordinator: no decision yet, so it waits"]
for j in [0:n - 1]:
if j != i and (state[j] == "committed" or state[j] == "aborted"):
return [state[j], 0 - 1, "asks " + name(j) + ", which has " + state[j] + ", and " + verb(present(state[j])) + " too"]
for j in [0:n - 1]:
if j != i and state[j] == "idle":
return ["aborted", j, "asks " + name(j) + ", and aborts too"]
return ["", 0 - 1, "asks the others, all in doubt too, so it waits, its data locked"]
def present(s):
if s == "committed":
return "commit"
return "abort"
def outcome(r):
# [split, against the coordinator, in doubt at the end, committed though
# someone never voted yes]
False => c
False => a
False => doubt
False => against
False => no_yes
for i in [0:len(r[1]) - 1]:
if r[8][i] < 0:
True => no_yes
r[1][i] => s
if s == "committed":
True => c
if s == "aborted":
True => a
if s == "prepared":
True => doubt
if r[4] != "" and (s == "committed" or s == "aborted") and s != past(r[4]):
True => against
return [c and a, against, doubt, c and no_yes]
def wrong(o):
return o[0] or o[1] or o[3]
def letters(r):
"" => out
for s in r[1]:
if out != "":
out + " " => out
if s == "committed":
out + "c" => out
elif s == "aborted":
out + "a" => out
elif s == "prepared":
out + "?" => out
else:
out + "-" => out
return out
def crash_points(votes, timeout, back, horizon):
# the number of steps the coordinator takes with no crash
return run(votes, "wait", timeout, back, 0 - 1, horizon)[5]
def patterns(n):
[[]] => out
for k in [1:n]:
[] => more
for p in out:
more + [p + [True]] => more
more + [p + [False]] => more
more => out
return out
def census(n, strategy, timeout, back, horizon):
# over every vote pattern and every crash point (and none): [runs,
# wrong (split or against the coordinator), in doubt at the end, most
# ticks locked]
0 => runs
0 => bad
0 => doubt
0 => most
for votes in patterns(n):
for c in [0 - 1:crash_points(votes, timeout, back, horizon)]:
run(votes, strategy, timeout, back, c, horizon) => r
outcome(r) => o
runs + 1 => runs
if wrong(o):
bad + 1 => bad
if o[2]:
doubt + 1 => doubt
for x in r[2]:
if x > most:
x => most
return [runs, bad, doubt, most]
Python projection (twopc.py)
def strategies():
return ["wait", "ask peers", "presume abort", "presume commit"]
def name(i):
return "P" + str(i + 1)
def run(votes, strategy, timeout, back, crash, horizon):
n = len(votes)
state = []
since = []
until = []
noted = []
for v in votes:
state = state + ["idle"]
since = since + [0 - 1]
until = until + [0 - 1]
noted = noted + [""]
events = []
labels = []
phase = "prepare"
nxt = 0
decision = ""
logged = False
told = []
tell_at = 0
done = False
steps = 0
down = False
crashed_once = False
up_at = 0 - 1
if crash == 0:
down = True
crashed_once = True
events = events + [[0, "the coordinator crashes before its first step"]]
if back > 0:
up_at = back + 1
for t in range(1, horizon+1):
if down and up_at == t:
down = False
phase = "tell"
tell_at = 0
if not logged:
events = events + [[t, "the coordinator is back; with no decision logged, it decides abort"]]
decision = "abort"
logged = True
steps = steps + 1
labels = labels + ["decide abort on its return"]
else:
events = events + [[t, "the coordinator is back with " + decision + " logged, and tells everyone again"]]
elif not down and not done:
steps = steps + 1
if phase == "prepare":
i = nxt
nxt = nxt + 1
labels = labels + ["prepare " + name(i)]
if state[i] == "idle" and votes[i]:
state[i] = "prepared"
since[i] = t
told = told + [i]
events = events + [[t, "prepare " + name(i) + ": it votes yes and locks its data"]]
if nxt == n:
phase = "decide"
else:
if state[i] == "idle":
state[i] = "aborted"
until[i] = t
events = events + [[t, "prepare " + name(i) + ": it votes no"]]
phase = "decide"
decision = "abort"
elif phase == "decide":
if decision == "":
decision = "commit"
logged = True
labels = labels + ["log " + decision]
events = events + [[t, "the coordinator logs " + decision]]
phase = "tell"
tell_at = 0
else:
i = told[tell_at]
tell_at = tell_at + 1
labels = labels + ["tell " + name(i)]
if state[i] == "prepared":
state[i] = past(decision)
until[i] = t
events = events + [[t, "tell " + name(i) + " " + decision + ": it " + verb(decision) + " and unlocks"]]
elif state[i] == past(decision):
events = events + [[t, "tell " + name(i) + " " + decision + ": it had already " + past(decision)]]
else:
events = events + [[t, "tell " + name(i) + " " + decision + ": but it had already " + state[i]]]
if crash > 0 and steps == crash and not crashed_once:
down = True
crashed_once = True
events = events + [[t, "the coordinator crashes"]]
if back > 0:
up_at = t + back + 1
if not down and phase == "tell" and tell_at >= len(told):
done = True
known = ""
if logged:
known = decision
for i in range(0, n):
if state[i] == "prepared" and t - since[i] >= timeout:
r = learn(state, votes, i, strategy, down, known, n)
if r[0] != "":
state[i] = r[0]
until[i] = t
if r[1] >= 0:
state[r[1]] = "aborted"
until[r[1]] = t
events = events + [[t, name(r[1]) + ", never asked, aborts on its own"]]
events = events + [[t, name(i) + " in doubt: " + r[2]]]
elif noted[i] != r[2]:
noted[i] = r[2]
events = events + [[t, name(i) + " in doubt: " + r[2]]]
locked = []
still = []
for i in range(0, n):
if since[i] < 0:
locked = locked + [0]
still = still + [False]
elif until[i] < 0:
locked = locked + [horizon - since[i]]
still = still + [True]
else:
locked = locked + [until[i] - since[i]]
still = still + [False]
final = ""
if logged:
final = decision
return [events, state, locked, still, final, steps, until, labels, since]
def verb(d):
if d == "commit":
return "commits"
return "aborts"
def past(d):
if d == "commit":
return "committed"
return "aborted"
def learn(state, votes, i, strategy, down, decision, n):
if strategy == "presume abort":
return ["aborted", 0 - 1, "presumes abort and unlocks"]
if strategy == "presume commit":
return ["committed", 0 - 1, "presumes commit and unlocks"]
if strategy == "wait":
return ["", 0 - 1, "waits, its data locked"]
if not down:
if decision != "":
return [past(decision), 0 - 1, "asks the coordinator: " + decision]
return ["", 0 - 1, "asks the coordinator: no decision yet, so it waits"]
for j in range(0, n):
if j != i and (state[j] == "committed" or state[j] == "aborted"):
return [state[j], 0 - 1, "asks " + name(j) + ", which has " + state[j] + ", and " + verb(present(state[j])) + " too"]
for j in range(0, n):
if j != i and state[j] == "idle":
return ["aborted", j, "asks " + name(j) + ", and aborts too"]
return ["", 0 - 1, "asks the others, all in doubt too, so it waits, its data locked"]
def present(s):
if s == "committed":
return "commit"
return "abort"
def outcome(r):
c = False
a = False
doubt = False
against = False
no_yes = False
for i in range(0, len(r[1])):
if r[8][i] < 0:
no_yes = True
s = r[1][i]
if s == "committed":
c = True
if s == "aborted":
a = True
if s == "prepared":
doubt = True
if r[4] != "" and (s == "committed" or s == "aborted") and s != past(r[4]):
against = True
return [c and a, against, doubt, c and no_yes]
def wrong(o):
return o[0] or o[1] or o[3]
def letters(r):
out = ""
for s in r[1]:
if out != "":
out = out + " "
if s == "committed":
out = out + "c"
elif s == "aborted":
out = out + "a"
elif s == "prepared":
out = out + "?"
else:
out = out + "-"
return out
def crash_points(votes, timeout, back, horizon):
return run(votes, "wait", timeout, back, 0 - 1, horizon)[5]
def patterns(n):
out = [[]]
for k in range(1, n+1):
more = []
for p in out:
more = more + [p + [True]]
more = more + [p + [False]]
out = more
return out
def census(n, strategy, timeout, back, horizon):
runs = 0
bad = 0
doubt = 0
most = 0
for votes in patterns(n):
for c in range(0 - 1, crash_points(votes, timeout, back, horizon)+1):
r = run(votes, strategy, timeout, back, c, horizon)
o = outcome(r)
runs = runs + 1
if wrong(o):
bad = bad + 1
if o[2]:
doubt = doubt + 1
for x in r[2]:
if x > most:
most = x
return [runs, bad, doubt, most]