Deciding Reachability under Persistent x86-TSO
summary
Shows that reachability for the persistent x86-TSO (Px86) model is decidable reachability by giving a new semantics equivalent to Raad et al.’s Px86 that is a well-structured system. Key steps: transform non‑FIFO behaviors into per‑variable FIFO buffers plus a single merge buffer, replace reorderings with an exact finite-state protocol, and encode channels with a monotone ordering so WSTS machinery applies. The construction preserves reachability and handles both TSO and persistency stages.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 0:15Background
- 6:42Semantics
- 8:08Verification of Concurrent Programs
- 14:52Adapting SC Techniques
- 19:12SC Semantics
related talks
23mPersistence Semantics for Weak Memory
25mParametrised Verification of Intel-x86 Programs
23mA Reachability Logic for a Weak Memory Model with Promises
16mPersistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-
22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
14mMaking Weak Memory Models Fair
23mMemory Consistency Model Status Update