- Minki Cho*, Seoul National University, Korea
- Sung-Hwan Lee*, Seoul National University, Korea
- Dongjae Lee, Seoul National University, Korea
- Chung-Kil Hur, Seoul National University, Korea
- Ori Lahav, Tel Aviv University, Israel
* The first two authors contributed equally to this work.
We formally show that sequential reasoning is adequate and sufficient for
establishing soundness of various compiler optimizations under
weakly consistent shared-memory concurrency.
Concretely, we introduce a sequential model and show that
behavioral refinement in that model entails contextual refinement
in the Promising Semantics model, extended with non-atomic accesses for non-racy code.
This is the first work to achieve such result for a full-fledged model
with a variety of C11-style concurrency features.
Central to our model is the lifting of the common data-race-freedom assumption,
which allows us to validate irrelevant load introduction,
a transformation that is commonly performed by compilers.
As a proof of concept, we develop an optimizer for a toy concurrent language,
and certify it (in Coq) while relying solely on the sequential model.
We believe that the proposed approach provides useful means for compiler developers
and validators, as well as a solid foundation for the development of
certified optimizing compilers for weakly consistent shared-memory concurrency.