Model Checking for a Multi-Execution Memory Model

Explore advanced concepts in multi-execution memory models through this conference talk from ACM SIGPLAN's OOPSLA. Delve into the challenges of Promising and Weakestmo models, which justify concurrent program outcomes by considering multiple candidate executions collectively. Discover how this characteristic, while beneficial for hardware compilation and compiler optimizations, complicates reasoning and model checking. Learn about Weakestmo2, a strengthened version of Weakestmo that constrains multi-execution nature while preserving key properties like DRF theorems and compilation to hardware models. Examine novel concepts such as load buffering race freedom and certification locality, which help characterize surprisingly weak program behaviors. Gain insights into WMC, a model checker for Weakestmo2 that offers performance comparable to tools for per-execution models.