System-level weak memory models: The need for formalisation, ISA semantics integ...
summary
Argues for fully formalised system-level weak memory models and presents an executable Coq/ROCK-style library that composes a full instruction-set semantics with a separate concurrency semantics via algebraic effects so models are plug-and-play. Implements and tests prototypes on ARM user-mode and an ARM virtual-memory promising model, extracts runnable C code, and uses it to find surprising ordering/TLB and read-after-read anomalies between axiomatic and operational views. Notes current limits: no device or infinite-execution modeling yet.
AI-written summary · about
chapters (7)
- 0:00System-level weak memory models
- 2:11Limitations of modeling
- 5:21Why formalize ISA semantics
- 8:10Reusable formal framework
- 12:45Infinite executions and partial models
- 15:16Challenges and future work
- 16:40Q&A: GPUs and system issues
related talks
26mArchSem: Reusable Rigorous Semantics of Relaxed Architectures
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
16mCompositional Symbolic Execution for the Next 700 Memory Models
01h 11mProgramming language memory models: Problems, solutions, and directions
31mFormal Specification
30mA Tale of Shared Memory Concurrency in Programming Languages
23mVerified Compilation of C Programs with a Nominal Memory Model
36mFlexible Instruction-Set Semantics via Abstract Monads