一句话：提出 Arancini 混合二进制翻译器，借统一 IR 与形式验证的强到弱内存映射，为弱内存架构实现正确、完整且高效的跨架构仿真。
跨架构二进制翻译在异构计算中日益重要，但强内存模型（如 x86-64）到弱内存模型（Arm/RISC-V）的并发程序翻译存在正确性风险；静态翻译完整性不足，动态翻译性能受限。作者提出 Arancini 混合二进制翻译器，核心包括统一静态与动态翻译的 ArancinIR、形式化 ArancinIR 内存模型、形式验证 x86-64 到 Arm/RISC-V 的强到弱映射方案，并实现完整高效的翻译器。评估使用多线程基准与 Arm/RISC-V 后端，表明其比 QEMU 系翻译器最高快 5 倍，同时保证正确性与完整性。该工作是首个由形式证明指导、确保强内存客户机在弱内存宿主上正确执行的混合翻译器，也是首个处理 Arm 混合大小访问的翻译器。
Binary translation is a powerful approach to support cross-architecture emulation of unmodified binaries in increasingly heterogeneous computing environments. However, binary translation systems face correctness issues, due to the strong-on-weak memory model mismatch (e.g., from x86-64 to Arm/RISC-V) for concurrent programs. Besides, the current landscape of binary translation systems is fundamentally limited in terms of completeness for static systems and performance for dynamic ones. To address these limitations, we propose Arancini, a hybrid binary translator system designed and implemented from the ground up that strives for correct, complete, and efficient emulation for weak memory model architectures. Our system makes three foundational contributions to achieve these design goals: ArancinIR, a unified intermediate representation for static and dynamic binary translators; a formalization of ArancinIR,'s memory model and formally verified mapping schemes from x86-6 to Arm and RISC-V, to ensure strong-on-weak correctness; and Arancini, a complete and performant hybrid binary translator, implementing the verified mapping schemes for correctness. We evaluate Arancini using a multi-threaded benchmark suite with two backends (Arm and RISC-V), and show that Arancini can be up to 5× faster than QEMU--based translators while ensuring correctness and completeness. To our knowledge, Arancini is the first hybrid binary translator whose implementation is guided by formal proofs, to ensure correct execution of strong memory guests on weak memory hosts. It is also the first translator to address mixed-sized accesses for Arm targets.
@inproceedings{ReimersS0AKRSG026,
title = {Arancini: A Hybrid Binary Translator for Weak Memory Model Architectures},
author = {Sebastian Reimers and Dennis Sprokholt and Martin Fink and Theofilos Augoustis and Simon Kammermeier and Rodrigo C. O. Rocha and Tom Spink and Redha Gouicem and Soham Chakraborty and Pramod Bhatotia},
booktitle = {ASPLOS},
year = {2026},
doi = {10.1145/3779212.3790127}
}