A Denotational Semantics for SPARC TSO

Ryan Kavanagh and Stephen Brookes A Denotational Semantics for SPARC TSO Electronic Notes in Theoretical Computer Science 336 April 16, 2018 The Thirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII) 223-239 1571-0661 10.1016/j.entcs.2018.03.025
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.