Verifying Concurrent Multicopy Search Structures
summary
Proves that multicopy search structures satisfy linearizability by isolating a search recency property and a template for upsert/search/maintenance that works over lists, trees or arbitrary DAGs. Shows the invariant that the first reachable is most recent, implements a helping protocol for search linearization, verifies two templates (LSM DAG and Differential File), and produces a verified concurrent in‑memory LSM tree (unsorted root array + sorted string tables) in Iris with SMT aid from Grasshopper.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:12Multicopy Search Structures
- 1:11Goal
- 2:03Proof
- 3:10Example
- 4:58Search Recency
- 6:27Invariant
- 8:08Template Algorithm
- 9:36Plan
- 13:26Conclusion
related talks
12mProving Highly-Concurrent Traversals Correct
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)
19mEfficient Linearizability Monitoring
24mA Concurrent Program Logic with a Future and History
22mVerifying Lock-Free Traversals in Relaxed Memory Separation Logic
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
20mVisibility Reasoning for Concurrent Snapshot Algorithms