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.

翻译：并发系统的验证 notoriously 困难：细微的错误可能仅在罕见的线程交错下显现，且现有工具通常需要侵入式插桩或不切实际的执行模型。本文提出OmniLink，一种基于TLA+验证并发实现是否符合高层次规约的新方法。与先前基于TLA+、采用称为轨迹验证技术的方法不同，OmniLink将系统事件视为黑盒，仅关注其发生的时间区间及其在TLA+中的语义含义，通过求解动作的逻辑全序进行验证。与已有的基于线性一致性检查（已具备时间区间动作全序求解能力）的方法不同，OmniLink采用灵活的规约语言，并提供一种基于现成模型检测工具的差异化线性一致性检查方法。相较于现有线性一致性检查工具，OmniLink具备不同的特性，我们证明其在大规模验证任务中优于当前最优技术。我们的评估验证了WiredTiger（一种先进的工业数据库存储层）、Balanced Augmented Tree（BAT，研究社区提出的先进无锁数据结构）以及ConcurrentQueue（一种采用激进性能优化策略的流行无锁队列）。我们使用OmniLink改进了WiredTiger现有的TLA+模型，并开发了能精确匹配被建模系统行为（包括非线性一致性行为）的新TLA+模型。OmniLink能够发现测试系统中人为注入的已知错误，并协助发现了两个先前未知的错误（BAT中1个，ConcurrentQueue中1个），这些错误已得到相应系统作者的确认。