Ryan Kavanagh ; Stephen Brookes - A Denotational Semantics for SPARC TSO

lmcs:4051 - Logical Methods in Computer Science, May 8, 2019, Volume 15, Issue 2 - https://doi.org/10.23638/LMCS-15(2:10)2019
A Denotational Semantics for SPARC TSO

Authors: Ryan Kavanagh ; Stephen Brookes

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.

Volume: Volume 15, Issue 2
Published on: May 8, 2019
Accepted on: May 8, 2019
Submitted on: November 6, 2017
Keywords: Computer Science - Programming Languages,F.3.2


Consultation statistics

This page has been seen 470 times.
This article's PDF has been downloaded 401 times.