Verifiably correct transactional memory

To ensure correctness, concurrent programs on multicore systems must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer.

This project addresses programmability of concurrent programs through the use of transactional memory, focusing on some of the main challenges surrounding this, and taking the key steps necessary to facilitate wide-scale adoption.

In particular, the team will develop theoretical advances in our understanding of transactional memory correctness, methodological advances in verification techniques for it, and pragmatic advances via the development of application-aware transactional memory designs. Verification tools will support each of these steps.