Chakraborty, S. (2021). Robustness between Weak Memory Models. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 173–182). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_26
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
Conference Series: Formal Methods in Computer-Aided Design
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
Number of Pages:
TU Wien Academic Press
Robustness of a concurrent program ensures that its behaviors on a weak concurrency model are indistinguishable from those on a stronger model. Enforcing robustness is particularly useful when porting or migrating applications between architectures. Existing tools mostly focus on ensuring sequential consistency (SC) robustness which is a stronger condition and may result in unnecessary fences. To address this gap, we analyze and enforce robustness between weak memory models, more specifically for two mainstream architectures: x86 and ARM (versions 7 and 8). We identify robustness conditions and develop analysis techniques that facilitate porting an application between these architectures. To the best of our knowledge, this is the first approach that addresses robustness between the hardware weak memory models. We implement our robustness checking and enforcement procedure as a compiler pass in LLVM and experiment on a number of standard concurrent benchmarks. In almost all cases, our procedure terminates instantaneously and insert significantly less fences than the naive schemes that enforce SC-robustness.