We introduce a denotational semantic framework for shared-memory concurrent programs in a C11-style memory model. This denotational approach is an alternative to techniques based on "execution graphs" and axiomatizations, and it allows for compositional reasoning. Our semantics generalizes from traces (sequences of actions) to pomsets (partial orders of actions): instead of traces and interleaving, we embrace "true" concurrency. We build on techniques from our prior work that gives a denotational semantics to SPARC TSO. We add support for C11's wider range of memory orderings, e.g., acquire-release and relaxed, and support for local variables and various synchronization primitives, while eliminating significant amounts of technical bookkeeping. Our approach features two main components. We first give programs a syntax-directed denotation in terms of sets of pomsets of memory actions. We then give a race-detecting executional interpretation of pomsets using footprints and a local view of state.
In prior work @cite_2 , we give a semantics to the SPARC TSO weak memory model using pomset denotations and executions, and buffered state. The semantics developed in this paper is a significant step forward toward greater generality and wider applicability. Rather than attempt to model out-of-order execution by explicitly modelling buffers, both in pomset generation and in execution, we use the relaxed composition operator and leverage pomset structure. To enforce a total order on writes during execution, TSO executions were parametrized with linearizations of writes. In contrast, C11 executions totally order @math actions via the @math relation, thereby reducing technical overhead.
@cite_2
2964334533
Abstract The SPARC TSO weak memory model is defined axiomatically, with a non-compositional formulation that makes modular reasoning about programs difficult. Our denotational approach uses pomsets to provide a compositional semantics capturing exactly the behaviours permitted by SPARC TSO. Our approach facilitates the study of SPARC TSO and supports modular analysis of program behaviour.