Relaxed Memory Concurrency Re-executed
summary
Proposes XMM, an almost per‑execution semantics that enforces memory consistency by adding an in‑order execute rule and an out‑of‑order reexecute rule that replays subsets of committed events, which prevents thin‑air reads while keeping standard compiler and hardware optimizations valid. Instantiation XC20 proves DRF guarantees and supports thread sequentialization—claimed first in its class. Implements XMC model checker built on GenMC with a deterministic reexecution heuristic based on buffered races; XMC is sound and verifies realistic benchmarks with performance comparable to baseline in many cases.
AI-written summary · about
chapters (8)
- 0:00Relaxed memory concurrency intro
- 2:37Thin air values in C20
- 5:07Introducing XMM model
- 6:50XMM prevents thin air reads
- 8:39Thread sequencing in XMM
- 11:30XMC model checker for XC20
- 13:21XMM advantages and future
- 14:49Q&A
related talks
16mModel Checking for a Multi-Execution Memory Model
13mThe Semantics of Shared Memory in Intel CPU/FPGA Systems
22mIn-order execution nails every weak memory behavior
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
01h 11mProgramming language memory models: Problems, solutions, and directions
30mA Tale of Shared Memory Concurrency in Programming Languages
23mMemory Consistency Model Status Update
01h 02mMemory and Compilers