Runtime Protocol Refinement Checking for Distributed Protocol Implementations
summary
Ellsberg implements runtime protocol refinement checking as a local per-node checker (Go implementation) that compares observed send/receive traces to a protocol spec, uses incremental BFS enumeration plus a user-supplied inference function to validate each outgoing message, and assumes fail‑stop processes in the asynchronous/partially synchronous model. It runs with two cores, imposes low latency and keeps up with Etcd (trace processing ≥2x generation), and successfully finds previously reported bugs — 10 across Etcd, Zookeeper, and Redis Raft.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 2:24Local runtime checking with Elsburg
- 7:43Concurrent execution in traces
- 10:36Incremental trace checking
- 13:05Summary and evaluation
- 15:13Conclusion and Q&A
related talks
20mModel Checking Distributed Protocols in Must
14mA Refinement Methodology for Distributed Programs in Rust
13mTesting LLM-Generated Distributed Protocol Code
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
39mProtocol engineering for communicating actors
31mModel Checking Distributed Software Systems
26mIs this really a refactoring? Automated equivalence checking for Erlang projects
40mImplementing Distributed Consensus