Thread-modular Analysis of Release-Acquire Concurrency
summary
A thread-modular abstract-interpretation method targets RA (release-acquire) programs by encoding per-variable modification orders as a PO domain and using an upper approximation alpha# abstraction with Galois-backed alpha/gamma to preserve soundness. The prototype PRIORI implements these transfer functions, proves lattice and widening properties, and beats or matches state-of-the-art on benchmarks (example: a case analyzed in 0.06s) while handling verification and refutation; known limits include VBMC’s 500 view-switch baseline and some false positives (e.g., Fibonacci) from numeric/PO imprecision.
AI-written summary · about
chapters (6)
- 0:00Start
- 0:22The Release Acquire (RA) Memory Model
- 5:00Existing Analysis Technique for RA Memory Model
- 6:59Executions as Modification Orders
- 9:03Forgetting Stores: Second Level Abstraction
- 14:10Summary and Future Work
related talks
23mA Denotational Approach to Release/Acquire Concurrency
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
15mModal Abstractions for Virtualizing Memory Addresses
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
30mImplementing and Verifying Release-Acquire Transactional Memory in C11
15mSoundness of Predictive Concurrency Analyses