https://binary-translation.github.io/index.html

  * Binary Translation

  * Navigation

  * 
  * Contact

  * Home
  * 
  * Memory Models
  * 
  * Static Translation
  * 
  * Dynamic Translation
  * 

Binary Translators for Weak Memory Model Architectures

Tools that correctly translate concurrent x86 binary programs to
Armv8

---------------------------------------------------------------------

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 program, 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.
---------------------------------------------------------------------

Binary Translators

Static Binary Translation with Lasagne

Lasagne
(Static)

Dynamic Binary Translation with Risotto

Risotto
(Dynamic)



About This Site

Lasagne and Risotto correctly translate concurrent x86 binary
programs to Armv8.

Services

  *  
  * Contact

Created by Dennis based on Feeling Responsive and intel-mpx.

  *