Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-
summary
The paper introduces POG, the first program logic for persistent x86, and an Ix86 instrumented semantics that reduces Px86 by removing the pbuffer via a translation that adds per-location versions. It builds a compiler-like translation (Px86→Ix86), a transformation that replaces flush-optimised with flush in epoch patterns, and a three versions per location encoding (volatile, sync, persistent) that reproduces out‑of‑order and flush semantics and is used to mechanically verify representative examples.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:15Computer Storage
- 0:35What is Non-Volatile Memory (NVM)?
- 0:48Formal Persistency (Low-Level) Semantics
- 1:22X86: (Volatile) Concurrent Hardware Model (TSO)
- 2:21Px86: (Persistent) Concurrent Hardware Model
- 4:31Towards a Persistent Program Logic
- 5:27Contributions
- 10:321x86 and Asynchronous Persists - Naive Attempt
- 11:27Ix86 and Asynchronous Persists
- 13:43Weak Asynchronous Persists
- 14:36Eliminating flushopt Instructions
- 15:12Conclusions
related talks
22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
19mAn Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T...
17mPutting Weak Memory in Order via a Promising Intermediate Representation
23mPersistence Semantics for Weak Memory
30mDeciding Reachability under Persistent x86-TSO
01h 11mProgramming language memory models: Problems, solutions, and directions
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
17mInferring Likely Counting-related Atomicity Program Properties for Persistent...