Model Checking C/C++ with Mixed-Size Accesses
summary
Presents an algorithm that lets a DPOR-based model checker handle C/C++ mixed-size accesses by treating whole instructions atomically while allowing revisits that keep sets of writes, claiming completeness, optimality, and polynomial space. Implements Mixer inside GenMC, introduces multi-revisits to retain previously removed writes so executions with split byte accesses become reachable, verifies Linux lo clients up to four threads (explorations growing to tens of thousands) and reports under 2× overhead on non-MSA benchmarks.
AI-written summary · about
chapters (16)
- 0:00Model checking mixed-size accesses
- 1:01Concurrency and weak memory
- 2:25Linux kernel loff example
- 3:28Stateless model checking limits
- 4:50Dynamic partial reduction graphs
- 6:14DPR incremental exploration
- 8:21DPR consistency and optimality
- 9:05DPR mixed-size problem
- 10:53Mixer multi-revisits solution
- 13:23Ensuring optimality with type breaking
- 14:27Mixer evaluation on Linux kernel
- 15:33Mixer recap and extensions
- 15:55Q&A keep sets optimality
- 17:00Q&A read/write splitting
- 18:07Q&A memory models UB
- 18:49Q&A related work checks
related talks
16mModel Checking for a Multi-Execution Memory Model
26mArmed cats: formal concurrency modelling at Arm
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
01h 11mProgramming language memory models: Problems, solutions, and directions
18mMix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
16mCompound Memory Models
23mVerifying Observational Robustness Against a C11-style Memory Model
30mStateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applic