We present a coverage-guided testing algorithm for distributed systems implementations. Our main innovation is the use of an abstract formal model of the system that is used to define coverage. Such abstract models are frequently developed in the early phases of protocol design and verification but are infrequently used at testing time. We show that guiding random test generation using model coverage can be effective in covering interesting points in the implementation state space. We have implemented a fuzzer for distributed system implementations and abstract models written in TLA+. Our algorithm achieves better coverage over purely random exploration as well as random exploration guided by different notions of scheduler coverage and mutation. In particular, we show consistently higher coverage on implementations of distributed consensus protocols such as Two-Phase Commit and the Raft implementations in Etcd-raft and RedisRaft and detect bugs faster. Moreover, we discovered 12 previously unknown bugs in their implementations, four of which could only be detected by model-guided fuzzing.

Probabilistic data structures are used in applications that manage large datasets due to their time and space efficiency. These applications can accommodate approximate results from probabilistic data structures and replicated systems that use them can take advantage of the efficiency gained from weaker synchronization and consistency among replicas.

In this paper, we propose conflict-free replicated data types (CRDTs) for probabilistic data structures with approximate membership queries. Specifically, we introduce Conflict-Free Replicated Bloom Filters and Conflict-Free Replicated Cuckoo Filters, which are the conflict-free versions of traditional Bloom and Cuckoo filters. We provide implementations of these data structures in an open-source repository and present an evaluation of the approximate query results across various workload and replica synchronization configurations.

Controlled concurrency testing (CCT) is an effective approach for testing distributed system implementations. However, existing CCT tools suffer from the drawbacks of language dependency and the cost of source code instrumentation, which makes them difficult to apply to real-world production systems. We propose DSTest, a generalized CCT tool for testing distributed system implementations. DSTest intercepts messages on the application layer and, hence, eliminates the instrumentation cost and achieves language independence with minimal input. We provide a clean and modular interface to extend DSTest for various event schedulers for CCT. We package DSTest with three well-known event schedulers and validate the tool by applying it to popular production systems.