A Denotational Semantics for SPARC TSO

TL;DR

This paper introduces a denotational semantics for the SPARC TSO memory model using pomsets, enabling modular reasoning and precise behavioral capture compared to the traditional axiomatic approach.

Contribution

It presents a novel compositional semantics for SPARC TSO based on pomsets, improving modular analysis and understanding of weak memory behaviors.

Findings

Semantic model is sound and complete relative to axiomatic account

Supports modular analysis of program behaviors

Facilitates reasoning about weak memory models

Abstract

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.