← 研踪 PaperTrailarXiv:2601.11836 · v2
OmniLink: Specification-Based Trace Validation of Concurrent Systems with Substep Linearizability
首次提交 2026-01-17 07:51
版本更新 2026-11-06 06:47
雷达观测 2026-11-09 10:16
摘要
Concurrent systems are notoriously difficult to validate. We present OmniLink, a methodology for validating traces of concurrent implementations against high-level specifications in TLA+. Unlike prior TLA+ based approaches, 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, OmniLink implements substep linearizability semantics, relies on a flexible specification language, accelerates checking with user-customizable path pruning specifications, and can detect violations due to weak memory effects between operations. Our evaluation validates WiredTiger, a state-of-the-art industrial database storage layer; 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. OmniLink detects injected and previously fixed bugs in the systems under test. It also uncovers a previously unknown bug in BAT that has been confirmed by its authors.
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-06 06:47 · 最新观测版本
OmniLink: Specification-Based Trace Validation of Concurrent Systems with Substep Linearizability
Concurrent systems are notoriously difficult to validate. We present OmniLink, a methodology for validating traces of concurrent implementations against high-level specifications in TLA+. Unlike prior TLA+ based approaches, 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, OmniLink implements substep linearizability semantics, relies on a flexible specification language, accelerates checking with user-customizable path pruning specifications, and can detect violations due to weak memory effects between operations. Our evaluation validates WiredTiger, a state-of-the-art industrial database storage layer; 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. OmniLink detects injected and previously fixed bugs in the systems under test. It also uncovers a previously unknown bug in BAT that has been confirmed by its authors.
查看此版本解读 →查看此版本原文 ↗