Risotto: a dynamic binary translator for weak memory model architectures

Redha Gouicem, Dennis Sprokholt, Jasper Ruehl, Rodrigo Rocha, Tom Spink, Soham Chakraborty, Pramod Bhatotia

Research output: Chapter in Book/Report/Conference proceedingConference contribution

5 Downloads (Pure)

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: First, 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. Second, we implement these verified mappings in Risotto, a QEMU-based DBT system that optimizes memory fence placement while ensuring correctness. Risotto further improves performance via cross-architecture dynamic linking of native shared libraries and faster yet 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.
Original languageEnglish
Title of host publicationProceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1 (ASPLOS 2023)
EditorsTor M. Aamodt, Natalie Enright Jerger, Michael Swift
Place of PublicationNew York, NY
PublisherACM
Pages107–122
Number of pages16
Volume1
ISBN (Electronic)9781450399159
DOIs
Publication statusPublished - 21 Dec 2022
Event28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2023) - Vancouver, Canada
Duration: 25 Mar 202329 Mar 2023
https://asplos-conference.org/

Conference

Conference28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2023)
Abbreviated titleASPLOS'23
Country/TerritoryCanada
CityVancouver
Period25/03/2329/03/23
Internet address

Keywords

  • Binary translation
  • Memory models
  • Formal verification

Fingerprint

Dive into the research topics of 'Risotto: a dynamic binary translator for weak memory model architectures'. Together they form a unique fingerprint.

Cite this