PI: John Wickerson, Imperial College London

  • Concurrent programming is hard, but transactional memory promises to make it simpler.
  • Transactional memory lets programmers make a group of instructions execute ‘instantaneously’ by marking them as a ‘transaction’.
  • However, transactional memory is notoriously hard to specify and implement correctly in compilers.
  • The aim of this project is to build a framework for testing whether or not compilers are implementing this form of concurrency correctly.

The scope of this project has broadened considerably compared to the original workplan. The original focus was on testing the compilation of transactional C/C++ concurrency. However, we soon realised that the proposed approach could be applied to test the compilation of any C/C++ concurrency, in a way that has never been tried before, but which has the potential to be a hugely valuable technique for improving compiler reliability. This generalisation has the potential to greatly amplify the impact of our work.

We have developed a prototype tool that uses a combination of techniques (automatic testcase generation, semantics-preserving code mutation, and exhaustive simulation) to search for bugs in the way mainstream compilers translate concurrent C/C++ (including atomic operations). The tool is open-sourced and available under a permissive licence. It has generated and run hundreds of thousands of tests on several mainstream compilers targeting a range of architectures. Our efforts have revealed concurrency-related bugs in historic versions of the GCC compiler, as well as two non-concurrency-related bugs in recent versions of GCC and the IBM XL compiler.The diagram below illustrates the structure of the tool.

PUBLICATIONS. Our prototype tool has been presented at a scientific meeting at the UCL Computer Science department (November 2018) and at the S-REPLS programming languages workshop (February 2019). [1] Matt Windsor, Alastair F. Donaldson, John Wickerson: C4: the C compiler concurrency checker. ISSTA 2021: 670-673

RELATED GRANTS. This project is also being partially funded by the EPSRC Programme Grant “IRIS: Interface Reasoning for Interacting Systems” (£6.1M, 2018–2023).

IMPACT.  “The programmability of concurrent systems, especially under weak-memory models, is an important challenge for Arm. This is an active area of interest to Arm, and we are delighted to see work that looks at a fuller formalisation of C++ transactional memory.”
– Nathan Chong, formerly Principal Researcher at Arm, now Principal Engineer at Amazon Web Services –