Trace Validation of Unmodified Concurrent Systems with OmniLink

TL;DR

OmniLink tackles the challenge of validating concurrent systems by aligning timeboxed traces from real executions with high-level TLA+ specifications through a TLC-based linearizability check. It blends non-intrusive tracing, rr deterministic replay, and model-checking to bridge the gap between trace validation and full formal verification, enabling analysis of true multithreaded interleavings. The approach supports non-linearizable behaviors and partial instrumentation, and its evaluation on WiredTiger, BAT, and ConcurrentQueue reveals both known and previously unknown bugs, while outperforming a state-of-the-art linearizability checker at scale. The work demonstrates practical utility for industrial and research systems, enabling precise debugging, model refinement, and broader applicability of formal methods to real-world concurrent software.

Abstract

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.

Figures (6)

• Figure 1: OmniLink's overall design. The system's API is exercised with a fuzzer in the context of rr chaos mode. The resulting time-boxed traces of API calls and return values are stored in a trace DB. These traces are consumed by the model checking process that either passes linearization, or fails. In case of failure, the user can inspect the counter-example using our custom trace viewer. Blue boxes are inputs provided by the user to OmniLink. The fuzzer is partially auto-generated. The non-blue pieces are provided by OmniLink.
• Figure 2: Illustration of OmniLink's linearization process relative to Listing \ref{['lst:queue-api']}, for 5 operations across 3 threads.
• Figure 3: Grammar of traces used by OmniLink.
• Figure 4: Runtime in seconds, varying operations.
• Figure 5: Peak memory usage in GB, varying operations.