Translation validation for weak memory models

We intend to develop tools to check whether mappings from high-level languages to lower-level ones are sound with respect to weak memory models - examples include: compiler mappings from C++ to AArch64 assembly, or Linux kernel concurrency libraries.

This project will involve getting familiar with such models, and with the various tools available to develop and test those models (e.g. the herd+diy toolsuite of Alglave and Maranget).

We intend for the project to have both practical aspects (e.g. implementation and testing) and theoretical ones (e.g. justifying the soundness of our approach formally).