Expand description
The Synod protocol of Multi-Paxos: ballots, acceptors, scouts, commanders and leaders.
Status: implementation. Space: bounded by membership and by the distance between the collection watermark and the frontier — see the section on it below, and the condition it carries.
van Renesse, R. and Altinbuken, D. (2015) ‘Paxos Made Moderately Complex’, ACM Computing
Surveys, 47(3), pp. 1–36, §2. Figures 4, 6 and 7 are quoted above the code that implements
them. The edition matters: the 2011 Cornell technical report of the same title numbers its
figures differently and its acceptor differs materially from this one, so a reader checking the
code against the page needs to know which page. See CLAUDE.md, Reference material.
The cross-check is Liu, Y.A., Chand, S. and Stoller, S.D. (2019) ‘Moderately Complex Paxos Made Simple’, PPDP ’19 — the same algorithm specified in DistAlgo with machine-checked TLA+ safety proofs. It reports four liveness violations in this specification when messages can be lost, which is this repository’s setting rather than a hypothetical one, and one further issue in the acceptor. Three of the four and the acceptor issue are fixed here; each is cited where it departs from the survey’s pseudocode.
§What it guarantees, and what it does not
S1 [always] At most one proposal is ever chosen for a slot
S2 [always] A chosen proposal is one some process proposed
S3 [Ω settles] Progress — every proposed slot eventually has a proposal chosenS1 and S2 hold whatever the schedule, whatever the ballots in flight and whatever has crashed. S3 does not, and the source is blunt about it: §3 opens by observing that duelling leaders can preempt one another for ever and that the Synod protocol guarantees nothing about progress “even in the absence of any failure whatsoever”.
§Roles, and where each one lives
§4.4 says the roles are co-located on one machine in practice, and that is the shape built here: one protocol per process holding both the acceptor and the leader. Neither has a vocabulary the other does not, and both send and receive on the same wire, so composing them as children would buy two wrap functions and a message split that carries nothing.
Scouts and commanders are the leader’s own bookkeeping rather than child protocols, for the
question link.rs asks of everything: does this thing have a vocabulary of its own? It does
not. What a scout is, concretely, is a waitfor set and a union of pvalues; what a commander
is, is a waitfor set and the pvalue it is responsible for. The source models them as threads
because it is written in a language where a thread is the cheapest way to say “wait for a
majority”. Here they are the leader’s own scout and commanders fields, and the mapping
from each figure’s for ever / switch receive arm to where it went is stated above the
handler that took it.
The source’s constraints on their number are in the types rather than in a comment: at most one
scout, “and only for its own ballots”, is an Option; at most one commander per ⟨ballot, slot⟩ (Invariant C1) is a map keyed by slot, cleared when the ballot changes.
§Departure: a p2b names its slot
Figure 4 answers a p2a with ⟨p2b, self(), ballot_num⟩ — no slot. It does not need one:
the reply goes to the commander thread that sent the request, and the thread’s identity is what
routes it. Folding commanders into the leader removes that identity, and a leader running
commanders for several slots at once cannot tell from ⟨p2b, α, b⟩ which of them answered. So
the slot travels in the message.
This is the structural decision above paying for itself, and it is the whole of the price: no
guarantee changes, because the slot was already determined by the request the reply answers.
⟨p1b, α, b, r⟩ needs no such addition — a leader runs at most one scout, so its ballot routes
it.
§Departure: a reply naming a ballot below the attempt’s is stale, and is discarded
The same cause, and it is the half that bites. Figures 6(a) and 6(b) branch on b' = b and
treat everything else as a preemption, which is sound for a thread: a reply to a request the
thread did not send cannot reach it, because the thread that sent that request has exited and
the reply is addressed to it. A scout that is a field has no such address, so a late answer
to the previous attempt arrives at the current one.
Taking the figure literally there is a liveness bug, and it was measured before this guard
existed. A leader is preempted, climbs, and starts a scout for the new ballot; the second
acceptor’s answer to the old ballot then arrives, fails b' = b, and takes the else arm —
which discards the running scout and reports a preemption the leader correctly ignores, because
the ballot in it is below the one it now holds. The leader is left with no scout, not active,
and nothing in the sweep to restart it. It stops for ever, while Ω goes on trusting it.
So a reply is classified against the attempt it reaches: above its ballot is a preemption, equal is an answer, and below is an answer to an attempt that has already exited and is discarded. Under Figure 6’s own model the third case cannot arise, which is why the figure does not name it.
§Departure: the acceptor accepts under b ≥ ballot_num, and adopts what it accepts
Figure 4 accepts a pvalue only when b = ballot_num, and Figure 6(a)’s commander treats any
reply naming a different ballot as a preemption. The two compose only because §2.3 asserts that
every p2b carries b' ≥ b, and that assertion rests on the acceptor having seen phase 1
before phase 2 — which the link beneath this module does not guarantee.
The case is concrete rather than theoretical. An acceptor’s p1a dies at a session ending; the
scout completes with a majority that excludes it; the retransmitted p2a then reaches an
acceptor whose ballot_num is below b. Under the survey’s text that acceptor refuses,
answers with its own lower ballot, and the commander reads the mismatch as a preemption and
exits — while the leader ignores the preemption, because the ballot in it is below its own.
The slot then has no commander, so the retry sweep no longer covers it, and nothing moves until
the phase-two escalation notices a whole timeout later.
So the acceptor here takes the 2011 report’s condition — if b ≥ ballot_num then ballot_num := b; accepted := accepted ∪ {⟨b,s,c⟩} — which is also the fix Liu et al. give for what they name
the useless-replies issue in this acceptor. Every p2b then names a ballot at least as high as
the request’s, the commander’s else-arm is a genuine preemption again, and the property §2.3
asserts without support holds here by construction.
Safety is unaffected, and this is the one place to be sure of it. Invariant A1 — an acceptor
adopts strictly increasing ballots — still holds: ballot_num only ever moves up. A2 becomes
“accepts ⟨b,s,c⟩ only where b = ballot_num after the adoption in the same transition”,
which is what the argument in §2.4 actually uses: what matters is that an acceptor which has
adopted b never afterwards accepts below b, and adopting on the way in makes that more
true rather than less. A4 is unaffected because it is enforced by the leader (C1), not the
acceptor.
§Departure: liveness comes from Ω, not from the source’s pinging
§3 has a preempted leader monitor the preempting one by pinging it on a regular basis, backing
off with an AIMD timeout, and says outright that “this concept is called failure detection”.
This module composes EventualLeaderDetector instead and acts on Trust: it starts a scout
for its next ballot when trusted, and stays passive otherwise. A preemption moves ballot_num
past the ballot that beat it but starts no scout unless this process is still trusted, which is
what stops the duel §3 opens by describing.
What differs: Ω names one leader, where the source’s scheme lets any correct leader win a
race and merely makes the loser wait longer each time. Ω is the stronger assumption and the
cheaper mechanism, and it is conditional on everything its own chain is conditional on —
stated at each link in docs/conditional-guarantees.md rather than collapsed into one claim
here. What it costs is that a correct process Ω does not trust will not lead however long it
waits.
§Colocation: the replica is on this machine, so two messages are this layer’s
§4.4 describes the deployment this module is built for: “each machine that runs a replica also runs a leader… the replica can send a proposal for a particular slot to its local leader, say λ, rather than broadcasting the request to all leaders. If λ is passive, monitoring another leader λ′, it forwards the proposal to λ′. If λ is active, it will start a commander.”
Taking that shape puts two messages here that a separated deployment would put above, and one of them is on this layer’s own figure:
- A commander announces its decision to every process. Figure 6(a)’s last line,
∀ρ ∈ replicas : send(ρ, ⟨decision, s, c⟩). Every process raisesInd::Decision, not only the one whose commander counted the majority, because a log above cannot be built from a decision one process holds. The addressees are the processes of the run: colocation makes the replica set and the acceptor set one here. - A leader that cannot act on a proposal forwards it to the process Ω trusts. Not on any figure — §4.4’s sentence above. Without it a proposal made at a process Ω never trusts is never acted on at all.
What this costs, and it is not free: the delivery of a proposal now rests on the detector. A
proposal goes to one process where it used to reach every leader, so a request handed to a
process whose detector names a leader that has crashed is lost. Nothing here recovers it — the
layer above must ask again, and multi_paxos_replica’s re-proposal timeout is what does. Before
colocation an inaccurate detector cost nothing for delivery; it now costs a request, and the
suite drives that case rather than assuming it away.
A Propose that arrived is never forwarded again. Two processes whose detectors disagree
would otherwise pass one back and forth for as long as they disagree. The message carries no hop
count and needs none: an arrived proposal is handled locally or dropped, so the path is at most
two hops by construction, and the asker’s own timeout is what recovers a drop.
§Departure: a leader answers a re-proposal for a decided slot
The leader-side half of the fourth liveness fix Liu et al. describe, and the half without which
the replica’s re-proposal is a loop rather than a recovery. A decision is announced once, by
the commander that counted the majority, which then exits. A process the announcement never
reached has no other way back: nothing here retransmits a decision once its commander is gone,
the retry sweep walks the waitfor sets of live commanders, and the session link does not
resend across an ending.
So a leader keeps the slots it has seen decided, and answers a Propose for one with
⟨decision, s, c⟩ sent to the asker alone — one message, where the announcement was a
fan-out. Liu et al. put it directly: a leader “can then work on deciding for that slot if a
decision for it has not been made; otherwise, it can send back the decision for that slot”.
Without the answer, a re-proposal for a decided slot meets the ∄c' guard, is dropped, and the
asker re-proposes for ever.
The command in the answer comes from the decision, never from proposals. The first draft
took it from proposals[slot], arguing that for a decided slot that is the decided command — it
was the commanded value in the ballot that decided, and any later adoption’s pmax writes it
back. That argument holds for the leader that decided and for any leader that adopted afterwards,
and it is false for the third case: a leader that commanded something else for the slot, was
preempted, and never adopted again. Nothing rewrites that leader’s proposals; the announcement
of the real decision still marks the slot decided; and a forwarded re-proposal would then be
answered with a command that was never chosen, which a replica whose detector names that process
would apply. the_answer_names_the_decided_command_not_the_answerers_own_stale_proposal is the
schedule. So decided keeps the command beside the slot, filled from the same two places every
process learns a decision — its own commander counting a majority, and another’s announcement —
and R1 is what makes either source the right one. A consequence worth having: any process that
knows the decision can answer, not only the leader that made it.
A leader that has yielded forwards even for a slot it remembered. The same root, on the
liveness side. A trusted process that has not yet adopted remembers a proposal for adopted to
command; if it is preempted first and Ω has moved on, it yields with the entry still in
proposals, and the ∄c' guard would then drop every later proposal its own replica makes for
that slot — never forwarded, never commanded by anyone, the one slot nobody else will propose
for, and the re-proposal that exists for exactly this wedge defeated by the process’s own memory.
So the guard applies only where this process can act, and a passive, untrusted process forwards
and forgets: what it remembered is dead weight, and anything a majority accepted comes back
through pmax if it ever leads again.
a_proposal_remembered_by_a_leader_that_then_yields_is_forwarded_when_asked_again is that
schedule.
§Departure: three liveness fixes from the cross-check
Each is reachable here because this link loses messages, and each is Liu et al.’s.
| Where | What is lost | What happens | What this leader does |
|---|---|---|---|
| Phase 1 | p1a | no p1b majority and no preemption ever arrives, so the leader waits for ever | restarts phase one after a timeout |
| Phase 2 | p2b | no decision for that slot, and if it happens at every leader the layer above stalls too | resends p2a for that slot once a round trip has passed |
| Phase 2 | preempt | a majority has moved to a higher ballot, so p2a can never reach one — the leader sends for ever and decides nothing | restarts phase one after a timeout |
The third is the one a naive design gets wrong. Resending p2a cannot help once a majority
holds a higher ballot; the leader has to go back to phase 1. A single retransmission sweep over
unanswered requests recovers from the first two and loops for ever on the third.
§Retransmission: how often it is asked, and how often it is done
One timer, at Timing::retransmit, runs the sweep. It used to decide both questions, and that
was the mistake: every suite here configures retransmit at half the simulator’s delivery
bound, so a request went out again before an answer to it could possibly have arrived. Measured
over ten entries at five processes, phase two cost 3.6× what the algorithm needs — two
thirds of it the protocol talking over itself.
So the sweep decides how often the question is asked and resend_after
decides the answer. Timing::retransmit below the delivery bound is not a tuning choice, it
is a mistake — the same shape as detect_after’s own note about exceeding the bound by a
margin, and with the same remedy: state what the parameter has to exceed. Here the sweep may be
as fine as you like, because it is no longer what sets the rate.
A tick-driven resend is a stubborn link’s idiom in the first place — resend because the
network may have dropped it — and this module runs over a session link, which drops nothing
while a session holds. The only loss is at a session ending, and the establishment that follows
is when a resend can succeed. That event is what resend_to acts on, which
makes the sweep a backstop rather than the mechanism. This is the first module in the repository
to act on SessionEstablished rather than merely propagate it; docs/conditional-guarantees.md
records what that obliges.
Both restarts rerun phase one under the same ballot. For a lost p1a the rerun is
idempotent: an acceptor that already adopted the ballot answers again, and the scout recollects.
For a lost preemption the rerun is how the leader learns what it missed — acceptors that have
moved answer p1b naming their higher ballot, the scout reports that as a preemption, and only
then does ballot_num move. Minting a higher ballot on every timeout would discard phase-two
work already accepted under the current ballot and learn nothing a rerun does not.
The fourth violation is in the replica: if no decision arrives for a slot, every replica stops
applying from that slot, slot_out stops moving, WINDOW fills and the system wedges. Its fix
has two halves. The replica re-proposes after a timeout, which is multi_paxos_replica’s; and
the leader answers a re-proposal for a decided slot, which is this module’s and is the departure
above.
§Space
Bounded, and this is an implementation. An acceptor keeps one pvalue per slot between the
collection watermark and the frontier; a leader keeps one proposal and one decision record over
the same range; and what each member last said it had applied is one entry per member. None of
them grows with the slots handled, which is what docs/bounded-space.md asks of an
implementation.
Both of the source’s reductions are applied. §4 opens by saying “the described protocol is not
practical” and gives them: §4.1, one pvalue per slot rather than one per ⟨ballot, slot⟩,
is the section below; §4.2, collecting below a watermark, is the one after it.
The bound is conditional, and the condition is the source’s own. Collection needs f + 1 of
the 2 f + 1 members reporting their progress, so a run in which f have crashed collects
nothing and grows again — “no garbage collection could be done”, as §4.2 puts it. That is
specified behaviour rather than a defect, and
collection_stalls_when_too_few_members_remain_to_report is there so nobody later reads a stall
as one.
The set of decided slots grows the same way, and the announcement is work per decision rather than per tick: one fan-out when a commander completes, plus one directed answer per re-proposal for a slot already decided. Both are bounded by membership for a given slot and unbounded in slots, which is the same statement as everything else here.
What is bounded is the retry sweep, and it is worth stating precisely because the obvious
claim is wrong. The sweep visits the outstanding waitfor sets: each is bounded by membership,
but their number is not — it grows with the slots proposed and not yet decided. So the sweep
costs membership times the slots in flight. A decision retires its commander and leaves the
sweep, so once the work completes the sweep is empty, which is the window
tests/common::assert_send_rate_flat! measures. Nothing here resends history.
§§4.1: an acceptor keeps only the highest-ballot pvalue per slot
The first of the source’s reductions, applied. §4.1 gives the reason in one sentence:
First, note that although a leader obtains for each slot a set of all accepted pvalues from a majority of acceptors, it only needs to know if this set is empty or not, and if not, what the maximum pvalue is. Thus, a large step toward practicality is that acceptors only maintain the most recently accepted pvalue for each slot (
⊥if no pvalue has been accepted) and return only these pvalues in ap1bmessage to the scout. This gives the leader all information needed to enforce Invariant C2.
So accepted is keyed by slot, the scout reduces per slot as it collects, and p1b carries one
entry per slot. What this removes is growth in the number of ballots a run has seen; what it
leaves is growth in slots, which is §4.2’s and not this section’s.
The comparison is the leader’s, not the acceptor’s, and the sentence quoted above splits it
that way: an acceptor keeps “the most recently accepted pvalue”, and the leader is what “needs
to know … what the maximum pvalue is”. An acceptor writes over its record with no comparison,
because its own promise has already ordered the writes — a stored pvalue’s ballot became
ballot_num when it was stored, ballot_num never falls, and the b ≥ ballot_num arm admits
nothing below it. The one case where an arriving ballot is not strictly above the stored one is
equality, where A4 makes the command the same. A guard there would be a branch nothing can take.
The scout is where the maximum is genuinely taken: two acceptors answering one phase one can
report different ballots for one slot, and nothing orders their answers. That is keep_max, and
it is load-bearing — a scout keeping the last arrival instead of the highest would hand pmax a
command a lower ballot proposed, which is a split slot. Nothing in the suite caught that
until this change measured it: the property used to be structural, carried by the old
⟨ballot, slot⟩ key’s iteration order rather than by any code, and a structural property is one
no test has to name. Moving the reduction to collection time made it code, and code gets a test.
Invariant A4 stops being structural, and does not stop being true. The old key was
⟨ballot, slot⟩, which made “at most one command per ballot and slot” the map’s own property.
A4 was never the acceptor’s to enforce: Invariant C1 gives it — at most one commander per
⟨ballot, slot⟩ — and the leader is what holds C1. The old key bought a second, redundant
enforcement and cost a dimension of growth.
§The record of a choice may be overwritten while the choice stands
The paper raises this against its own reduction, and it is worth stating in full because a reader who assumes otherwise would take a correct run for a broken one:
This optimization leads to a worrisome effect. We know that when a majority of acceptors have accepted the same pvalue
⟨b, s, c⟩, then proposalcis chosen for slots. Consider now the following scenario. […] Acceptorsα₁andα₂accept⟨⟨0, λ⟩, 1, c⟩, and thus proposalcis chosen for slot 1 by ballot⟨0, λ⟩. However, leaderλcrashes before learning this. Now leaderλ′gets acceptorsα₂andα₃to adopt ballot⟨0, λ′⟩. After determining the maximum pvalue among the responses, leaderλ′has to select proposalc. Now suppose that acceptorα₂accepts⟨⟨0, λ′⟩, 1, c⟩. At this point, there is no majority of acceptors that store the same most recently accepted pvalue, and in fact no proof that ballot⟨0, λ⟩even chose proposalc, as that part of the history has been overwritten.
And the answer: “However, the leader of any ballot b after ⟨0, λ⟩ can only select
⟨b, 1, c⟩. This is by Invariant C2 and because acceptors α₁ and α₂ both accepted
⟨⟨0, λ⟩, 1, c⟩ and together form a majority.”
What the reduction discards is evidence, not agreement. The fact outlives the record because
every later ballot had to read the maximum from a majority, and any two majorities intersect —
so the choice is carried forward by a chain of adoptions rather than by anything still stored.
agreement_survives_the_record_of_it_being_overwritten drives exactly the paper’s scenario and
asserts the non-vacuity half from acceptor state: no majority still holds the chosen proposal at
the instant the assertion is made.
One consequence for the suite, and it is why the checker was built the way it was: a checker
reading acceptor state would now be wrong. tests/multi_paxos_synod.rs feeds its checker from
the trace — what was sent, what was indicated — so the reduction does not reach it.
§§4.2: collecting what enough replicas already hold
The second reduction, and what makes this an implementation. §4.2 separates two things, and only the second is this module’s:
In our description of Paxos, much information is kept about slots that have already been decided. Some of this is unavoidable. For example, because commands may be decided in multiple slots, replicas each maintain a set of all decisions to filter out such duplicates. […] But some state, and indeed some work that results from having that state, is unnecessary. The leader maintains state for each slot in which it has a proposal. […] Similarly, even if the state reduction of Section 4.1 is implemented, each acceptor maintains state for each slot. However, once at least
f + 1replicas have learned about the decision of some slot, it is no longer necessary for leaders and acceptors to maintain this state — replicas can learn decisions, and the application state that results from those decisions, from one another.
So each replica reports its slot_out periodically, every process keeps what it was told, and
everything below the highest slot f + 1 members have applied to is discarded: the acceptor’s
pvalues, the leader’s proposals, the record of which slots are decided. The replica’s own
duplicate filter is the unavoidable half and is bounded by a retention window instead — see
crate::multi_paxos_replica, which explains why no watermark bounds it.
§The hazard the section names, and the clause that answers it
However, we must prevent other leaders from mistakenly concluding that the acceptors have not accepted any pvalues for the garbage-collected slots. To achieve this, the state of an acceptor can be extended with a new variable that contains a slot number: all pvalues lower than that slot number have been garbage collected. This slot number must be included in
p1bmessages so that leaders can skip the lower numbered slots.
Before collection, an acceptor reporting nothing for a slot meant nothing had been accepted for
it. Afterwards it means one of two things, and collected is the only thing that tells them
apart. A leader that read a collected slot as free would put a second command up for a slot
already decided — a split slot, reached from the opposite direction to synod-ignore-pmax.
The skip is in two places, and the second is not on the page. adopted drops proposals
below the watermark it was told about, which covers what a leader already held; on_propose
refuses a slot below the watermark, which covers one arriving afterwards. Only the first was
written at first, and agreement_holds_across_a_collection split a slot on the second: the
successor adopted cleanly and was then asked for a different command for a collected slot, and
commanded it. The page does not need the second clause because there a propose comes from a
replica whose slot_in never falls below its own slot_out; nothing in a port guarantees
that, and a layer that assumes its caller is well behaved is not one.
synod-skip-collected is the mutation registered against both.
§What collecting costs, and the transfer that pays for it
Collecting at f + 1 means f correct replicas may be behind — and everything that could have
helped them is precisely what was discarded. This layer no longer holds the decision, and the
leader’s answer to a re-proposal needs that record. A correct process that missed one decision
would be stranded for ever, which is what a_replica_stranded_by_a_collection_catches_up_ from_a_peer drove before the transfer existed: one replica at slot_out = 1 with the leader
holding zero decisions.
The section’s own justification is the remedy — “replicas can learn decisions […] from one
another” — so this layer carries the ask and the answer without holding either. A refused
proposal raises Ind::Collected; the layer above asks with Cmd::CatchUp; the peer’s layer
above answers with Cmd::Teach, from its decisions, and the answers arrive as the ordinary
⟨decision, s, c⟩ the replica already handles. A replica further behind than the retention
window cannot be caught up at all, because nobody holds those decisions any more; that is where
a deployment takes a snapshot, which is outside the paper.
§The boundary this module does not cross
This is crash-stop, which is the source’s own model rather than a scope dodge. A crashed state machine there “will make no more transitions and thus its current state is fixed indefinitely”, and a process that comes back off disk “is not theoretically considered crashed—it is simply slow for a while”. There is no third case, and a process that returns having forgotten what it knew is the first one acting when it is not permitted to.
The simulator can produce that case, and Ω will trust such a process again, so the consequence
has to be stated rather than assumed away. The round counter is volatile: its scope is this
incarnation. A process that restarts re-mints a ballot it has already used; an acceptor still
holding that ballot accepts a second, different proposal under it; and two proposals accepted at
one ballot and slot is exactly what Invariant A4 forbids and what the argument that two
majorities agree depends on. A durable ballot counter, read back in on_recovery, is what
makes leading again after a restart legal, and it belongs with the rest of §4.3 (Keeping State
on Disk) in the fail-recovery change.
A returning process could instead lead under a new identity, which is sound for the leader role — ballot uniqueness is a proposer-side obligation and the proposer set need not be fixed — and unsound for the acceptor role, because majorities of two different acceptor sets need not intersect. The source’s own answer to that is reconfiguration (§5’s Cheap Paxos “reconfigures the system replacing the suspected acceptor with a fresh one”), decided in a slot like any other command. There are no slots to decide it in until the replica exists, so the membership here is fixed for the run.
§The figures
process Acceptor()
var ballot_num := ⊥, accepted := ∅;
for ever
switch receive()
case ⟨p1a, λ, b⟩ :
if b > ballot_num then
ballot_num := b;
end if
send(λ, ⟨p1b, self(), ballot_num, accepted⟩);
end case
case ⟨p2a, λ, ⟨b, s, c⟩⟩ :
if b = ballot_num then
accepted := accepted ∪ {⟨b, s, c⟩};
end if
send(λ, ⟨p2b, self(), ballot_num⟩);
end case
end switch
end for
end processFigure 4. Pseudocode for an acceptor. The p2a arm departs — see above.
process Commander(λ, acceptors, replicas, ⟨b, s, c⟩)
var waitfor := acceptors;
∀α ∈ acceptors : send(α, ⟨p2a, self(), ⟨b, s, c⟩⟩);
for ever
switch receive()
case ⟨p2b, α, b'⟩ :
if b' = b then
waitfor := waitfor − {α};
if |waitfor| < |acceptors|/2 then
∀ρ ∈ replicas :
send(ρ, ⟨decision, s, c⟩);
exit();
end if
else
send(λ, ⟨preempted, b'⟩);
exit();
end if
end case
end switch
end for
end process
process Scout(λ, acceptors, b)
var waitfor := acceptors, pvalues := ∅;
∀α ∈ acceptors : send(α, ⟨p1a, self(), b⟩);
for ever
switch receive()
case ⟨p1b, α, b', r⟩ :
if b' = b then
pvalues := pvalues ∪ r;
waitfor := waitfor − {α};
if |waitfor| < |acceptors|/2 then
send(λ, ⟨adopted, b, pvalues⟩);
exit();
end if
else
send(λ, ⟨preempted, b'⟩);
exit();
end if
end case
end switch
end for
end processFigure 6. (a) a commander, (b) a scout.
process Leader(acceptors, replicas)
var ballot_num = (0, self()), active = false, proposals = ∅;
spawn(Scout(self(), acceptors, ballot_num));
for ever
switch receive()
case ⟨propose, s, c⟩ :
if ∄c' : ⟨s, c'⟩ ∈ proposals then
proposals := proposals ∪ {⟨s, c⟩};
if active then
spawn(Commander(self(), acceptors, replicas, ⟨ballot_num, s, c⟩));
end if
end if
end case
case ⟨adopted, ballot_num, pvals⟩ :
proposals := proposals ◁ pmax(pvals);
∀⟨s, c⟩ ∈ proposals :
spawn(Commander(self(), acceptors, replicas, ⟨ballot_num, s, c⟩));
active := true;
end case
case ⟨preempted, ⟨r', λ'⟩⟩ :
if ⟨r', λ'⟩ > ballot_num then
active := false;
ballot_num := (r' + 1, self());
spawn(Scout(self(), acceptors, ballot_num));
end if
end case
end switch
end for
end processFigure 7. Pseudocode skeleton for a leader. The spawn(Scout(…)) calls depart — see above.
Structs§
- Ballot
- A ballot number:
⟨round, leader⟩, ordered lexicographically. - Multi
Paxos Synod - The Synod protocol: acceptor and leader in one process, as §4.4 co-locates them.
- Pvalue
p = ⟨b, s, c⟩— a ballot number, a slot number and a command.
Enums§
- Cmd
- Requests from the layer above.
- Ind
- Indications to the layer above.
- Synod
Msg - What this layer puts on the wire, beneath the link.
- Wire
- The wire, multiplexing the leader detector and the Synod protocol itself.