Translation validation for weak memory models
Lead Research Organisation:
University College London
Department Name: Computer Science
Abstract
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).
People |
ORCID iD |
Jade Alglave (Primary Supervisor) | |
Luke Geeson (Student) |
Studentship Projects
Project Reference | Relationship | Related To | Start | End | Student Name |
---|---|---|---|---|---|
EP/V519625/1 | 01/10/2020 | 30/09/2026 | |||
2525880 | Studentship | EP/V519625/1 | 10/05/2021 | 30/09/2024 | Luke Geeson |