A Denotational Semantics for SPARC TSO
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.