writ-problems/two-phase-commit/two-phase-commit-timeout.writ at main · writ-lang/writ-problems · GitHub

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
; Two-phase commit PLUS a participant timeout — the tempting fix, and the trade.
; agree to abort, and never one of each.
;
; THE SETTING. Some work has to happen in two places at once — money leaves one
; ledger and arrives in another, say. Neither place can see the other's
; internals, and either may fail. A COORDINATOR asks each PARTICIPANT whether it
; can commit; if all say yes it decides commit, otherwise abort; then it tells
; each participant what was decided.
;
; A participant that has voted yes is PREPARED, and that is the important word:
; it has promised to commit if told to, so it may no longer decide for itself.
; It holds its locks and waits.
;
; A MESSAGE IS A SLOT. `vote` is the participant's message to the coordinator;
; `inbox` is the coordinator's message back. Both are `maybe`, so an empty slot
; is "nothing has been sent", which is a state the model can be asked about.
;
; The coordinator may CRASH at any moment — including after deciding, and
; including after telling one participant and not the other.

(load "stdlib.writ")

(schema tpc
  (type vote-t (yes no))
  (type dec-t  (commit abort))
  ; A participant's own view of the work: not yet voted, promised, or finished.
  (type pstate (working prepared committed aborted))
  (type cstate (collecting decided crashed))

  (type participant
    (arrow state (to pstate))
    (maybe vote  vote-t)              ; in flight to the coordinator
    (maybe inbox dec-t))              ; in flight to this participant

  (type coordinator
    (arrow state (to cstate))
    (maybe decision dec-t)))

(instance start tpc
  (coordinator c  (state collecting) (decision vacant))
  (participant p1 (state working) (vote vacant) (inbox vacant))
  (participant p2 (state working) (vote vacant) (inbox vacant)))

(use tpc)
(initial start)

; ── phase one, and phase two, for one participant ─────────────────────────────
; Written once and instantiated per participant. A form renames and pastes, so
; this is the same five moves twice, not a loop.

(form (participant-moves P YES NO DELIVER APPLY-C APPLY-A)
  ; Voting yes IS preparing: the participant gives up deciding for itself.
  (transition YES
    (when (is P.state working))
    (do (set P.state prepared) (set P.vote yes)))
  ; Voting no is a unilateral abort, and is always safe — nobody was promised
  ; anything.
  (transition NO
    (when (is P.state working))
    (do (set P.state aborted) (set P.vote no)))
  ; Phase two: the decision travels to one participant at a time.
  (transition DELIVER
    (when (and (is c.state decided) (not (defined P.inbox))))
    (do (set P.inbox c.decision)))
  (transition APPLY-C
    (when (and (is P.state prepared) (is P.inbox commit)))
    (do (set P.state committed)))
  (transition APPLY-A
    (when (and (is P.state prepared) (is P.inbox abort)))
    (do (set P.state aborted))))

(participant-moves p1 p1-yes p1-no deliver-p1 p1-commit p1-abort)
(participant-moves p2 p2-yes p2-no deliver-p2 p2-commit p2-abort)

; ── the decision: taken once, by the coordinator alone ────────────────────────
; `all` and `some` quantify over the roster, so these two moves are written once
; however many participants there are.

(transition c-commit
  (when (and (is c.state collecting) (all (p participant) (is p.vote yes))))
  (do (set c.decision commit) (set c.state decided)))

(transition c-abort
  (when (and (is c.state collecting) (some (p participant) (is p.vote no))))
  (do (set c.decision abort) (set c.state decided)))

; ── the fault ─────────────────────────────────────────────────────────────────
; The coordinator stops. Nothing it would have done afterwards exists.

(transition c-crash
  (when (not (is c.state crashed)))
  (do (set c.state crashed)))

; ── the "fix": a prepared participant that gives up waiting ───────────────────
; The blocking above is intolerable in practice — locks held for ever — so the
; obvious remedy is to let a participant abort once it can see the coordinator
; is gone. `writ compare` prices what that costs.

(form (timeout P T)
  (transition T
    (when (and (is P.state prepared) (is c.state crashed)
               (not (defined P.inbox))))
    (do (set P.state aborted))))

(timeout p1 p1-timeout)
(timeout p2 p2-timeout)