Efficient Decrease-And-Conquer Linearizability Monitoring
summary
Presents a decrease-and-conquer framework that reduces linearizability monitoring to finding linearizability-preserving values, proving polynomial-time equivalence between the two problems under the unambiguity restriction (each inserted value is distinct). Instantiates the framework for registers, sets, stacks, queues and priority queues, gives a stack algorithm improved to n log n using segment/interval trees, and implements a tool that processes histories of a million operations in under a second and significantly outperforms prior monitors.
AI-written summary · about
chapters (8)
- 0:00Linearizability monitoring intro
- 1:47Complexity of verifying linearizability
- 3:35Existing tractable approaches
- 5:20Decrease-and-conquer framework
- 6:01Preserving values explained
- 7:04Preserving values for stacks
- 9:10Algorithm complexity & optimizations
- 9:53Experimental results
related talks
19mEfficient Linearizability Monitoring
20mFixed Parameter Tractable Linearizability Monitoring
25mThe Path to Durable Linearizability
12mCompositionality and Observational Refinement for Linearizability with Crashes
24mA Compositional Theory of Linearizability
01h 10mWorkshop. Lincheck: Testing concurrency on the JVM (Part 1)
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
24mA Concurrent Program Logic with a Future and History