Putting Weak Memory in Order via a Promising Intermediate Representation

Explore an innovative approach to developing an 'in-order' shared-memory concurrency model for languages like C and C++ in this conference talk from PLDI 2023. Delve into the challenges of creating a model that executes instructions following program order while supporting non-atomic accesses and validating compiler optimizations. Learn how the researchers utilize the distinction between a source model and an intermediate representation (IR) model to achieve this goal. Examine the implications for relaxed atomic accesses and the proposed pragmatic approach to address load-store reordering. Gain insights into the mechanized Coq proofs for the correctness of mappings from source to IR and from IR to Armv8. Discover how this work relates an in-order source model to an out-of-order IR model, aiming to create an in-order source semantics without performance overhead for non-atomics.