Specifying Paxos for System Builders: Pseudocode Made Executable

1 Introduction

• Paxos-SB addresses replication and consensus in distributed systems where processes may fail and messages may be lost, delayed, reordered, or duplicated.These protocols replicate servers and agree on the sequence of client requests served.Source: §1 · p. 1
• Paxos-SB combines a robust C implementation with clean pseudocode detailing critical practical considerations.The implementation is about 7000 lines in C, while the pseudocode is about 330 lines across 13 figures.Source: §1 · pp. 1–2
• Paxos-SB distinguishes itself with prudent leader election and active normal-case execution, making it more robust and responsive in the presence of failures.Source: §1 · p. 2
• DistAlgo expresses the protocol pseudocode straightforwardly, essentially line by line, as directly executable code requiring only Python to run.The specification is a precise, pseudocode-level executable version of Paxos-SB.Source: §1 · p. 2
• Direct execution helped clarify protocol logic and led to fixes for hard-to-catch pseudocode omissions and liveness bugs, though not in the C code.The DistAlgo program is similar in size to the pseudocode and about one-tenth as efficient as the C code, with excellent latency.Source: §1 · p. 2

2.1 Paxos for System Builders

• Each server’s extensive data structures track its main state, received messages, ordering status, timers, and client-update handling status.The main states are LEADER ELECTION, REG LEADER, and REG NONLEADER.Source: §2.1 · p. 3
• Servers track installed view and executed sequence position; View Change/VC Proof, Prepare/Prepare OK, and Proposal/Accept messages support election, preparation, and global ordering, respectively.Source: §2.1 · pp. 3–4
• Requiring a majority to move to a new view prevents a minority from disrupting progress, at the cost of O(N^2) View Change messages.A server’s timeout alone does not trigger a new view; the majority must time out and decide to move.Source: §2.1 · p. 4
• Nonleaders send Accept messages to all servers, allowing every server to order updates; this costs O(N^2) rather than O(N) messages but reduces latency and improves fault tolerance.In the normal-case flow, the leader proposes a sequence number, servers respond with Accept messages, and servers order an update after enough Accepts.Source: §2.1 · pp. 4–5

2.2 DistAlgo

• DistAlgo processes support setup, run, and receive definitions, while received messages can be handled asynchronously or synchronously.Receive definitions handle matching messages at yield points, and await statements wait for conditions or a timeout.Source: §2.2 · pp. 5–6
• DistAlgo patterns match messages in sent and received histories, and queries express quantification, comprehension, or aggregation over sets or sequences.DistAlgo also supports automatic forward and backward visualization of replays to aid understanding of protocol runs.Source: §2.2 · p. 6
• DistAlgo’s main definition can specify run configuration, including requirements such as logical clocks.Source: §2.2 · p. 6

3.1 Data structures and message types

• DistAlgo represents pseudocode data structures with built-in types and dictionaries, and adds bound_updates to fix an omission where the pseudocode used it without defining it.The implementation also initializes variables whose initial values were unspecified in the pseudocode, confirming them against the C code.Source: §3.1 · pp. 7, 8, 10

3.2 Leader election

• Leader election waits for View Change messages from a majority before moving to a new leader, while a higher installed view in a VC Proof updates the attempted view.A server enters the prepare phase if it is the designated leader; otherwise, it becomes a non-leader.Source: §3.2 · p. 12
• DistAlgo follows the pseudocode line by line, with an added state update and self-message handling that fix a leader-election liveness bug.The authors also add a state update needed to maintain correct protocol state.Source: §3 · p. 7, §3.2 · p. 12

3.3 Global ordering

• The global-ordering translation expresses four protocol blocks, including Proposal handling that updates state, syncs to disk, and sends Accept messages to all servers.The blocks cover client updates, Proposal and Accept receipt, and execution of ordered updates.Source: §3.3 · p. 12
• Servers propose client updates, send Accept messages to all servers, and let any server record a majority-accepted update and execute successive ordered updates.The client-update handler queues new updates, forwards them when the server is a nonleader, or proposes the next update when it is the leader.Source: §3.3 · p. 14
• Two small changes fix a liveness bug and an omission: Proposal handling adds a line before disk sync and Accept, while Advance_Aru() now invokes update execution after advancing Local_Aru.The call to Advance_Aru() was also removed from Upon_Executing_Client_Update(), where it was unnecessary.Source: §3.3 · p. 14

3.4 Complete executable specification

• Direct execution also requires time-library imports and parameters, omitted helper functions, Client processes, and a main routine to create, configure, and start processes.These additions are described as straightforward to write in DistAlgo.Source: §3.4 · p. 14
• Recovery is handled through disk-sync library calls and setup-time initialization from disk rather than a separate procedure; the performance comparison uses Paxos-SB’s default no-disk behavior.The authors say this approach minimally affects program size and execution but would clutter the data-structure and initialization specification.Source: §3.4 · p. 15

4.1 Omissions fixed

• Two pseudocode omissions were fixed: client-update execution was never invoked, and bound(U) was undefined; the fixes invoke execution as Local Aru advances and define bound updates by sequence number.The bound mapping records the update assigned to each sequence number when processing a higher-view Proposal.Source: §4.1 · pp. 15–16

4 Direct execution, checking, and analysis

• Runtime checking models process and communication failures without changing protocol code, and exposed two liveness bugs in the pseudocode.Safety properties were agreement and validity; liveness properties used timeouts.Source: §4 · p. 15, §4.2 · p. 16

4.2 Liveness bugs fixed

• A server could wait indefinitely for Accepts because it dropped its own Accept; the fix delivers that Accept locally before broadcasting it.The pseudocode’s vote rule counts the Proposal itself, so a server waits for one fewer than a majority of Accepts.Source: §4.2 · pp. 16–17
• After a crashed server and temporary network-wide delay, both remaining servers could wait for each other’s View Change and leave the protocol stuck.The fix receives the server’s own View Change before applying it to data structures.Source: §4.2 · p. 17

4.3 Resulting specification and direct execution

• The complete DistAlgo specification is under 600 lines, with about 200 lines for leader election, the prepare phase, and global ordering.The total includes comments, blank lines, client processes, and setup.Source: §4.3 · p. 17
• The specification is close in size to the pseudocode and can be run directly with Python.The reported performance is about 10 times the C code’s running time.Source: §4.3 · pp. 17–18
• About 170 seconds for 200,000 requests and less than 1.7 ms average request latency; the DistAlgo program ran about 10 times slower than the C code.The measurement used three servers, two clients with 100,000 requests each, and averaged five runs.Source: §4.3 · p. 18

5 Related work and conclusion

• Formal efforts include Dafny specifications and checked proofs for Paxos-based replication, a TLA+ safety proof for Multi-Paxos, and Ivy and Veil encodings for automated proofs.Other cited work develops a Raft variant specification and safety proof in Coq.Source: §5 · pp. 18–19
• The cited specifications are either large and complex or omit important practical aspects, whereas DistAlgo maps closely to expert-designed practical pseudocode.Source: §5 · p. 19
• The authors conclude that expressing protocol pseudocode in DistAlgo is straightforward and that precise executable specifications helped reveal and fix omissions and liveness bugs.They identify a higher-level declarative specification for Paxos-SB as ongoing and future work.Source: §5 · p. 19

• The pseudocode covers data structures, message types, conflict checks, and rules for updating Global History.Source: Figure 2 · p. 24, Figure 3 · p. 25, Figure 4 · p. 26
• Leader election and the prepare phase are followed by procedures for shifting leader and non-leader states.Source: Figure 6 · p. 28, Figure 7 · p. 28, Figure 8 · p. 29
• The remaining figures cover global ordering, its utility procedures, client update handling and utilities, and recovery.Source: Figure 10 · p. 29, Figure 11 · p. 30, Figure 12 · p. 30

B Paxos for System Builders in DistAlgo

• The excerpts identify Client_Update, View_Change, VC_Proof, Prepare, and Prepare_OK as Message classes, but they do not show the specific fields or contents of any class.Source: B Paxos for System Builders in DistAlgo · p. 32
• Proposal, accept, and globally ordered update messages bind client updates to sequence numbers and views.Proposals include the server, view, sequence number, and update; accepts identify the view and proposal sequence number.Source: B Paxos for System Builders in DistAlgo · pp. 32–33
• Server state tracks its role and installed views, alongside global history and added indexes for received proposals and bound updates.The added indexes record the maximum sequence number received in global history and map sequence numbers to updates from the highest-view proposals.Source: B Paxos for System Builders in DistAlgo · p. 33
• Timers govern progress checks and resending client updates, while the server maintains a queue of pending client requests.On progress-timer expiration, a server attempts a new view; an update timer expiration resends a request to the leader.Source: B Paxos for System Builders in DistAlgo · pp. 33–34

• View_Change messages are rejected when addressed to the local server, outside leader election, during progress-timer activity, or for an already installed attempt.The conflict checks return TRUE for these conditions.Source: B Paxos for System Builders in DistAlgo · p. 34
• For a sequence with an existing proposal, a higher-view proposal replaces it, clears recorded accepts, and records its update as a bound update.The code also updates the maximum sequence number received for a newly received proposal.Source: B Paxos for System Builders in DistAlgo · p. 35
• Accept messages are ignored if the sequence is already globally ordered, the accept threshold has been reached, or that server has already supplied an accept.The threshold check compares the number of recorded accepts with int(N/2).Source: B Paxos for System Builders in DistAlgo · p. 35
• A Globally_Ordered_Update is recorded only when its sequence already has a history entry without such an update.Source: B Paxos for System Builders in DistAlgo · p. 35
• When the progress timer expires, the server shifts to leader election for Last_Attempted + 1.The implementation also starts a VC_Proof timer.Source: B Paxos for System Builders in DistAlgo · pp. 34, 36

B Paxos for System Builders in DistAlgo

• A VC proof advances Last_Attempted to the installed view, then sends its leader to prepare and other servers to regular nonleader operation.View-change proofs update state only when the installed view exceeds Last_Installed.Source: B Paxos for System Builders in DistAlgo · p. 36
• The prepare leader broadcasts its view and data-list state, while servers reply with Prepare_OK and a floor(N/2)+1 quorum marks the view prepared.The leader transitions to regular-leader operation when enough Prepare_OK messages for the view arrive.Source: B Paxos for System Builders in DistAlgo · pp. 36–37
• Prepare data lists recover entries above aru from global history, preferring a globally ordered update when present and otherwise using the proposal.The list is constructed in sequence-number order through max_seq_received.Source: B Paxos for System Builders in DistAlgo · p. 37
• After becoming regular leader, a server enqueues unbound pending updates, removes bound updates, resets Last_Proposed to Local_Aru, and sends a proposal.A regular nonleader records Last_Installed from Last_Attempted, ensures its progress timer is running, and syncs to disk.Source: B Paxos for System Builders in DistAlgo · pp. 37–39
• On receiving a proposal, a server updates its data, syncs to disk, processes its own Accept locally, and then broadcasts the Accept to all servers.The local Receive_Accept call is explicitly added before the broadcast.Source: B Paxos for System Builders in DistAlgo · pp. 37–38
• A sequence is globally ready when its history contains a proposal and at least floor(N/2) accepts; the code omits a same-view check because data-structure conflict checks test it.Once an accept arrives, the procedure applies it to data structures and, when the update is globally ordered, applies that update and advances ARU.Source: B Paxos for System Builders in DistAlgo · pp. 35, 38, 39
• Advancing ARU executes consecutive globally ordered updates, and the implementation adds the sole call to client-update execution, absent from the pseudocode.The execution handler replies to the client and clears its pending update when applicable.Source: B Paxos for System Builders in DistAlgo · pp. 35, 38, 39
• The client-update handler routes updates according to server state: nonleaders forward them to the leader, while regular leaders enqueue accepted updates and send proposals.During leader election, updates not addressed to the local server are ignored.Source: B Paxos for System Builders in DistAlgo · p. 39
• The code adds a bound-update check and a VC_Proof timeout handler that broadcasts proofs to all servers and restarts the timer.The timeout handler sends VC_Proof with the server's Last_Installed value.Source: B Paxos for System Builders in DistAlgo · p. 40
• Servers check each incoming message for conflicts before dispatching it to the corresponding protocol handler.The shown handlers cover View_Change, VC_Proof, Prepare, Prepare_OK, Proposal, and Accept messages.Source: B Paxos for System Builders in DistAlgo · p. 40
• Clients send timestamped requests sequentially, wait for each reply, and record request-to-reply times to calculate average latency and total time.The client stores each request and reply time, then averages the measured delays across its requests.Source: B Paxos for System Builders in DistAlgo · p. 40

C A Run of Paxos for System Builders in DistAlgo

• The run used three servers and three clients, with 100,000 requests per client.Source: C A Run of Paxos for System Builders… · p. 41
• Two logged clients averaged 0.0016162170124053956 and 0.0016252124166488647 seconds per request, respectively.Each client issued 100,000 requests; the log reports total times of 162.07355737686157 and 162.86385893821716 seconds.Source: C A Run of Paxos for System Builders… · p. 41
• The log records termination of the main process after the run.Source: C A Run of Paxos for System Builders… · p. 41