Skip to main content
PRL Project
close window

Code for Simple Consensus

Code extracted from Nuprl in January 2012 represents work in progress and may vary from current library protocols.

Code Header

pecification rsc (* ------ Parameters ------ *) (* consensus on commands of arbitrary type Cmd with equality decider (cmdeq) *) parameter Cmd, cmdeq : Type * Cmd Deq parameter coeff : Int parameter flrs : Int (* max number of failures *) parameter locs : Loc Bag (* locations of (3 * flrs + 1) replicas *) parameter clients : Loc Bag (* locations of the clients to be notified *) (* ------ Imported Nuprl declarations ------ *) import length poss-maj list-diff deq-member from-upto bag-append Memory1 (* ------ Type definitions ------ *) type Inning = Int type CmdNum = Int type RoundNum = CmdNum * Inning type Proposal = CmdNum * Cmd type Vote = (RoundNum * Cmd) * Loc (* ------ Messages ------ *) internal vote : Vote internal retry : RoundNum * Cmd internal decided : CmdNum output notify : Proposal input propose : Proposal (* ------ Variables ------ *) variable sender : Loc variable loc : Loc variable ni : RoundNum variable n : CmdNum (* ------ Auxiliaries ------ *) let init x loc = {x} ;;

NewVoters and ReplicaState

(* ---------- ReplicaState: a state machine ---------- *) (* -- inputs -- *) let vote2prop loc (((n,i),c),loc’) = {(n,c)} ;; class Proposal = propose’base || (vote2prop o vote’base);; let update_replica (n,c) (max,missing) = if n > max then (n, missing ++ (from-upto (max + 1) n)) else if deq-member (op =) n missing then (max, list-diff (op =) missing [n]) else (max,missing) ;; class ReplicaState = Memory1 (init (0,nil)) update_replica Proposal ;; (* ---------- NewVoters ---------- *) let when_new_proposal loc (n,c) (max,missing) = if n > max or deq-member (op =) n missing then {(n,c)} else {} ;; class NewVoters = when_new_proposal o (Proposal, ReplicaState) ;;

Quorum

(* ---------- QuorumState ---------- *) let newvote ni ((ni’,c),sender) (cmds,locs) = ni = ni’ & !(deq-member (op =) sender locs);; let add_to_quorum ni ((ni’,c),sender) (cmds,locs) = if newvote ni ((ni’,c),sender) (cmds,locs) then (c.cmds, sender.locs) else (cmds,locs);; class QuorumState ni = Memory1 (init (nil,nil)) (add_to_quorum ni) vote’base ;; (* ---------- Quorum ---------- *) let roundout loc (((n,i),c),sender) (cmds,_) = if length cmds = 2 * flrs then let (k,x) = poss-maj cmdeq (c.cmds) c in if k = 2 * flrs + 1 then bag-append (decided’broadcast locs n) (notify’broadcast clients (n,x)) else { retry’send loc ((n,i+1), x) } else {} ;; let when_quorum ni loc vote state = if newvote ni vote state then roundout loc vt state else {} ;; class Quorum ni = (when_quorum ni) o (vote’base, QuorumState ni) ;; (* ---------- Round ---------- *) class Round (ni,c) = Output(\loc.vote’broadcast locs ((ni,c),loc)) || Once(Quorum ni) ;;

NewRounds and Voters

(* ---------- NewRoundsState ---------- *) let vote2retry loc ((ni,c),sender) = {(ni,c)};; let RoundInfo = retry’base || (vote2retry o vote’base);; let update_round n ((m,i),c) round = if n = m & round < i then i else round ;; class NewRoundsState n = Memory1 (init 0) (update_round n) RoundInfo ;; (* ---------- NewRounds ---------- *) let when_new_round n loc ((m,i),c) round = if n = m & round < i then {((m,i),c)} else {} ;; class NewRounds n = (when_new_round n) o (RoundInfo, NewRoundsState n) ;; (* ---------- Voter ---------- *) class Halt n = (\_.\m. if m = n then {()} else {}) o decided’base;; class Voter (n,c) = Round ((n,0),c) || ((NewRounds n >>= Round) until (Halt n));;

Top Level

(* ---------- Replica ---------- *) class Replica = NewVoters >>= Voter;; (* ---------- Main program ---------- *) main Replica @ locs ;;
close window