arXiv subjects

A. Jesse Jiryu Davis

Publications and source records attributed to A. Jesse Jiryu Davis.

4 recordsLinked to original sources

arXiv2026

The Polyglot's Dilemma: Conformance Testing a Dozen Specs in as Many Languages

MongoDB maintains client libraries in a dozen programming languages, used by tens of thousands of organizations and millions of developers. Most are implemented natively rather than as wrappers around a shared core. Ensuring consistent behavior across these libraries, comprising millions of lines of code, is hard but essential. Over eleven years, we developed a specification-based testing approach: tests are written once in YAML and executed by language-specific interpreters for each library. We describe the evolution from many ad-hoc formats to a Unified Test Format, which allowed us to delete over 22,000 lines of test code. The rate of nonconformance bugs fell up to 86% in drivers that adopted YAML tests (though results varied). We report lessons learned about declarative test design, test architecture, schema evolution, and the limits of unification.

cs.SE↗

arXiv2026

Trace Validation of Unmodified Concurrent Systems with OmniLink

Concurrent systems are notoriously difficult to validate: subtle bugs may only manifest under rare thread interleavings, and existing tools often require intrusive instrumentation or unrealistic execution models. We present OmniLink, a new methodology for validating concurrent implementations against high-level specifications in TLA+. Unlike prior TLA+ based approaches which use a technique called trace validation, OmniLink treats system events as black boxes with a timebox in which they occurred and a meaning in TLA+, solving for a logical total order of actions. Unlike prior approaches based on linearizability checking, which already solves for total orders of actions with timeboxes, OmniLink uses a flexible specification language, and offers a different linearizability checking method based on off-the-shelf model checking. OmniLink offers different features compared existing linearizability checking tools, and we show that it outperforms the state of the art on large scale validation tasks. Our evaluation validates WiredTiger, a state-of-the-art industrial database storage layer, as well as Balanced Augmented Tree (BAT), a state-of-the art lock-free data structure from the research community, and ConcurrentQueue, a popular lock-free queue featuring aggressive performance optimizations. We use OmniLink to improve WiredTiger's existing TLA+ model, as well as develop new TLA+ models that closely match the behavior of the modeled systems, including non-linearizable behaviors. OmniLink is able to find known bugs injected into the systems under test, as well as help discover two previously unknown bugs (1 in BAT, 1 in ConcurrentQueue), which we have confirmed with the authors of those systems.

cs.SE↗

arXiv2025

LeaseGuard: Raft Leases Done Right

Raft is a leading consensus algorithm for replicating writes in distributed databases. However, distributed databases also require consistent reads. To guarantee read consistency, a Raft-based system must either accept the high communication overhead of a safety check for each read, or implement leader leases. Prior lease protocols are vaguely specified and hurt availability, so most Raft systems implement them incorrectly or not at all. We introduce LeaseGuard, a novel lease algorithm that relies on guarantees specific to Raft elections. LeaseGuard is simple, rigorously specified in TLA+, and includes two novel optimizations that maximize availability during leader failover. The first optimization restores write throughput quickly, and the second improves read availability. We evaluate LeaseGuard with a simulation in Python and an implementation in LogCabin, the C++ reference implementation of Raft. By replacing LogCabin's default consistency mechanism (quorum checks), LeaseGuard reduces the overhead of consistent reads from one to zero network roundtrips. It also improves write throughput from ~1000 to ~10,000 writes per second, by eliminating contention between writes and quorum reads. Whereas traditional leases ban all reads on a new leader while it waits for a lease, in our LeaseGuard test the new leader instantly allows 99% of reads to succeed.

cs.DC↗

arXiv2020

eXtreme Modelling in Practice

Formal modelling is a powerful tool for developing complex systems. At MongoDB, we use TLA+ to model and verify multiple aspects of several systems. Ensuring conformance between a specification and its implementation can add value to any specification; it can avoid transcription errors, prevent bugs as a large organization rapidly develops the specified code, and even keep multiple implementations of the same specification in sync. In this paper, we explore model-based testing as a tool for ensuring specification-implementation conformance. We attempted two case studies: model-based trace-checking (MBTC) in the MongoDB Server's replication protocol and model-based test-case generation (MBTCG) in MongoDB Realm Sync's operational transformation algorithm. We found MBTC to be impractical for testing that the Server conformed to a highly abstract specification. MBTCG was highly successful for Realm Sync, however. We analyze why one technique succeeded and the other failed, and advise future implementers making similar attempts at model-based testing.

cs.SE↗