Robustness between Weak Memory Models

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

7 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 202
EditorsRuzica Piskac, Michael W. Whalen
PublisherTU Wien
ISBN (Electronic)978-3-85448-046-4
Publication statusPublished - 2021
Event21st Conference on Formal Methods in Computer-Aided
Design: FMCAD 2021
- online event
Duration: 18 Oct 202122 Oct 2021
Conference number: 21


Conference21st Conference on Formal Methods in Computer-Aided


  • weak memory model
  • robustness
  • LLVM
  • concurrency


Dive into the research topics of 'Robustness between Weak Memory Models'. Together they form a unique fingerprint.

Cite this