Efficient Linearizability Monitoring
summary
Revisits monitoring linearizability for stacks queues and (multi)sets and gives concrete algorithms with proven complexities: stacks O(n^2), queues O(n log n), (multi)sets O(n) under the differentiated data independence assumption. Implements LiMo and benchmarks it against Violin showing better efficiency and scalability. Introduces a Q-tree for containment checks and a small model property used for queues, gives counterexamples to earlier correctness proofs, and ships artifacts and proofs so the algorithms can be independently verified.
AI-written summary · about
chapters (17)
- 0:00Linearizability monitoring intro
- 1:03Linearizability correctness
- 2:06Monitoring problem and histories
- 3:52Flaws in prior algorithms
- 4:33Stack linearizability algorithm
- 7:24Handling incomplete ops
- 8:49Queue small model property
- 10:12Queue tree construction
- 11:56Multiset monitoring linear time
- 12:40Conclusion and future work
- 13:22Q&A
- 13:46Multiset operations
- 15:32Queue algorithm complexity
- 15:55Peek operation compatibility
- 16:58Proof confidence and bugs
- 18:04Monitoring definition and scope
- 18:24Weaker linearizability future
related talks
10mEfficient Decrease-And-Conquer Linearizability Monitoring
20mFixed Parameter Tractable Linearizability Monitoring
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
25mThe Path to Durable Linearizability
14mVerifying Concurrent Multicopy Search Structures
21mMechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Libr
12mCompositionality and Observational Refinement for Linearizability with Crashes
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency