RELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
summary
RELINCHE is a model checker that verifies per-object atomicity plus preserved synchronization under weak memory by establishing refinement between an implementation and a partial lock specification; it runs the most-parallel client to enumerate executions, computes minimal extensions that would invalidate each output, and then ensures every implementation trace matches a spec trace or is forbidden by some extension. The tool scales to clients with up to 7–9 library calls, finds minimal counterexamples with 4–7 calls, and discovers real bugs in libcds.
AI-written summary · about
chapters (10)
- 0:00RELINCHE introduction
- 1:26Linearizability under weak memory
- 3:08Relaxed linearizability with sync
- 5:18Partial locks for relaxed specs
- 7:26Verify implementation vs specs
- 9:11Scaling with parallel clients
- 11:40Exhaustive checking algorithm
- 13:49Performance and scalability
- 14:11Summary and contributions
- 14:35Q&A
related talks
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
12mCompositionality and Observational Refinement for Linearizability with Crashes
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
39mLincheck: Testing concurrency on the JVM
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
25mThe Path to Durable Linearizability
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency