PI: Mark Batty, Co-I: Radu Grigore, University of Kent
- Prose specifications of relaxed memory behaviour are imprecise and lead to bugs in language specifications, processors, compilers and vendor-endorsed programming idioms.
- Mechanised formal models have been used in academia to unambiguously specify and verify relaxed memory behaviour.
- PrideMM is a Solver for Relaxed Memory Models, which improves on state of-the-art descriptions of the concurrency behaviour of programming languages.
- PrideMM provides a platform for comparison, testing, and refinement of relaxed memory models.
Modern computer systems have relaxed memory: they exhibit highly unintuitive memory behaviour as a result of aggressive processor and compiler optimisations. At the same time, these systems are specified with relatively imprecise prose specifications, leading to bugs in language specifications, deployed processors, compilers and vendor-endorsed programming idioms. A push from academia has, in place of prose, introduced mechanised formal models that unambiguously specify relaxed memory behaviour, together with proofs and simulation tools that allow the validation of key design goals.
This project concerns PrideMM: a solver that allows one to run tests over state-of-the-art descriptions of the concurrency behaviour of programming languages. Previous relaxed memory simulators were based on ad-hoc backends or SAT solvers. Additional computational complexity arises in cutting-edge language models that must consider multiple paths of control flow, so the simulator backend embodies a problem outside of the scope of SAT. The problem is, however, within the scope of rapidly improving QBF solvers, atop which PrideMM is built.
The Web Interface to PrideMM is an essential outcome of this project. It allows one to run large batteries of automatically generated tests, and compare its runtime to those of the existing state of the art. The goal of PrideMM is to facilitate discussion with the specifiers of industrial concurrency models, promoting the latest academic solutions to open problems faced by industry.
PUBLICATIONS. [1] M. Batty et al. “PrideMM: A Solver for Relaxed Memory Models”, draft paper detailing representations of key memory models, a proof-of-concept backend, and a specification language that marries expressiveness and ease of solving. [2] M. Janota, R. Grigore, V. Manquinho. “On the Quest for an Acyclic Graph” draft paper on finding acyclic graphs under a set of constraints, a general problem central to PrideMM.
RELATED GRANTS. Dr Mark Batty, EPSRC Grant: “Compositional, dependency-aware C++ concurrency”, PI, £98,786, 04/2018-03/2020. Dr Mark Batty, EPSRC Grant “Verifiably Correct Transactional Memory”, Co-I, £82,904, 07/2018-06/2021. PrideMM is the starting point for tools envisaged by these two grants.
IMPACT. “I believe that a well-reasoned memory model is the most important feature of any parallel programming platform, and that Mark Batty’s work has contributed to building confidence in these models more than anyone else’s.”
– Olivier Giroux, Distinguished Architect at NVIDIA, Chair of Concurrency & Parallelism for ISO C++ –
