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)

Related work

• [1] Herding Cats: Modelling, Simulation, Testing, and Data Mining for Weak Memory
• [2] Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
• [3] The semantics of transactions and weak memory in x86, Power, ARM, and C++
• [4] Armed Cats: Formal Concurrency Modelling at Arm

Contacts for the project

• Dennis Sprokholt (TU Delft)
• Soham Chakraborty (TU Delft)