Kavanagh, Ryan and Brookes, Stephen - A Denotational Semantics for SPARC TSO

lmcs:4051 - Logical Methods in Computer Science, May 8, 2019, Volume 15, Issue 2
A Denotational Semantics for SPARC TSO

Authors: Kavanagh, Ryan and Brookes, Stephen

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.


Source : oai:arXiv.org:1711.00931
DOI : 10.23638/LMCS-15(2:10)2019
Volume: Volume 15, Issue 2
Published on: May 8, 2019
Submitted on: November 6, 2017
Keywords: Computer Science - Programming Languages,F.3.2


Share