Building a Linearizability Checker in Rust
I have been working through the implementation of the Raft consensus algorithm in Rust. Part of doing that properly is being able to test it: you need to throw concurrent histories at your implementation and ask whether they are consistent with what a correct register (or log, or key-value store) is supposed to do. That question has a precise name — linearizability — and answering it algorithmically turns out to be a genuinely interesting problem.