Trace Validation of Unmodified Concurrent Systems with OmniLink

TL;DR

OmniLink is a novel validation methodology for concurrent systems that uses TLA+ and model checking to verify correctness, outperforming existing tools and discovering new bugs in industrial and research systems.

Contribution

The paper introduces OmniLink, a flexible, non-intrusive validation approach that improves linearizability checking and bug detection in concurrent systems using TLA+ and model checking.

Findings

Successfully validated WiredTiger, BAT, and ConcurrentQueue systems.

Discovered two previously unknown bugs in concurrent data structures.

Outperformed existing linearizability checking tools on large-scale validation tasks.

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.