论文库

原文摘要

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.