Weak Memory Demands Model-based Compiler Testing
summary
Claim: hardware is using RV 8.2a with Large Systems Extension behaviors more aggressively, so compiled C/C++ can exhibit outcomes not allowed by the C++ model. Evidence: tesat (a compiler-to-model simulator) and updated herd semantics reveal a real LLVM miscompilation where dead‑register rewriting turns a swap destination into the zero register, letting the swap reorder past a DMBLD acquire fence. Result: tesat finds quite a few compiler and toolchain bugs and the LLVM case is reproducible and reported.
AI-written summary · about
chapters (7)
- 0:00Model-based compiler testing intro
- 2:29Hardware relaxations matter now
- 4:36Updating compilers for new hardware
- 6:19Revisiting edge-case test generators
- 8:23Compiler optimization soundness
- 10:51Weak memory testing summary
- 13:22Q&A on bugs and models
related talks
01h 11mProgramming language memory models: Problems, solutions, and directions
01h 02mThe Two Memory Models
22mReconciling High-level Optimizations and Low-level Code in LLVM
01h 02mMemory and Compilers
17mRecent Developments in Optimizing Compilers for RISC-V
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
28mMemory simulations, security and optimization in a verified compiler
32mBit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebr...