Parametrised Verification of Intel-x86 Programs
summary
Proves that k‑alternation bounded reachability for Intel eTSO is decidable even when the number of identical threads is unbounded, overcoming the need to refer to thread identities by (1) introducing an equivalent NTW‑load (DLTSO) semantics with subprocess staging and per‑variable NTW buffers to capture reorderings, (2) encoding bounded alternation by splitting threads into stage subprocesses, and (3) giving a novel reduction to well‑structured transition systems over BQOs so that parameterized eTSO reachability is decidable under the k‑alternation restriction.
AI-written summary · about
chapters (13)
- 0:00Parameterized verification intro
- 1:04Intel x86 weak memory
- 2:32Total Store Ordering model
- 5:20Extended TSO with non-temporal writes
- 8:54Classical TSO verification
- 11:01What is parameterized verification
- 12:51Undecidability of parameterized verification
- 13:34Challenges in extended TSO verification
- 15:44Well-structured transition systems
- 17:07Dual-load TSO model
- 19:55DLTSO for bounded alternation
- 21:01Process decomposition under ETSO
- 24:14Summary and future
related talks
30mDeciding Reachability under Persistent x86-TSO
22mExtending Intel-x86 Consistency and Persistency: Formalising the Semantics of In
26mContext-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
22mContext-Bounded Verification of Thread Pools
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
19mCommutativity Simplifies Proofs of Parameterized Programs
19mScenario-based Proofs for Concurrent Objects