Proving Binary Translation between Architectures
Master Project


Project description

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[1] 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[2]
  • Mapping Transactional Memory[3]
  • Mapping Mixed-Size Accesses[4]
  • Mapping to other Architectures

In this master thesis project you will write proofs for any of these (or related) topics.

Requirements

  • Familiarity with a Proof Assistant, such as Agda (or Coq)

Contacts for the project


Proving Binary Translation between Architectures

Supervisor(s): Dennis Sprokholt, Soham Chakraborty
Posted: December 20, 2021