Summary: | 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. It uses
buffered states and an inductive definition of execution to assign an
input-output meaning to pomsets. We show that our denotational account is sound
and complete relative to the axiomatic account, that is, that it captures
exactly the behaviours permitted by the axiomatic account. Our compositional
approach facilitates the study of SPARC TSO and supports modular analysis of
program behaviour.
|