Persistence Semantics for Weak Memory

on YouTube ↗23m

" summary

Introduces PTSO: an integration of epoch persistency with x86/SPARC TSO that gives both operational and declarative semantics and a machine-checked proof of their equivalence. Defines persistent fences (epoch boundaries) and synchronous persist (flush) behavior, supports multiple crashes and recovery, and proposes a programming pattern plus the correctness condition persistent linearizability. Builds and verifies two persistent queue implementations (Michael‑Scott and a locking queue) and proves they satisfy the condition.

AI-written summary · about

" chapters (15)

1. 0:00Intro
2. 0:27History
3. 1:14What is Persistent Memory?
4. 2:29(Sequential) Hardware
5. 3:15What is Memory Persistency Model?
6. 4:13What Can Go Wrong?
7. 5:16Persistent Fence
8. 6:31What Can Go Wrong (Continued)?
9. 10:15Total Store Ordering (TSO)
10. 12:36Persistent TSO (PTSO)
11. 13:53Contributions
12. 14:50Verifying programs under PTSO
13. 18:02Persistent Linearisability
14. 19:23What about Multiple Crashes?
15. 20:26Conclusions

" related talks

• 30mDeciding Reachability under Persistent x86-TSOParosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan · POPL 2021
• 12mSPHT: Scalable Persistent Hardware TransactionsDaniel Castro, Alexandro Baldassin, João Barreto, Paolo Romano · FAST '21
• 21mCSL and relaxed memoryStephen Brookes · O'Hearn Fest (POPL 2024)
• 22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of InAzalea Raad, Viktor Vafeiadis, Luc Maranget · POPL 2022
• 01h 13mTransactional memoryMaurice Herlihy · Hydra 2020
• 16mPersistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-Azalea Raad, Ori Lahav, Viktor Vafeiadis · OOPSLA 2020
• 36mATOMICALLY { DELETE YOUR ACTORS }John A De Goes, Wiem Zine Elabadine · Scalar 2019
• 01h 00mWhat did C++ do for Transactional Memory?Michael S Wong · CppCon 2014