15210 LABEL:LastPageNov. 06, 2017May 08, 2019 [Theory of computation]:
Denotational semantics; Concurrency

# A Denotational Semantics for SPARC TSO

Ryan Kavanagh  and  Stephen Brookes  Computer Science Department
Carnegie Mellon University
Pittsburgh, PA, USA  {rkavanagh<EMAIL_ADDRESS>
###### 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.

###### Key words and phrases:

SPARC TSO, denotational semantics, pomsets, concurrency, weak memory models.

Funded in part by a Natural Sciences and Engineering Research Council of
Canada (NSERC) Postgraduate Scholarship.

##  1\. Introduction

A memory model specifies what values can be read by a thread from a given
memory location during execution. Traditional concurrency research has assumed
sequential consistency, wherein memory actions operate atomically on a global
state, and a read is guaranteed to observe the value most recently written to
that location globally. Consequently, “the result of any execution is the same
as if the operations of all the processors were executed in some sequential
order” [Lam79]. However, sequential consistency negatively impacts
performance, and modern architectures often provide much weaker guarantees.
These weaker guarantees mean that classical concurrency algorithms, which
often assume sequential consistency, can behave in unexpected ways. Consider,
for example, the Dekker algorithm on a system using the SPARC instruction set.
The Dekker algorithm seeks to ensure that at most one process enters a
critical section at a time. Executing the following instance of the Dekker
algorithm on a sequentially consistent system from an initial state where
memory locations $w$, $x$, $y$, $z$ are all zero will ensure that we end in a
state where not both $z$ and $w$ are set to one:

$(x:=1;\mathbf{if}\ y=0\ \mathbf{then}\ z:=1\ \mathbf{else}\
\mathbf{skip})\operatorname{{\|}}(y:=1;\mathbf{if}\ x=0\ \mathbf{then}\ w:=1\
\mathbf{else}\ \mathbf{skip}).$

However, the SPARC ISA provides the weaker SPARC TSO (total store ordering)
memory model. Under SPARC TSO, it is possible to start from the aforementioned
initial state and end in a state where both $z$ and $w$ are set to one, thus
violating mutual exclusion.

Weak memory models are often described in standards documents using natural
language. This informality makes it difficult to reason about how programs
will behave on systems that use these memory models. The SPARC Architecture
Manual [SPA92] gives an axiomatic description of TSO using partial orders of
actions. We present this description in Section 2; other axiomatic approaches
are discussed in Section 5. Despite their formality, it is hard to use
axiomatic accounts to reason about the behaviour of programs. This is because
the axiomatic approach is non-compositional and precludes modular reasoning.
We address this problem by presenting a denotational semantics for SPARC TSO
in Section 3. Our denotational semantics assigns to each program a collection
of pomsets. Pomsets are generalizations of traces and were first used by Pratt
[Pra86] to give denotational semantics for concurrency, and later by Brookes
[Bro16a], with some modifications, to study weak memory models. We illustrate
our semantics by validating various litmus tests and expected program
equivalences. To ensure our denotational semantics accurately captures the
behaviour of SPARC TSO, we show in Section 4 that from every denotation of a
program we can derive a collection of partial orders satisfying the axiomatic
description of Section 2 and, moreover, that we can derive every such partial
order from the denotation.

##  2\. An Axiomatic Account

The SPARC manual [SPA92] gives an axiomatic description of TSO in terms of
partial orders of actions. Unfortunately, this description is incomplete
because it fails to specify the fork and join behaviour of TSO. In this
section, we complete the SPARC manual’s account of TSO with an account of
forking and joining. Before doing so, we give an informal description of TSO
to help build intuition.

A system providing the TSO weak memory model can be thought of as a collection
of processors, each with a write buffer. Whenever a processor performs a
write, it places it in its write buffer. The buffer behaves as a queue, and
writes migrate out of the buffers one at a time, and shared memory applies
them according to a global total order. Whenever a processor tries to read a
location, it first checks its buffer for a write to that location. If it finds
one, it uses the value of the most recent such write; otherwise, it looks to
shared memory for a value. Because of buffering, it is possible for writes and
reads to be observed out of order relative to the program order.

###  2.1. Program Order Pomsets

To make the above intuition precise, we must formalize the notion of a program
order, i.e., the ordering of read and write actions specified by a program. We
do so by means of partially-ordered multisets.

A (strict) partially-ordered multiset or pomset $(P,<,\Phi)$ over a label set
$L$ consists of a strict poset $(P,<)$ of “action occurrences” and a function
$\Phi:P\to L$ mapping each action occurrence to its label or “action”.

We frequently write just $P$ for $(P,<,\Phi)$, in which case we let $<_{P}$
and $\Phi_{P}$ denote its obvious components. Denote by $\mathrm{Pom}(L)$ the
set of pomsets over $L$. We remark that pomsets are a natural generalization
of traces. Indeed, all traces are simply pomsets where the underlying order is
total.

We do not usually make the poset $P$ explicit, because the structure of the
pomset is invariant under relabellings of the elements of $P$. Consequently,
we identify pomsets $(P,<,\Phi)$ and $(P^{\prime},<^{\prime},\Phi^{\prime})$
if there exists an order isomorphism $\phi:P\to P^{\prime}$ such that
$\Phi=\Phi^{\prime}\circ\phi$. We usually denote the elements of the pomset
using just their labels, but we sometimes need to specify their exact
occurrence, in which case we write $l_{p}$, where $l=\Phi(p)$.

It is useful to draw a pomset $P$ as a labelled directed acyclic graph, where
multiple vertices can have the same label and we have an edge $a\to b$ if
$a<_{P}b$. For clarity, we always omit edges obtained by transitivity of
$<_{P}$. For example, the following graph depicts the pomset where
$P=\\{0,1,2,3\\}$, the order is given by $0<1$, $1<2$, $0<2$, and $0<3$, and
$\Phi$ is given by $\Phi(0)=a$, $\Phi(1)=b$, $\Phi(2)=a$, and $\Phi(3)=c$:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
5.16377pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{c}$}}}}}}}{\hbox{\kern 29.16377pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
5.16379pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
64.44966pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
64.44966pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{b\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
98.74132pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
98.74132pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{a}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

We assume a countably infinite set of locations $\mathrm{Loc}$, ranged over by
metavariables $x,y,z,\dotsc$, and a set of values $V$, ranged over by $v$. In
our examples, we will take $V$ to be the set of integers. We call $x:=v$ a
global write action, $x=v$ a read action, and $\delta$ a skip action. Let
${\mathcal{A}_{w}}$ and ${\mathcal{A}_{r}}$ be the sets of global write
actions and read actions, respectively.

A program order is a pomset $P$ over the set
${\mathcal{A}_{PO}}={\mathcal{A}_{w}}\cup{\mathcal{A}_{r}}\cup\\{\delta\\}$ of
action labels that satisfies the (locally) finite height property, that is,
such that for all $b\in P$, the set $\\{a\in P\mid a<_{P}b\\}$ is finite.

Informally, the finite height property guarantees that all actions in $P$ can
be executed after finitely many other actions, i.e., that the program order
contains no unreachable actions.

Intuitively, the program order

$\textstyle{x:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y=1}$$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y=1}$

describes the parallel execution of writing 2 to $x$ before reading 1 from
$y$, and writing 1 to $y$ before reading 1 from $y$, with no other ordering
constraints.

###  2.2. TSO Axioms

We now turn our attention to our completed version of the axiomatic account
given in the SPARC manual. To do so, we first introduce the notion of state
and the requisite notation.

A global state is a finite partial function from locations $\mathrm{Loc}$ to
values $V$. We let $\Sigma_{PO}=\mathrm{Loc}\rightharpoonup_{fin}V$ be the set
of global states, and use $\sigma$ to range over $\Sigma_{PO}$.

Given any set $S$ and partial order $<_{S}$ on it, every element $s\in S$
determines a set $s{\downarrow}_{S}=\\{s^{\prime}\in S\mid
s^{\prime}<_{S}s\\}\cup\\{s\\}$ called its lower closure. Write
$s\mathrel{\operatorname{{\|}}}_{S}s^{\prime}$ to denote that $s$ and
$s^{\prime}$ are not comparable under the reflexive closure $\leq_{S}$ of
$<_{S}$, and write $s\mathrel{{\leq}{\geq}}_{S}s^{\prime}$ to denote that they
are comparable.

Let $P$ be a program order and $<_{T}$ be a strict partial order on the
elements of $P$. We say $<_{T}$ is TSO-consistent with $P$ from (the initial
state) $\sigma$ if it satisfies the following six axioms:

(O):

Ordering: $<_{T}$ totally orders the write actions ${\mathcal{A}_{w}}$ of $P$.

(V):

Value: for all reads ${(x=v)}_{r}$ in $P$, either

(a):

there exists a write ${(x:=v^{\prime})}_{w}$ maximal under $<_{T}$ amongst all
writes to $x$ in ${(x=v)}_{r}{\downarrow}_{T}$, all writes to $x$ in
${(x=v)}_{r}{\downarrow}_{P}$ are in ${(x:=v^{\prime})}_{w}{\downarrow}_{T}$,
and $v=v^{\prime}$; or

(b):

there exists a write ${(x:=v^{\prime})}_{w}$ maximal under $<_{P}$ amongst all
writes to $x$ in ${(x=v)}_{r}{\downarrow}_{P}$, and both
${(x=v)}_{r}<_{T}{(x:=v^{\prime})}_{w}$ and $v=v^{\prime}$; or

(c):

there are no writes to $x$ in ${(x=v)}_{r}{\downarrow}_{T}$ or
${(x=v)}_{r}{\downarrow}_{P}$, and $\sigma(x)=v$.

(L):

LoadOp: for all reads $r\in P$ and all actions $a\in P$, $r<_{P}a$ implies
$r<_{T}a$.

(S):

StoreStore: for all writes $w,w^{\prime}\in P$, $w<_{P}w^{\prime}$ implies
$w<_{T}w^{\prime}$.

(F):

Fork: if $\alpha_{1}<_{P}\alpha_{2}$, $\alpha_{1}<_{P}\alpha_{3}$, and
$\alpha_{2}\mathrel{\operatorname{{\|}}}_{P}\alpha_{3}$, then
$\alpha_{1}<_{T}\alpha_{2}$ and $\alpha_{1}<_{T}\alpha_{3}$.

(J):

Join: if $\alpha_{1}<_{P}\alpha_{3}$, $\alpha_{2}<_{P}\alpha_{3}$, and
$\alpha_{1}\mathrel{\operatorname{{\|}}}_{P}\alpha_{2}$, then
$\alpha_{1}<_{T}\alpha_{3}$ and $\alpha_{2}<_{T}\alpha_{3}$.

The fork axiom is easily understood by: if
$\alpha_{1}\leftarrow\alpha_{1}\rightarrow\alpha_{3}$ in $P$, then
$\alpha_{2}\leftarrow\alpha_{1}\rightarrow\alpha_{3}$ or
$\alpha_{1}\rightarrow\alpha_{2}\rightarrow\alpha_{3}$ in $(P,{<_{T}})$; the
join axiom is symmetric. We simply say $<_{T}$ is TSO-consistent with $P$ if
there exists some initial state $\sigma$ from which they are TSO-consistent.
It will be useful to identify $<_{T}$ and the pomset $T=(P,<_{T},\Phi_{P})$. ∎

Axioms (O), (Va), (Vb), (L), and (S) are directly adapted from the formal
specification given in Appendix K.2 of [SPA92]. We introduce axiom (Vc) to
simplify our presentation of examples. By requiring that programs first write
to any locations from which they read, it can be omitted, and apart from
examples, we will assume throughout that our TSO-consistent orders do not
require (Vc). Though the formal specification does not provide axioms (F) and
(J), they are consistent with the behaviour intended by Appendix J.6 of
[SPA92]. Intuitively, axiom (Vb) requires that whenever a processor reads from
a location, it must use the most recent write to that location in its write
buffer (if it exists). If there is no such write in its write buffer, but we
have observed a global write to that location, then (Va) requires that the
most recent such write be the one read. Our presentation differs slightly from
the formal specification. In particular, we do not consider instruction
fetches or atomic load-store operations, and we do not consider flush actions,
because they can be implemented as a derived action in our semantics by
forking and immediately joining. To be consistent with our pomset development,
we also assume the order to be strict.

As the following proposition’s corollary shows, if $<_{T}$ is TSO-consistent
for $P$, then there exists a (not necessarily unique) total order on $P$ that
is TSO-consistent with $P$ and contains $<_{T}$. As a result, we can view all
orders that are TSO-consistent with $P$ as weakenings of total orders that are
TSO-consistent with $P$. The proposition follows by a straightforward check of
the axioms, where (V) is the only axiom that is not immediate.

######  Proposition 1.

Let $<_{T}$ be TSO-consistent for $P$ and $a,b\in P$ be two actions such that
$a\mathrel{\operatorname{{\|}}}_{T}$ b. Let $<_{ab}$ be the transitive closure
of ${<_{T}}\cup\\{(a,b)\\}$. If there exist maximum writes under $a$ and $b$
relative to $\leq_{T}$, call them $\mu_{a}$ and $\mu_{b}$, respectively. If
either $\mu_{a}$ and $\mu_{b}$ exist and $\mu_{a}<_{T}\mu_{b}$, or $\mu_{a}$
does not exist, then $<_{ab}$ is TSO-consistent for $P$. ∎

######  Corollary 2.

If $P$ is a finite program order pomset and $<_{T}$ a partial order TSO-
consistent with $P$, then there exists a total order $\sqsubset_{T}$ TSO-
consistent with $P$ such that ${<_{T}}\subseteq{\sqsubset_{T}}$. ∎

Despite Corollary 2, one should be careful not to conflate the notion of
linearisation with that of TSO-consistent total orders. Consider, for example,
the program order

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
40.41315pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
40.41315pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{x=2}$}}}}}}}{\hbox{\kern 94.46164pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
151.28793pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
151.28793pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=3}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

The linearisation ${x:=2}<{x:=3}<{x=3}<{x=2}$ is not TSO-consistent with the
program order because it violates (Va); the order ${x=2}<{x:=2}<{x=3}<{x:=3}$
is not a linearisation of the program order but is TSO-consistent with it.

When we have a write followed by a read in the program order, but swapped in
the linear order, as in this example, we can imagine the write having gotten
stuck in the write buffer, and observing the read before the write.

##  3\. A Denotational Account

So far we have dealt with program orders in the abstract. To make the rest of
our development more concrete, we restrict our attention to program orders for
well-defined programs in the simple imperative language given below. These
program orders are defined in Section 3.2.

Restricting our attention to program orders of these well-defined programs
raises the question of compositionality. The key is to find a way to derive
TSO-consistent orders for a sequential composition $c_{1};c_{2}$ or parallel
composition $c_{1}\operatorname{{\|}}c_{2}$ given TSO-consistent orders for
$c_{1}$ and $c_{2}$. This is infeasible with the axiomatic approach, which
requires reasoning about whole programs and is inherently non-compositional.
In contrast, a denotational approach using pomsets is compositional: it allows
us to derive the meaning of a program vis-à-vis a weak memory model from the
meanings of its parts vis-à-vis the memory model.

Our denotational semantics has two components. The first associates to each
program a set of TSO pomsets, which serves as the abstract meaning or
denotation of the program. This component is described in Section 3.3. The
second associates to each pomset a set of executions, which describe its
input-output behaviours. This is described in Section 3.4.2.

###  3.1. A Simple Imperative Language

We express our programs using a simple imperative language. This formalism
avoids the complexity of high-level languages, while still capturing the
programs we are interested in. In the syntax below, $e$ ranges over integer
expressions, $b$ over boolean expressions, $c$ over commands, and $p$ over
programs. We distinguish between commands and programs, because although
commands can be composed to form new commands, programs are assumed to be
syntactically complete and executable. This distinction will be useful later
when we consider executions, where we will assume programs are executed from
initial states with empty buffers, but impose no such constraint on executions
for commands.

$\displaystyle v$ $\displaystyle::=\dotsc,-2,-1,0,1,2,\dotsc$ $\displaystyle
e$ $\displaystyle::=v\mid x\mid e_{1}+e_{2}\mid e_{1}*e_{2}\mid\cdots$
$\displaystyle b$ $\displaystyle::=\mathit{true}\mid\mathit{false}\mid\neg
b\mid e_{1}=e_{2}\mid e_{1}<e_{2}\mid b_{1}\vee b_{2}\mid b_{1}\land
b_{2}\mid\cdots$ $\displaystyle c$ $\displaystyle::=\mathbf{skip}\mid x:=e\mid
c_{1};c_{2}\mid c_{1}\operatorname{{\|}}c_{2}\mid\mathbf{if}\ b\
\mathbf{then}\ c_{1}\ \mathbf{else}\ c_{2}\mid\mathbf{while}\ b\ \mathbf{do}\
c$ $\displaystyle p$ $\displaystyle::=c$

Let $\mathsf{VExp}$ denote the set of integer expressions, $\mathsf{BExp}$ the
set of boolean expressions, and $\mathsf{Cmd}$ the set of commands.

###  3.2. PO Pomsets

Given a command $c$ in our language, we must now compile it down to its set
${\mathcal{P}_{PO}}(c)$ of program order pomsets. We need operations for the
sequential and parallel composition of pomsets over the same set of labels.
When defining compositions of pomsets, we assume without loss of generality
that the underlying posets are disjoint.

The sequential composition $(P_{0},{<_{0}},\Phi_{0});(P_{1},{<_{1}},\Phi_{1})$
is $(P_{0},{<_{0}},\Phi_{0})$ whenever $P_{0}$ is infinite, and otherwise it
is $({P_{0}}\cup{P_{1}},{<_{0}}\cup{<_{1}}\cup P_{0}\times
P_{1},\Phi_{0}\cup\Phi_{1})$. The parallel composition
$(P_{0},{<_{0}},\Phi_{0})\operatorname{{\|}}(P_{1},{<_{1}},\Phi_{1})$ of
pomsets is $(P_{0}\cup P_{1},{<_{0}}\cup{<_{1}},\Phi_{0}\cup\Phi_{1})$. The
empty pomset $\mathbf{0}=(\emptyset,\emptyset,\emptyset)$ is the unit for
sequential and parallel composition. Given a pomset $P$ on a set of labels $L$
and a subset $L^{\prime}\subseteq L$, the restriction
$P{\restriction}_{L^{\prime}}$ of $P$ to $L^{\prime}$ is the pomset on
$\Phi^{-1}(L^{\prime})$ whose ordering is induced by $P$. The deletion of
$L^{\prime}$ from $P$ is $P{\restriction}_{L\setminus L^{\prime}}$. We lift
these operations to sets of pomsets in the obvious manner, e.g.,
$S_{1};S_{2}=\\{P_{1};P_{2}\mid P_{i}\in S_{i}\\}$. ∎

Because the skip action $\delta$ has no effects, we identify program orders
$P$ and $P^{\prime}$ whenever there exists a non-empty pomset $P_{\delta}$
that can be obtained in two ways: by deleting a finite number of $\delta$
actions from $P$ and also by deleting a finite number of $\delta$ actions from
$P^{\prime}$. This means, e.g., that we identify $\\{\delta\\};P$,
$\\{\delta\\}\operatorname{{\|}}P$, and $P$ whenever $P\neq\mathbf{0}$, but
$\\{\delta\\};\mathbf{0}=\\{\delta\\}\neq\mathbf{0}$.

We begin with the program order denotation of expressions. To each expression
$e$, we assign a set ${\mathcal{P}_{PO}}(e)$ of tuples of program orders and
corresponding values:

$\displaystyle{\mathcal{P}_{PO}}$
$\displaystyle:\mathsf{VExp}\to\wp(\mathrm{Pom}({\mathcal{A}_{PO}})\times V)$
$\displaystyle{\mathcal{P}_{PO}}(v)$ $\displaystyle=\\{(\\{\delta\\},v)\\}$
$\displaystyle{\mathcal{P}_{PO}}(x)$ $\displaystyle=\\{(\\{x=v\\},v)\mid v\in
V\\}$ $\displaystyle{\mathcal{P}_{PO}}(e_{1}\odot e_{2})$
$\displaystyle=\\{(P_{1}\operatorname{{\|}}P_{2},v_{1}\odot
v_{2})\mid(P_{i},v_{i})\in{\mathcal{P}_{PO}}(e_{i})\\}$

where $\odot$ ranges over binary operations. Read expressions $x$ are
associated with arbitrary values in $V$ for reasons of compositionality: we do
not know with which writes the read may eventually be composed, and so we need
to permit reading arbitrary values. We chose to evaluate binary operations
$e_{1}\odot e_{2}$ in parallel; one could just as legitimately have chosen to
sequentialise the evaluation and written $P_{1};P_{2}$. We assume $v_{1}\odot
v_{2}\in V$ to be the result of applying the binary operation $\odot$ to
$v_{1}$ and $v_{2}$. We handle program orders for unary expressions
analogously, and assume $\neg b^{\prime}$ is the result of negating the
boolean value $b^{\prime}$. To simplify the clauses involving conditionals, we
give helper functions $\mathcal{P}_{\mathit{true}}(b)$ and
$\mathcal{P}_{\mathit{false}}(b)$ to extract the pomsets corresponding to the
given boolean values from ${\mathcal{P}_{PO}}(b)$.

$\displaystyle{\mathcal{P}_{PO}}$
$\displaystyle:\mathsf{BExp}\to\wp(\mathrm{Pom}({\mathcal{A}_{PO}})\times\mathrm{Bool})$
$\displaystyle{\mathcal{P}_{PO}}(b)$
$\displaystyle=\\{(\\{\delta\\},b)\\}\qquad(b\in\\{\mathit{true},\mathit{false}\\})$
$\displaystyle{\mathcal{P}_{PO}}(\neg b)$ $\displaystyle=\\{(P,\neg
b^{\prime})\mid(P,b^{\prime})\in{\mathcal{P}_{PO}}(e)\\}$
$\displaystyle{\mathcal{P}_{PO}}(e_{1}\odot e_{2})$
$\displaystyle=\\{(P_{1}\operatorname{{\|}}P_{2},v_{1}\odot
v_{2})\mid(P_{i},v_{i})\in{\mathcal{P}_{PO}}(e_{i})\\}$
$\displaystyle\mathcal{P}_{\mathit{true}}(b)$
$\displaystyle=\\{P\mid(P,\mathit{true})\in{\mathcal{P}_{PO}}(b)\\}$
$\displaystyle\mathcal{P}_{\mathit{false}}(b)$
$\displaystyle=\\{P\mid(P,\mathit{false})\in{\mathcal{P}_{PO}}(b)\\}$

Note that in the case of boolean binary operations, the $e_{i}$ might be
integer or boolean expressions, and the corresponding semantic clause for
${\mathcal{P}_{PO}}(e_{i})$ should be used.

We give the program order denotation of commands in a similar manner, this
time associating sets of program orders to each command phrase:

$\displaystyle{\mathcal{P}_{PO}}$
$\displaystyle:\mathsf{Cmd}\to\wp(\mathrm{Pom}({\mathcal{A}_{PO}}))$
$\displaystyle{\mathcal{P}_{PO}}(\mathbf{skip})$
$\displaystyle=\\{\\{\delta\\}\\}$ $\displaystyle{\mathcal{P}_{PO}}(x:=e)$
$\displaystyle=\\{P;\\{x:=v\\}\mid(P,v)\in{\mathcal{P}_{PO}}(e)\\}$
$\displaystyle{\mathcal{P}_{PO}}(c_{1};c_{2})$
$\displaystyle={\mathcal{P}_{PO}}(c_{1});{\mathcal{P}_{PO}}(c_{2})$
$\displaystyle{\mathcal{P}_{PO}}(c_{1}\operatorname{{\|}}c_{2})$
$\displaystyle={\mathcal{P}_{PO}}(c_{1})\operatorname{{\|}}{\mathcal{P}_{PO}}(c_{2})$
$\displaystyle{\mathcal{P}_{PO}}(\mathbf{if}\ b\ \mathbf{then}\ c_{1}\
\mathbf{else}\ c_{2})$
$\displaystyle=\mathcal{P}_{\mathit{true}}(b);{\mathcal{P}_{PO}}(c_{1})\cup\mathcal{P}_{\mathit{false}}(b);{\mathcal{P}_{PO}}(c_{2})$
$\displaystyle{\mathcal{P}_{PO}}(\mathbf{while}\ b\ \mathbf{do}\ c)$
$\displaystyle=\bigcup_{n=0}^{\infty}I^{n}(b,c)\cup I^{\omega}(b,c),$

where $I^{0}(b,c)=\mathcal{P}_{\mathit{false}}(b)$ and
$I^{n+1}(b,c)=\mathcal{P}_{\mathit{true}}(b);{\mathcal{P}_{PO}}(c);I^{n}(b,c)$.

The only interesting clause is for $\mathbf{while}\ b\ \mathbf{do}\ c$. Here,
we take union of all of the finite unrollings $I^{n}(b,c)$ of the loop. We
must also consider the case of an infinite loop. This is captured by
$I^{\omega}(b,c)$, which describes the infinite pomset obtained by unrolling
the loop countably infinitely many times. The $\mathbf{while}\ b\ \mathbf{do}\
c$ clause also illustrates why we associate the pomset $\\{\delta\\}$ instead
of $\mathbf{0}$ to values: otherwise, we would have
${\mathcal{P}_{PO}}(\mathbf{while}\ \mathit{false}\ \mathbf{do}\
c)=\\{\mathbf{0}\\}$, and this would break our intuition that this program
should be denotationally equivalent to $\mathbf{skip}$. It would also have no
executions under the formal account of Section 3.4.

To illustrate the above semantic clauses, we return to the Dekker program from
the introduction. This program has pomsets of each of the following forms, for
each choice of $v\neq 0$ and $v^{\prime}\neq 0$:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-13.94443pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.49644pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-13.94443pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
22.65851pt\raise-23.38887pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{z:=1}$}}}}}}}{\hbox{\kern
20.41312pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w:=1}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-16.08333pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.49644pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-13.94443pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=v}$}}}}}}}{\hbox{\kern
22.65851pt\raise-23.38887pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern
20.41312pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w:=1}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-13.94443pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
20.41312pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
36.59943pt\raise-16.08333pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.47218pt\raise-23.38887pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=v}$}}}}}}}{\hbox{\kern-16.10066pt\raise-45.80551pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{z:=1}$}}}}}}}{\hbox{\kern
33.59943pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-15.79166pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
20.41312pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
36.59943pt\raise-14.2361pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=v}$}}}}}}}{\hbox{\kern
20.70218pt\raise-23.0972pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=v^{\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

The first program order describes an execution where we read both $y=0$ and
$x=0$ and where Dekker fails. The next three forms of program order describe
executions in which one or both reads obtain a non-zero value.

###  3.3. TSO Pomsets

In this subsection, we assign a set $\mathcal{P}_{TSO}(p)$ of TSO pomsets to
each program $p$, serving as the abstract meaning or denotation of the program
$p$ under the TSO memory model. To do so, we will need to carefully model
write buffers. For compactness, we will write $\mathcal{P}$ instead of
$\mathcal{P}_{TSO}$ in this section’s semantic clauses.

We introduce a set $\mathrm{BLoc}=\\{\bar{x}\mid x\in\mathrm{Loc}\\}$ of
buffer locations, assumed to be in bijection with $\mathrm{Loc}$, and let the
set of buffer write actions be
${\mathcal{A}_{b}}=\\{{\bar{x}}~{}:=~{}v\mid{\bar{x}}~{}\in~{}\mathrm{BLoc},\
v~{}\in~{}V\\}$. An action ${\bar{x}}~{}:=~{}v$ by a thread denotes adding a
write $x~{}:=~{}v$ to the thread’s write buffer. The set of TSO actions
${\mathcal{A}_{TSO}}$ then consists of ${\mathcal{A}_{PO}}$ extended with
${\mathcal{A}_{b}}$. A TSO pomset will then be a pomset in
$\mathrm{Pom}({\mathcal{A}_{TSO}})$ satisfying the finite height property.

To capture the effects of buffers, we parametrize our semantic clauses with
lists of global write actions, which represent the writes currently in our
buffer. We let $\mathsf{Ls}={\mathcal{A}_{w}}~{}\mathsf{list}$ be the set of
all lists. The intuition is that write buffers behave as queues under TSO, and
we can use a list $L\in\mathsf{Ls}$ to model a queue by dequeuing from the
head of the list and enqueuing at the end of the list. For expository
convenience, we identify lists and linear pomsets, where we say a pomset is
linear if its underlying poset is linear. Explicitly, we identify ${{[\,\,]}}$
with the empty pomset $\mathbf{0}$, and
${[\,\lambda_{1},\dotsc,\lambda_{n}\,]}$ with the pomset
$\\{\lambda_{1}\\};\cdots;\\{\lambda_{n}\\}$. To minimize notation, we
leverage this identification and write $L;L^{\prime}$ to denote the
concatenation of $L$ and $L^{\prime}$.

The semantic clauses are given in two strata. The semantic clauses
$\mathcal{B}$ for “basic TSO pomsets” capture the meaning of the syntactic
phrases in a manner very similar to the program order definitions in Section
3.2. $\mathcal{B}$ assign to each command phrase a function from buffer lists
to a set of pairs of TSO pomsets and buffer lists. We present these clauses
using the abbreviation $\mathcal{B}_{L}(c)=\mathcal{B}(c)(L)$. The pomset
component of $\mathcal{B}_{L}(c)$ captures the meaning of the phrase in the
presence of the buffer $L$, while the buffer component describes the state of
the buffer after performing the actions associated with the phrase. In the
second stratum, we use $\mathcal{P}$ clauses to capture the meaning of the
phrase in the presence of buffer flushing. Flushing a write from a buffer $L$
consists of dequeuing a global write $x:=v$ from $L$ and inserting it in the
pomset. $\mathcal{P}_{L}(c)=\mathcal{P}(c)(L)$ is again a subset of
$\mathrm{Pom}({\mathcal{A}_{TSO}})\times\mathsf{Ls}$.

To generate TSO pomsets, we modify the semantic clauses generating program
orders in four key places to get our basic pomsets. The first is for write
commands $x:=e$. Starting from a buffer $L\in\mathsf{Ls}$, we get the pomset
$P$ and associated value $v$ for $e$ from the denotation $\mathcal{P}_{L}(e)$
instead of ${\mathcal{P}_{PO}}(e)$. The buffer $L$ may have changed to a
buffer $L^{\prime}$ while we were evaluating $e$, and $\mathcal{P}_{L}(e)$
also gives us this $L^{\prime}$. Instead of immediately making a global write
to $x$ as we would have in the program order clause, we enqueue the global
write on the buffer $L^{\prime}$:

$\mathcal{B}_{L}(x:=e)=\\{(P;\\{\bar{x}:=v\\},L^{\prime};\\{x:=v\\})\mid(P,v,L^{\prime})\in\mathcal{P}_{L}(e)\\}.$

We must also change the semantic clauses for read expressions. By axiom (Vb),
whenever we read from a location $x$, we must use the most recent value
available for it in the write buffer, if available. We use the following
helper function to convert a buffer $L\in\mathsf{Ls}$ to a partial function
$\beta_{L}:\mathrm{Loc}\rightharpoonup_{fin}V$ giving us the value of the most
recent write in $L$ to a given location:

$\displaystyle\beta_{{{[\,\,]}}}(x)$ $\displaystyle=\mathit{undefined,}$
$\displaystyle\beta_{L;\\{x:=v\\}}(y)$ $\displaystyle=\begin{cases}v&\text{if
}x=y\\\ \beta_{L}(y)&\text{otherwise}.\end{cases}$ (1)

Then, the semantic clause giving us the basic pomsets for reads is

$\mathcal{B}_{L}(x)=\\{(\\{x=v\\},v,L)\mid\beta_{L}(x)=v\\}\cup\\{(\\{x=v\\},v,L)\mid
x\notin\operatorname{dom}(\beta_{L}),v\in V\\}.$

The first part tells us to use the value associated with $x$ in the buffer
$L$, if available. The second part uses arbitrary values if the value is
unavailable, as with program orders.

The third major change involves parallel composition. We explain parallel
composition of expressions; parallel composition of commands is analogous. By
axioms (F) and (J), we must flush our buffers before every fork and join. We
therefore begin by flushing our entire buffer, i.e., by taking $L$ and placing
it at the beginning of our pomset. Having flushed the buffer, we then evaluate
the $e_{i}$ with empty buffers and get back pomsets $P_{i}$ and $v_{i}$.
Because we can only join threads if their buffers are empty, we require that
these $P_{i}$ and $v_{i}$ be associated with empty buffers in
$\mathcal{P}_{{[\,\,]}}(e_{i})$. We then proceed as for the program order, and
add the parallel composition of the $P_{i}$ to our pomset, and compute the
value $v_{1}\odot v_{2}$. Because we just joined two empty buffers, our
resulting buffer is empty:

$\mathcal{B}_{L}(e_{1}\odot
e_{2})=\\{(L;(P_{1}\operatorname{{\|}}P_{2}),v_{1}\odot
v_{2},{{[\,\,]}})\mid(P_{i},v_{i},{{[\,\,]}})\in\mathcal{P}_{{[\,\,]}}(e_{i})\\}.$

Finally, when we sequentially compose two commands $c_{1}$ and $c_{2}$
(assuming no forking or joining), $c_{2}$ continues executing from the buffer
$c_{1}$ finished with. $\mathcal{P}(c_{1})$ and $\mathcal{P}(c_{2})$ are both
functions of type
$\mathsf{Ls}\to\wp(\mathrm{Pom}({\mathcal{A}_{TSO}})\times\mathsf{Ls})$ and
are not composable qua functions. Consequently, we need to define a
composition operation capturing the above the operational intuition. This
composition is the polymorphic function $\operatorname{\curvearrowright}$,
where $S\in\wp(\mathrm{Pom}\times A)$ and $f\in A\to\wp(\mathrm{Pom}\times
B)$:

$\displaystyle{\operatorname{\curvearrowright}}:\forall A.\forall
B.\wp(\mathrm{Pom}\times A)\to(A\to\wp(\mathrm{Pom}\times
B))\to\wp(\mathrm{Pom}\times B)$ $\displaystyle S$
$\displaystyle\operatorname{\curvearrowright}f=\\{(P;P^{\prime},b)\mid{(P,a)\in
S}\land{(P^{\prime},b)\in f(a)}\\}.$

Taking $A=B=\mathsf{Ls}$, sequential composition can be expressed using as

$\mathcal{B}_{L}(c_{1};c_{2})=\mathcal{P}_{L}(c_{1})\operatorname{\curvearrowright}\mathcal{P}(c_{2}).$

Explicitly, this means
$\mathcal{B}_{L}(c_{1};c_{2})=\\{(P_{1};P_{2},L_{2})\mid(P_{1},L_{1})\in\mathcal{P}_{L}(c_{1}),(P_{2},L_{2})\in\mathcal{P}_{L_{1}}(c_{2})\\}$.
This idiom of chaining pairs of pomsets and buffers together using
$\operatorname{\curvearrowright}$ will be useful throughout. We make
$\operatorname{\curvearrowright}$ polymorphic so that we can handle, e.g., the
case of $A=\mathsf{Ls}$ and $B=V\times\mathsf{Ls}$ below.

The remainder of the basic clauses are analogous to those for program order
pomsets, subject to the modifications described above:

$\displaystyle\mathcal{B}$
$\displaystyle:\mathsf{VExp}\to\mathsf{Ls}\to\wp(\mathrm{Pom}({\mathcal{A}_{TSO}})\times
V\times\mathsf{Ls})$ $\displaystyle\mathcal{B}_{L}(v)$
$\displaystyle=\\{(\\{\delta\\},v,L)\\}$ $\displaystyle\mathcal{B}$
$\displaystyle:\mathsf{BExp}\to\mathsf{Ls}\to\wp(\mathrm{Pom}({\mathcal{A}_{TSO}})\times\mathrm{Bool}\times\mathsf{Ls})$
$\displaystyle\mathcal{B}_{L}(\neg e)$ $\displaystyle=\\{(P,\neg
b,L^{\prime})\mid(P,b,L^{\prime})\in\mathcal{B}_{L}(e)\\}$
$\displaystyle\mathcal{P}_{L,\mathit{true}}(b)$
$\displaystyle=\\{(P,L^{\prime})\mid(P,\mathit{true},L^{\prime})\in\mathcal{P}_{L}(b)\\}$
$\displaystyle\mathcal{P}_{L,\mathit{false}}(b)$
$\displaystyle=\\{(P,L^{\prime})\mid(P,\mathit{false},L^{\prime})\in\mathcal{P}_{L}(b)\\}$
$\displaystyle\mathcal{B}$
$\displaystyle:\mathsf{Cmd}\to\mathsf{Ls}\to\wp(\mathrm{Pom}({\mathcal{A}_{TSO}})\times\mathsf{Ls})$
$\displaystyle\mathcal{B}_{L}(\mathbf{skip})$
$\displaystyle=\\{(\\{\delta\\},L)\\}$
$\displaystyle\mathcal{B}_{L}(c_{1}\operatorname{{\|}}c_{2})$
$\displaystyle=\\{(L;(P_{1}\operatorname{{\|}}P_{2}),{{[\,\,]}})\mid(P_{i},{{[\,\,]}})\in\mathcal{P}_{{[\,\,]}}(c_{i})\\}$
$\displaystyle\mathcal{B}_{L}(\mathbf{if}\ b\ \mathbf{then}\ c_{1}\
\mathbf{else}\ c_{2})$
$\displaystyle=\left(\mathcal{P}_{L,\mathit{true}}(b)\operatorname{\curvearrowright}\mathcal{P}(c_{1})\right)\cup\left(\mathcal{P}_{L,\mathit{false}}(b)\operatorname{\curvearrowright}\mathcal{P}(c_{2})\right)$
$\displaystyle\mathcal{B}_{L}(\mathbf{while}\ b\ \mathbf{do}\ c)$
$\displaystyle=\bigcup_{n=0}^{\infty}I_{L}^{n}(b,c)\cup I_{L}^{\omega}(b,c)$

where $I_{L}^{0}(b,c)=\mathcal{P}_{L,\mathit{false}}(b)$ and
$I_{L}^{n+1}(b,c)=\mathcal{P}_{L,\mathit{true}}(b)\operatorname{\curvearrowright}\mathcal{P}(c)\operatorname{\curvearrowright}I^{n}(b,c)$.
The set
$I^{\omega}_{L}(b,c)\subseteq\mathrm{Pom}({\mathcal{A}_{TSO}})\times\\{{{[\,\,]}}\\}$
contains all infinite pomsets obtained through countably infinitely many
unfoldings; because we can never observe the buffer at the end, we treat it as
empty to simplify presentation.

We now turn our attention to flushing. The intent is that a thread can flush
arbitrarily many of its writes at any point in its execution. Thus, the
pomsets associated with flushes for a buffer $L$ are the prefixes $L^{\prime}$
of $L$, and the resulting buffers are the remainders of $L$. We use
$\operatorname{split}(L)$ to denote these prefix-suffix pairs:

$\displaystyle\operatorname{split}:\mathsf{Ls}\to\wp(\mathrm{Pom}({\mathcal{A}_{TSO}})\times\mathsf{Ls})$
$\displaystyle\operatorname{split}(L)=\\{(L^{\prime},L^{\prime\prime})\mid
L=L^{\prime};L^{\prime\prime}\\}$

We introduce a variant of $\operatorname{\curvearrowright}$ to cope with
triples of pomsets, values, and buffers, and will rely on types to
disambiguate the version needed in any given situation:

$\displaystyle{\operatorname{\curvearrowright}}:\forall A.\forall
B.\wp(\mathrm{Pom}\times A\times B)\to(B\to\wp(\mathrm{Pom}\times
B))\to\wp(\mathrm{Pom}\times A\times B)$ $\displaystyle S$
$\displaystyle\operatorname{\curvearrowright}f=\\{(P;P^{\prime},A,B^{\prime})\mid{(P,A,B)\in
S}\land{(P^{\prime},B^{\prime})\in f(B)}\\}$

We define the TSO pomsets $\mathcal{P}$ in terms of $\mathcal{B}$ and
$\operatorname{split}$. $\mathcal{P}$ composes $\operatorname{split}$ and
$\mathcal{B}$ in a manner that we can flush some writes from the buffer, then
evaluate $e$ or perform $c$, and then flush some writes at the end:

$\displaystyle\mathcal{P}_{L}(e)$
$\displaystyle=\operatorname{split}(L)\operatorname{\curvearrowright}\mathcal{B}(e)\operatorname{\curvearrowright}\operatorname{split}$
$\displaystyle\mathcal{P}_{L}(c)$
$\displaystyle=\operatorname{split}(L)\operatorname{\curvearrowright}\mathcal{B}(c)\operatorname{\curvearrowright}\operatorname{split}$

We can validate various expected equivalences by unfolding these definitions.
For example, sequential composition of commands is associative, because

$\mathcal{P}_{L}(c_{1};(c_{2};c_{3}))=\operatorname{split}(L)\operatorname{\curvearrowright}\penalty
0\mathcal{B}(c_{1})\operatorname{\curvearrowright}\operatorname{split}\operatorname{\curvearrowright}\mathcal{B}(c_{2})\operatorname{\curvearrowright}\operatorname{split}\operatorname{\curvearrowright}\mathcal{B}(c_{3})\operatorname{\curvearrowright}\operatorname{split}=\mathcal{P}_{L}((c_{1};c_{2});c_{3}).$

Using the identity $\mathbf{0};P=P$ and the fact that parallel composition of
pomsets is associative, one can show that parallel composition of commands is
associative, i.e., that
$\mathcal{P}_{L}(c_{1}\operatorname{{\|}}\,(c_{2}\operatorname{{\|}}c_{3}))=\mathcal{P}_{L}((c_{1}\operatorname{{\|}}c_{2})\operatorname{{\|}}c_{3})$.
The parallel composition of pomsets commutes, so the parallel composition of
commands commutes, i.e.,
$\mathcal{P}_{L}(c_{1}\operatorname{{\|}}c_{2})=\mathcal{P}_{L}(c_{2}\operatorname{{\|}}c_{1})$.

To illustrate the effects of flushing and the effect of buffers on reads, we
consider the expression $x$ in the presence of the buffer
$L={[\,x:=3,y:=2\,]}$. The triples $(P,v,L^{\prime})\in\mathcal{P}_{L}(x)$ are
of the form

$\displaystyle P$ $\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
15.02425pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=3}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle=3$ $\displaystyle L^{\prime}$
$\displaystyle={[\,x:=3,y:=2\,]}$ $\displaystyle P$
$\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
15.02425pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
24.02423pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
24.02423pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle=3$ $\displaystyle L^{\prime}$
$\displaystyle={[\,y:=2\,]}$ $\displaystyle P$
$\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
15.02425pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
24.02423pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
24.02423pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
65.85051pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
65.85051pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=2}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle=3$ $\displaystyle L^{\prime}$
$\displaystyle={{[\,\,]}}$ $\displaystyle P$
$\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=v}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle\in V$ $\displaystyle L^{\prime}$
$\displaystyle={[\,y:=2\,]}$ $\displaystyle P$
$\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
64.6676pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
64.6676pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=2}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle\in V$ $\displaystyle L^{\prime}$
$\displaystyle={{[\,\,]}}$ $\displaystyle P$
$\displaystyle=(\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
25.41313pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{y:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
66.78574pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
66.78574pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=v}$}}}}}}}\ignorespaces}}}}\ignorespaces)$
$\displaystyle v$ $\displaystyle\in V$ $\displaystyle L^{\prime}$
$\displaystyle={{[\,\,]}}$

In the first case, the resulting $P$ denotes performing the read without also
doing any flushing. In this case, because we have a write to $x$ in the
buffer, the read from $x$ must use its value. The second and third case give
rise to pomsets denoting performing the read before doing one or two flushes.
In the fourth and fifth cases, we first flush the write to $x$ from the
buffer; the value $v$ read from $x$ is then free to range over all possible
values because there are no other writes to $x$ in the buffer. Finally, in the
last case, we flush all of the writes from the buffer before reading $x$, and
the value read from $x$ is again unconstrained.

The TSO pomsets of a program $p$ are
$\mathcal{P}_{TSO}(p)=\\{P\mid(P,{{[\,\,]}})\in\mathcal{P}_{{[\,\,]}}(p)\\}$.
∎ This definition selects pomsets with empty buffers from
$\mathcal{P}_{{[\,\,]}}(p)$ because we expect programs to be run from an empty
buffer and to only stop after emptying all buffers.

We illustrate the constructions by giving four example families of TSO pomsets
for the Dekker program from the introduction, again assuming $v\neq 0$ and
$v^{\prime}\neq 0$:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
23.0161pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{y}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.49644pt\raise-22.41664pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-58.77771pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
22.65851pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-58.77771pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{z}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-80.22212pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
23.0161pt\raise-68.22215pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{w}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-80.22212pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{z:=1}$}}}}}}}{\hbox{\kern
20.41312pt\raise-89.66656pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w:=1}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
23.0161pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{y}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
22.65851pt\raise-22.41664pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-58.77771pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.49644pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-58.77771pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{z}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-80.22212pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
23.0161pt\raise-68.22215pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{w}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-80.22212pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{z:=1}$}}}}}}}{\hbox{\kern
20.41312pt\raise-89.66656pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w:=1}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
23.0161pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{y}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-38.49997pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.49644pt\raise-22.41664pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-36.36107pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=v}$}}}}}}}{\hbox{\kern
22.65851pt\raise-45.80551pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=0\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-58.77771pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern
23.0161pt\raise-68.22215pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{w}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
37.68275pt\raise-80.22212pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern
20.41312pt\raise-89.66656pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{w:=1}$}}}}}}}\ignorespaces}}}}\ignorespaces,\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
16.41315pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-15.1111pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
21.93277pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{y}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
36.59943pt\raise-12.9722pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y=v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
0.0pt\raise-35.38884pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
20.41312pt\raise-22.41664pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{y:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
36.59943pt\raise-35.97218pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x:=1}$}}}}}}}{\hbox{\kern
20.70218pt\raise-44.83328pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{x=v^{\prime}}$}}}}}}}\ignorespaces}}}}\ignorespaces.$

In the first family of pomsets, we flush the writes immediately after
inserting them in the buffers, while in the second, we flush the writes to $x$
and $y$ after reading $y$ and $x$. In the third family, we flush $x$ right
after placing its write in the buffer, but fall into the $\mathit{false}$ case
of the conditional after reading some value $v\neq 0$, thus taking the
$\mathbf{skip}$ branch. In the fourth pomset, we read $y$ after placing the
write $x:=1$ in the buffer, but before it gets flushed, and both threads fall
into the $\mathbf{skip}$ branch.

####  3.3.1. Laws of parallel programming

Because parallel composition of pomsets is associative and commutative, and
because sequential composition of pomsets is associative, we satisfy many laws
of parallel programming from [Bro96] and [JPR12] for free. Let $C\equiv
C^{\prime}$ whenever $\mathcal{P}_{L}(C)=\mathcal{P}_{L}(C^{\prime})$ for all
$L$. Our semantics satisfies:

$\displaystyle\mathbf{skip};c$ $\displaystyle\equiv c\equiv c;\mathbf{skip}$
$\displaystyle(c_{1};c_{2});c_{3}$ $\displaystyle\equiv c_{1};(c_{2};c_{3})$
$\displaystyle c_{1}\operatorname{{\|}}c_{2}$ $\displaystyle\equiv
c_{2}\operatorname{{\|}}c_{1}$
$\displaystyle(c_{1}\operatorname{{\|}}c_{2})\operatorname{{\|}}c_{3}$
$\displaystyle\equiv c_{1}\operatorname{{\|}}(c_{2}\operatorname{{\|}}c_{3})$
$\displaystyle(\mathbf{if}\ b\ \mathbf{then}\ c_{1}\ \mathbf{else}\
c_{2});c_{3}$ $\displaystyle\equiv\mathbf{if}\ b\ \mathbf{then}\ c_{1};c_{3}\
\mathbf{else}\ c_{2};c_{3}$ $\displaystyle\mathbf{while}\ b\ \mathbf{do}\ c$
$\displaystyle\equiv\mathbf{if}\ b\ \mathbf{then}\ (c;\mathbf{while}\ b\
\mathbf{do}\ c)\ \mathbf{else}\ \mathbf{skip}$

Because we must flush buffers before every fork and join, $\mathbf{skip}$ is
not a unit for parallel composition under TSO:
$\mathbf{skip}\operatorname{{\|}}c\not\equiv c$.

###  3.4. Executions

Our TSO pomset semantics gives an abstract account capturing families of
possible executions. However, compositionality comes with its price: we
associate to programs some pomsets that cannot in any real sense be
“executed”. Consider for example, the pomset $\bar{x}:=2\to x:=2\to
x=1\to\cdots$ for the program $c~{}=~{}(x~{}:=~{}2;~{}\mathbf{if}\
~{}x~{}=~{}1~{}\ \mathbf{then}\ c_{1}\ \mathbf{else}\ c_{2})$. In no
circumstance do we expect to execute $c_{1}$ when this program is run alone,
and so the above TSO pomset has, in a sense made precise later, no executional
meaning. However, compositionality requires this pomset be associated with the
command $c$, because one could execute $c_{1}$ if our program were instead
$c\operatorname{{\|}}x:=1$. Our notion of execution filters out these pomsets
with no executional meaning and yields an input/output behaviour for programs
built from their pomset semantics.

####  3.4.1. Buffered States

Our notion of execution uses buffered global state, i.e., a global state with
a write buffer per thread. We execute threads individually. Each thread’s
execution starts from a state with a buffer, which in combination reflect that
thread’s view of shared memory. Let
$\mathrm{Locs}=\mathrm{BLoc}\cup\mathrm{Loc}$ be the set of all locations. We
use elements of $\Sigma=(\mathrm{BLoc}\penalty
1000\rightharpoonup_{fin}\penalty
1000(V\times\mathbb{N})/{\approx})\times(\mathrm{Loc}\penalty
1000\rightharpoonup_{fin}\penalty 1000V)$ to model the combination of a global
state and a buffer, where $\approx$ is given by $(v,n)\approx(v^{\prime},m)$
if and only if both $n=m$, and $v=v^{\prime}$ or $n=0$. Because $\mathrm{Loc}$
and $\mathrm{BLoc}$ are disjoint, we identify $\Sigma$ with its obvious
inclusion in
$\mathrm{Locs}\rightharpoonup_{fin}({(V\times\mathbb{N})/{\approx}}\cup V)$.
The intuition is that if $\sigma(\bar{x})=(v,n)$, then there are $n$ writes to
$x$ in $\sigma$’s write buffer, and the most recent buffer write to $\sigma$
had the value $v$. We need to keep track of the number $n$ of writes to $x$
still in the buffer to know whether we should continue reading $x$ from the
buffer after a flush. We identify $(v,0)$ and $(v^{\prime},0)$ for all $v$ and
$v^{\prime}$ because one should not be able to observe a value for a write
that is no longer in the buffer, and this identification allows us to “forget”
the value by setting $n$ to $0$. For $x,y,z,\dotsc\in\mathrm{Locs}$ and
$u,v,w,\dotsc$ in the corresponding subset of
$((V\times\mathbb{N})/\approx)\cup V$, we denote by
$\left[x:u,y:v,z:w,\dotsc\right]$ the buffered state with graph
$\\{(x,u),(y,v),(z,w),\dotsc\\}$. For compactness of notation, we write
$v_{n}$ for the equivalence class of $(v,n)$ in $(V\times\mathbb{N})/\approx$.

####  3.4.2. Footprints

Footprints are the first step towards formalizing execution and filtering out
unexecutable pomsets. Informally, a footstep
$(\sigma,\tau)\in\Sigma\times\Sigma$ of an action $\lambda$ is a minimal piece
of state $\sigma$ required to be able to perform $\lambda$, and a description
$\tau$ of the effects of performing $\lambda$. For example, to perform a
global write $x:=v$, $x$ must be in the domain of the initial state and
present in the buffer, so
$\sigma=[x:v^{\prime},\bar{x}:v^{\prime\prime}_{n+1}]$ for some $v^{\prime}$
and $v^{\prime\prime}$, and the result is setting the global value of $x$ to
$v$ while removing one occurrence of $x$ from the buffer, so
$\tau=[x:v,\bar{x}:v^{\prime\prime}_{n}]$. Though $v$ and $v^{\prime\prime}$
are unrelated, this gives the correct behaviour in the context of command
pomsets because global writes to $x$ occur in the same order as buffer writes
to $x$. To perform a read action $x=v$, we must either have no entries for $x$
in the buffer and have $x:v$ in the global state, or we must have $x$ in the
buffer with value $v$, i.e., $\bar{x}:v_{n}$ for some $n>0$. We call the set
of footsteps associated with an action its footprint. Pomsets also have
footsteps and footprints.

TSO footprints for actions are given as follows:

$\displaystyle\llbracket x=v\rrbracket$
$\displaystyle=\\{([x:v,\bar{x}:v_{0}],{\left[\,\right]}),([\bar{x}:v_{n+1}],{\left[\,\right]})\mid
n\in\mathbb{N}\\}$ $\displaystyle\llbracket\bar{x}:=v\rrbracket$
$\displaystyle=\\{([\bar{x}:v^{\prime}_{n}],[\bar{x}:v_{n+1}])\mid
v^{\prime}\in V\land n\in\mathbb{N}\\}$ $\displaystyle\llbracket
x:=v\rrbracket$
$\displaystyle=\\{([x:v^{\prime},\bar{x}:v^{\prime\prime}_{n+1}],[x:v,\bar{x}:v^{\prime\prime}_{n}])\mid
v^{\prime},v^{\prime\prime}\in V\land n\in\mathbb{N}\\}$
$\displaystyle\llbracket\delta\rrbracket$
$\displaystyle=\\{({\left[\,\right]},{\left[\,\right]})\\}$ ∎

To give footprints to pomsets, we need to know when it makes sense to combine
two footsteps sequentially or in parallel. We say two states $\sigma_{1}$ and
$\sigma_{2}$ are consistent, $\sigma_{1}\mathrel{\Uparrow}\sigma_{2}$, if for
all $x\in\operatorname{dom}(\sigma_{1})\cap\operatorname{dom}(\sigma_{2})$,
$\sigma_{1}(x)=\sigma_{2}(x)$. In this case, $\sigma_{1}\cup\sigma_{2}$ is
also a state. Let
$\sigma\setminus\operatorname{dom}(\tau)=\sigma{\restriction}_{\operatorname{dom}(\sigma)\setminus\operatorname{dom}(\tau)}$.
Then the result of updating $\sigma$ by $\tau$ is
$\left[\sigma\mid\tau\right]=(\sigma\setminus\operatorname{dom}(\tau))\cup\tau$.
To sequence the footprint $(\sigma_{1},\tau_{1})$ before the footprint
$(\sigma_{2},\tau_{2})$, we must ensure that the result of the first
computation from its initial state, $\left[\sigma_{1}\mid\tau_{1}\right]$, is
consistent with the requirements $\sigma_{2}$ of the second computation, i.e.,
we must ensure
$\left[\sigma_{1}\mid\tau_{1}\right]\mathrel{\Uparrow}\sigma_{2}$. In this
case, sequentially performing both computations requires that the initial
state provide everything required by the first computation, plus everything
required by the second computation not already provided by the first one. This
is $\sigma_{1}\cup(\sigma_{2}\setminus\operatorname{dom}(\tau_{1}))$. The
effects of the two computations are the first’s effects updated by the effects
of the second one, $\left[\tau_{1}\mid\tau_{2}\right]$. Consequently, for
states $(\sigma_{i},\tau_{i})$ such that
$\left[\sigma_{1}\mid\tau_{1}\right]\mathrel{\Uparrow}\sigma_{2}$, we define
their sequential composition to be:

$(\sigma_{1},\tau_{1})\mathrel{{\triangleleft}}(\sigma_{2},\tau_{2})=(\sigma_{1}\cup(\sigma_{2}\setminus\operatorname{dom}(\tau_{1})),\left[\tau_{1}\mid\tau_{2}\right]).$

This lifts to an associative operation on $\Sigma\times\Sigma$:

$S_{1}\mathrel{{\triangleleft}}S_{2}=\\{(\sigma_{1},\tau_{1})\mathrel{{\triangleleft}}(\sigma_{2},\tau_{2})\mid(\sigma_{i},\tau_{i})\in
S_{i}\land\left[\sigma_{1}\mid\tau_{1}\right]\mathrel{\Uparrow}\sigma_{2}\\}.$

To account for global writes occurring elsewhere during the program, we
parametrize the rules assigning footprints $\llbracket P\rrbracket_{\Lambda}$
to pomsets $P$ by a list $\Lambda$ containing a linearisation of the pomset as
a subsequence, combined with any number of other global writes that represent
flushes from buffers belonging to other threads. Because these global writes
are performed, in principle, by other threads, they should not affect the
buffers in the footprints associated with $P$. The exact mechanics of how
$\Lambda$ and $P$ interact in producing footprints will be made clear below.
Formally, given a pomset $P$, we let $\operatorname{Lin}(P)$ be the set of its
linearisations. Then the clauses are parametrized by
$\Lambda\in\Gamma(P)=\bigcup_{L\in\mathsf{Ls}}\operatorname{Lin}(P\operatorname{{\|}}L)$,
where given some global-write environment $\Lambda\in\Gamma(P)$, we identify
$P$ with its image in $\Lambda$. So $\Lambda$ is a linearisation of $P$
interspersed with global writes that will not involve buffers. In particular,
when $P$ is $\\{\lambda\\}$, then every $\Lambda\in\Gamma(P)$ will be of the
form $\Lambda_{1};\\{\lambda\\};\Lambda_{2}$ for some unique
$\Lambda_{1},\Lambda_{2}\in\mathsf{Ls}$. This fact will be important for
understanding the (Act) rule below. Because $\Lambda$ is a linearisation, it
totally orders the writes it contains, including those of $P$.

Given some $L\in\mathsf{Ls}$, let $\llbracket L\rrbracket^{*}$ be inductively
defined on the structure of $L$ as follows:

$\displaystyle\llbracket\,{{[\,\,]}}\,\rrbracket^{*}$
$\displaystyle=\\{({\left[\,\right]},{\left[\,\right]})\\}$
$\displaystyle\llbracket\\{x:=v\\};L\rrbracket^{*}$
$\displaystyle=\\{([x:v^{\prime}],[x:v])\mid v^{\prime}\in
V\\}\mathrel{{\triangleleft}}\llbracket L\rrbracket^{*}$

The intuition here is that the foreign buffer flushes in $L$ should only
affect the global part of the state and have no effect on our buffer. Given a
list ${[\,x_{1}:=v_{1},\dotsc,x_{n}:=v_{n}\,]}$, we write $\llbracket
x_{1}:=v_{1},\dotsc,x_{n}:=v_{n}\rrbracket^{*}$ for
$\llbracket{[\,x_{1}:=v_{1},\dotsc,x_{n}:=v_{n}\,]}\rrbracket^{*}$.

We will need to know if buffered states have empty buffers. We let
$\zeta(\sigma)$ hold if and only if for all
$x\in\operatorname{dom}(\sigma{\restriction}_{\mathrm{BLoc}})$,
$\sigma(x)=v_{0}$. In other words, $\zeta(\sigma)$ holds if and only if
$\sigma$ “has an empty buffer”. Thus, for example, both
$\zeta({\left[\,\right]})$ and $\zeta([x:1,\bar{y}:2_{0}])$, but neither
$\zeta([x:1,\bar{x}:2_{5}])$ nor $\zeta([\bar{y}:1_{1}])$.

The footprint $\llbracket P\rrbracket_{\Lambda}$ of a pomset $P$ under a
global-write environment $\Lambda\in\Gamma(P)$ is the smallest set closed
under the following three rules:

(Act):

If $P=\\{\lambda\\}$ for some action $\lambda$ and
$\Lambda=\Lambda_{1};P;\Lambda_{2}$ for some
$\Lambda_{1},\Lambda_{2}\in\mathsf{Ls}$, then $\llbracket
P\rrbracket_{\Lambda}=\llbracket\Lambda_{1}\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket\lambda\rrbracket\mathrel{{\triangleleft}}\llbracket\Lambda_{2}\rrbracket^{*}$.

(Seq):

If $P=P_{1};P_{2}$ and $\Lambda=\Lambda_{1};\Lambda_{2}$, then $\llbracket
P_{1}\rrbracket_{\Lambda_{1}}\mathrel{{\triangleleft}}\llbracket
P_{2}\rrbracket_{\Lambda_{2}}\subseteq\llbracket P\rrbracket_{\Lambda}$.

(Par):

If $P=P_{1}\operatorname{{\|}}P_{2}$, $\Lambda_{1}$ is the result of deleting
the read and buffer write actions of $P_{2}$ from $\Lambda$, $\Lambda_{2}$ is
the symmetric restriction, $(\sigma_{i},\tau_{i})\in\llbracket
P_{i}\rrbracket_{\Lambda_{i}}$, $\zeta(\sigma_{i})$ and $\zeta(\tau_{i})$
($i=1,2$), and $\sigma_{1}\Uparrow\sigma_{2}$, then
$(\sigma_{1}\cup\sigma_{2},\tau_{1}\cup\tau_{2})\in\llbracket
P\rrbracket_{\Lambda}$. ∎

This definition is inspired by Lamport’s “happened before” relation [Lam78].
In the case of (Act), for a given $P=\\{\lambda\\}$ and $\Lambda\in\Gamma(P)$,
the intuition is that $\Lambda$ specifies that the global writes in
$\Lambda_{1}$ happened before $\lambda$, and that $\lambda$ happened before
the global writes in $\Lambda_{2}$. In the case of (Seq), for $\llbracket
P_{i}\rrbracket_{\Lambda_{i}}$ to be well-defined, we are implicitly assuming
that $\Lambda_{i}\in\Gamma(P_{i})$. (Seq) tells us that the result of
sequentially executing a program in the presence of global writes should be
the same as executing the pieces sequentially in the presence of the
appropriate subset of global writes. Finally, in (Par), the restrictions of
$\Lambda$ are such that both parallel components observe all writes in the
same order, and this is how we simulate the effects of writes to a global
state. One can show that the set $\llbracket P\rrbracket_{\Lambda}$ is well-
defined with regards to our identification of pomsets up-to-isomorphism. In
particular, $\llbracket(P_{1};P_{2});P_{3}\rrbracket_{\Lambda}=\llbracket
P_{1};(P_{2};P_{3})\rrbracket_{\Lambda}$ and
$\llbracket(P_{1}\operatorname{{\|}}P_{2})\operatorname{{\|}}P_{3}\rrbracket_{\Lambda}=\llbracket
P_{1}\operatorname{{\|}}(P_{2}\operatorname{{\|}}P_{3})\rrbracket_{\Lambda}$.

We give various results below that simplify computing the footprint of
pomsets. By Proposition 3, a pomset has a footprint only if it is series-
parallel. A pomset is series-parallel or SP if it is linear, or if it is the
sequential or parallel composition of SP pomsets.

The maximal linear segments of a SP pomset are its SP components; any SP
pomset can be uniquely decomposed into these. To compute the footprint of a
pomset $P$, we can use Proposition 4 and 6 to first decompose $P$ into its
series-parallel components, each of which will be linear. We can then compute
the footprints of these linear components using Corollary 5 and Proposition 7,
and combine them using the appropriate applications of (Seq) and (Par).

We use these results to illustrate how global-write environments simulate the
effects of global writes. Let $P_{1}$ and $P_{2}$ be the pomsets

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
14.66666pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
38.66666pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
38.66666pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
95.49295pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
95.49295pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=3}$}}}}}}}\ignorespaces}}}}\ignorespaces\qquad\text{and}\qquad\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
14.66666pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\bar{x}:=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
38.66666pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
38.66666pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x=3\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
92.71515pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
92.71515pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{x:=3}$}}}}}}}\ignorespaces}}}}\ignorespaces,$

respectively, and let $P=P_{1}\operatorname{{\|}}P_{2}$. Consider the global-
write environments

$\displaystyle\Lambda$
$\displaystyle={[\,\bar{x}:=2,\bar{x}:=3,x:=2,x=3,x:=3,x=3\,]}$
$\displaystyle\Lambda_{1}$ $\displaystyle={[\,\bar{x}:=2,x:=2,x:=3,x=3\,]}$
$\displaystyle\Lambda_{2}$ $\displaystyle={[\,\bar{x}:=3,x:=2,x=3,x:=3\,]}.$

We see that $\Lambda$ is a global-write environment for $P$, and that
$\Lambda_{i}$ is the restriction of $\Lambda$ given by the (Par) rule for
$P_{i}$ and is again a global-write environment for $P_{i}$. To compute the
footprint of $P$, we must begin by applying the (Par) rule and recursively
compute the footprint of $P_{i}$ under $\Lambda_{i}$. We first consider
$\llbracket P_{1}\rrbracket_{\Lambda_{1}}$. By Corollary 5, it is given by

$\llbracket\bar{x}:=2\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=3\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket x=3\rrbracket,$

where we omitted the instances of the unit
$\llbracket{{[\,\,]}}\rrbracket^{*}$ for the $\mathrel{{\triangleleft}}$
operation. Simplifying this expression, we get that $\llbracket
P_{1}\rrbracket_{\Lambda_{1}}=\\{(\left[x:v,\bar{x}:v^{\prime}_{n}\right],\left[x:3,\bar{x}:2_{n}\right])\mid
v,v^{\prime}\in V\land n\in\mathbb{N}\\}$. Despite there being no write of $3$
to $x$ in $P_{1}$, the presence of such a global write in $\Lambda_{1}$ and
its position in $\Lambda_{1}$ mean that the read $x=3$ can be executed by
$P_{1}$. More interesting, perhaps, is the footprint $\llbracket
P_{2}\rrbracket_{\Lambda_{2}}$, and in particular, how the global write $x:=2$
does not interfere with the read $x=3$ thanks to buffering. Again by Corollary
5, it is given by

$\llbracket\bar{x}:=3\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket
x=3\rrbracket\mathrel{{\triangleleft}}\llbracket x:=3\rrbracket.$

The subexpression
$\llbracket\bar{x}:=3\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket^{*}$ simplifies to

$\\{(\left[x:v,\bar{x}:v^{\prime}_{n}\right],\left[x:2,\bar{x}:3_{n+1}\right])\mid
v,v^{\prime}\in V\land n\in\mathbb{N}\\}$ (2)

Because for each
$(\sigma,\tau)\in\llbracket\bar{x}:=3\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket^{*}$ we have $\tau(\bar{x})=3_{n}$ for some $n>0$, i.e.,
because $\tau$’s buffer has a write to $x$, the footsteps
$(\left[x:3,\bar{x}:v_{0}\right],{\left[\,\right]})\in\llbracket
x=3\rrbracket$ describing a read of $3$ from shared memory are ignored when
combining $\llbracket\bar{x}:=3\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket^{*}$ with $\llbracket x=3\rrbracket$ using the
$\mathrel{{\triangleleft}}$ operation. Instead,
$\llbracket\bar{x}:=3\rrbracket\mathrel{{\triangleleft}}\llbracket
x:=2\rrbracket^{*}$ gets combined with the subset
$\\{(\left[\bar{x}:3_{n+1}\right],{\left[\,\right]})\mid
n\in\mathbb{N}\\}\subseteq\llbracket x=3\rrbracket$ to give (2) again. Then
combining (2) with $\llbracket x:=3\rrbracket$ gives us $\llbracket
P_{2}\rrbracket_{\Lambda_{2}}=\\{(\left[x:v,\bar{x}:v^{\prime}_{n}\right],\left[x:3,\bar{x}:3_{n}\right])\mid
v,v^{\prime}\in V\land n\in\mathbb{N}\\}$. Finally, we get $\llbracket
P\rrbracket_{\Lambda}=\\{(\left[x:v,\bar{x}:v_{0}\right],\left[x:3,\bar{x}:v_{0}\right])\mid
v\in V\\}$ by combining these footprints using the (Par) rule.

One can show by induction on the rules defining footprints that:

######  Proposition 3.

For all $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$ and $\Lambda\in\Gamma(P)$, if
$\llbracket P\rrbracket_{\Lambda}\neq\emptyset$, then $P$ is SP. ∎

The following proposition shows that the execution of a pomset $P$ in a
global-write environment $\Lambda$ can be thought of as executions of parts of
$P$ interspersed with environment steps from $\Lambda$. Its corollary shows
how to efficiently compute the footprint of linear pomsets.

######  Proposition 4.

If $P=P_{1};\dotsc;P_{n}$ and
$\Lambda=E_{0};\Lambda_{1};E_{1};\dotsb;\Lambda_{n};E_{n}\in\Gamma(P)$ such
that $\Lambda_{i}\in\Gamma(P_{i})$ and $E_{i}\in\mathsf{Ls}$ for all $i$, then

$\llbracket P\rrbracket_{\Lambda}=\llbracket
E_{0}\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket
P_{1}\rrbracket_{\Lambda_{1}}\mathrel{{\triangleleft}}\llbracket
E_{1}\rrbracket^{*}\mathrel{{\triangleleft}}\dotsb\mathrel{{\triangleleft}}\llbracket
P_{n}\rrbracket_{\Lambda_{n}}\mathrel{{\triangleleft}}\llbracket
E_{n}\rrbracket^{*}.$

Without loss of generality, the $\Lambda_{i}$ and $E_{i}$ can be chosen such
that the first and last elements of $\Lambda_{i}$ are in $P_{i}$. ∎

######  Corollary 5.

If $P={[\,\lambda_{1},\dotsc,\lambda_{n}\,]}$ and
$\Lambda=E_{0};\\{\lambda_{1}\\};E_{1};\dotsb;\\{\lambda_{n}\\};E_{n}\in\Gamma(P)$,
then

$\llbracket P\rrbracket_{\Lambda}=\llbracket
E_{0}\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket\lambda_{1}\rrbracket\mathrel{{\triangleleft}}\llbracket
E_{1}\rrbracket^{*}\mathrel{{\triangleleft}}\dotsb\mathrel{{\triangleleft}}\llbracket\lambda_{n}\rrbracket\mathrel{{\triangleleft}}\llbracket
E_{n}\rrbracket^{*}.$ ∎

We can similarly decompose parallel compositions of pomsets when computing
footprints.

######  Proposition 6.

If $P=P_{1}\operatorname{{\|}}\dotsb\operatorname{{\|}}P_{n}$,
$\Lambda\in\Gamma(P)$, and for all $i$, $\Lambda_{i}\in\Gamma(P_{i})$ is
obtained from $\Lambda$ by deleting the read and buffer write actions not in
$P_{i}$, then

$\llbracket P\rrbracket_{\Lambda}=\llbracket
P_{1}\rrbracket_{\Lambda_{1}}\operatorname{{\|}}\dotsb\operatorname{{\|}}\,\llbracket
P_{n}\rrbracket_{\Lambda_{n}},$

where the associative binary operator $\operatorname{{\|}}$ on subsets of
$\Sigma\times\Sigma$ is given by

$S_{1}\operatorname{{\|}}S_{2}=\\{(\sigma_{1}\cup\sigma_{2},\tau_{1}\cup\tau_{2})\mid(\sigma_{i},\tau_{i})\in
S_{i},\zeta(\sigma_{i}),\zeta(\tau_{i}),\sigma_{1}\mathrel{\Uparrow}\sigma_{2},\tau_{1}\mathrel{\Uparrow}\tau_{2}\\}.$
∎

Finally, we can characterize the footprints of the above “environment steps”
using the following lemma, which can be shown by induction on the length of
$\Lambda$:

######  Proposition 7.

For all $\Lambda\in\mathsf{Ls}$ and
$(\sigma,\tau)\in\llbracket\Lambda\rrbracket^{*}$, we have $x:=v\in\Lambda$
for some $v$ if and only if $x\in\operatorname{dom}(\sigma)$. For no
$\bar{x}\in\mathrm{BLoc}$ do we have
$\bar{x}\in\operatorname{dom}(\sigma)\cup\operatorname{dom}(\tau)$. Moreover,
$\operatorname{dom}(\sigma)=\operatorname{dom}(\tau)$. For all
$x\in\operatorname{dom}(\sigma)$ and $v\in V$, we have $(\left[\sigma\mid
x:v\right],\tau)\in\llbracket\Lambda\rrbracket^{*}$. If $x:=v$ is the maximal
write to $x$ in $\Lambda$, then $\tau(x)=v$. ∎

To better understand and characterize pomset executions, we introduce the
characteristic $\operatorname{\chi}_{x}(P)\in\mathbb{N}\times\mathbb{N}$ of a
location $x$ in a series-parallel pomset $P$. Intuitively, when
$\operatorname{\chi}_{x}(P)=(g,b)$, $g$ is the number of global writes to $x$
in $P$ that do not have a buffer entry witnessing them, and $b$ describes the
number of buffer entries left to be flushed after executing $P$. The
characteristic is inductively given on the structure of $P$ as follows:

$\displaystyle\operatorname{\chi}_{x}(\\{y:=v\\})$
$\displaystyle=\begin{cases}(1,0)&x=y\\\ (0,0)&x\neq y\end{cases}$
$\displaystyle\operatorname{\chi}_{x}(\\{\bar{y}:=v\\})$
$\displaystyle=\begin{cases}(0,1)&x=y\\\ (0,0)&x\neq y\end{cases}$
$\displaystyle\operatorname{\chi}_{x}(y=v)$ $\displaystyle=(0,0)$
$\displaystyle\operatorname{\chi}_{x}(\delta)$ $\displaystyle=(0,0)$
$\displaystyle\operatorname{\chi}_{x}(P_{1}\operatorname{{\|}}P_{2})$
$\displaystyle=(g_{1}+g_{2},b_{1}+b_{2})$
$\displaystyle\operatorname{\chi}_{x}(P_{1};P_{2})$
$\displaystyle=(g_{1}+\max\\{g_{2}-b_{1},0\\},b_{2}+\max\\{b_{1}-g_{2},0\\}),$

where $\operatorname{\chi}_{x}(P_{i})=(g_{i},b_{i})$. It is not hard to show
that the characteristic $\operatorname{\chi}_{x}(P)$ is well-defined.

As shown in Proposition 8 below, the concept of characteristic is closely
related to that of the differential. Where $g_{x}$ and $b_{x}$ are the number
of global and buffer write actions to $x$ in a pomset $P$, respectively, call
$\operatorname{\Delta}_{x}(P)=b_{x}-g_{x}$ the differential of $x$ in $P$.

######  Proposition 8.

For all $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$, if
$\operatorname{\chi}_{x}(P)=(g,b)$, then $\operatorname{\Delta}_{x}(P)=b-g$. ∎

The following proposition tells us that the number of buffer entries for $x$
in the final state of a footstep of a pomset $P$ is determined by the
differential of $x$ in $P$ and by the number of buffer entries for $x$ in the
initial state. For compactness, let $\sigma[\bar{x}]=n$ whenever
$\sigma(\bar{x})=v_{n}$.

######  Proposition 9.

For all $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$, $\Lambda\in\Gamma(P)$,
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$, and
$\bar{x}\in\operatorname{dom}(\sigma)$, if
$\bar{x}\in\operatorname{dom}(\tau)$, then
$\tau[\bar{x}]=\sigma[\bar{x}]+\operatorname{\Delta}_{x}(P)$. ∎

######  Corollary 10.

Let $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$, $\Lambda\in\Gamma(P)$,
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$, and
$\operatorname{\chi}_{x}(P)=(g,b)$. Then $\tau[\bar{x}]=\sigma[\bar{x}]+b-g$.
In particular, when $g=0$, then $\tau[\bar{x}]=\sigma[\bar{x}]+b$. ∎

The following lemma is useful in bounding the characteristic of $P$. In
particular, it implies that if there exists a $\Lambda\in\Gamma(P)$ and a
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$ such that $\zeta(\sigma)$
and $\zeta(\tau)$, then $\operatorname{\chi}_{x}(P)=(0,0)$.

######  Lemma 11.

Let $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$, $\Lambda\in\Gamma(P)$,
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$, and
$\operatorname{\chi}_{x}(P)=(g,b)$. Then $\sigma[\bar{x}]\geq g$, and if
$\bar{x}\notin\operatorname{dom}(\sigma)$, then $g=0$. Moreover,
$\tau[\bar{x}]\geq b$, and if $\bar{x}\notin\operatorname{dom}(\tau)$, then
$b=0$. ∎

######  Corollary 12.

If $(\sigma,\tau)\in\llbracket
P_{1}\operatorname{{\|}}P_{2}\rrbracket_{\Lambda}$, then
$\operatorname{\chi}_{x}(P_{i})=(0,0)$ and $\operatorname{\chi}_{x}(P)=(0,0)$.
∎

In certain cases, we can “read off” from $P$ and $\Lambda$ what certain values
in a footstep should be. We can show by induction on the derivation of
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$ that:

######  Proposition 13.

Let $P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$, $\Lambda\in\Gamma(P)$,
$(\sigma,\tau)\in\llbracket P\rrbracket_{\Lambda}$ and let
$\operatorname{\chi}_{x}(P)=(g,b)$. Let ${\\{\rho^{(i)}\\}}_{i=1..k}$ be the
minimal reads ${\\{x=v^{(i)}\\}}_{i=1..k}$ from $x$ under $<_{P}$.

  1. (1)

If there exist $i_{1},\dotsc,i_{l}$, $l\geq 1$, such that there are no writes
to $x$ or $\bar{x}$ in
$\bigcup_{j=1}^{l}\rho^{(i_{j})}{\downarrow}_{\Lambda}$, then
$\bar{x}\in\operatorname{dom}(\sigma)$, there exists a $v$ such that
$v=v^{(i_{1})}=\dotsb=v^{(i_{l})}$, $\sigma(\bar{x})=v_{n}$ for some $n\geq
g$, and $\sigma(x)=v$ when $n=0$.

  2. (2)

If there exists a maximal global write $x:=v$ to $x$ under $<_{\Lambda}$ (it
may be in $P$ or not), then $\tau(x)=v$. Moreover,
$x\in\operatorname{dom}(\tau)$ if and only if there exists a global write to
$x$ in $\Lambda$.

  3. (3)

If there exists a maximal buffer write $\bar{x}:=v$ to $x$ under
$<_{\Lambda}$, then $\tau(\bar{x})=v_{n}$ for some $n\geq b$. Moreover,
$\bar{x}\in\operatorname{dom}(\tau)$ if and only if there exists a global
write to $x$ or a buffer write to $\bar{x}$ in $P$.

  4. (4)

If there exist no buffer writes $\bar{x}:=v$ and
$\bar{x}\in\operatorname{dom}(\tau)$, then where $\sigma(\bar{x})=v_{n}$, we
have $\tau(\bar{x})=v_{m}$ for some $m$.

As a corollary, we validate the intuition that the final state should be
determined by the total order imposed by $\Lambda$ on the writes, where
$\beta$ is as in (1):

######  Corollary 14.

For all $P$, $\Lambda\in\Gamma(P)$, and $(\sigma,\tau)\in\llbracket
P\rrbracket_{\Lambda}$, we have
$\tau{\restriction}_{\mathrm{Loc}}=\beta_{\Lambda{\restriction}_{\mathcal{A}_{w}}}$.
∎

####  3.4.3. Executions

Let $\llbracket P\rrbracket^{\zeta}_{\Lambda}=\\{(\sigma,\tau)\in\llbracket
P\rrbracket_{\Lambda}\mid\zeta(\sigma)\land\zeta(\tau)\\}$ be the subset of
footsteps with empty buffers. The set of TSO executions of a finite pomset $P$
is given by the set
$\mathcal{E}(P)=\\{(\sigma,\left[\sigma\mid\tau\right])\mid\Lambda\in\operatorname{Lin}(P),(\sigma^{\prime},\tau)\in\llbracket
P\rrbracket^{\zeta}_{\Lambda},\sigma^{\prime}\subseteq\sigma\\}$; infinite
pomsets are considered in Section 3.6. These executions take all of the states
$\sigma$ containing a minimal fragment $\sigma^{\prime}$ required to execute
$P$ to that state updated with the effects $\tau$ of $P$. The set of TSO
executions for a program $p$ is then
$\mathcal{E}(p)=\bigcup_{P\in\mathcal{P}_{TSO}(p)}\mathcal{E}(P)$. We say that
a finite pomset $P$ and a program $p$ are TSO executable if $\mathcal{E}(P)$
and $\mathcal{E}(p)$ are non-empty, respectively.

We illustrate TSO pomset executions by validating the IRIW litmus test, i.e.,
by showing that all writes appear in the same order to all threads. For
example, starting from a state initialized to zero, executing the program

${x:=1}\operatorname{{\|}}{y:=1}\operatorname{{\|}}{(w_{1}:=x;w_{2}:=y)}\operatorname{{\|}}{(z_{1}:=y;z_{2}:=x)}$

under TSO should never give a state consistent with
$\left[w_{1}:1,w_{2}:0,z_{1}:1,z_{2}:0\right]$. To show this, it is sufficient
to show that the following pomset $P$ is not executable:

$\textstyle{\bar{x}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\bar{y}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{y=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x:=1}$$\textstyle{y:=1}$$\textstyle{y=0}$$\textstyle{x=0.}$

Consider some $\Lambda\in\operatorname{Lin}(P)$. Without loss of generality,
assume $x:=1<_{\Lambda}y:=1$. To get an execution, we must apply (Par), and
eventually we will need to compute $\llbracket P_{4}\rrbracket_{\Lambda_{4}}$
where $P_{4}$ is $y=1\to x=0$ and $\Lambda_{4}$ is such that
$x:=1<_{\Lambda_{4}}y:=1$. To be able to execute $y=1$ and still get a
footstep with an empty initial buffer, we need $\Lambda_{4}$ to satisfy
$y:=1<y=1$. But then $\llbracket P_{4}\rrbracket_{\Lambda_{4}}=\llbracket
x:=1,y:=1\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket\\{y=1\\}\rrbracket_{{[\,y=1\,]}}\mathrel{{\triangleleft}}\llbracket\\{x~{}=~{}0\\}\rrbracket_{{[\,x=0\,]}}$,
and there are no footsteps in $\llbracket
x:=1,y:=1\rrbracket^{*}\mathrel{{\triangleleft}}\llbracket\\{y=1\\}\rrbracket_{{[\,y=1\,]}}$
that can be combined with those in
$\llbracket\\{x=0\\}\rrbracket_{{[\,x=0\,]}}$ to get states with empty
buffers. This means we cannot combine footsteps from $P_{4}$ to get footsteps
for $P$ using the (Par) rule, and so $\llbracket P\rrbracket_{\Lambda}$ will
be empty.

As discussed in the introduction, the Dekker mutual exclusion algorithm fails
under TSO. Indeed, the second pomset for Dekker on page 3.3 can be executed
from an initial state having both $x$ and $y$ set to zero. To do so, we take a
$\Lambda$ such that ${y~{}=~{}0}<_{\Lambda}{y~{}:=~{}1}$ and
${x~{}=~{}0}<_{\Lambda}{x~{}:=~{}1}$, and apply (Par) followed by (Seq).

In contrast, the Peterson algorithm successfully enforces mutual exclusion
under TSO. Consider the following instance of the Peterson algorithm:

${(x:=1;\mathbf{if}\ x=2\ \mathbf{then}\ l:=1\ \mathbf{else}\
\mathbf{skip})}\operatorname{{\|}}{(x:=2;\mathbf{if}\ x=1\ \mathbf{then}\
r:=1\ \mathbf{else}\ \mathbf{skip})}.$

Starting from the initial state $\left[x:0,l:0,r:0\right]$, one cannot execute
the above under TSO and reach a state where both $l$ and $r$ are 1. In showing
this, we can safely ignore all pomsets where a read from $x$ appears before
the global write to $x$, because whenever we have $\bar{x}:=v\to
x=v^{\prime}\to x:=v$ in a command’s TSO pomset, we must have $v=v^{\prime}$.
This implies that if a thread reads $x$ before it does the global write to
$x$, it will take the $\mathbf{skip}$ branch of the conditional. It is then
sufficient to show that the following pomset is not executable:

$\textstyle{{\bar{x}}:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x:=1\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x=2}$$\textstyle{{\bar{x}}:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x:=2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x=1.}$

Consider some $\Lambda\in\operatorname{Lin}(P)$. Without loss of generality,
assume $x:=1<_{\Lambda}x:=2$. To get an execution, we must apply (Par) and
derive a footstep for the bottom row $P_{2}$ under some $\Lambda_{2}$ where
$x:=1<_{\Lambda_{2}}x:=2$. To compute this footstep, we must repeatedly apply
(Seq), and will eventually reach the stage where $\llbracket
P_{2}\rrbracket_{\Lambda_{2}}=\\{(\left[x~{}:~{}0\right],\left[x~{}:~{}2\right])\\}\mathrel{{\triangleleft}}\llbracket
x=1\rrbracket_{{[\,x=1\,]}}$. But this footprint must be empty, because
$\left[x:0\mid x:2\right]$ is not consistent with $\left[x:1\right]$. We thus
cannot apply (Par) and we conclude that the pomset is not executable. It
follows that the Peterson algorithm enforces mutual exclusion under TSO.

###  3.5. Fences

We can extend the above semantics to deal with fences. This extension will not
be referenced in subsequent sections, and we mention it here merely to
emphasize the flexibility of our general development.

A fence constrains the reordering of memory actions. To capture fences, we
first introduce a command $\mathbf{fence}$. Under TSO, fences cause all
actions before the fence to be observed before any actions after the fence. It
is sufficient to flush the thread’s buffer to ensure this, giving rise to the
semantic clause
$\mathcal{P}_{L}(\mathbf{fence})=\\{(L;\\{\delta\\},{{[\,\,]}})\\}$.

###  3.6. Infinite executions

Though we cannot capture the input-output behaviour of infinite pomsets (such
executions have no “final state”), we can describe their executions in terms
of executions of finite pomsets. We first characterize the “phased executions”
describing infinite executions. Then we describe when a phased execution is an
execution of a given infinite pomset.

The set
$\mathcal{P}_{\mathcal{E}}(\sigma)\subseteq\mathrm{Pom}(\Sigma\times\mathcal{P}_{TSO}\times\Sigma)$
of execution-from-$\sigma$ pomsets is coinductively defined by:

  1. (1)

if $P$ is finite and $(\sigma,\tau)\in\mathcal{E}(P)$, then
$\\{(\sigma,P,\tau)\\}\in\mathcal{P}_{\mathcal{E}}(\sigma)$; and

  2. (2)

if $P$ is finite, $(\sigma,\tau)\in\mathcal{E}(P)$, and
$E\in\mathcal{P}_{\mathcal{E}}(\left[\sigma\mid\tau\right])$, then
$\\{(\sigma,P,\tau)\\};E\in\mathcal{P}_{\mathcal{E}}(\sigma)$.

All pomsets in $\mathcal{P}_{\mathcal{E}}(\sigma)$ are linear, satisfy the
finite-height property, and are series-parallel. Given an
$E\in\mathcal{P}_{\mathcal{E}}(\sigma)$, its underlying TSO pomset
$\pi_{2}(E)$ is obtained by sequentially composing its pomsets in the obvious
manner. Explicitly, $\pi_{2}(E)=(\bigcup_{e\in
E}\\{e\\}\times(\pi_{2}\circ\Phi_{E})(e),{<},\Phi)$, where
$\Phi(e,p)=\Phi_{\Phi_{E}(e)}(p)$, and $(e_{0},p_{0})<(e_{1},p_{1})$ if and
only if $e_{0}<_{E}e_{1}$, or $e_{0}=e_{1}$ and $p_{0}<_{\Phi(e_{0})}p_{1}$.

An execution pomset $E$ is a phased execution of $P\in\mathcal{P}_{TSO}$ if
$P=\pi_{2}(E)$. Let
$\mathcal{P}_{\mathcal{E}}(P)=\bigcup_{\sigma\in\Sigma}\\{E\in\mathcal{P}_{\mathcal{E}}(\sigma)\mid\pi_{2}(E)=P\\}$
be the set of execution pomsets of $P$.

This definition captures the “termination” axiom [SPA92, p. 283] that
guarantees fair executions. A pomset $P$ satisfies this axiom if for all write
actions $w$ to $x$ and all infinite sequences
$r_{1}<_{P}r_{2}<_{P}r_{3}<_{P}\cdots$ of read actions from $x$, there exists
a $j$ such that $w<_{P}r_{j}$. This axiom prohibits, e.g., the non-terminating
execution of the program $y:=1\operatorname{{\|}}\mathbf{while}\ y=0\
\mathbf{do}\ \mathbf{skip}$. For every
$E\in\mathcal{P}_{\mathcal{E}}(\sigma)$, $\pi_{2}(E)$ satisfies the
termination axiom. Indeed, consider a write action $w$ and an infinite
sequence ${\\{r_{i}\\}}_{i\in\mathbb{N}}$ in $\pi_{2}(E)$. There exists an
$e\in E$ such that $w\in e$. Because each of the pomsets in $E$ is finite and
$E$ is linear, there exists an $e^{\prime}$ and an $i$ such that
$e<_{E}e^{\prime}$ and $r_{i}\in e^{\prime}$. Then $w<_{\pi_{2}(E)}r_{i}$ by
definition.

######  Proposition 15.

We can characterize phased executions of pomsets $P$ as follows:

  1. (1)

if $P$ is finite, then every $E$ in $\mathcal{P}_{\mathcal{E}}(P)$ is finite;

  2. (2)

if some $E\in\mathcal{P}_{\mathcal{E}}(P)$ is finite, then $P$ is finite;

  3. (3)

if $P$ is finite, $(\sigma,\tau)\in\mathcal{E}(P)$, then
$(\sigma,P,\tau)\in\mathcal{P}_{\mathcal{E}}(P)$;

  4. (4)

if
$\\{(\sigma_{1},P_{1},\tau_{2})\\};\cdots;\\{(\sigma_{n},P_{n},\tau_{n})\\}\in\mathcal{P}_{\mathcal{E}}(P)$
is finite, then $P=P_{1};\cdots;P_{n}$,
$\sigma_{i+1}=\left[\sigma_{i}\mid\tau_{i}\right]$ for $1\leq i<n$, and
$(\sigma_{1},\left[\sigma_{1}\mid\tau_{1}\mid\cdots\mid\tau_{n}\right])\in\mathcal{E}(P)$.

##  4\. Soundness and Completeness

We show that our denotational account of TSO in Section 3 is sound and
complete relative to the axiomatic account of Section 2. Soundness implies
that we capture only behaviours permitted by the axiomatic account;
completeness implies that we capture all behaviours permitted by the axiomatic
account. Because all TSO-consistent orders are contained in TSO-consistent
total orders by Corollary 2 and can be obtained by weakening these, it is
sufficient to show that we capture all TSO-consistent total orders. We
identify total orders and lists.

###  4.1. Soundness

We call a function
$f:\mathrm{Pom}({\mathcal{A}_{PO}})\to\wp({\mathcal{A}_{PO}}~{}\mathsf{list})$
sound when for every program $p$ and finite pomset
$P\in{\mathcal{P}_{PO}}(p)$, if $L\in f(P)$, then $L$ is TSO-consistent with
$P$.

We will construct such an $f$ and show that it is sound in this subsection,
and we will show that it is complete in the next subsection. We begin by
giving an important characterization of pomsets for programs.

######  Lemma 16.

For every program $p$ and pomset $P\in\mathcal{P}_{TSO}(p)$, there exists an
order isomorphism $\omega:P{\restriction}_{\mathcal{A}_{b}}\to
P{\restriction}_{\mathcal{A}_{w}}$ such that if $\omega(\bar{x}:=v)=(y:=w)$,
then $y=x$ and $w=v$, and such that for all $b\in
P{\restriction}_{\mathcal{A}_{b}}$, we have $b<_{P}\omega(b)$. ∎

For programs, this means that global writes appear after the corresponding
write to the buffer, that global writes occur in the same order as the writes
to the buffer, and that all writes to the buffer give rise to global writes.
We call a series-parallel TSO pomset for which such an $\omega$ exists for
each of its SP components well-balanced; these “patch together” to form an
$\omega$ for the entire pomset. Given a program $p$, all TSO pomsets in
$\mathcal{P}_{TSO}(p)$ are well-balanced, and finite
$P\in\mathcal{P}_{TSO}(p)$ have a unique such $\omega$. We assume in the rest
of this section that our TSO pomsets are well-balanced.

Consider the function
$U:\mathrm{Pom}({\mathcal{A}_{TSO}})\to\mathrm{Pom}({\mathcal{A}_{PO}})$ that
takes each TSO pomset to its underlying program order. It does so by first
deleting all global write actions, and then relabelling all buffer write
actions $\bar{x}:=v$ by corresponding global write actions $x:=v$. We identify
all reads in $P$ with the corresponding reads in $U(P)$ and
$(x:=v)=\omega(\bar{x}:=v)$ with the write $x:=v$ below $\bar{x}:=v$. We can
imagine $U$ and the identifications as being given in the following diagram,
where dashed arrows indicate identifications, solid arrows indicate the pomset
orders, and the $\lambda_{j}$ are arbitrary read actions:

$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\bar{x}:=v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{i+2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{k}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x:=v\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{k+2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{U}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{i}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{x:=v\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{i+2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{k}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\lambda_{k+2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\cdots}$$\textstyle{U(P)}$

By observing that the PO pomset clauses are essentially special cases of the
TSO pomset clauses, we have that for all programs $p$,
$U(\mathcal{P}_{TSO}(p))\subseteq{\mathcal{P}_{PO}}(p)$. This inclusion is
actually an equality, because given any program order $P$ for $p$, we can
construct a TSO pomset $P^{\prime}$ such that $U(P^{\prime})=P$ by immediately
flushing the buffer with $\operatorname{split}$ after every write, i.e., by
replacing all occurrences of $x:=v$ in $P$ with $\bar{x}:=v\to x:=v$ to get
$P^{\prime}$.

Let the set $\mathcal{T}(P)$ of TSO-consistent total orders of
$P\in\mathrm{Pom}({\mathcal{A}_{TSO}})$ be given by

$\mathcal{T}(P)=\bigcup_{P^{\prime}\in
U^{-1}(P)}\\{\Lambda{\restriction}_{\mathcal{A}_{PO}}\mid\Lambda\in\operatorname{Lin}(P^{\prime})\land\llbracket
P^{\prime}\rrbracket^{\zeta}_{\Lambda}\neq\emptyset\\}.$

Informally, $\mathcal{T}(P)$ captures the linearisations of TSO pomsets in
$U^{-1}(P)$ that give rise to TSO executions of pomsets.

We will eventually show that $\mathcal{T}$ is sound. First, we prove a few
technical lemmas that will be useful in showing axiom (V) is satisfied. The
first implies that (Va) is satisfied.

######  Lemma 17.

Let $P$ be a TSO pomset and $\Lambda\in\Gamma(P)$ such that $\llbracket
P\rrbracket^{\zeta}_{\Lambda}\neq\emptyset$. Let ${(x=v)}_{r}\in P$ be a read
action such that for all buffered write actions $b<_{P}{(x=v)}_{r}$, its
corresponding global write action $\omega(b)$ satisfies
$\omega(b)<_{P}{(x=v)}_{r}$. If there exists a write ${(x:=v^{\prime})}_{w}$
maximal under $<_{\Lambda}$ amongst all writes to $x$ in
${(x=v)}_{r}{\downarrow}_{\Lambda}$ and all global writes to $x$ in
${(x=v)}_{r}{\downarrow}_{P}$ are in
${(x:=v^{\prime})}_{w}{\downarrow}_{\Lambda}$, then $v^{\prime}=v$.

######  Proof 4.1.

By the remarks on page 3.4.2, it is sufficient to consider only linear pomsets
$P$. Let $\Lambda_{L}=r{\downarrow}_{\Lambda}\setminus r$, $\Lambda_{R}$ be
such that $\Lambda=\Lambda_{L};\Lambda_{R}$, $L=P\cap\Lambda_{L}$, and
$R=P\cap\Lambda_{R}$. Let $(g,b)=\operatorname{\chi}_{x}(P)$, then by Lemma
11, we have $g=b=0$. Consider some arbitrary footstep
$(\sigma,\tau)\in\llbracket P\rrbracket^{\zeta}_{\Lambda}$, and let
$(\sigma_{L},\tau_{L})\in\llbracket L\rrbracket_{\Lambda_{L}}$ and
$(\sigma_{R},\tau_{R})\in\llbracket R\rrbracket_{\Lambda_{R}}$ be the
footsteps combined by (Seq) to form $(\sigma,\tau)$. Then because
$\sigma_{L}\subseteq\sigma$ and $\zeta(\sigma)$, we have $\zeta(\sigma_{L})$.
Because $L$ has the same number of buffer writes to $\bar{x}$ as global writes
to $x$, we have $\operatorname{\chi}_{x}(L)=(0,0)$ by Lemma 11 and Proposition
8. So by Corollary 10, we get $\tau_{L}[\bar{x}]=\sigma[\bar{x}]=0$. By
Proposition 7, we then get $\tau_{L}(x)=v^{\prime}$, and also that
$\sigma_{R}(x)=v$. Because
$\left[\sigma_{L}\mid\tau_{L}\right]\mathrel{\Uparrow}\sigma_{R}$ by (Seq), we
conclude $v^{\prime}=v$.

The following lemma implies that (Vb) is satisfied.

######  Lemma 18.

Let $P$ be a TSO pomset and $\Lambda\in\Gamma(P)$ such that $\llbracket
P\rrbracket^{\zeta}_{\Lambda}\neq\emptyset$. Let ${(x=v)}_{r}\in P$ be a read
action such that there exists a buffered write action
$b^{\prime}<_{P}{(x=v)}_{r}$ writing to $x$. Let ${(\bar{x}:=v^{\prime})}_{b}$
be the maximal such $b^{\prime}$ with regards to $<_{P}$. If
${(x=v)}_{r}<_{P}\omega({(\bar{x}:=v^{\prime})}_{b})$, then $v=v^{\prime}$.

######  Proof 4.2.

It is again sufficient to consider only linear $P$. Let $\Lambda_{L}$,
$\Lambda_{R}$, $L$, $R$, $(\sigma_{L},\tau_{L})$, and $(\sigma_{R},\tau_{R})$
be as in the proof of Lemma 17. By Proposition 9, we have
$\tau_{L}[\bar{x}]=\sigma_{L}[\bar{x}]+b_{x}-g_{x}$, where $b_{x}$ and $g_{x}$
are the number of buffer writes and global writes to $x$ in $L$, respectively.
But $\sigma_{L}[\bar{x}]=\sigma[\bar{x}]=0$, and well-balancedness and the
last hypothesis imply $b_{x}>g_{x}$, so $\tau_{L}[\bar{x}]>0$ and
$\tau_{L}(\bar{x})=v^{\prime}_{m}$ for some $v$ and $m>0$. But
$\sigma_{R}(\bar{x})=v_{n}$ for some $v$ and $n$ as well. Because
$\left[\sigma_{L}\mid\tau_{L}\right]\mathrel{\Uparrow}\sigma_{R}$ by (Seq), we
conclude $v^{\prime}=v$.

######  Theorem 19.

The function $\mathcal{T}$ is sound.

######  Proof 4.3.

Let $p$ be an arbitrary program, and let $P^{\prime}\in{\mathcal{P}_{PO}}(p)$,
$P\in U^{-1}(P^{\prime})$, and $\Lambda\in\operatorname{Lin}(P)$ be arbitrary
such that there exists a $(\sigma,\tau)\in\llbracket
P\rrbracket^{\zeta}_{\Lambda}$. Let
$L=\Lambda{\restriction}_{\mathcal{A}_{PO}}$. We check the six axioms to show
that $L$ is TSO-consistent for $U(P)=P^{\prime}$ from $\sigma$.

Axiom (O). This is clearly satisfied, because $U$ leaves reads untouched, and
there is an order isomorphism between global writes in $P$ and global writes
in $U(P)$ by Lemma 16, and linearisations preserve all elements.

Axiom (Va). Let ${(x=v)}_{r}\in U(P)$ be an arbitrary read, and assume we have
some write ${(x:=v^{\prime})}_{w}$ maximal amongst all writes to $x$ in
${(x=v)}_{r}{\downarrow}_{L}$, and that all writes to $x$ in
${(x=v)}_{r}{\downarrow}_{U(P^{\prime})}$ are in
${(x:=v^{\prime})}_{w}{\downarrow}_{L}$. That’s to say, assume the hypotheses
to (Va) hold for ${(x=v)}_{r}$. We must show $v=v^{\prime}$. Because all
writes to $x$ in ${(x=v)}_{r}{\downarrow}_{U(P^{\prime})}$ are in
${(x:=v^{\prime})}_{w}{\downarrow}_{L}$, this means all buffer writes to $x$
in ${(x=v)}_{r}{\downarrow}_{\Lambda}$ are in
${(x:=v^{\prime})}_{w}{\downarrow}_{L}$. Because $w$ appears in $L$, it is a
global write, and so all of the corresponding global writes for the buffer
writes to $x$ in ${(x=v)}_{r}{\downarrow}_{\Lambda}$ are also in
${(x:=v^{\prime})}_{w}{\downarrow}_{L}$. Then we can apply Lemma 17 and
conclude $v=v^{\prime}$.

Axiom (Vb). Let ${(x=v)}_{r}\in U(P)$ be an arbitrary read. Assume there
exists a write ${(x:=v^{\prime})}_{w}$ to $x$ maximal under $<_{P}$ amongst
all writes to $x$ in ${(x=v)}_{r}{\downarrow}_{U(P)}$, but that
${(x=v)}_{r}<_{L}{(x:=v^{\prime})}_{w}$. We must show that $v^{\prime}=v$.
That ${(x:=v^{\prime})}_{w}<_{U(P)}{(x=v)}_{r}$ implies
${(\bar{x}:=v^{\prime})}_{w}<_{P}{(x=v)}_{r}$, and
${(x=v)}_{r}<_{L}{(x:=v^{\prime})}_{w}$ implies
${(x=v)}_{r}<_{P}\omega({(\bar{x}:=v^{\prime})}_{w})$. So by Lemma 18, we have
$v^{\prime}=v$.

Axiom (Vc). Let ${(x=v)}_{r}\in U(P)$ be an arbitrary read. If there exist no
writes ${(x:=v^{\prime})}_{w}<_{U(P)}{(x=v)}_{r}$ in $U(P)$, then there exist
no buffered writes ${(\bar{x}:=v^{\prime})}_{w}<_{P}{(x=v)}_{r}$ in $P$, and
so by Proposition 13, axiom (Vc) is satisfied.

Axiom (L). Consider some arbitrary read action $r\in U(P)$ and action $a$ such
that $r<_{U(P)}a$. Because linearisation preserves order, it is sufficient to
show that $r<_{P}a$. If $a$ is also a read action, then $U$ leaves $a$
untouched, and so $r<_{p}a$. If $a$ is a write action, then there exists a
corresponding buffered write $a^{\prime}$ in $P$ such that $r<_{P}a^{\prime}$
and $\omega(a^{\prime})=a$. By Lemma 16, $a^{\prime}<\omega(a^{\prime})$, so
$r<_{P}a$ by transitivity.

Axiom (S). Lemma 16 implies there exists an order isomorphism between
$P{\restriction}{\mathcal{A}_{w}}$ and $U(P){\restriction}{\mathcal{A}_{w}}$,
so $w<_{P}w^{\prime}$ implies $w<_{U(P)}w^{\prime}$. Linearisation preserves
order, so $w<_{U(P)}w^{\prime}$ implies $w<_{\Lambda}w^{\prime}$. Because $w$
and $w^{\prime}$ are global writes, $w<_{L}w^{\prime}$ as desired.

Axiom (F). Let $\alpha_{1},\alpha_{2},\alpha_{3}\in U(P)$ be arbitrary such
that $\alpha_{1}<_{U(P)}\alpha_{3}$, $\alpha_{1}<_{U(P)}\alpha_{3}$, and
$\alpha_{2}\mathrel{\operatorname{{\|}}}_{U(P)}\alpha_{3}$. If $\alpha_{1}$ is
a write, then it is sufficient to observe that by the definition of TSO
pomsets for parallel compositions of expressions or commands, for any buffered
write $b$ such that $b<_{P}\alpha_{2}$ and $b<_{P}\alpha_{3}$ for some
$\alpha_{2}\mathrel{\operatorname{{\|}}}_{P}\alpha_{3}$, we have
$\omega(b)<_{P}\alpha_{2}$ and $\omega(b)<_{P}\alpha_{3}$. For then
$\alpha_{1}<_{L}\alpha_{2}$ and $\alpha_{1}<\alpha_{3}$. If $\alpha_{1}$ is a
read, then we are done by (L).

Axiom (J). Let $\alpha_{1},\alpha_{2},\alpha_{3}\in U(P)$ be arbitrary such
that $\alpha_{1}<_{U(P)}\alpha_{3}$, $\alpha_{2}<_{U(P)}\alpha_{3}$, and
$\alpha_{1}\mathrel{\operatorname{{\|}}}_{U(P)}\alpha_{2}$. If $\alpha_{1}$
and $\alpha_{2}$ are reads, then we are done by (L), so assume without loss of
generality that $\alpha_{1}$ is some write ${(x:=v)}_{w}$. Then $\alpha_{1}$
corresponds to some buffered write ${(\bar{x}:=v)}_{w}$ in $P$. By the dual
observation to that in (F), we have that if $b$ is a buffered write such that
for some $a$ and $c$, $a<_{P}c$ and $b<_{P}a$ but
$a\mathrel{\operatorname{{\|}}}_{P}b$, then $\omega(b)<_{P}a$. So we get
$\alpha_{1}<_{L}\alpha_{3}$ as desired. A symmetric argument applies when
$\alpha_{2}$ is a write.

###  4.2. Completeness

We call a function
$f:\mathrm{Pom}({\mathcal{A}_{PO}})\to\wp({\mathcal{A}_{PO}}~{}\mathsf{list})$
complete when for every program $p$ and finite pomset
$P\in{\mathcal{P}_{PO}}(p)$, if $L\in{\mathcal{A}_{PO}}~{}\mathsf{list}$ is
TSO-consistent with $P$, then $L\in f(P)$.

Our goal is to show that $\mathcal{T}$ is complete. To do so, we first
construct a pomset $s(P,L)\in U^{-1}(P)$ for any
$P\in\mathrm{Pom}({\mathcal{A}_{PO}})$ and total order $L$ that is TSO-
consistent with $P$. Let the underlying set $s(P,L)$ be given by
$\\{0\\}\times P\cup\\{1\\}\times P{\restriction}_{\mathcal{A}_{w}}$. Let
$\Phi_{s(P,L)}$ be given by $\Phi_{s(P,L)}((i,p))=(\bar{x}:=v)$ if both $i=0$
and $\Phi_{P}(p)=(x:=v)$, and $\Phi_{s(P,L)}((i,p))=\Phi_{P}(p)$ otherwise.
Intuitively, $<_{s(P,L)}$ merges the global writes into the program order in
the places specified by $L$. Let $<_{s(P,L)}$ be the least strict partial
order generated by the following collection of inequalities:  (i)
$(0,p)<_{s(P,L)}(0,p^{\prime})$if $p<_{P}p^{\prime}$;  (ii)
$(1,w)<_{s(P,L)}(1,w^{\prime})$if $w\mathrel{{\leq}{\geq}}_{P}w^{\prime}$ and
$w<_{L}w^{\prime}$;  (iii) $(0,w)<_{s(P,L)}(1,w)$if $w\in
P{\restriction}_{\mathcal{A}_{w}}$;  (iv) $(0,p)<_{s(P,L)}(1,w)$if
$p\mathrel{{\leq}{\geq}}_{P}w$ and $p<_{L}w$; and  (v)
$(1,w)<_{s(P,L)}(0,p)$if $w\mathrel{{\leq}{\geq}}_{P}p$ and $w<_{L}p$.  We
identify the program order actions in $P$ with their corresponding instances
in $s(P,L)$, that is, we identify all read actions $r$ of $P$ with $(0,r)$ in
$s(P,L)$, and all global write actions $w$ of $P$ with the global write action
$(1,w)$ in $s(P,L)$. We leverage this identification below to lift $L$ from
$P$ to $s(P,L)$.

The proof of completeness can be broken down into three lemmas as follows:

######  Lemma 20.

If $p$ is a program, $P\in{\mathcal{P}_{PO}}(p)$, and $L$ is TSO-consistent
with $P$, then $s(P,L)\in\mathcal{P}_{TSO}(p)$ and $U(s(P,L))=P$. ∎

######  Lemma 21.

If $P\in\mathrm{Pom}({\mathcal{A}_{PO}})$ and $L$ is TSO-consistent with $P$,
there exists a $\Lambda\in\operatorname{Lin}(s(P,L))$ such that
$\Lambda{\restriction}_{\mathcal{A}_{PO}}=L$. ∎

######  Lemma 22.

If $p$ is a program, $P\in\mathcal{P}_{TSO}(p)$, $L_{0}\in\mathsf{Ls}$, $L$ is
TSO-consistent with $U(P)\operatorname{{\|}}L_{0}$,
$\Lambda\in\operatorname{Lin}(P\operatorname{{\|}}L_{0})$, and
$\Lambda{\restriction}_{\mathcal{A}_{PO}}=L$, then $\llbracket
P\rrbracket^{\zeta}_{\Lambda}\neq\emptyset$. ∎

The presence of $L_{0}$ in the statement of Lemma 22 lets us use an induction
hypothesis in the case where $P$ is a parallel composition of pomsets, because
when we want to apply the induction hypothesis to one of the pomsets, we need
to be able to reference the global writes in the other pomset.

######  Theorem 23.

The function $\mathcal{T}$ is complete.

######  Proof 4.4.

Given a program $p$, a $P\in{\mathcal{P}_{PO}}(P)$ and an $L$ that is TSO-
consistent with $P$, we have by Lemma 20 that $s(P,L)\in U^{-1}(P)$. By Lemma
21, we have a $\Lambda\in\operatorname{Lin}(s(P,L))$ such that
$\Lambda{\restriction}_{\mathcal{A}_{PO}}=L$. By Lemma 22 with
$L_{0}={{[\,\,]}}$, $\llbracket
s(P,L)\rrbracket^{\zeta}_{\Lambda}\neq\emptyset$. So $L\in\mathcal{T}(P)$, and
we conclude completeness.

##  5\. Related Work

Other approaches to semantics for weak memory models mostly use execution
graphs and operational semantics. Execution graphs [BOS+11, BA08] serve to
describe the executional behaviour of an entire program, an inherently non-
modular approach. We see our denotational framework as offering an alternative
basis for program analysis, compositional and modular by design. Boudol and
Petri [BP09] gave an operational semantics framework for weak memory models
that uses buffered states. Jagadeesan et al. [JPR12] adapted a fully abstract,
trace-based semantics by Brookes [Bro96] to give a fully abstract denotational
semantics for TSO. Higham and Kawash [HK00] gave an axiomatic semantics for
TSO using linearizations. They showed their semantics to be equivalent to an
abstract machine with buffers based on the informal description in [SPA92].
Their account does not consider forking and joining of processes. Demange et
al. [DLZ+13] proposed a tractable memory model consistent with the Java Memory
Model. They give an operational semantics using buffers and an axiomatic
account and show the two to be equivalent. Sewell et al. [SSO+10] gave a TSO-
like memory model for x86, formalized in HOL4. Alglave et al. [AMT14] gave a
generic axiomatic framework for describing weak memory models and showed how
to specialize it to various memory models. Jeffrey and Riely [JR19] give a
denotational account of relaxed memory models using event structures.

Pratt [Pra86] was the first to generalize from traces to pomsets in the study
of concurrency. He introduced the parallel composition operations we presented
in Section 3 and he used pomsets in the study of concurrent processes.
Building on Pratt’s work, Brookes [Bro15, Bro16a, Bro16b] introduced a pomset
framework to study weak memory. This framework used Pratt’s parallel
composition operator, and its sequential composition is a variant of Pratt’s
concatenation operation. The TSO semantics given above builds on Brookes’s
work. The key technical differences involve adapting pomset semantics to
incorporate state equipped with abstract buffers, with careful accounting to
deal properly with order relaxations allowed by TSO. Our formal axiomatization
of SPARC TSO, including full treatment of forks and joins, is a crucial part
of the set-up, allowing us to be precise about the relationship between our
abstract denotational semantics and the more concrete and informal
characterization of TSO that appears in the manual.

##  6\. Conclusion

Our denotational semantics accurately captures the behaviours of SPARC TSO,
and its compositionality enables us reason modularly about programs. The main
strength of the pomset approach is its conceptual simplicity. Unlike trace
semantics, which include irrelevant orderings of actions, our pomset semantics
specifies only relevant orderings of actions. Its simplicity also makes it
readily adaptable to other memory models. For example, to capture SPARC PSO,
which relaxes TSO to provide only per-location global orders on writes, we
conjecture that it is sufficient to replace the single buffer parameter $L$ in
the $\mathcal{B}_{L}$ semantic clauses with families
${\\{L_{x}\\}}_{x\in\mathrm{Loc}}$ of buffers, and to then modify the buffer
flushing clauses in the obvious manner and to handle store barrier “stbar”
commands. Memory models provided by modern processors are often much weaker
than TSO and PSO. To model these, we conjecture that it is sufficient to
specify the correct set of actions, and to modify the semantic clauses
generating pomsets and footsteps accordingly. We believe pomset semantics
provide fertile ground for future research in semantics for weak memory
models.

## Acknowledgements

This paper is an extended version of one [KB18] presented at MFPS XXXIII. The
authors gratefully acknowledge feedback from anonymous reviewers and from
André Platzer.

## References

  * [AMT14] Jade Alglave, Luc Maranget, and Michael Tautschnig.  Herding cats: Modelling, simulation, testing, and data mining for weak memory.  ACM Trans. Program. Lang. Syst., 36(2):7:1–7:74, July 2014.
  * [BA08] Hans-J. Boehm and Sarita V. Adve.  Foundations of the C++ concurrency memory model.  In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’08, pages 68–78, New York, NY, USA, 2008. ACM.
  * [BOS+11] Mark Batty, Scott Owens, Susmit Sarkar, Peter Sewell, and Tjark Weber.  Mathematizing C++ concurrency.  In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’11, pages 55–66, New York, NY, USA, 2011. ACM.
  * [BP09] Gérard Boudol and Gustavo Petri.  Relaxed memory models: An operational approach.  In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’09, pages 392–403, New York, NY, USA, 2009. ACM.
  * [Bro96] Stephen Brookes.  Full abstraction for a shared variable parallel language.  Information and Computation, 127:145–163, 1996.
  * [Bro15] Stephen Brookes.  Partial order semantics and weak memory.  Invited talk, Domains XII, Boole Symposium, University of Cork, August 2015.
  * [Bro16a] Stephen Brookes.  A denotational semantics for weak memory concurrency.  Invited talk, Mathematical Foundations of Computer Science, May 2016\.
  * [Bro16b] Stephen Brookes.  A denotational semantics for weak memory concurrency.  Midlands Graduate School in the Foundations of Computing Science, April 2016.
  * [DLZ+13] Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, and Jan Vitek.  Plan B: A buffered memory model for Java.  In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’13, pages 329–342, New York, NY, USA, 2013. ACM.
  * [HK00] Lisa Higham and Jalal Kawash.  Memory consistency and process coordination for SPARC multiprocessors.  In Proceedings of the 7th International Conference on High Performance Computing, HiPC ’00, pages 355–366, London, UK, UK, 2000. Springer-Verlag.
  * [JPR12] Radha Jagadeesan, Gustavo Petri, and James Riely.  Brookes is relaxed, almost!  In Proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS’12, pages 180–194, Berlin, Heidelberg, 2012. Springer-Verlag.
  * [JR19] Alan Jeffrey and James Riely.  On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory.  Logical Methods in Computer Science, 15(1), March 2019.