The aim of this project is to build a foundation for rigorous testing and verification of C++ programs that use Transactional memory (TM). TM is a programming abstraction that promises high-performance, easy-to-use concurrency. It allows programmers to group instructions into a transaction, the execution of which appears instantaneous to other threads. After twenty years of development in academia, there is now a flurry of commercial activity around TM in both hardware and software. Intel x86 and IBM Power processors now include TM, and a proposal for adding TM into C++ is currently aiming for official adoption in 2020.
Though programmer-friendly, TM has been associated with numerous security vulnerabilities and exploits, and is notoriously tricky for processor architects and language designers to implement correctly. We plan to address this challenge using formal methods. Specifically, we will produce the first formal semantics for C++ that accounts for both TM and atomic operations. We will then use this as a basis for mechanically proving key properties of C++ TM, and for generating test-cases for checking that currently-available C++ TM implementations are specification-compliant. In short: our aim is to build a foundation for rigorous testing and verification of C++ programs that use TM.
Researchers: John Wickerson, Imperial College London.