Automated Robustness Verification of Concurrent Data Structure Libraries Against(…)
summary
An automated procedure verifies that C11-style concurrent data-structure implementations are robust by checking that every relaxed-memory execution is possible under SC, using an automated SMT encoding that inductively enforces an HBSC⇒HB invariant and a stronger induced subgraph robustness predicate for return-affecting accesses. The method adds compositional SC fences when needed, ships as an open-source tool, and successfully verifies a portfolio of real stacks, queues, sets and logs (artifacts available and results reproduced).
AI-written summary · about
chapters (10)
- 0:00Concurrency and memory models
- 1:46RC11 concurrent libraries
- 3:56Robustness verification
- 6:02Non-robust behavior
- 8:09Verification procedure
- 11:41Inductive robustness proof
- 16:18SMT for robustness checks
- 18:24Real-world library challenges
- 19:47Non-compositionality and fences
- 20:28Conclusion
related talks
23mVerifying Observational Robustness Against a C11-style Memory Model
17mDynamic Robustness Verification against Weak Memory
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
24mSaturn: a library of verified concurrent data structures for OCaml 5
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
14mVerifying Concurrent Multicopy Search Structures
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
14mMaking Weak Memory Models Fair