two-phase-commit-lossy.writ

; Two-phase commit over a network that DROPS messages and retransmits them.
; 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 network loses a message, and the coordinator sends it again ───────────
; `deliver` already fires whenever the inbox is empty, so losing a message
; simply re-enables delivery. There is no crash here: the coordinator is alive
; throughout, and this is a CORRECT, retransmitting protocol. It is also the
; model on which `live` and `inevitable` part company.

(form (lossy P LOSE)
  (transition LOSE
    (when (and (defined P.inbox) (is P.state prepared)))
    (do (vacate P.inbox))))

(lossy p1 lose-p1)
(lossy p2 lose-p2)