Model Checking for a Multi-Execution Memory Model
summary
Introduces load buffering race freedom and certification locality as concrete constraints that rule out surprising out‑of‑thin‑air behaviors, defines a strengthened Weakestmo as Weakestmo2 that preserves DRF theorems, hardware compilation and local transformation correctness, and implements WMC — a GenMC‑based model checker that enumerates in‑order executions, only attempts promises when a detected buffer race occurs, and certifies promises by local re‑execution. Benchmarks show WMC is faster than several multi‑execution tools and close to the best per‑execution tools.
AI-written summary · about
chapters (10)
- 0:00Multi-execution memory models
- 1:26Out-of-order execution issues
- 2:30Multi-execution model checking challenges
- 4:33Weak memory model properties
- 5:59World buffering race freedom
- 8:10Certification locality and branches
- 10:00Model checker implementation
- 11:26Performance comparison
- 12:48Conclusion and contributions
- 13:30Q&A
related talks
22mRelaxed Memory Concurrency Re-executed
21mModel Checking C/C++ with Mixed-Size Accesses
21mWeak Memory Demands Model-based Compiler Testing
23mMemory Consistency Model Status Update
14mMaking Weak Memory Models Fair
32mMemory Model
01h 11mProgramming language memory models: Problems, solutions, and directions
26mKater: Automating Weak Memory Model Metatheory and Consistency Checking