Visibility Reasoning for Concurrent Snapshot Algorithms

on YouTube ↗20m

" summary

Applies visibility relations to prove linearizability for three Jayanti algorithms, giving a reusable, layered proof instead of locating linearization points. Formalizes Jayanti’s concrete forwarding ideas as forwarding axioms (plus nine obligations), shows those axioms imply the snapshot core property and yield a total order on writes, and proves layerability → linearizability for all three variants. Proofs are paper-level, abstract (no executable-code verification reported), and the first axiomatization of concurrent snapshot correctness that captures Jayanti’s informal intuitions.

AI-written summary · about

" chapters (21)

1. 0:00Concurrent snapshots
2. 0:22Concurrent snapshot execution
3. 1:39Linearization point method
4. 1:54Alternative: Axiomatizing visibility relations
5. 2:52Non-linearizable scenario
6. 3:27In this talk: Jayanti's snapshot algorithms
7. 5:41Overview
8. 6:13Forwarding in Jayanti's algorithm 1
9. 7:20Concurrent execution of Jayanti's algorithm 1
10. 8:04Jayanti's original forwarding principles
11. 9:07New (abstract) forwarding principles
12. 10:50Jayanti's multi-writer/single-scanner algorithm
13. 11:29Jayanti's multi-writer/multi-scanner algorithm
14. 12:20Abstract visibility relations for Jayanti's algorithm 1
15. 13:34Order notations
16. 14:19Formalizing the first forwarding principle
17. 14:55Formalizing the second forwarding principle
18. 16:05Core snapshot axiom
19. 16:23Snapshot axioms for linearizability
20. 17:09Main proof 1: Forwarding principles imply snapshot
21. 18:20Main proof 2: Snapshot axioms imply linearizability

" related talks

• 12mProving Highly-Concurrent Traversals CorrectAleksandar Nanevski, Adam Morrison, Constantin Enea, Sharon Shoham, Yotam M. Y. Feldman, Artem Khyzha, Noam Rinetzky · OOPSLA 2020
• 25mThe Path to Durable LinearizabilityAzalea Raad, Viktor Vafeiadis, Emanuele D'Osualdo · POPL 2023
• 23mStratified Commutativity in Verification Algorithms for Concurrent ProgramsAndreas Podelski, Azadeh Farzan, Dominik Klumpp · POPL 2023
• 24mA Concurrent Program Logic with a Future and HistoryThomas Wies, Roland Meyer, Sebastian Wolff · OOPSLA 2022
• 24mA Compositional Theory of LinearizabilityZhong Shao, Arthur Oliveira Vale, Yixuan Chen · POPL 2023
• 12mCompositionality and Observational Refinement for Linearizability with CrashesZhong Shao, Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You · OOPSLA 2024
• 19mScenario-based Proofs for Concurrent ObjectsEric Koskinen, Constantin Enea · OOPSLA 2024
• 20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...Robbert Krebbers, Jonas Kastberg Hinrichsen, Jules Jacobs · POPL 2024