Module protocol 

The consensus controller: ubft_new’s four machines, fixed and faster.

rhdl_ubft keeps ubft_new’s structure state for state: a LEADER machine that proposes, a FAST path (two rounds of votes), a SLOW path (signed certify shares, then commit votes) and a VIEW change. It also keeps the mailbox layout (crate::layout) and the wait timeout counted in polls. What changes is how each state does its work, and seven bugs.

ubft_new (a7537bd)	rhdl_ubft
the fast path sends each vote to one queue pair, then moves on	crate::broadcast: every replica, nothing dropped
the leader never votes, so 2f + 1 of 2f + 1 is unreachable and every slot falls to the slow path	the leader votes like everyone else
after its first slow decision the leader returns as a follower; nobody proposes again	the leader returns to LEADER
k = slot + 1 repeats every G_T slots; prepares and votes are never cleared, so a reused slot decides stale values	k is the slot’s sequence number; votes carry (view, k)
the slow path never broadcasts certify_valid, so no peer verifies a share	it does
view-change and new-view records are sent without their valid flags	the flags are sent
the signed summary is view<<48 ^ slot<<32 ^ k<<16 ^ m (collides: k=1,m=0 and k=2,m=196608), and the library hashes one byte of it	(view, slot, k, m) as four 32-bit words, all 16 bytes signed
a vote is the word 1: it binds nothing, so an equivocating leader can split the replicas	a vote is (tag(view, k), m); a quorum counts only votes for the replica’s own m
the prepare carries no view, so an old view’s proposal is voted on in the next	the prepare is (k, m, view)
the new leader picks the highest k it is told about and everyone installs it	every replica picks the value reported by f + 1 records (see View change)
each mailbox word is its own HBM read	one burst per poll (crate::fetch)
signing and verifying stop the kernel (3.07M and 10.4M cycles)	a service on streams (crate::setup)

A slot, fast path

1. The leader takes the slot’s proposal from input, RDMA-writes (k, m, view) into prepare on its N − 1 peers and writes it into its own HBM. (Every broadcast below is followed by the same local write: the RoCE stack has no connection to the replica itself.)
2. Every replica polls prepare until k arrives for this view, then writes its will_cert vote (tag(view, k), m) on every replica.
3. With 2f + 1 votes for its own (view, k, m) it writes will_commit.
4. With 2f + 1 matching will_commit votes it decides: (k, m) goes to output and remoteUpdate.

A poll that does not find what it waits for counts toward wait. Past it, the replica falls back to the slow path for the same slot.

A slot, slow path

The replica signs the summary through the service, writes its 64-byte share and then certify_valid on every replica, and verifies each peer’s share as its flag appears, one at a time. With 2f + 1 valid shares (its own included) it writes commit, and with 2f + 1 commits it decides. A timeout here starts a view change.

View change

The view advances and the leader rotates (view mod N). Every replica posts a record of what it voted for in the slot: (view, slot | phase << 16, k, m), phase 0 nothing, 1 will_cert, 2 will_commit or commit. Once it holds 2f + 1 records for the view, each replica reads them all and decides for itself: the (k, m) reported by at least f + 1 records with phase ≥ 1, the highest such k. It installs that in its own prepare and runs the slot again on the fast path. If no value has f + 1 reports, none can have been decided, and the new leader proposes from its queue.

Status: a value-binding prototype, not uBFT’s recovery. The original uBFT (LPD-EPFL/ubft 504eba0) recovers through certified commit histories: every fast commit is turned into a CB-broadcast slow commit before a view is sealed, and the new view takes the highest commit view per instance from quorum-certified histories (docs/rhdl_ubft-original-baseline.md). The rule here uses each replica’s latest uncertified self-report instead. Atlas’s counterexample shows two honest replicas can choose different candidates when a faulty one writes different records to each, and an all-n quorum loses liveness to one silent replica. The original fast-to-slow bridge, tail-CB and certified histories are scheduled to replace it.

The argument this prototype was built on, for uBFT’s n = 2f + 1: a decision needs 2f + 1 = n matching votes, so every replica voted for the decided (k, m), and the f + 1 honest ones report it. At most f lying records cannot reach f + 1 for another value. No replica trusts the leader’s choice.

Trust model

• A replica writes only its own vote and record slots in a peer’s mailbox. This is the disaggregated-memory assumption uBFT rests on. It must be enforced on the receive side, per sending queue pair. Not enforced yet: DSig’s on-chip fabric checks only the destination region, and a per-sender slot guard is pending (Atlas’s proposal). Until it lands, every claim below assumes it.
• Slow-path shares are signed. The other mailboxes are protected by the point above.
• The argument above covers odd n (uBFT’s 2f + 1). For even n the quorums overlap less, and this page claims nothing.
• Liveness needs the replicas to be correct and the network to deliver within wait polls. A Byzantine replica can stall progress (it can always refuse to vote, since the quorum is everyone), but under the model above it cannot make two replicas decide differently.

Modules

st

Controller states. The names follow ubft_new’s (FAST_WAIT_PREPARE and so on); a POLL_* state starts a fetch and its WAIT_* state reads the result.

sub

Submachines (ubft_new’s SubMachine).

Structs

ProtocolIn

Inputs of the controller.

ProtocolOut

Outputs of the controller.

ProtocolState

The controller’s registers. N is the most replicas the build supports, G the window.

Functions

choose

The value reported by at least f + 1 of the valid records, if any (at most one can be: 2(f + 1) > n).

count_flags

How many of the first n one-word flags equal tag.

count_votes

Votes for (tag, m) among the first n two-word votes.

fresh_status

A run’s measurements before it starts.

protocol_kernel

The controller.

vote_tag

The vote word for (view, k): view’s low 8 bits over k’s low 24. Never zero for k ≥ 1, so a cleared mailbox is never a vote.