Verification of Concurrent Programs under Release-Acquire Concurrency

on YouTube ↗01h 04m

" summary

Shows that reachability under release‑acquire is undecidable for finite‑state programs by a PCP reduction using four threads that guess and verify sequences; the undecidability survives simple context bounds. Introduces K‑bounded view switches as an RA‑specific under‑approximation, gives a polynomial translation to sequential consistency with K+N context switches, implements a VBMC tool that translates to CBMC, and reports real bugs found with at most five view switches. Parameterized results: decidable without CAS, PSPACE‑complete for loop‑free distinguished threads and EXPTIME when one unrestricted distinguished thread is added.

AI-written summary · about

" chapters (28)

1. 0:00Introduction
2. 0:43Motivation for concurrency
3. 2:28Weak memory models
4. 3:31Release-acquire semantics
5. 4:55Release-acquire vs sequential consistency
6. 6:41Execution graphs
7. 8:45Declarative semantics conditions
8. 10:09Release-acquire properties
9. 11:32Release-acquire summary
10. 11:52Operational semantics
11. 16:25Atomic read-write ops
12. 19:15Sample execution
13. 22:05Reachability problem
14. 23:30State reachability decidability
15. 24:53Undecidability proof
16. 27:25Encoding PCP
17. 31:20Verification challenges
18. 34:54Fixing verification approach
19. 40:40Context-bounded analysis
20. 43:10View-bounded reachability
21. 49:05ViewBounded reduction
22. 53:40ViewBounded Model Checker
23. 55:46Tool comparison
24. 56:29Parameterized reachability
25. 57:30Parameterized reachability without CAS
26. 59:39Reachability with distinguished threads
27. 1:00:23Complexity results
28. 1:01:27Q&A

" related talks

• 22mOptimal Stateless Model Checking under the Release-Acquire SemanticsTuan Phong Ngo · OOPSLA 2018
• 26mContext-Bounded Verification of Liveness for Multithreaded Shared-Memory ProgramsRupak Majumdar, Georg Zetzsche, Ramanathan S. Thinniyam, Pascal Baumann · POPL 2021
• 15mThread-modular Analysis of Release-Acquire ConcurrencyDivyanjali Sharma, Subodh Sharma · SAS 2021
• 23mA Denotational Approach to Release/Acquire ConcurrencyOri Lahav, Ohad Kammar, Yotam Dvir · GALOP 2024
• 21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)Peter Müller, Marco Eilers, Thibault Dardinier · PLDI 2023
• 23mAn Operational Approach to Library Abstraction under Relaxed Memory ConcurrencyOri Lahav, Abhishek Kr Singh · POPL 2023
• 19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation LogicJanggun Lee, Jeehoon Kang, Jaehwang Jung, Sunho Park, Jeho Yeon · PLDI 2025
• 23mStratified Commutativity in Verification Algorithms for Concurrent ProgramsAndreas Podelski, Azadeh Farzan, Dominik Klumpp · POPL 2023