一句话：形式化 QEMU 中间表示的内存模型，提出经形式验证的强到弱内存映射，并在 Risotto 中高效实现。
动态二进制翻译（DBT）可用于跨架构仿真未修改的二进制程序，但在从强内存一致性架构向弱内存一致性架构仿真并发程序时，会同时面临正确性与性能挑战。作者报告了 QEMU 在 Arm 宿主上仿真 x86 二进制时出现的多个翻译错误。为此，论文提出端到端方案：首先形式化 QEMU 中间表示的内存模型，并据此给出经形式验证的映射方案，以弥合强到弱内存一致性的语义鸿沟；随后在基于 QEMU 的 DBT 系统 Risotto 中实现这些映射，在保证正确性的前提下优化内存栅栏放置，并通过跨架构动态链接原生共享库以及快速且正确的比较并交换（CAS）翻译进一步提升仿真性能。使用多线程基准套件与真实应用评估表明，Risotto 相比存在错误翻译的 QEMU 平均提升 6.7% 的仿真性能，同时保证正确性。
Dynamic Binary Translation (DBT) is a powerful approach to support cross-architecture emulation of unmodified binaries. However, DBT systems face correctness and performance challenges, when emulating concurrent binaries from strong to weak memory consistency architectures. As a matter of fact, we report several translation errors in QEMU, when emulating x86 binaries on Arm hosts. To address these challenges, we propose an end-to-end approach that provides correct and efficient emulation for weak memory model architectures. Our contributions are twofold: we formalize QEMU’s intermediate representation’s memory model, and use it to propose formally verified mapping schemes to bridge the strong-on-weak memory consistency mismatch. Secondly, we implement these verified mappings in Risotto, a QEMU-based DBT system that optimizes memory fence placement while ensuring correctness. Risotto further enhances the emulation performance via cross-architecture dynamic linking of native shared libraries, and fast and correct translation of compare-and-swap operations. We evaluate Risotto using multi-threaded benchmark suites and real-world applications, and show that Risotto improves the emulation performance by 6.7% on average over ”erroneous” QEMU, while ensuring correctness.
@inproceedings{GouicemSRRS0B23,
title = {Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures},
author = {Redha Gouicem and Dennis Sprokholt and Jasper Ruehl and Rodrigo C. O. Rocha and Tom Spink and Soham Chakraborty and Pramod Bhatotia},
booktitle = {ASPLOS},
year = {2022},
doi = {10.1145/3567955.3567962}
}