Model-Guided Fuzzing for Apache Accord
Evaluating Predicate-Based Coverage as a Practical Alternative to TLA+
S. Stoicescu (TU Delft - Electrical Engineering, Mathematics and Computer Science)
B. Özkan – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
E.B. Gülcan – Mentor (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Jérémie Decouchant – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A. Katsifodimos – Graduation committee member (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Alexey Gotsman – Graduation committee member
Benedict Elliott Smith – Graduation committee member
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Distributed consensus protocols are the backbone of modern cloud infrastructure, ensuring consistency across replicated state machines. Leaderless consensus algorithms, such as Apache Accord, achieve optimal latency (1-RTT) by effectively distributing the ordering load across the cluster; however, this comes at the cost of significant algorithmic complexity during fault recovery. When a coordinating node crashes, surviving replicas must reconstruct dependency and ordering information by combining partial histories. A recent report by Ryabinin et al. demonstrates that non-trivial linearizability bugs can occur in Accord's recovery logic under very specific network and node failure conditions.
Finding such flaws through trace-guided fuzzing is infeasible because the number of message interleavings makes almost every execution appear distinct. We adapt ModelFuzz, which uses abstract TLA+ states as a coverage signal, by extending Accord's testing framework with controlled message delivery, crash injection, and a mapping from implementation executions to the formal model. We also introduce predicate coverage, a lighter-weight alternative derived from protocol stages, quorum progress, and crashed replicas. ModelFuzz achieves the highest TLA+ state coverage, while the most detailed predicate configuration can outperform unguided baselines but remains significantly behind ModelFuzz. Controlled exploration also exposes a reproducible internal correctness failure in Accord.