Deterministic Raft, checked in this tab
A five-node Raft cluster, simulated deterministically, with a linearizability checker running in this page. The whole execution is a pure function of one seed.
The checker implements Wing & Gong’s algorithm with P-compositionality. It is not the serious tool - Porcupine is: Go, bitset state, parallel search, years of use against real systems. Its 103 Jepsen etcd histories and published verdicts are what kedge is validated against, vendored under the MIT licence with thanks to Anish Athalye. I have not benchmarked the two against each other, so no speed comparison is quoted here; kedge’s own timings are below.
Verdict
checking…put get never answered - may still take effect the operation no ordering can explain last step of the longest ordering that does work
| history | ops | Porcupine says | kedge says | steps | time |
|---|
Two of the 103 histories, checked in your browser against the verdicts Porcupine publishes in
porcupine_test.go. The full run - 102 histories that carry a published verdict -
is npm run corpus; it matched all 102 in 1.1 s. The 103rd,
etcd_095.log, is empty: that run’s etcd cluster failed to start, and Porcupine
asserts nothing about it either.
Deciding whether a history is linearizable is NP-complete, so the search needs a step
budget and the answer is linearizable, not-linearizable, or
unknown. Every other checker in this portfolio reports unknown
because its author chose to be honest about coverage. This one reports it because the
alternative is a search that does not finish.
Starving it is the test that matters. At a 1,000-step budget kedge answers 82 of the 102
histories correctly and reports unknown on the other 20 - and gets
zero wrong. Under pressure it gives up; it does not guess.
src/bugs.js. Nothing is hidden.