AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

Beitragende

  • Martin Beck - , Dresden Research Lab Huawei Technologies (Autor:in)
  • Koustubha Bhat - , Dresden Research Lab Huawei Technologies (Autor:in)
  • Lazar Stričević - , Dresden Research Lab Huawei Technologies (Autor:in)
  • Geng Chen - , Huawei Technologies Co., Ltd. (Autor:in)
  • Diogo Behrens - , Dresden Research Lab Huawei Technologies (Autor:in)
  • Ming Fu - , Dresden Research Lab Huawei Technologies (Autor:in)
  • Viktor Vafeiadis - , Max Planck Institute for Software Systems (Autor:in)
  • Haibo Chen - , Huawei Technologies Co., Ltd., Shanghai Jiao Tong University (Autor:in)
  • Hermann Härtig - , Seniorprofessor für Betriebssysteme, Technische Universität Dresden (Autor:in)

Abstract

CPUs with weak memory-consistency models (WMMs), such as Arm and RISC-V, are rapidly increasing their market share. Porting legacy x86 applications to such CPUs requires introducing extra synchronization to prevent WMM-related concurrency bugs - -a task often left to human experts. Given the rarity of such experts and the enormous size of legacy applications, we develop AtoMig, an effective, fully automated tool for porting large, real-world applications to WMM CPU architectures. AtoMig detects shared memory access patterns with novel static analysis strategies and performs program transformations to properly protect them from WMM effects. In the absence of sufficiently scalable verification methods, AtoMig shows practicality of focusing on code patterns more prone to WMM faults, trading off completeness for scalability. We validate the correctness of AtoMig's transformations on several small concurrent benchmarks via model checking. We demonstrate the scalability and performance of our approach by applying AtoMig to popular real-world large code bases with up to millions of lines of code, viz., MariaDB, Postgres, SQlite, LevelDB, and Memcached. As part of this work, we also found a WMM bug in MariaDB, which AtoMig fixes automatically.

Details

OriginalspracheEnglisch
TitelASPLOS 2023 - Proceedings of the 28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems
Redakteure/-innenTor M. Aamodt, Natalie Enright Jerger, Michael Swift
Herausgeber (Verlag)Association for Computing Machinery
Seiten61-73
Seitenumfang13
ISBN (elektronisch)9781450399166
PublikationsstatusVeröffentlicht - 27 Jan. 2023
Peer-Review-StatusJa

Publikationsreihe

ReiheASPLOS: Architectural Support for Programming Languages and Operating Systems
Band2

Konferenz

Titel28th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2023
Dauer25 - 29 März 2023
StadtVancouver
LandKanada

Schlagworte

Schlagwörter

  • memory consistency models, parallelism and concurrency, static analysis, sustainability