Two-Phase Commit

Two-Phase Commit (2PC) is the standard protocol for distributed transactions. One coordinator sends prepare, participants vote yes/no, and the coordinator decides commit (all yes) or abort (any no).

The spec

Source

module TwoPhaseCommit

// Two-Phase Commit (2PC) protocol for distributed transactions.
// One coordinator, N+1 participants. Coordinator sends prepare,
// participants vote yes/no, coordinator decides commit (all yes)
// or abort (any no). Participants apply the decision.
//
// Key invariant: all participants that decide agree on the outcome.
// If any participant commits, no participant aborts (and vice versa).
//
// Use: specl check two-phase-commit.specl -c N=2 --no-deadlock --no-auto --bfs
// Verified: N=2 -> OK (134 states, 0.0s)

const N: 0..3

// Coordinator state: 0=init, 1=waiting, 2=committed, 3=aborted
var coord_pc: 0..3

// Per-participant state: 0=init, 1=voted_yes, 2=voted_no, 3=committed, 4=aborted
var part_pc: Dict[0..N, 0..4]

// Votes received by coordinator
var vote: Dict[0..N, 0..1]  // 0=no vote yet/no, 1=yes
var voted: Dict[0..N, Bool]

init {
    coord_pc = 0;
    part_pc = {p: 0 for p in 0..N};
    vote = {p: 0 for p in 0..N};
    voted = {p: false for p in 0..N};
}

// Coordinator sends prepare (transitions to waiting)
action Prepare() {
    require coord_pc == 0;
    coord_pc = 1;
}

// Participant votes yes
action VoteYes(p: 0..N) {
    require coord_pc == 1;
    require part_pc[p] == 0;
    part_pc = part_pc | {p: 1};
    vote = vote | {p: 1};
    voted = voted | {p: true};
}

// Participant votes no
action VoteNo(p: 0..N) {
    require coord_pc == 1;
    require part_pc[p] == 0;
    part_pc = part_pc | {p: 2};
    vote = vote | {p: 0};
    voted = voted | {p: true};
}

// Coordinator decides commit (all voted yes)
action DecideCommit() {
    require coord_pc == 1;
    require all p in 0..N: voted[p] == true;
    require all p in 0..N: vote[p] == 1;
    coord_pc = 2;
}

// Coordinator decides abort (at least one voted no)
action DecideAbort() {
    require coord_pc == 1;
    require any p in 0..N: voted[p] == true and vote[p] == 0;
    coord_pc = 3;
}

// Participant applies commit decision
action ParticipantCommit(p: 0..N) {
    require coord_pc == 2;
    require part_pc[p] == 1;
    part_pc = part_pc | {p: 3};
}

// Participant applies abort decision
action ParticipantAbort(p: 0..N) {
    require coord_pc == 3;
    require part_pc[p] == 1 or part_pc[p] == 2;
    part_pc = part_pc | {p: 4};
}

// Agreement: no participant commits while another aborts
invariant Agreement {
    all i in 0..N: all j in 0..N:
        not (part_pc[i] == 3 and part_pc[j] == 4)
}

// Validity: if coordinator commits, all participants voted yes
invariant CommitImpliesAllYes {
    coord_pc == 2 implies all p in 0..N: vote[p] == 1
}

What to notice

• Quantifiers in guards. require all p in 0..N: voted[p] == true — the coordinator waits for all votes. require any p in 0..N: voted[p] == true and vote[p] == 0 — abort if any vote is no.
• implies in invariants. coord_pc == 2 implies all p in 0..N: vote[p] == 1 — if committed, all must have voted yes.
• Agreement invariant. No participant commits while another aborts — the fundamental safety property of 2PC.

specl check two-phase-commit.specl -c N=2 --no-deadlock