Verifiably correct transactional memory

Multi-core computing architectures have become ubiquitous over the last decade.

Start date


End date



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.

Funding amount





  • University of Sheffield
  • University of Kent associate partners
  • ARM Ltd
  • Mozilla Limited
  • DePaul University
  • University of Augsburg
  • University of Paderborn
  • University of Queensland
  • Victoria University of Wellington.