Abstract
We investigate the problem of developing an "in-order" shared-memory
concurrency model for languages like C and C++, which executes instructions
following their program order, and is thus more amenable to reasoning and
verification compared to recent complex proposals with out-of-order
execution. We demonstrate that it is possible to fully support non-atomic
accesses in an in-order model in a way that validates all compiler
optimizations that are performed in single-threaded code (including
irrelevant load introduction). The key to doing so is to utilize the
distinction between a source model (with catch-fire semantics) and an
intermediate representation (IR) model (with undefined value for racy reads)
and formally establish the soundness of mapping from source to IR. As for
relaxed atomic accesses, an in-order model must forbid load-store
reordering. We discuss the rather limited performance impact of this fact
and present a pragmatic approach to this problem, which, in the long term,
requires a new kind of hardware store instructions for implementing relaxed
stores. The source and IR semantics proposed in this paper are based on
recent versions of the promising semantics, and the correctness proofs of
the mappings from the source to the IR and from the IR to Armv8 are
mechanized in Coq. This work is the first to formally relate an in-order
source model and an out-of-order IR model with the goal of having an
in-order source semantics without any performance overhead for non-atomics.