Atomic memory operations (‘atomics’) are a key programming construct in the world’s most efficient concurrent algorithms. Recognising this, mainstream languages like C, C++, and Java now offer built-in support for a range of atomics. However, the concurrency semantics of these languages are notoriously complicated, so it’s hard to be sure that compilers correctly implement such constructs. Compiler bugs are particularly egregious because they undermine source-level analyses.
In this talk, we discuss ACT, an in-development toolkit for checking the compilation of C11 atomics against the language’s standard memory model. ACT brings together tools like Memalloy (which generates C programs with known visible outcomes when mis-compiled), Herd (which exhaustively simulates C and assembly programs against their respective memory models), and Litmus (which stress-tests programs on real hardware), alongside novel components (such as converters from compiler assembly output to sanitised litmus tests ready for Herd and Litmus consumption). It exposes a workflow that allows automatic checking for discrepancies in the memory state sets observed on the compiled program with regards to the original generated program; this, in turn, helps us find compiler bugs. ACT supports remote compilation, as well as stress-testing, via SSH and SCP.
ACT presently targets a subset of the 32-bit x86 architecture and GCC-style compilers (for example, GCC itself and Clang). We have large-scale plans for ACT’s development, including adding ‘fuzz-testing’ support by mutating the generated C in ways that could affect compilation; extending it to support other architectures (such as Arm and POWER); and expanding both ACT and Herd to understand more of the idioms and instructions that real-world compilers output.