Luke Geeson

ALT It is critical that compilers are correct! Finding bugs is one aspect of testing the correctness of compilers in wide use today. A compiler is correct if every compiled program behaves as allowed by the semantics of its source code - else there is a bug. Memory consistency models define the semantics of concurrent programs. We focus on how to detect concurrency bugs introduced by compilers, as identified using memory models. We seek a testing technique that automatically covers concurrency bugs up to fixed bounds on program sizes and that scales to find bugs in compiled programs with many lines of code. Otherwise, a testing technique can miss bugs. Unfortunately, the state-of-the-art techniques are yet to satisfy all of these properties. We present the Téléchat compiler testing tool for concurrent programs. Téléchat finds a concurrency bug when the behaviour of a compiled program, as allowed by its architecture memory model, is not a behaviour of the source program [...]

ALT Unfortunately, relaxed memory order does not fully define the semantics of these operations as they are implemented in compilers. This has been discussed in academia and several attempts have been made to define memory models for C/C++. Compilers, which map C/C++ semantics to instructions, have to decide on which C/C++ semantics to implement. Our testing, using the Téléchat compiler testing tool, shows that current compiler implementations are wrong, compared to recent C/C++ models (such as that of Lahav et. al). This post summarizes my findings on the topic, condensed for the wider LLVM/GCC community with the intention of fixing the implementation of relaxed atomics as it is used in practice. I propose that we: Implement Hans Boehm’s branch-after-load proposal Make Lahav et. al’s C/C++ memory model the de-facto model of GCC and LLVM. Once completed, I will test the implementation using the Téléchat compiler testing tool.