Arancini: A Hybrid Binary Translator for Weak Memory Model Architectures

Sebastian Reimers, Dennis Sprokholt, Martin Fink, Theofilos Augoustis, Simon Kammermeier, Rodrigo C. O. Rocha and 4 others

To run an old x86 program on a new Arm or RISC-V chip without its source, a binary translator rewrites it — but doing this ahead of time is fast yet cannot handle every program, doing it while running handles everything but is slow, and worst of all, the new chips reorder memory more aggressively than x86 did, so a naive translation silently breaks multi-threaded code; this paper (TU Munich, TU Delft, St Andrews) builds Arancini, which does both kinds of translation through one shared representation and inserts exactly the memory fences a mathematical proof says are needed, running correct concurrent code up to 5 times faster than a leading translator.

The argument in one glance

Problem

Running old x86 binaries on new Arm and RISC-V chips is fast, or complete, or correct — pick two

The hardware world is shifting from x86-64 to Arm and RISC-V, in servers, laptops, and phones alike, and a great deal of existing software has no source code to recompile. A binary translator bridges the gap by rewriting an application's machine code from one instruction set to another. There are two ways to do it, and each sacrifices something. A static translator rewrites the whole binary ahead of time and optimizes it heavily, so it runs fast — but it cannot handle every program, because reconstructing a binary's control flow and jump targets is undecidable in general, so some programs it simply fails to translate. A dynamic translator rewrites code fragments as they execute, so it handles anything, but it pays for that completeness with slow runtime compilation and a merely local view that blocks optimization. And lurking beneath both is a correctness trap: x86-64 has a strong memory model that keeps concurrent memory accesses in order, while Arm and RISC-V have weaker models that reorder them, so a naive translation of a multi-threaded program can silently behave differently on the new chip.
What people did

Use a static translator for speed, or a dynamic one for completeness

The established options are exactly those two. Static translators lift a binary to a high-level compiler representation like LLVM, optimize the whole program, and emit a fast native binary. Dynamic translators, like QEMU, translate small fragments at runtime into a low-level form and run them, handling any program including ones with dynamic jumps that static tools choke on.
Why it fell short

Neither is fast, complete, and correct at once, and concurrency makes it worse

The two approaches sit at opposite corners. Static translation is fast — a state-of-the-art static tool runs only two to three times slower than native — but fundamentally incomplete: programs using jump tables and function pointers create control flow that cannot be recovered ahead of time, so the translator fails on them. Dynamic translation is complete but slow — a state-of-the-art dynamic tool runs five to ten times slower than native. Neither can be fast and complete together. And on concurrent programs both risk being wrong: because the host reorders memory more than the guest, correctness demands inserting precisely the right memory fences on the host to restore the guest's ordering, and getting this wrong changes behavior. QEMU was shown to mistranslate concurrent programs and responded by disabling concurrency entirely, gutting performance. The problem is subtler still for mixed-size accesses — reading and writing overlapping memory in different byte widths — whose concurrency behavior prior verified schemes did not even model.
This paper's idea

One IR for both translation styles, with formally proven fence placement

Arancini is a hybrid binary translator that pursues correctness, completeness, and speed together. It statically translates as much of a binary as possible for speed, and falls back to dynamic translation only for the fragments static analysis cannot reach, gaining a dynamic translator's completeness at near-static performance. The two phases share a single new low-level intermediate representation, ArancinIR, which retains enough structure for whole-program optimization yet lowers quickly for just-in-time translation. Crucially, its memory model and its mappings from x86-64 down to Arm and RISC-V are formally verified in a proof assistant — including the subtle semantics of mixed-size accesses — so the fences it inserts are provably correct and provably minimal. The result runs correct, complete concurrent translations up to five times faster than a leading dynamic translator.

Why this problem is worth solving

The move off x86 makes binary translation broadly necessary, and it exposes a three-way tension no prior system resolves.

A binary translator takes an application compiled for one instruction set and makes it run on another, which matters enormously as industry shifts from x86-64 to Arm and RISC-V and vast amounts of legacy software have no source to recompile. Two designs dominate. A static binary translator does the work ahead of time: it lifts the guest binary to a high-level intermediate representation, applies a full compiler’s optimizations, and emits a native host binary, so the result is fast. But it is necessarily incomplete, because recovering a program’s control flow and jump targets from raw machine code is undecidable in general, and a binary blurs distinctions the source had — pointer versus constant, data versus instruction bytes — so static tools fail to translate some programs outright. A dynamic binary translator instead translates fragments at runtime within their actual execution context, which makes it complete — it can always translate what it is about to run — but it pays with runtime compilation latency and a local-only view that forecloses many optimizations, so it is slow. Fast-but-incomplete or complete-but-slow: the field has had to choose, and a hybrid that statically translates what it can and dynamically handles the rest could in principle have both.

The deeper hazard is that translating concurrency between memory models can be silently wrong.

Every multi-core architecture has a memory consistency model defining which reorderings of concurrent memory accesses are allowed. x86-64’s model is strong: it keeps write-write and read-read-or-write pairs in order by default, so programmers rely on that ordering. Arm and RISC-V have weaker models that permit those reorderings, providing explicit fences and atomic instructions to restore order only where asked. When a concurrent x86-64 program is translated to Arm or RISC-V, the host is therefore free to reorder accesses the guest guaranteed were ordered, which can make the translated program behave differently — a correctness bug that appears only under concurrency and specific timing. To be correct, the translator must insert exactly the right host fences to re-impose the guest’s ordering; too few is wrong, and too many is slow. QEMU was shown to get this wrong and simply disabled concurrency, sacrificing performance for safety. And modern memory models add mixed-size accesses — concurrent reads and writes to overlapping memory at different byte widths, as used in Linux kernel locks and page-table manipulation — whose ordering semantics are subtle and which prior verified mapping schemes did not model at all. Translating concurrency correctly, across this mismatch and its mixed-size complications, is the crux.

What people did before, and where it broke

Static binary translators (for example Lasagne). Lift the whole binary to LLVM, optimize globally, emit a fast native binary. Where it broke. They are incomplete — undecidable control-flow recovery means programs with jump tables and function pointers cannot be translated ahead of time, so the tool fails on them.
Dynamic binary translators (for example QEMU, Risotto). Translate fragments at runtime for full completeness. Where it broke. Runtime compilation and a local-only view make them slow, five to ten times slower than native, so their completeness comes at a steep performance price.
QEMU on concurrent programs. Translate multi-threaded code across the memory-model mismatch. Where it broke. It was shown to mistranslate concurrency and responded by disabling concurrency altogether, badly hurting performance rather than fixing correctness.
Prior verified mapping schemes (for example those in Lasagne and Risotto). Prove correct x86-64-to-Arm memory mappings. Where it broke. They did not model mixed-size accesses, and targeted only Arm, leaving the subtle mixed-size cases and RISC-V uncovered.
The gap. No system was correct, complete, and fast at once: a hybrid translator sharing one IR across static and dynamic paths, with formally verified, minimal fence placement that also handles mixed-size accesses and RISC-V. Building that is what Arancini contributes.

How Arancini works

Hybrid translation over one verified intermediate representation

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

The idea

Do both kinds of translation, and let the dynamic path cover only what the static path cannot. Arancini’s architectural bet is that the fast-or-complete dilemma is false if you combine the two: statically translate the whole binary you can see, run that optimized native code for the overwhelming majority of execution, and invoke dynamic translation only when control reaches an address static analysis never resolved. In their measurements the static path handles nearly everything — at most a couple of percent of unique instructions are translated dynamically, often the same handful triggered by a thread starting after a system call — so the system runs at close to static speed while retaining a dynamic translator’s ability to handle anything. Marrying an ahead-of-time path for performance with a runtime path for the cases the compiler cannot resolve statically is the same complete-and-fast reconciliation the work on dynamic binary translation for weak memory architectures covered elsewhere on this site pursues, and Arancini pushes it further by making the static path carry the load and the dynamic path merely fill the gaps.

Bridge the two worlds with a single intermediate representation. The technical enabler is ArancinIR, one low-level representation that both translation paths share. This is not trivial, because static translation wants a high-level, whole-program view for aggressive optimization while dynamic translation wants a low-level, machine-close form that lowers fast and interacts with emulated hardware state — historically forcing separate representations, like LLVM IR for one and a tiny code-generator IR for the other. ArancinIR is designed to be liftable up into LLVM IR for the static path yet close enough to the binary to be JIT-compiled directly for the dynamic path, so the frontend and the semantics are shared and the two paths produce matching, interoperable code. Designing one intermediate representation that retargets cleanly across very different lowering paths and backends, rather than maintaining a separate one for each, is the same unifying-IR strategy the work on a retargetable, extensible synthesis-based compiler covered elsewhere on this site adopts, letting a single representation serve uses that would otherwise each demand their own.

Make correctness a proof, not a hope — down to minimal fences and mixed-size accesses. Arancini’s signature move is to treat the memory-model translation as something to be formally verified rather than tested. It defines a weak memory model for ArancinIR and mechanizes, in the Agda proof assistant, correct mappings from x86-64 into ArancinIR and from there down to both Armv8 and RISC-V, with the model including the subtle semantics of mixed-size accesses. Because the mappings are proven, the fences and atomics Arancini emits are guaranteed to enforce x86-64 ordering on the weaker host, and proven minimal — no weaker fence would suffice — which is exactly why correctness does not cost excessive slowdown. Establishing that a low-level translation preserves the source’s semantics by mechanized proof, rather than trusting that the generated code happens to behave, is the same guarantee the work on lightweight modular verification of WebAssembly-to-native translation covered elsewhere on this site delivers, turning “we believe this translation is correct” into “we have proven it.”

Following a concurrent program through Arancini

Translating a multi-threaded x86-64 lock to Arm, correctly

A trace, following the paper's design, of how Arancini preserves x86-64 memory ordering when translating concurrent code to a weaker host.

Step 1 of 5

An x86-64 binary uses a lock with ordered accesses

The guest program is multi-threaded and relies on x86-64's strong memory model, which keeps its write-write and read pairs in order — for instance a lock structure from the Linux kernel or C library, some of whose accesses are mixed-size.

On x86-64 the hardware provides this ordering for free, so the program never asked for explicit fences.

Why it works

The static path carries the program, the dynamic path only the exceptions. Doing everything dynamically is slow and everything statically is impossible → but static translation handles all but a couple of percent of unique instructions, with dynamic translation filling only the unresolved addresses → so the system runs near static speed while remaining as complete as a dynamic translator.
One shared IR lets the two paths interoperate. Static and dynamic translation want different levels of abstraction, which normally forces separate representations → but ArancinIR is high enough to feed LLVM optimization and low enough to JIT directly → so both paths share a frontend and semantics and produce matching code that switches cleanly at runtime.
Proven mappings make concurrency correct by construction. Reordering on the weaker host can silently break translated concurrent programs → but mechanized proofs establish that the inserted fences and atomics enforce the guest’s ordering → so correctness is guaranteed rather than tested, unlike QEMU which had to disable concurrency to be safe.
Minimal fences keep correctness cheap. Correctness could be bought by conservatively over-fencing, which would be slow → but the proofs show the mappings are minimal, no weaker fence suffices → so the translator adds only the barriers it must, which is why the correct translation stays fast.
Modeling mixed-size accesses closes a real hole. Real locks and kernel code do concurrent overlapping accesses at different byte widths, which prior schemes ignored → but ArancinIR’s memory model includes mixed-size semantics and the Arm mapping is proven for them → so programs relying on mixed-size concurrency translate correctly, not just the simple cases.

What it costs (trade-offs and scope)

Translation still costs multiples of native speed. Arancini’s output runs several times slower than native (about eight times on Arm and four and a half on RISC-V by geometric mean, improving to roughly six and just under four when linked to native libraries), because it emulates full guest state; its win is over dynamic translators and its completeness over static ones, not parity with native.
The prototype does not implement every feature yet. The design is complete-capable like a dynamic translator, but the authors note they have not implemented all the features of the mature tools they compare against, so it is a research system demonstrating the approach rather than a drop-in replacement.
Mixed-size support is partial and conditional. The verified mixed-size handling is for Arm; the RISC-V model does not currently support mixed-size accesses, and even on Arm the mixed-size correctness holds only when the target has atomic instructions of the correct operand size.
The proofs cover the mappings, not the whole implementation. What is formally verified is the memory-mapping schemes that Arancini follows; the guarantee is that those rules are correct and that Arancini uses them, not an end-to-end proof of the entire frontend, optimizer, and backend.
It is one guest, specific hosts, and a specific workload. The evaluation uses an x86-64 frontend with Arm and RISC-V backends on particular machines and a multi-threaded benchmark suite; the static path still depends on lifting, with the dynamic fallback catching what lifting cannot resolve.

The evaluation

Correct, complete, and fast cross-ISA translation of concurrent code

Property	Static translator (Lasagne)	Dynamic translator (Risotto/QEMU)
Completeness
Performance vs native
Concurrency correctness
Fence placement
Targets	Arm	Arm

From the paper's evaluation on the Phoenix multi-threaded benchmark suite with x86-64 guests and Arm and RISC-V backends. Arancini is a hybrid translator whose static path handles all but about 2 percent of unique instructions, giving completeness like a dynamic translator at near-static performance — up to 5 times faster than the dynamic translator Risotto — while its formally verified mappings ensure correct, minimal fence placement, including mixed-size accesses on Arm, where QEMU had to disable concurrency to stay safe.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

The contribution is a binary translator that refuses the usual trade-offs: it is complete like a dynamic translator, nearly as fast as a static one, and correct for concurrency by mechanized proof. Arancini achieves this with a single unified intermediate representation shared by its static and dynamic paths, a hybrid design where static translation carries the program and dynamic translation fills only the gaps, and formally verified x86-64-to-Arm and x86-64-to-RISC-V memory mappings — proven in Agda and including mixed-size access semantics — that place minimal, correct fences. It runs correct concurrent translations up to five times faster than a leading dynamic translator, where QEMU had to disable concurrency. Read it within scope. It is still multiples slower than native, since it emulates full guest state; it is a research prototype that has not implemented every feature of the mature tools it beats; its mixed-size support is verified for Arm only and needs correctly-sized target atomics, with RISC-V mixed-size unsupported; and the proofs cover the mapping schemes rather than the entire implementation end to end. Within those bounds it is the first hybrid binary translator guided by formal proofs for strong-on-weak execution, and the first to handle mixed-size accesses for Arm.

Background

Why weak memory models make translation treacherous

It helps to appreciate why memory models sit at the center of this. On a single thread, a processor can reorder and overlap memory operations freely as long as the visible result is unchanged, and no one notices. Across threads sharing memory, those reorderings become visible, and each architecture draws its own line about which are allowed — its memory consistency model. x86-64 draws a strict line, forbidding most reorderings, so programmers writing for it lean on ordering they never had to request. Arm and RISC-V draw a looser line for the sake of performance and power, permitting reorderings x86 forbade and offering fences to claw ordering back where needed. This makes reasoning about concurrent behavior across architectures genuinely hard: whether a given translation is correct depends on formal properties of both memory models, and the differences are subtle enough that even careful engineers get them wrong, which is why the field has turned to formalizing these models precisely. Pinning down the exact ordering rules a piece of hardware guarantees, in a form rigorous enough to reason and build on, is the same foundational work the effort on synthesizing microarchitectural memory-ordering axioms covered elsewhere on this site undertakes, making the informal notion of “what this machine allows” into something provable. Arancini stands on that kind of formalization to translate concurrency without silently changing what a program means.

If you remember only three things

1. Cross-architecture binary translators, needed as computing shifts from x86-64 to Arm and RISC-V, have faced a three-way tension: static translation is fast (two to three times slower than native) but incomplete because recovering a binary's control flow is undecidable, dynamic translation is complete but slow (five to ten times slower than native), and both risk silently miscompiling concurrent programs because x86-64's strong memory model orders accesses that Arm and RISC-V's weaker models may reorder — a hazard prior verified schemes worsened by ignoring mixed-size accesses, and that led QEMU to disable concurrency entirely.
2. Arancini is a hybrid translator that statically translates the bulk of a binary for speed (handling all but about 2 percent of unique instructions) and dynamically translates only the fragments static analysis cannot reach for completeness, with both paths sharing ArancinIR — one unified low-level intermediate representation designed to lift into LLVM for whole-program optimization yet lower quickly for just-in-time code generation — and a hybrid binary format bundling the native translation, the original guest code, and switching metadata.
3. Its memory model and its mappings from x86-64 to Arm and RISC-V are formally verified in the Agda proof assistant, including the subtle semantics of mixed-size accesses, so the fences and atomics it inserts to re-impose x86-64 ordering on the weaker hosts are provably correct and provably minimal — keeping correct concurrent translation fast, up to five times faster than the dynamic translator Risotto; the first hybrid binary translator guided by formal proofs for strong-on-weak execution and the first to handle mixed-size accesses for Arm, though it remains multiples slower than native, is a prototype missing some features, and verifies the mappings rather than the whole implementation.

Check yourself

Check your understanding

1. What is the three-way tension that cross-architecture binary translators have faced?
2. Why is translating concurrent programs from x86-64 to Arm or RISC-V a correctness hazard?
3. How does Arancini get completeness, speed, and a shared toolchain at once?
4. What does Arancini formally verify, and what did it achieve?

Sources

The paper is “Arancini: A Hybrid Binary Translator for Weak Memory Model Architectures” by Sebastian Reimers, Dennis Sprokholt, Martin Fink, Theofilos Augoustis, Simon Kammermeier, Rodrigo C. O. Rocha, Tom Spink, Redha Gouicem, Soham Chakraborty, and Pramod Bhatotia (TU Munich, TU Delft, RWTH Aachen, University of St Andrews, and Huawei Research), published at ASPLOS 2026 (Volume 2), DOI 10.1145/3779212.3790127. It is released under a Creative Commons Attribution license.

This explainer is written from the full text of the authors’ open-access version. Everything above comes from the paper’s own sections: the introduction and background on the shift from x86-64 to Arm and RISC-V and the role of binary translation, the strengths and limits of static binary translators (fast but incomplete due to undecidable control-flow recovery, with a state-of-the-art static tool two to three times slower than native) and dynamic binary translators (complete but slow, five to ten times slower than native, with QEMU mistranslating concurrent programs and disabling concurrency); the strong-on-weak memory model mismatch, the concurrency primitives and fences of x86-64, Armv8, and RISC-V, and mixed-size concurrency with its worked example and real uses in Linux kernel locks, spinlocks, and page-table manipulation; the three challenges (unifying static and dynamic IRs, ensuring architectural correctness via a verified mapping scheme, and efficient switching via a hybrid binary format) and Arancini’s three contributions — ArancinIR as a unified low-level IR, the Agda-mechanized formal memory model with proven correct and minimal mappings from x86-64 to ArancinIR and to Armv8 and RISC-V including mixed-size accesses, and the hybrid translator with its static LLVM-based path and lightweight dynamic JIT path plus hybrid binary format; the system workflow (frontend lifting via verified mappings, static translation through LLVM, runtime fallback to dynamic translation on untranslated program counters, and use of native libraries); and the evaluation on the Phoenix benchmark suite across completeness (DBT-like coverage including map-reduce versions with jump tables and function pointers that Lasagne cannot translate), performance (geometric-mean overheads of about 8.01 times on Arm and 4.52 times on RISC-V versus native, improving to about 6.01 and 3.81 with native libraries, up to five times faster than Risotto, with at most about 2.1 percent of unique instructions translated dynamically), and correctness (proven minimal fence placement, translation of real lock structures including lockref’s mixed-size atomics proven for Arm, and the note that the RISC-V model does not currently support mixed-size accesses).