A Denotational Semantics for SPARC TSO
Ryan Kavanagh, Stephen Brookes · Electronic Notes in Theoretical Computer Science · 2018
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.