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 TSOArticle

Authors: Ryan Kavanagh ORCID; 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: April 22, 2019
    Submitted on: November 6, 2017
    Keywords: Computer Science - Programming Languages,F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Funder: Natural Sciences and Engineering Research Council of Canada

    1 Document citing this article

    Consultation statistics

    This page has been seen 1276 times.
    This article's PDF has been downloaded 475 times.