Proving Binary Translation between Architectures
Translating programs from one CPU architecture — such as x86, Arm, RISCV, or PowerPC — to another, is a challenging problem. When porting a program between these architectures, one must take care that the resulting program remains correct. In particular, a concurrent program may display many different outcomes, which depend on the interleaving and CPU-level reordering of instructions that access memory; This interleaving and reordering behavior differs between architectures.
Weak memory models describe the observable behavior of a program for a particular CPU architecture. We wrote proofs in Agda for mapping memory-access instructions between several architectures. However, many proofs opportunities remain:
- Mapping Persistency
- Mapping Transactional Memory
- Mapping Mixed-Size Accesses
- Mapping to other Architectures
In this master thesis project you will write proofs for any of these (or related) topics.
- Familiarity with a Proof Assistant, such as Agda (or Coq)
-  Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
-  Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
-  The semantics of transactions and weak memory in x86, Power, ARM, and C++
-  Armed Cats: Formal Concurrency Modelling at Arm
Contacts for the project
Supervisor(s): Dennis Sprokholt, Soham Chakraborty
Posted: December 20, 2021