Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures

Redha Gouicem, Dennis Sprokholt, Jasper Ruehl, Rodrigo C. O. Rocha, Tom Spink, Soham Chakraborty and 1 other

To run old x86 programs on new Arm chips, an emulator like Qemu translates the code as it runs — but x86 and Arm disagree about how memory operations can be reordered across threads, so Qemu sprinkles in memory fences to force x86's stricter order, which is both slow (fences can be 75 percent of the runtime) and, the authors show, still wrong for atomic operations; this work from TU Munich, TU Delft and collaborators builds Risotto, which uses a theorem prover to derive the minimal correct set of fences, and also calls native Arm libraries and instructions directly, making emulation faster and provably correct at once.

The argument in one glance

Problem

Running old x86 software on new Arm chips means bridging two memory models

The hardware world is shifting from x86 toward Arm and RISC-V, but the mountain of existing x86 software will not run on those chips. A dynamic binary translator solves this by translating a program's instructions from the guest architecture to the host as it runs. The genuinely hard part is concurrency. Different architectures make different promises about how one thread's memory operations can be reordered as seen by another. The x86 model is strong and forbids most reorderings; the Arm model is weak and permits many. Translate a multi-threaded x86 program naively onto Arm and it can behave in ways x86 never would.
What people did

Insert memory fences everywhere to force the stronger order

The standard fix, used by the state-of-the-art translator Qemu, is to insert memory fences — barrier instructions that block reordering — so that Arm respects x86's stricter ordering. Qemu inserts them conservatively, placing a fence before essentially every memory access to be safe. It also translates the program's shared libraries from guest to host code along with everything else, and routes atomic read-modify-write operations through helper-function calls.
Why it fell short

Qemu is both slow and, for atomics, actually wrong

This backfires twice. On performance, the blanket fences over-enforce ordering beyond what x86 requires, blocking the reorderings the CPU is allowed to make and preventing adjacent fences from merging; fences alone account for up to 75 percent of a benchmark's runtime. On correctness, the authors discover and report several real bugs: Qemu's handling of atomic operations and certain fences produces outcomes that x86 forbids. They even find the official Arm memory-model specification itself needed fixing to allow a correct mapping.
This paper's idea

Prove the minimal correct fences, and use native host code directly

Risotto attacks both at once. It builds the first formal memory model of Qemu's intermediate representation and uses a theorem prover to derive mapping schemes that insert only the minimal fences needed for correctness — weaker and fewer than Qemu's — and to prove the fence-merging optimizations sound. On top of that, it links directly to the machine's native shared libraries instead of translating guest copies, and translates atomic compare-and-swap straight to Arm's native atomic instruction. The result is emulation that is faster and provably correct together.

Why this problem is worth solving

The heart of the difficulty is a mismatch of promises between two architectures, so it is worth being precise about what a memory model is.

A memory model defines what orderings of memory operations a program can observe across threads. The intuitive model, sequential consistency, says everything happens in a single interleaved order matching each thread’s program order. Real hardware is weaker than this for speed: to keep its pipelines and caches busy, a processor may let a later load or store appear to execute before an earlier one, as long as a single thread cannot tell. How much reordering is allowed differs by architecture. The x86 model is strong: it permits only one kind of reordering, a store followed by a load to a different location. The Arm model is weak: independent loads and stores to different locations may freely reorder. This gap is the whole problem for binary translation. If an x86 program relies on two writes being seen in order — which x86 guarantees — and you translate it naively to Arm, Arm may reorder them, and another thread sees an impossible state. To prevent this, the translator inserts memory fences: instructions that forbid specific reorderings across them. Fences restore the guest’s ordering on the host, but they are expensive, because each one forces the processor to stall its reordering machinery exactly where the hardware wanted to run ahead. So the translator faces a bind: too few fences and the program is wrong, too many and it is slow.

The reason Qemu lands on the wrong side of that bind is that it reasons informally, and concurrency punishes informal reasoning.

Qemu’s strategy is to be conservative: put a fence before nearly every memory access, hoping that enforcing more ordering than x86 needs is at least safe. Both halves of that hope fail. It is slow because the extra fences forbid reorderings that x86 actually allows, so the Arm processor cannot use scheduling freedom it legitimately has, and because a fence before every access leaves no adjacent fences to merge into cheaper combined ones — the paper measures fences at up to seventy-five percent of runtime, forty-eight percent on average. And it is still not correct, because the subtle cases — atomic read-modify-write operations and certain fence placements — are exactly where informal reasoning slips. Qemu translates atomics as calls to helper functions built on compiler intrinsics whose generated instructions vary by compiler version, and it uses a fence pattern that a later optimization can transform into an illegal reordering. The authors exhibit concrete concurrent programs where Qemu’s translation yields an outcome x86 forbids. Worse, they find that even the official Arm model specification did not support a correct, efficient mapping and had to be revised. The lesson is that getting strong-on-weak translation both fast and correct is not something eyeballing the fences can deliver — it needs a formal model you can prove things against, which is what makes the effort worthwhile.

What people did before, and where it broke

Insert a fence before every memory access (Qemu’s blanket policy). Conservatively over-order everything so the host cannot violate the guest’s ordering. Where it broke. It blocks reorderings x86 legitimately allows and leaves no adjacent fences to merge, so fences dominate runtime — up to seventy-five percent — and it is still wrong on the atomic cases informal reasoning misses.
Translate atomics via helper functions and compiler intrinsics. Emulate each read-modify-write by calling into a helper that uses the compiler’s atomic built-ins. Where it broke. The instructions the built-ins emit change with the compiler version, so the same atomic can be translated inconsistently, and the extra jumps cost performance while the ordering guarantees do not match x86’s.
Translate the program’s shared libraries along with its code. Treat guest application and guest library uniformly, translating both to the host ISA. Where it broke. Translated code is slower than natively compiled code, and it needlessly re-translates functions — like the C library — that already exist in optimized native form on the host, and it forces slow software floating-point emulation.
Insert fences by model-checking the whole program. Analyze the program to compute where fences are truly needed. Where it broke. Optimal fence placement is undecidable in general, and model checking to place fences is computationally expensive and rarely scales beyond small programs.
The gap. Every approach either over-fenced without a correctness argument, translated code the host could run natively, or tried a whole-program analysis that does not scale. What was missing was a formally verified, per-pattern mapping that inserts the minimal correct fences by construction, combined with using native host code where it exists — which is exactly what fast, correct strong-on-weak translation needs.

How Risotto works

Making x86-on-Arm emulation both provably correct and fast

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Prove the translation correct instead of hoping it is. Concurrency bugs are precisely the ones that escape informal reasoning, which is how a mature system like Qemu ended up shipping translations that produce outcomes x86 forbids. Risotto’s foundational move is to build a formal memory model of the translator’s intermediate representation and use a theorem prover to establish that each mapping and optimization preserves the guest’s semantics — turning “this looks right” into a machine-checked proof, and even surfacing a flaw in the official Arm specification that then got fixed. Bringing rigorous, machine-checked verification to a low-level correctness property that the field had been handling by careful-but-fallible hand-argument is the same discipline the memory-safe-C work covered elsewhere on this site embodies, replacing informal assurances about pointer behavior with a guarantee the system can actually prove.

Enforce exactly the ordering required, and not a fence more. Qemu is slow because it over-enforces, fencing against reorderings x86 permits, out of an abundance of caution that a proof makes unnecessary. Once you can prove which orderings actually matter, you can insert the minimal, weakest fences that preserve correctness and let the processor reorder everywhere else, and let adjacent fences merge. Stripping away the conservative, defensive work that a full analysis shows is not needed — keeping only what correctness genuinely requires — is the same instinct behind the recommendation-compiler work covered elsewhere on this site, which proves the framework’s blanket safety checks redundant in context and deletes them, trading blind caution for analyzed minimalism.

Use the real native mechanism instead of a slow emulated stand-in. Emulation has a habit of re-doing work the host could do directly: translating a guest copy of a library the host already has natively, or routing an atomic through a helper function when the host has a single instruction for it. Risotto instead reaches for the native thing — calling the host’s own shared libraries through the procedure linkage table, and lowering compare-and-swap straight to Arm’s native atomic instruction — so the emulated program runs real host code where it can. Bypassing a costly generic detour to hit the hardware’s real, fast primitive directly is the same move the ququart-compilation work covered elsewhere on this site makes when it drops a slow general path in favor of the machine’s actual fast operation, spending effort to reach the native mechanism rather than emulating around it.

Following a concurrent x86 program through Risotto

Translating a multi-threaded x86 program with an atomic

Tracing one program shows how verification and native code compound.

Step 1 of 5

An x86 binary with threads, an atomic, and a library call arrives

A multi-threaded x86 program relies on the strong ordering x86 guarantees between its writes, uses an atomic compare-and-swap to coordinate, and calls into a shared library such as OpenSSL. It must run unchanged on an Arm machine, preserving exactly the behaviors x86 would allow and no others.

Naively translated to weak Arm, the writes could reorder and the atomic could be mistranslated.

Why it works

Inserting only the minimal proven fences restores the processor’s legal freedom. Qemu fences before nearly every access, forbidding reorderings x86 actually allows → but a verified mapping inserts only the fences x86 semantics require and no more → so the Arm processor reorders where it legally can and adjacent fences merge, cutting the dominant fence cost.
A formal model lets concurrency optimizations run without introducing bugs. Optimizations sound for sequential code can be wrong for concurrent code, so a cautious translator either skips them or ships bugs → but proving each transformation preserves the intermediate representation’s memory model makes it safe → so fence-merging and reordering apply confidently instead of being avoided or breaking correctness.
A direct native atomic is both correct and cheaper than a helper call. Qemu routes atomics through version-dependent helper functions whose ordering does not match x86 → but lowering compare-and-swap straight to Arm’s native instruction gives matching full-fence semantics in one instruction → so the atomic is provably correct and avoids the helper-call jumps.
Calling native libraries beats translating slower guest copies. Translated code cannot match a native compiler’s optimization, and the host often already has the library → but intercepting library calls and invoking the host’s native version directly runs real optimized code → so library-heavy programs reach native speed for that portion, up to a twenty-three-times speedup.
Native libraries also replace slow software floating-point with hardware instructions. Emulating floating point across implementations is hard, so Qemu falls back to slow software floating-point → but a native host library uses the machine’s real floating-point instructions → so numerically heavy library calls gain further on top of avoiding translation.

What it costs (trade-offs and scope)

The verification covers the mappings and specific optimizations, not all of Qemu. Risotto formally models the intermediate representation and proves its mapping schemes and named transformations correct; it is a verified core built into Qemu, not a whole-system proof, so unverified parts of the emulator remain trusted.
The average fence speedup is modest. The verified minimal-fence mappings improve performance by 6.7 percent on average, up to 19.7 percent; the dramatic numbers come from the library linker, which only helps programs that lean heavily on shared libraries.
The dynamic linker needs a hand-written signature description and an assumption. Because guest and host application binary interfaces differ, each native library function needs an interface description of its argument types to marshal values, and correctness assumes the native library and emulated code do not concurrently touch the same data — safe in the tested applications but not guaranteed in general.
The atomic speedup is contention-dependent. Direct compare-and-swap beats Qemu by up to 48 percent only under low contention; under high contention the atomic instruction itself dominates and the two perform similarly, since Qemu’s helper also ends up using the same native instruction.
Short native calls do not reach native speed. For very short library functions like some math routines, the cost of marshaling arguments between guest and host conventions dominates, so Risotto speeds them up but falls short of a native binary.
It is scoped to x86-on-Arm user-mode emulation. The formal models and mappings are specific to x86, Arm, and Qemu’s intermediate representation; the methodology generalizes to other strong-on-weak pairs, but the proofs and results here are for this case, and optimal fence placement in general remains undecidable.

The evaluation

Three ways to run concurrent x86 binaries on Arm

Property	Qemu	No fences (incorrect oracle)
Correctness of ordering
Fence policy
Shared libraries		Translate guest copies
Atomic compare-and-swap		Helper-function call
Performance versus Qemu	Baseline

Three ways to emulate concurrent x86 on Arm, evaluated on the PARSEC and Phoenix benchmark suites plus OpenSSL, SQLite, and the math library, on a Marvell ThunderX2 Arm server. The no-fences variant is incorrect but reveals that fences are up to 75 percent (48 percent average) of Qemu's runtime. Risotto's formally verified minimal-fence mappings improve performance 6.7 percent on average (up to 19.7 percent) while being provably correct, its dynamic linker reaches native speed for library-heavy code (up to 23 times faster), and its direct compare-and-swap is up to 48 percent faster under low contention — fixing the correctness bugs Qemu has along the way.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

Risotto is a rare thing: a systems paper that makes emulation both faster and provably correct at once. It shows that Qemu, the state-of-the-art translator, is simultaneously slow — inserting a fence before nearly every access, so fences are up to 75 percent of runtime — and, on atomics and some fences, actually wrong, producing outcomes x86 forbids; it even finds and gets fixed a flaw in the official Arm memory-model specification. Its answer is to build the first formal model of Qemu’s intermediate representation, prove minimal-fence mappings and merging optimizations correct in a theorem prover, and add two systems wins: linking native host libraries and lowering compare-and-swap to a native Arm instruction. Read it with its scope. The verification is of the mappings and named optimizations, not all of Qemu, so much of the emulator stays trusted. The fence work yields a modest 6.7 percent average; the eye-catching numbers are the library linker, which needs a hand-written signature description per library and only helps library-heavy programs, and the atomic win is only under low contention. It is scoped to x86-on-Arm user-mode emulation. The durable lesson is that for concurrency, correctness and performance are not opposed but joined at the hip: a proof of what ordering is truly needed is exactly what licenses you to stop over-fencing and go faster.

Background

Why weak memory models keep breaking otherwise-careful systems

It helps to see Risotto’s Qemu bugs not as a lapse but as the norm for weak memory. The reason concurrency is so treacherous is that a weak memory model makes a program’s observable behavior nondeterministic in a way that depends on invisible microarchitectural choices — which loads and stores the hardware quietly reorders — so the space of outcomes a correct translation must preserve is large, subtle, and impossible to survey by testing, since a bug may surface only on one processor under one timing. This is why informal reasoning, even by experts building a system as scrutinized as Qemu, ships translations that are wrong in cases no one thought to check, and why the field increasingly turns to formal models that enumerate the allowed behaviors precisely and let tools prove a transformation stays inside them. The nondeterministic-quantum-program verification work covered elsewhere on this site confronts the same shape of problem from another domain, building a rigorous logic to reason about programs whose outcomes are a distribution rather than a single value, because eyeballing nondeterministic behavior does not work. The broad lesson is that once a system’s correctness depends on all the ways execution could legally interleave or reorder, the only reliable path is a formal account of that space and machine-checked proofs against it — testing can find bugs but never their absence.

If you remember only three things

1. Dynamic binary translators like Qemu run unmodified x86 programs on Arm by translating instructions at runtime, and the hard part is concurrency: x86 has a strong memory model that forbids most cross-thread reorderings while Arm is weak and allows many, so the translator must insert memory fences to preserve x86 ordering. Qemu inserts them conservatively — a fence before nearly every access — which over-enforces and makes fences up to 75 percent (48 percent average) of runtime, and yet the authors find its atomic and some fence handling is still incorrect, producing outcomes x86 forbids, and even the official Arm memory-model spec needed a fix (which they got accepted).
2. Risotto attacks correctness and performance together. It builds the first formal concurrency memory model of Qemu's intermediate representation in the Agda theorem prover, then derives and proves mapping schemes (x86 to intermediate representation to Arm) that insert only the minimal, weakest fences needed for correctness, plus proves the fence-merging and reordering optimizations sound so they run safely. It adds two systems optimizations: a dynamic linker that intercepts shared-library calls at the procedure linkage table and invokes the machine's native libraries directly (marshaling arguments via a signature-description interface language), and a direct translation of x86 compare-and-swap to Arm's native atomic instruction, whose full-fence semantics provably match, fixing Qemu's bug and skipping the helper-call detour.
3. On PARSEC and Phoenix plus OpenSSL, SQLite, and the math library on a Marvell ThunderX2 Arm server, Risotto's verified minimal-fence mappings improve performance 6.7 percent on average (up to 19.7 percent) while being provably correct, the dynamic linker reaches native speed for library-heavy code (up to 23 times faster, and native floating-point too), and direct compare-and-swap is up to 48 percent faster under low contention. Its limits: the verification covers the mappings and named optimizations rather than all of Qemu, the average fence speedup is modest, the linker needs a hand-written per-library signature description and assumes native and emulated code do not race on shared data, the atomic win is contention-dependent, short library calls do not match native speed, and it is scoped to x86-on-Arm user-mode emulation.

Check yourself

Check your understanding

1. Why does translating a concurrent x86 program to Arm require inserting memory fences?
2. What two problems did the authors find with Qemu's approach to memory ordering?
3. How does Risotto make its fence insertion both correct and faster than Qemu's?
4. Which statement best reflects the scope and limits of Risotto?

Sources

The paper is “Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures” by Redha Gouicem, Dennis Sprokholt, Jasper Ruehl, Rodrigo C. O. Rocha, Tom Spink, Soham Chakraborty, and Pramod Bhatotia, published at ASPLOS 2023, DOI 10.1145/3567955.3567962. The authors are at TU Munich, TU Delft, the University of Edinburgh, and the University of St Andrews.

This explainer is written from the full 16-page text. Everything above comes from the paper’s own sections: the introduction and background on weak versus strong memory models and dynamic binary translation, and Qemu’s Tiny Code Generator intermediate representation; the motivation exposing Qemu’s concrete correctness errors in translating atomic read-modify-write operations and the Fmr fence (the MPQ, SBQ, and FMR example programs producing x86-forbidden outcomes), the compiler-version inconsistency in helper functions, and the reported flaw in the Arm-Cats memory model that was accepted upstream; the performance analysis showing fences at up to 75 percent (48 percent average) of runtime and the shared-library translation issue; the formal TCG intermediate-representation concurrency memory model built in the Agda theorem prover with verified x86-to-intermediate-representation and intermediate-representation-to-Arm mappings and proven optimizations (fence merging, redundant-access elimination, reordering); the Risotto system with its verified mappings, the dynamic host library linker using the procedure linkage table and an interface definition language for argument marshaling, and the direct compare-and-swap translation to Arm’s casal instruction; and the evaluation on PARSEC, Phoenix, OpenSSL, SQLite, and the math library on a Marvell ThunderX2 server, reporting the 6.7 percent average (up to 19.7 percent) fence-mapping improvement, dynamic-linker speedups up to 23 times matching native, and the up-to-48-percent compare-and-swap improvement under low contention.