AtoMig: Automatically Migrating Millions Lines of Code from TSO to WMM.
ASPLOS (2)(2023)
摘要
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.
更多查看译文
关键词
memory consistency models, parallelism and concurrency, static analysis, sustainability
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要