Title
Risotto: A Dynamic Binary Translator for Weak Memory Model Architectures
Author
Gouicem, Redha (Technische Universität München)
Sprokholt, D.G. (TU Delft Programming Languages)
Ruehl, Jasper (Technische Universität München)
Rocha, Rodrigo C.O. (University of Edinburgh)
Spink, Tom (University of St Andrews)
Chakraborty, S.S. (TU Delft Programming Languages)
Bhatotia, Pramod (Technische Universität München)
Contributor
Aamodt, Tor M. (editor)
Jerger, Natalie Enright (editor)
Swift, Michael (editor)
Date
2022
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.
Subject
Binary translation
formal verification
memory models
To reference this document use:
http://resolver.tudelft.nl/uuid:2ea32c53-5665-41ca-a6da-43117f917334
DOI
https://doi.org/10.1145/3567955.3567962
Publisher
Association for Computing Machinery (ACM)
Embargo date
2023-07-01
ISBN
978-1-4503-9915-9
Source
ASPLOS 2023 - Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
Event
28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2023, 2023-03-25 → 2023-03-29, Vancouver, Canada
Series
International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
Bibliographical note
Green Open Access added to TU Delft Institutional Repository ‘You share, we take care!’ – 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.
Part of collection
Institutional Repository
Document type
conference paper
Rights
© 2022 Redha Gouicem, D.G. Sprokholt, Jasper Ruehl, Rodrigo C.O. Rocha, Tom Spink, S.S. Chakraborty, Pramod Bhatotia