@inproceedings{2ea32c53566541caa6da43117f917334,
title = "Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures",
abstract = "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. ",
keywords = "Binary translation, formal verification, memory models",
author = "Redha Gouicem and Dennis Sprokholt and Jasper Ruehl and Rocha, {Rodrigo C.O.} and Tom Spink and Soham Chakraborty and Pramod Bhatotia",
note = "Green Open Access added to TU Delft Institutional Repository {\textquoteleft}You share, we take care!{\textquoteright} – Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public. ; 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2023 ; Conference date: 25-03-2023 Through 29-03-2023",
year = "2022",
doi = "10.1145/3567955.3567962",
language = "English",
series = "International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS",
publisher = "Association for Computing Machinery (ACM)",
pages = "107--122",
editor = "Aamodt, {Tor M.} and Jerger, {Natalie Enright} and Michael Swift",
booktitle = "ASPLOS 2023 - Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems",
address = "United States",
}