Binary Translators for Weak Memory Model Architectures
What is Binary Translation?
While x86 previously dominated the CPU market, we see Arm emerge prominently in many domains; For instance, on servers and laptops. These architectures have different instruction sets and features, which makes it difficult to port existing x86 programs to Arm CPUs. In particular, these architectures have different memory models, which means that x86 and Arm reorder instructions differently during execution. That results in different behavior for the same concurrent programs.
We built two binary translators to address this problem, in different ways. Lasagne translates any x86 program statically to an Arm program. Risotto emulates the x86 program dynamically on an Arm machine. For either case, we provide mechanized proofs that demonstrate the correctness of the translation w.r.t. the memory models of x86 and Arm.
