An earlier version of this paper appeared in LICS2016.

# On Thin Air Reads: Towards an Event Structures Model of Relaxed Memory

Alan Jeffrey  Mozilla Research  and  James Riely  DePaul University

###### Abstract.

To model relaxed memory, we propose _confusion-free event structures_ over an
alphabet with a _justification_ relation. Executions are modeled by
_justified_ configurations, where every read event has a justifying write
event. Justification alone is too weak a criterion, since it allows cycles of
the kind that result in so-called thin-air reads. _Acyclic justification_
forbids such cycles, but also invalidates event reorderings that result from
compiler optimizations and dynamic instruction scheduling. We propose the
notion of _well-justification_ , based on a game-like model, which strikes a
middle ground.

We show that well-justified configurations satisfy the _DRF theorem_ : in any
data-race free program, all well-justified configurations are sequentially
consistent. We also show that _rely-guarantee reasoning_ is sound for well-
justified configurations, but not for justified configurations. For example,
well-justified configurations are _type-safe_.

Well-justification allows many, but not all reorderings performed by relaxed
memory. In particular, it fails to validate the commutation of independent
reads. We discuss variations that may address these shortcomings.

###### Key words and phrases:

Relaxed Memory, Event Structures

##  1\. Introduction

The last few decades have seen several attempts to define a suitable semantics
for shared-memory concurrency under relaxed assumptions; see Batty et al.
[2015] for a recent summary. _Event structures_ [Winskel 1986] provide a way
to visualize all of the conflicting executions of a program as a single
semantic object. In this paper, we exploit the visual nature of event
structures to provide a fresh approach to relaxed memory models.

Consider a simple programming language where all values are booleans,
registers (ranged over by r) are thread-local and variables (ranged over by x
and y) are global. In order to define the semantics compositionally, variable
read is defined as a choice among the possible values that might be read. For
example, the event structure for (r=x; y=r;) is as follows.

$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{W}\smash{{y}\,0}$$\mathsf{W}\smash{{y}\,1}$

Register values are resolved via substitution and therefore do not appear in
the event structure. The arrows represent program order, and the zigzag
represents a primitive conflict. If two events are in conflict, then all
following events are also in conflict.

This structure has two maximal conflict-free _configurations_ , which
represent a possible execution of the program:

$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,0}$ and
$\displaystyle\leavevmode\hbox to99.81pt{\vbox
to15.84pt{\pgfpicture\makeatletter\hbox{\hskip 11.03302pt\lower-7.92188pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{ { {}{}{}}{}{
{}{}{}} {}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.1041pt}{-20.89304pt}\pgfsys@lineto{-15.6041pt}{-18.39304pt}\pgfsys@lineto{-10.6041pt}{-23.39304pt}\pgfsys@lineto{-5.6041pt}{-18.39304pt}\pgfsys@lineto{-0.6041pt}{-23.39304pt}\pgfsys@lineto{4.3959pt}{-18.39304pt}\pgfsys@lineto{9.3959pt}{-23.39304pt}\pgfsys@lineto{14.3959pt}{-18.39304pt}\pgfsys@lineto{19.3959pt}{-23.39304pt}\pgfsys@lineto{21.8959pt}{-20.89304pt}\pgfsys@lineto{32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{6.83302pt}{6.6723pt}\pgfsys@lineto{-6.83302pt}{6.6723pt}\pgfsys@curveto{-9.04219pt}{6.6723pt}{-10.83302pt}{4.88147pt}{-10.83302pt}{2.6723pt}\pgfsys@lineto{-10.83302pt}{-2.6723pt}\pgfsys@curveto{-10.83302pt}{-4.88147pt}{-9.04219pt}{-6.6723pt}{-6.83302pt}{-6.6723pt}\pgfsys@lineto{6.83302pt}{-6.6723pt}\pgfsys@curveto{9.04219pt}{-6.6723pt}{10.83302pt}{-4.88147pt}{10.83302pt}{-2.6723pt}\pgfsys@lineto{10.83302pt}{2.6723pt}\pgfsys@curveto{10.83302pt}{4.88147pt}{9.04219pt}{6.6723pt}{6.83302pt}{6.6723pt}\pgfsys@closepath\pgfsys@moveto{-10.83302pt}{-6.6723pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.50002pt}{-3.3393pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathsf{init}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{45.30869pt}{6.74966pt}\pgfsys@lineto{25.23303pt}{6.74966pt}\pgfsys@curveto{23.02386pt}{6.74966pt}{21.23303pt}{4.95883pt}{21.23303pt}{2.74966pt}\pgfsys@lineto{21.23303pt}{-2.74966pt}\pgfsys@curveto{21.23303pt}{-4.95883pt}{23.02386pt}{-6.74966pt}{25.23303pt}{-6.74966pt}\pgfsys@lineto{45.30869pt}{-6.74966pt}\pgfsys@curveto{47.51785pt}{-6.74966pt}{49.30869pt}{-4.95883pt}{49.30869pt}{-2.74966pt}\pgfsys@lineto{49.30869pt}{2.74966pt}\pgfsys@curveto{49.30869pt}{4.95883pt}{47.51785pt}{6.74966pt}{45.30869pt}{6.74966pt}\pgfsys@closepath\pgfsys@moveto{21.23303pt}{-6.74966pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.56604pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{R}\,\smash{{x}\,1}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{84.58073pt}{7.72188pt}\pgfsys@lineto{63.7087pt}{7.72188pt}\pgfsys@curveto{61.49953pt}{7.72188pt}{59.7087pt}{5.93105pt}{59.7087pt}{3.72188pt}\pgfsys@lineto{59.7087pt}{-3.72188pt}\pgfsys@curveto{59.7087pt}{-5.93105pt}{61.49953pt}{-7.72188pt}{63.7087pt}{-7.72188pt}\pgfsys@lineto{84.58073pt}{-7.72188pt}\pgfsys@curveto{86.7899pt}{-7.72188pt}{88.58073pt}{-5.93105pt}{88.58073pt}{-3.72188pt}\pgfsys@lineto{88.58073pt}{3.72188pt}\pgfsys@curveto{88.58073pt}{5.93105pt}{86.7899pt}{7.72188pt}{84.58073pt}{7.72188pt}\pgfsys@closepath\pgfsys@moveto{59.7087pt}{-7.72188pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.0417pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{W}\smash{{y}\,1}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{11.03302pt}{0.0pt}\pgfsys@lineto{20.57304pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.57304pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{49.50868pt}{0.0pt}\pgfsys@lineto{59.0487pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{59.0487pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
If we suppose that this code fragment is embedded in a larger program, the two
configurations are equally sensible: $x$ could be anything. However, if we
take $\mathsf{init}$ to be the top-level initialization of the program and
suppose that variables are initialized to $0$, then the first configuration
above seems sensible, whereas the second does not: $x$ must be $0$.

A read event is _justified_ by a matching _visible_ write, drawn with a dashed
arrow in the above configurations. Writes are _hidden_ if they occur later or
are blocked by an intervening write. When modeling executions of whole
programs, one expects that all reads in a configuration must be justified.

In a happens-before model [Manson et al. 2005], all concurrent writes are
visible, making this notion of justification quite permissive. Consider a
program with two threads and the corresponding event structure, with events
numbered for reference.

(r1=x; y=r1;) || (r2=y; x=r2;) ($P_{1}$)
$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,1}$12$\mathsf{R}\,\smash{{x}\,0}$11$\mathsf{W}\smash{{y}\,0}$15$\mathsf{W}\smash{{y}\,1}$16$\mathsf{R}\,\smash{{y}\,0}$13$\mathsf{R}\,\smash{{y}\,1}$14$\mathsf{W}\smash{{x}\,0}$17$\mathsf{W}\smash{{x}\,1}$18

Here, the events that are neither ordered nor in conflict are concurrent. The
event structure for $P_{1}$ has the following configuration, in which every
read event is justified by a matching write that is either before it, or
concurrent:

$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,0}$11$\mathsf{W}\smash{{y}\,0}$15$\mathsf{R}\,\smash{{y}\,0}$13$\mathsf{W}\smash{{x}\,0}$17
$C_{0}$

Unfortunately, the event structure also has a configuration in which there is
a cycle in justification-and-program-order:

$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,1}$12$\mathsf{W}\smash{{y}\,1}$16$\mathsf{R}\,\smash{{y}\,1}$14$\mathsf{W}\smash{{x}\,1}$18
$C_{1}$

Due to the cycle, any available value can be so justified, thus arising “out
of thin air”. Some memory models have undefined semantics in the presence of
such data races [Batty et al. 2011]. In the absence of such undefined
behaviors, however, languages that claim memory safety must disallow thin-air
values in order to preserve type safety.

Unfortunately, cycles such as those in configuration $C_{1}$ cannot be banned
outright without also banning useful program transformations, such as
instruction reordering. For example, consider the following program.

(r1=x; y=1;) || (r2=y; x=1;) ($P_{2}$)

The event structure for $P_{2}$ is the same as that for $P_{1}$ except that
all writes have value $1$. Thus, $P_{2}$ also allows configuration $C_{1}$.
Clearly, if the order of the two instructions is swapped in either thread of
$P_{2}$, then it is possible for both threads to read $1$. Since program
transformations may not introduce new behaviors, $C_{1}$ must also be
considered a valid configuration of the original program.

There are several models in the literature designed to allow configuration
$C_{1}$ for $P_{2}$, yet deny it for $P_{1}$. Roughly these can be divided
into two approaches: working with multiple executions [Manson et al. 2005;
Jagadeesan et al. 2010] or working with axioms and rewrite rules [Cenciarelli
et al. 2007; Saraswat et al. 2007; Pichon-Pharabod and Sewell 2016].

We propose a new approach, based on two-player games. The game is as follows:
we start in configuration $C$, and the player’s goal is to extend it to
configuration $D$. The opponent picks a configuration $C^{\prime}$ which
includes $C$, and whose new events are acyclically justified. The player then
picks a configuration $C^{\prime\prime}$ which includes $C^{\prime}$, and
whose new events are also acyclically justified. If $C^{\prime\prime}$
justifies $D$ then the player has won, otherwise the opponent has won. If the
player has a winning strategy for this game, we say that $C$ _Always
Eventually (AE) justifies_ $D$.

From this game, we can define the _well-justified_ configurations inductively:
$\emptyset$ is well-justified; if $C$ is well-justified and $C$ AE-justifies
$D$ then $D$ is well-justified.

Consider the following program, $P_{3}$.

r1=x; y=1; || r2=y; x=r2; ($P_{3}$)
$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{R}\,\smash{{x}\,0}$31$\mathsf{W}\smash{{y}\,1}$35$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,0}$33$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,0}$37$\mathsf{W}\smash{{x}\,1}$38

We show that both reads may be resolved to $1$ in the well-justified
configuration
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}32},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}36},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>In this case the cyclic justifier models a valid execution, caused by a
compiler or hardware optimization reordering (r1=x; y=1;) as (y=1; r1=x;).

We first show that $\emptyset$ AE-justifies
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>The opponent may choose any configuration acyclically justified from
$\emptyset$; the interesting choices are the maximal configurations
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}31},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}33},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}35},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
}\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}31},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}35},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Since both of these include
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>which justifies
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>the player does not have to add any events to justify
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Note that $\emptyset$ does _not_ AE-justify
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>since the opponent can choose the configuration
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}31},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}35},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}33},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
We now show that the configuration
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>AE-justifies
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}32},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}36},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>The opponent may choose any configuration acyclically justified from
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>since any choice includes
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>which justifies
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>the player does not have to add any events to justify
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}32},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}36},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>We have thus shown a cyclic configuration similar to $C_{1}$ is well-justified
for $P_{3}$.

$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,1}$38

This reasoning fails for configuration $C_{1}$ of $P_{1}$. In this case, the
player is unable to establish that $\emptyset$ AE-justifies
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}14},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>We provide a proof in §5. Intuitively, the only maximal configuration
available to the opponent is
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}11},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}13},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}15},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and this fails to justify
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>since there is no write of $1$ to $y$.

We review the literature on _confusion-free event structures_ in §2. In §3 we
define well-justification and provide further examples. We give the definition
for a Java-like happens-before model [Manson et al. 2005]. We discuss
synchronization actions, such as locks, in §6.

Perhaps the most important property of a relaxed memory model is _DRF_ : that
programs without data races behave as they would with strong memory—that is,
as they would with sequentially consistent memory [Lamport 1979]. In §4, we
describe our proof of the DRF theorem, which we have verified in Agda.

In §5, we show that invariant reasoning is possible using our definition. We
state a general theorem—also verified in Agda—which is sufficient to establish
type safety for static allocation.

We describe some of the limitations of our definition in §7. While the
definition presented here is a step in the right direction, it fails to
validate common reorderings, such as the reordering of reads on different
variables. We give an alternative definition that is better behaved on the
Java Memory Model causality test cases [Pugh 2004]. The induction principle
used in our proof of DRF fails for this alternative definition.

The paper ends with a discussion of related work and open problems.

The Agda development for this paper is available https://perma.cc/WAC3-JLXV.

##  2\. Event Structures

Event structures were introduced by Winskel [1988] as a non-interleaving model
of concurrency. They are notable for providing a compact model of concurrent
systems, for example an event structure model for $n$ concurrent processes
will often have only $O(n)$ events, compared to the $O(2^{n})$ states in a
labeled transition system.

In this section, we review the definitions associated with conflict-free
labeled event structures, and their visualization as graphs. Readers familiar
with event structures can skip to §3, where the new material begins.

A _partial order_ $(E,{\leq})$ is a set $E$ (the _event set_) equipped with a
reflexive, transitive, antisymmetric relation ${\leq}$ (the _causal order_). A
_well order_ is a partial order that has no

0123

infinite decreasing sequence.

We visualize partial orders as directed acyclic graphs where edges denote
order. For example the order on $\\{0,1,2,3\\}$ where $0\leq 1\leq 2$ and
$0\leq 3$ is visualized on the right.

A _prime event structure_ $(E,{\leq},{\mathrel{\\#}})$ is a well order
together with a symmetric relation ${\mathrel{\\#}}$ on $E$ (the _conflict_
relation), such that if $c\mathrel{\\#}d\leq e$ then $c\mathrel{\\#}e$.

For any prime event structure, define the _primitive conflict_ relation
${\mathrel{\\#_{\mu}}}$ on $E$ as $d\mathrel{\\#_{\mu}}e$ whenever
$d\mathrel{\\#}e$ and for any $d\geq b\mathrel{\\#}c\leq e$ we have $d=b$ and
$c=e$. Primitive conflict is also known as _minimal_ conflict. A prime event
structure is _confusion-free_ [Nielsen et al. 1979] whenever
$\mathrel{\\#_{\mu}}$ is transitive, and if $c\leq d\mathrel{\\#_{\mu}}e$ then
$c\leq e$.

For any confusion-free event structure, define the _primitive conflict
equivalence_ $d\sim e$ whenever $d=e$ or $d\mathrel{\\#_{\mu}}e$. It is
routine to show that primitive conflict equivalence is symmetric and
transitive, and hence forms an equivalence on $E$.

0123

We visualize confusion-free event structures by including the primitive
conflict equivalence in the visualization. For example the event structure
which extends the previous partial order with $1\mathrel{\\#}3$ and
$2\mathrel{\\#}3$ has $1\sim 3$, so is visualized as on the right.

A _labeled event structure_ $(E,{\leq},{\mathrel{\\#}},\lambda)$ over a _label
set_ $\Sigma$ is a prime event structure together with a function
$\lambda:E\mathbin{\rightarrow}\Sigma$.

We visualize labeled event structures as node-labeled graphs. For example the
labeled event structure which extends the previous event structure with
labeling $\lambda(0)=\mathsf{init}$,
$\lambda(1)=(\mathsf{R}\,\smash{{x}\,0})$,
$\lambda(2)=(\mathsf{W}\smash{{y}\,1})$ and
$\lambda(3)=(\mathsf{R}\,\smash{{x}\,1})$ is visualized as follows.

$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{R}\,\smash{{x}\,1}$

For any prime event structure, a set $C\subseteq E$ is _conflict-free_
whenever there is no $d,e\in C$ such that $d\mathrel{\\#}e$. $C$ is _down-
closed_ whenever $d\leq e\in C$ implies $d\in C$. A _configuration_ is a set
which is conflict-free and down-closed.

Since configurations are conflict-free, they can be visualized as node-labeled
directed acyclic graphs, for example the two largest configurations for the
previous labeled event structure are

$\leavevmode\hbox to99.81pt{\vbox
to15.84pt{\pgfpicture\makeatletter\hbox{\hskip 11.03302pt\lower-7.92188pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{\hbox to0.0pt{\hbox
to0.0pt{\hbox to0.0pt{\hbox to0.0pt{\hbox to0.0pt{\hbox to0.0pt{ { {}{}{}}{}{
{}{}{}} {}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.1041pt}{-20.89304pt}\pgfsys@lineto{-15.6041pt}{-18.39304pt}\pgfsys@lineto{-10.6041pt}{-23.39304pt}\pgfsys@lineto{-5.6041pt}{-18.39304pt}\pgfsys@lineto{-0.6041pt}{-23.39304pt}\pgfsys@lineto{4.3959pt}{-18.39304pt}\pgfsys@lineto{9.3959pt}{-23.39304pt}\pgfsys@lineto{14.3959pt}{-18.39304pt}\pgfsys@lineto{19.3959pt}{-23.39304pt}\pgfsys@lineto{21.8959pt}{-20.89304pt}\pgfsys@lineto{32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-68.10417pt}{-20.89304pt}\pgfsys@lineto{-65.60417pt}{-18.39304pt}\pgfsys@lineto{-60.60417pt}{-23.39304pt}\pgfsys@lineto{-55.60417pt}{-18.39304pt}\pgfsys@lineto{-50.60417pt}{-23.39304pt}\pgfsys@lineto{-45.60417pt}{-18.39304pt}\pgfsys@lineto{-40.60417pt}{-23.39304pt}\pgfsys@lineto{-35.60417pt}{-18.39304pt}\pgfsys@lineto{-32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{46.12607pt}{-21.86525pt}\pgfsys@lineto{48.62607pt}{-19.36525pt}\pgfsys@lineto{51.12607pt}{-21.86525pt}\pgfsys@lineto{82.11516pt}{-21.86525pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-68.10417pt}{-20.89304pt}\pgfsys@lineto{-65.60417pt}{-18.39304pt}\pgfsys@lineto{-60.60417pt}{-23.39304pt}\pgfsys@lineto{-55.60417pt}{-18.39304pt}\pgfsys@lineto{-50.60417pt}{-23.39304pt}\pgfsys@lineto{-45.60417pt}{-18.39304pt}\pgfsys@lineto{-40.60417pt}{-23.39304pt}\pgfsys@lineto{-35.60417pt}{-18.39304pt}\pgfsys@lineto{-32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{46.12607pt}{-21.86525pt}\pgfsys@lineto{48.62607pt}{-19.36525pt}\pgfsys@lineto{51.12607pt}{-21.86525pt}\pgfsys@lineto{82.11516pt}{-21.86525pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.82457pt}{-15.4065pt}\pgfsys@lineto{-7.32457pt}{-12.9065pt}\pgfsys@lineto{-2.32457pt}{-17.9065pt}\pgfsys@lineto{2.67543pt}{-12.9065pt}\pgfsys@lineto{7.67543pt}{-17.9065pt}\pgfsys@lineto{10.17543pt}{-15.4065pt}\pgfsys@lineto{15.4065pt}{-15.4065pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.1041pt}{-20.89304pt}\pgfsys@lineto{-15.6041pt}{-18.39304pt}\pgfsys@lineto{-10.6041pt}{-23.39304pt}\pgfsys@lineto{-5.6041pt}{-18.39304pt}\pgfsys@lineto{-0.6041pt}{-23.39304pt}\pgfsys@lineto{4.3959pt}{-18.39304pt}\pgfsys@lineto{9.3959pt}{-23.39304pt}\pgfsys@lineto{14.3959pt}{-18.39304pt}\pgfsys@lineto{19.3959pt}{-23.39304pt}\pgfsys@lineto{21.8959pt}{-20.89304pt}\pgfsys@lineto{32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{6.83302pt}{6.6723pt}\pgfsys@lineto{-6.83302pt}{6.6723pt}\pgfsys@curveto{-9.04219pt}{6.6723pt}{-10.83302pt}{4.88147pt}{-10.83302pt}{2.6723pt}\pgfsys@lineto{-10.83302pt}{-2.6723pt}\pgfsys@curveto{-10.83302pt}{-4.88147pt}{-9.04219pt}{-6.6723pt}{-6.83302pt}{-6.6723pt}\pgfsys@lineto{6.83302pt}{-6.6723pt}\pgfsys@curveto{9.04219pt}{-6.6723pt}{10.83302pt}{-4.88147pt}{10.83302pt}{-2.6723pt}\pgfsys@lineto{10.83302pt}{2.6723pt}\pgfsys@curveto{10.83302pt}{4.88147pt}{9.04219pt}{6.6723pt}{6.83302pt}{6.6723pt}\pgfsys@closepath\pgfsys@moveto{-10.83302pt}{-6.6723pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.50002pt}{-3.3393pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathsf{init}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{45.30869pt}{6.74966pt}\pgfsys@lineto{25.23303pt}{6.74966pt}\pgfsys@curveto{23.02386pt}{6.74966pt}{21.23303pt}{4.95883pt}{21.23303pt}{2.74966pt}\pgfsys@lineto{21.23303pt}{-2.74966pt}\pgfsys@curveto{21.23303pt}{-4.95883pt}{23.02386pt}{-6.74966pt}{25.23303pt}{-6.74966pt}\pgfsys@lineto{45.30869pt}{-6.74966pt}\pgfsys@curveto{47.51785pt}{-6.74966pt}{49.30869pt}{-4.95883pt}{49.30869pt}{-2.74966pt}\pgfsys@lineto{49.30869pt}{2.74966pt}\pgfsys@curveto{49.30869pt}{4.95883pt}{47.51785pt}{6.74966pt}{45.30869pt}{6.74966pt}\pgfsys@closepath\pgfsys@moveto{21.23303pt}{-6.74966pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.56604pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{R}\,\smash{{x}\,0}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{84.58073pt}{7.72188pt}\pgfsys@lineto{63.7087pt}{7.72188pt}\pgfsys@curveto{61.49953pt}{7.72188pt}{59.7087pt}{5.93105pt}{59.7087pt}{3.72188pt}\pgfsys@lineto{59.7087pt}{-3.72188pt}\pgfsys@curveto{59.7087pt}{-5.93105pt}{61.49953pt}{-7.72188pt}{63.7087pt}{-7.72188pt}\pgfsys@lineto{84.58073pt}{-7.72188pt}\pgfsys@curveto{86.7899pt}{-7.72188pt}{88.58073pt}{-5.93105pt}{88.58073pt}{-3.72188pt}\pgfsys@lineto{88.58073pt}{3.72188pt}\pgfsys@curveto{88.58073pt}{5.93105pt}{86.7899pt}{7.72188pt}{84.58073pt}{7.72188pt}\pgfsys@closepath\pgfsys@moveto{59.7087pt}{-7.72188pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{63.0417pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{W}\smash{{y}\,1}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{11.03302pt}{0.0pt}\pgfsys@lineto{20.57304pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.57304pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} { {}{}{}}{}{ {}{}{}} {{{{{}}{
{}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{49.50868pt}{0.0pt}\pgfsys@lineto{59.0487pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{59.0487pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\quad\mbox{and}\quad\leavevmode\hbox
to60.54pt{\vbox to13.9pt{\pgfpicture\makeatletter\hbox{\hskip
11.03302pt\lower-6.94966pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\hbox to0.0pt{\hbox to0.0pt{\hbox
to0.0pt{\hbox to0.0pt{\hbox to0.0pt{\hbox to0.0pt{\hbox to0.0pt{ { {}{}{}}{}{
{}{}{}} {}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.1041pt}{-20.89304pt}\pgfsys@lineto{-15.6041pt}{-18.39304pt}\pgfsys@lineto{-10.6041pt}{-23.39304pt}\pgfsys@lineto{-5.6041pt}{-18.39304pt}\pgfsys@lineto{-0.6041pt}{-23.39304pt}\pgfsys@lineto{4.3959pt}{-18.39304pt}\pgfsys@lineto{9.3959pt}{-23.39304pt}\pgfsys@lineto{14.3959pt}{-18.39304pt}\pgfsys@lineto{19.3959pt}{-23.39304pt}\pgfsys@lineto{21.8959pt}{-20.89304pt}\pgfsys@lineto{32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-68.10417pt}{-20.89304pt}\pgfsys@lineto{-65.60417pt}{-18.39304pt}\pgfsys@lineto{-60.60417pt}{-23.39304pt}\pgfsys@lineto{-55.60417pt}{-18.39304pt}\pgfsys@lineto{-50.60417pt}{-23.39304pt}\pgfsys@lineto{-45.60417pt}{-18.39304pt}\pgfsys@lineto{-40.60417pt}{-23.39304pt}\pgfsys@lineto{-35.60417pt}{-18.39304pt}\pgfsys@lineto{-32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{46.12607pt}{-21.86525pt}\pgfsys@lineto{48.62607pt}{-19.36525pt}\pgfsys@lineto{51.12607pt}{-21.86525pt}\pgfsys@lineto{82.11516pt}{-21.86525pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-68.10417pt}{-20.89304pt}\pgfsys@lineto{-65.60417pt}{-18.39304pt}\pgfsys@lineto{-60.60417pt}{-23.39304pt}\pgfsys@lineto{-55.60417pt}{-18.39304pt}\pgfsys@lineto{-50.60417pt}{-23.39304pt}\pgfsys@lineto{-45.60417pt}{-18.39304pt}\pgfsys@lineto{-40.60417pt}{-23.39304pt}\pgfsys@lineto{-35.60417pt}{-18.39304pt}\pgfsys@lineto{-32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{46.12607pt}{-21.86525pt}\pgfsys@lineto{48.62607pt}{-19.36525pt}\pgfsys@lineto{51.12607pt}{-21.86525pt}\pgfsys@lineto{82.11516pt}{-21.86525pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {{}} } \pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-9.82457pt}{-15.4065pt}\pgfsys@lineto{-7.32457pt}{-12.9065pt}\pgfsys@lineto{-2.32457pt}{-17.9065pt}\pgfsys@lineto{2.67543pt}{-12.9065pt}\pgfsys@lineto{7.67543pt}{-17.9065pt}\pgfsys@lineto{10.17543pt}{-15.4065pt}\pgfsys@lineto{15.4065pt}{-15.4065pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss} { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}
{}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {}
}{{{{}{}{{}} }}{{}} {} }{{{{}{}{{}} }}{{}} {{}} }
\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.15,0.15,0.15}\pgfsys@color@gray@stroke{0.15}\pgfsys@invoke{
}{}\pgfsys@moveto{-18.1041pt}{-20.89304pt}\pgfsys@lineto{-15.6041pt}{-18.39304pt}\pgfsys@lineto{-10.6041pt}{-23.39304pt}\pgfsys@lineto{-5.6041pt}{-18.39304pt}\pgfsys@lineto{-0.6041pt}{-23.39304pt}\pgfsys@lineto{4.3959pt}{-18.39304pt}\pgfsys@lineto{9.3959pt}{-23.39304pt}\pgfsys@lineto{14.3959pt}{-18.39304pt}\pgfsys@lineto{19.3959pt}{-23.39304pt}\pgfsys@lineto{21.8959pt}{-20.89304pt}\pgfsys@lineto{32.34192pt}{-20.89304pt}\pgfsys@stroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }
{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{6.83302pt}{6.6723pt}\pgfsys@lineto{-6.83302pt}{6.6723pt}\pgfsys@curveto{-9.04219pt}{6.6723pt}{-10.83302pt}{4.88147pt}{-10.83302pt}{2.6723pt}\pgfsys@lineto{-10.83302pt}{-2.6723pt}\pgfsys@curveto{-10.83302pt}{-4.88147pt}{-9.04219pt}{-6.6723pt}{-6.83302pt}{-6.6723pt}\pgfsys@lineto{6.83302pt}{-6.6723pt}\pgfsys@curveto{9.04219pt}{-6.6723pt}{10.83302pt}{-4.88147pt}{10.83302pt}{-2.6723pt}\pgfsys@lineto{10.83302pt}{2.6723pt}\pgfsys@curveto{10.83302pt}{4.88147pt}{9.04219pt}{6.6723pt}{6.83302pt}{6.6723pt}\pgfsys@closepath\pgfsys@moveto{-10.83302pt}{-6.6723pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-7.50002pt}{-3.3393pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\mathsf{init}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{
{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,1}\pgfsys@color@rgb@fill{0.9}{0.9}{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{}\pgfsys@moveto{45.30869pt}{6.74966pt}\pgfsys@lineto{25.23303pt}{6.74966pt}\pgfsys@curveto{23.02386pt}{6.74966pt}{21.23303pt}{4.95883pt}{21.23303pt}{2.74966pt}\pgfsys@lineto{21.23303pt}{-2.74966pt}\pgfsys@curveto{21.23303pt}{-4.95883pt}{23.02386pt}{-6.74966pt}{25.23303pt}{-6.74966pt}\pgfsys@lineto{45.30869pt}{-6.74966pt}\pgfsys@curveto{47.51785pt}{-6.74966pt}{49.30869pt}{-4.95883pt}{49.30869pt}{-2.74966pt}\pgfsys@lineto{49.30869pt}{2.74966pt}\pgfsys@curveto{49.30869pt}{4.95883pt}{47.51785pt}{6.74966pt}{45.30869pt}{6.74966pt}\pgfsys@closepath\pgfsys@moveto{21.23303pt}{-6.74966pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{24.56604pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{R}\,\smash{{x}\,1}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{}{}{{}}\pgfsys@moveto{11.03302pt}{0.0pt}\pgfsys@lineto{20.57304pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.57304pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>
Given labeled event structures
$\textnormal{{ES}}_{1}=(E_{1},{\leq}_{1},{\mathrel{\\#}}_{1},\lambda_{1})$ and
$\textnormal{{ES}}_{2}=(E_{2},{\leq}_{2},{\mathrel{\\#}}_{2},\lambda_{2})$
(without loss of generality, we assume event sets $\textnormal{{ES}}_{1}$ and
$\textnormal{{ES}}_{2}$ are disjoint) define the _parallel composite_ event
structure $\textnormal{{ES}}_{1}\mathbin{\parallel}\textnormal{{ES}}_{2}$ as
having:

  * •

event set $E$ is $E_{1}\cup E_{2}$,

  * •

causal order $\leq$ is ${\leq_{1}}\cup{\leq_{2}}$,

  * •

conflict $\mathrel{\\#}$ is ${\mathrel{\\#}_{1}}\cup{\mathrel{\\#}_{2}}$, and

  * •

labeling $\lambda$ is $\lambda_{1}\cup\lambda_{2}$.

The _sum_ event structure $\textnormal{{ES}}_{1}+\textnormal{{ES}}_{2}$ is the
same except:

  * •

conflict $\mathrel{\\#}$ is
${\mathrel{\\#}_{1}}\cup{\mathrel{\\#}_{2}}\cup(E_{1}\times
E_{2})\cup(E_{2}\times E_{1})$.

We write $0$ for the empty event structure with event set $\emptyset$.

For a label $\sigma\in\Sigma$, the prefix $\sigma\bullet\textnormal{{ES}}_{0}$
introduces a new $\sigma$-labeled event ordered before all the events of
$\textnormal{{ES}}_{0}$. It is defined as having:

  * •

event set $E$ is $E_{0}\cup\\{\bot\\}$,

  * •

causal order $\leq$ is ${\leq_{0}}\cup(\\{\bot\\}\times E)$,

  * •

conflict $\mathrel{\\#}$ is $\mathrel{\\#}_{0}$, and

  * •

labeling $\lambda$ is $\lambda_{0}\cup\\{(\bot,\sigma)\\}$.

Using an appropriate alphabet (discussed in more detail in §3), we can give
the semantics of a simple shared-memory concurrent language. The construction
uses sum, parallel composition, prefix and the empty event structure.

Let $r$ range over _registers_. A _store_ maps registers to values. Let $\rho$
range over stores and $\rho_{0}$ be the initial store, which maps all
registers to $0$. We write $\rho[r\mathbin{↦}v]$ for store update:

$\rho[r\mathbin{↦}v](r^{\prime})=\begin{cases}v&\allowbreak\;\text{if}\;\allowbreak
r=r^{\prime}\\\
\rho(r^{\prime})&\allowbreak\;\text{otherwise}\allowbreak\end{cases}$

Let $M$ range over _expressions_ , which may include registers, but not
variables. Let $V$ be a set of _values_. Let
$\mathcal{M}\llbracket\cdot\rrbracket$ be an interpretation that maps
expressions and stores to values.

We give the semantics of a single-threaded program, featuring reads, writes
and conditionals as an event structure:

$\displaystyle\mathcal{T}\llbracket r\,\text{{=}}\,x\\!\text{{;}}\;T\rrbracket
ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}\textstyle\sum_{v\in
V}(\mathsf{R}\,\smash{{x}\,v})\bullet\mathcal{T}\llbracket
T\rrbracket(ρ[r\mathbin{↦}v])$ $\displaystyle\mathcal{T}\llbracket
x\,\text{{=}}\,M\\!\text{{;}}\;T\rrbracket ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}(\mathsf{W}\smash{{x}\,\mathcal{M}\llbracket
M\rrbracket ρ})\bullet\mathcal{T}\llbracket T\rrbracket ρ$
$\displaystyle\mathcal{T}\llbracket\texttt{done}\rrbracket ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}0$
$\displaystyle\mathcal{T}\llbracket\texttt{if}\;M\;T_{1}\;\texttt{else}\;T_{0}\rrbracket
ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}\begin{cases}\mathcal{T}\llbracket
T_{0}\rrbracket ρ&\allowbreak\;\text{if}\;\allowbreak\mathcal{M}\llbracket
M\rrbracket ρ=0\\\ \mathcal{T}\llbracket T_{1}\rrbracket
ρ&\allowbreak\;\text{otherwise}\allowbreak\end{cases}$

A _program_ is an collection of threads
$T_{1}\mathbin{\parallel}\cdots\mathbin{\parallel}T_{n}$, interpreted as
parallel composition of event structures with an initial event:

$\mathcal{P}\llbracket
T_{1}\mathbin{\parallel}\cdots\mathbin{\parallel}T_{n}\rrbracket\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}\mathsf{init}\bullet(\mathcal{T}\llbracket
T_{1}\rrbracket
ρ₀\mathbin{\parallel}\cdots\mathbin{\parallel}\mathcal{T}\llbracket
T_{n}\rrbracket ρ₀)$

We use standard abbreviations. For example, the program

if (x==0) {y=1;}

desugars to the following.

r=x; if(r==0){y=1; done} else {done}

If we take $V=\\{0,\,\allowbreak 1\\}$, then this has semantics

$\mathsf{init}\bullet(((\mathsf{R}\,\smash{{x}\,0})\bullet(\mathsf{W}\smash{{y}\,1})\bullet
0)+((\mathsf{R}\,\smash{{x}\,1})\bullet 0))$

visualized as follows.

$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{R}\,\smash{{x}\,1}$

Note that in this semantics, conflict is only introduced by reads. Each
conflicting event represents the read of a distinct value; since only one
value can be read, the events are in primitive conflict.

##  3\. Memory Event Structures

A _memory alphabet_ $(\Sigma,R,W,J,K)$ consists of

  * •

a set $\Sigma$ (the _actions_),

  * •

set $R\subseteq\Sigma$ (the _read actions_)

  * •

set $W\subseteq\Sigma$ (the _write actions_),

  * •

binary relation $J\subseteq(W\times R)$ (_justification_), and

  * •

binary relation $K\subseteq J$ (_synchronized justification_).

When $(a,b)\in J$, we say that $a$ _justifies_ $b$. Synchronization does not
play a role in this section; we return to it in §6.

A _memory event structure_ over such a memory alphabet is a confusion-free
labeled event structure over $\Sigma$.

The prototypical memory alphabet consists of an initial action, and read and
write actions over some set of _variables_ $X$, and some set of _values_ $V$:

$\displaystyle\Sigma$ $\displaystyle=R\cup W$ $\displaystyle R$
$\displaystyle=\\{(\mathsf{R}\,\smash{{x}\,v})\mid x\in X,v\in V\\}$
$\displaystyle W$ $\displaystyle=\\{(\mathsf{W}\smash{{x}\,v})\mid x\in X,v\in
V\\}\cup\\{\mathsf{init}\\}$

In §2 we saw that such an alphabet can be used to give the semantics for a
simple shared-memory concurrent language. The justification relation for this
alphabet is that $\mathsf{init}$ justifies a read of $0$, and that a write of
$v$ justifies a read of $v$ to the same variable:

$\displaystyle J$
$\displaystyle=\\{(\mathsf{init},(\mathsf{R}\,\smash{{x}\,0}))\mid x\in X\\}$
$\displaystyle\cup\\{((\mathsf{W}\smash{{x}\,v}),(\mathsf{R}\,\smash{{x}\,v}))\mid
x\in X,v\in V\\}$

In a memory event structure, an event $e$ is a _read event_ whenever
$\lambda(e)\in R$, and a _write event_ whenever $\lambda(e)\in W$. The sets
$R$ and $W$ need not be disjoint; thus, a memory alphabet may include read-
modify-write actions such as exchange, compare-and-set or increment. The
semantics of these operators as event structures is straightforward, following
the style given in §2.

In a memory event structure, we can lift justification from labels to events,
but this is not just a matter of looking at the labeling, since events should
not be justified by later events, by events in conflict, or by events with an
intervening event in read-write conflict. For example, in the program

if(y){x=0;} else {x=1;x=x;}

has the following event structure semantics, where we visualize justification
as a dashed edge.

$\mathsf{init}$$\mathsf{R}\,\smash{{y}\,0}$$\mathsf{R}\,\smash{{y}\,1}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{W}\smash{{x}\,1}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{W}\smash{{x}\,1}$

There is no event labeled $(\mathsf{W}\smash{{y}\,1})$; therefore, the only
justified read of $y$ is 0, not 1. Neither event labeled
$(\mathsf{W}\smash{{x}\,0})$ justifies $(\mathsf{R}\,\smash{{x}\,0})$: one is
in conflict with it and the other is later. Finally, $\mathsf{init}$ does not
justify $(\mathsf{R}\,\smash{{x}\,0})$ because $(\mathsf{W}\smash{{x}\,1})$ is
an intervening event in read-write conflict. Thus, the only justified read of
$x$ is 1, not 0.

In a memory event structure, we say write event $d$ _justifies_ read event $e$
whenever:

  1. (1)

$(\lambda(d),\lambda(e))\in J$,

  2. (2)

we do not have $e<d$,

  3. (3)

we do not have $d\mathrel{\\#}e$, and

  4. (4)

there is no $d<b<c\sim e$ such that $(\lambda(b),\lambda(c))\in J$.

Visually these conditions are that $d$ cannot justify $e$ when:

$d$$e$ or $d$$e$ or $d$$b$$c$$e$

Item (4) provides a formal definition of what it means for $b$ to be in _read-
write conflict_ with $e$. The following statement is equivalent: “there is no
$d<b<e\sim c$ such that $b$ justifies $c$.” However, we cannot use this as the
definition without worrying about circularity.

######  Definition  (Justified).

A configuration $C$ is _justified_ whenever every read event in $C$ is
justified by at least one write event in $C$. ∎

For example, the program y=x; has two maximal configurations, but only one of
them is justified:

$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,0}$and$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{W}\smash{{y}\,1}$

An event may have multiple justifiers in a single configuration. In drawings,
we choose one. For example, the program (x=0; || r=x;) has only one maximal
configuration. The read event in this configuration has two justifiers:

$\mathsf{init}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{R}\,\smash{{x}\,0}$
$\mathsf{init}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{R}\,\smash{{x}\,0}$

Unfortunately, justified configurations, although necessary, are not a
sufficient condition for modeling valid executions, as they allow cycles in
the union of causal order and justification, which cause _thin air reads_. For
example, the program $P_{1}$ from the introduction includes the justified
configurations
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}11},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}13},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}15},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}12},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}14},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}16},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}18}\\}:$

(r1=x; y=r1;) || (r2=y; x=r2;)
$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,0}$11$\mathsf{W}\smash{{y}\,0}$15$\mathsf{R}\,\smash{{y}\,0}$13$\mathsf{W}\smash{{x}\,0}$17$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,1}$12$\mathsf{W}\smash{{y}\,1}$16$\mathsf{R}\,\smash{{y}\,1}$14$\mathsf{W}\smash{{x}\,1}$18

In the latter, there is a cycle in causal+justification order. It is
straightforward to ban such cycles.

Recall that a configuration is a subset of the event set $E$.

######  Definition  (Acyclically justified).

On configurations, define $C$ _justifies_ $D$ whenever for any read event
$d\in D\setminus C$ there exists a write event $c\in C$ such that $c$
justifies $d$.

Write $C\lesssim D$ whenever $C\subseteq D$ and $C$ justifies $D$.

Write $\lesssim^{*}$ for the reflexive, transitive closure of $\lesssim$.

Define $C$ is _acyclically justified_ whenever $\emptyset\lesssim^{*}C$. ∎

A justified configuration is acyclically justified whenever the order induced
by causal order and justification is acyclic. Any acyclically justified
configuration is also justified.

For example, for $P_{1}$, we have that
$\emptyset\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10}\\},$
since
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is not a read. In addition, we have
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>since
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>justifies both
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Taking a maximal configuration at each step, we have:

$\emptyset\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}11},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}13},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}15},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
However, there is no such chain leading from $\emptyset$ to
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}10},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}12},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}14},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}16},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Consider the following program.

y=x; || x=1 || r=y; ($P_{4}$)
$\mathsf{init}$40$\mathsf{R}\,\smash{{x}\,1}$42$\mathsf{R}\,\smash{{x}\,0}$41$\mathsf{W}\smash{{y}\,0}$45$\mathsf{W}\smash{{y}\,1}$46$\mathsf{R}\,\smash{{y}\,0}$43$\mathsf{R}\,\smash{{y}\,1}$44$\mathsf{W}\smash{{x}\,1}$47

In this case the write to $x$ is immediately available, since it is not
causally dependent on any read. Thus:

$\displaystyle\emptyset\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}41},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}45}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}41},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}45},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>$\displaystyle\emptyset\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}46}\\}\lesssim\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}46},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Here the read of $x$ is a coin-toss, which determines whether it is possible
to read $(\mathsf{R}\,\smash{{y}\,1})$: A configuration that contains
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>cannot also contain
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
The second of these sequences can be seen in Figure 1, read from top to
bottom. The events included in each successive configuration are highlighted
using a darker, blue background. Events that are in conflict with an included
event are covered in white. Thus in a maximal configuration, such as the last
configuration in Figure 1, all events are either highlighted or covered.

Acyclic justification rules out cycles, since in any acyclically justified
$C$, there must be configurations $\emptyset=C_{0}\lesssim\cdots\lesssim
C_{n}=C$, and for any read event $e\in C$ there must be a $j$ such that $e\in
C_{j+1}$ and a $d\in C_{j}$ which justifies $e$. Since configurations are
$\leq$-closed, this means that there is no infinite sequence $d_{1}\leq
e_{1},d_{2}\leq e_{2},\dots,$ where $d_{i}$ justifies $e_{i+1}$, and in
particular there are no cycles.

y=x; || x=1 || r=y;
$\mathsf{init}$40$\mathsf{R}\,\smash{{x}\,1}$42$\mathsf{R}\,\smash{{x}\,0}$41$\mathsf{W}\smash{{y}\,0}$45$\mathsf{W}\smash{{y}\,1}$46$\mathsf{R}\,\smash{{y}\,0}$43$\mathsf{R}\,\smash{{y}\,1}$44$\mathsf{W}\smash{{x}\,1}$47
$\mathsf{init}$40$\mathsf{R}\,\smash{{x}\,1}$42$\mathsf{R}\,\smash{{x}\,0}$41$\mathsf{W}\smash{{y}\,0}$45$\mathsf{W}\smash{{y}\,1}$46$\mathsf{R}\,\smash{{y}\,0}$43$\mathsf{R}\,\smash{{y}\,1}$44$\mathsf{W}\smash{{x}\,1}$47
$\mathsf{init}$40$\mathsf{R}\,\smash{{x}\,1}$42$\mathsf{R}\,\smash{{x}\,0}$41$\mathsf{W}\smash{{y}\,0}$45$\mathsf{W}\smash{{y}\,1}$46$\mathsf{R}\,\smash{{y}\,0}$43$\mathsf{R}\,\smash{{y}\,1}$44$\mathsf{W}\smash{{x}\,1}$47

Figure 1. Acyclic- and AE-justification for $P_{4}$

Unfortunately, acyclic justification is too strong a requirement, as it rules
out some valid executions in the presence of optimizations which reorder
memory accesses. For example, the program $\text{\ref{eq:p3}}=\texttt{(r=x;
y=1; || x=y;)}$ has the event structure given in the introduction. In this
case the cyclic justifier models a valid execution, caused by a compiler or
hardware optimization reordering (r=x; y=1;) as (y=1; r=x;). If we are going
to admit such reorderings, we cannot model valid executions by a property of
configurations, and must look at the entire event structure (this observation
was made, in a different model, by Batty et al. [2015]).

######  Definition  (Well-justified).

On configurations, define $C$ _always eventually justifies (AE-justifies)_ $D$
whenever for any $C\lesssim^{*}C^{\prime}$ there exists a
$C^{\prime}\lesssim^{*}C^{\prime\prime}$ such that $C^{\prime\prime}$
justifies $D$.

Write $C\sqsubseteq D$ whenever $C\subseteq D$ and $C$ AE-justifies $D$.

Write $\sqsubseteq^{*}$ for the reflexive, transitive closure of
$\sqsubseteq$.

Define $C$ is _well-justified_ whenever $C$ is justified and
$\emptyset\sqsubseteq^{*}C$. ∎

Note the player’s choice of $D$ is not required to include the opponents
choices in $C^{\prime}$. The definition requires only that the player can find
an extension $C^{\prime\prime}$ of $C^{\prime}$ that justifies every event in
$D$.

A well-justified configuration must be both justified and AE-justified. The
notion of AE-justification describes when a read event is justified by some
write event no matter which execution path is chosen. AE-justification has the
flavor of a two-player game: in a configuration $C_{i}$, the opponent chooses
a $C_{i}\lesssim C_{i}^{\prime}$, after which the player chooses a
$C_{i}^{\prime}\lesssim C_{i}^{\prime\prime}$ which justifies $C_{i+1}$. If
the player can justify $C_{i+1}$ regardless of the opponent move, then the
player wins the round. The player well-justifies $C$ if they can repeat this
game to move from the initial configuration $\emptyset$ to the final
configuration $C$.

Any acyclically justified configuration is AE-justified.

######  Example .

Consider the proof of acyclic justification given in Figure 1. Starting from
$C_{0}=\emptyset,$ the player follows the proof of acyclic justification to
select
$C_{1}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47}\\},$
then
$C_{2}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and finally
$C_{3}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}46},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>In each case, the events in $C_{i}$ are justified by an extension
$C^{\prime\prime}_{i-1}$ of $C_{i-1}$, regardless of the opponent’s choice of
$C^{\prime}_{i-1}$. For example, the opponent may choose
$C_{1}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Even though
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>are in conflict, the player may choose
$C_{2}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}46}\\};$
the read $(\mathsf{R}\,\smash{{x}\,1})$ of
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is justified by
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>which the opponent cannot remove.

For any opponent move $\emptyset\lesssim^{*}C_{0}^{\prime}$, the player must
choose $C_{0}^{\prime}\lesssim^{*}C_{0}^{\prime\prime}$ so that
$C_{0}^{\prime\prime}$ justifies $C_{1}$. In this case, the player can always
choose
$C_{0}^{\prime\prime}\supseteq\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>since
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>conflict with no event and do not require justification. The first two moves
of the player can be collapsed, choosing $C_{1}$ to be
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}47},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}42},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}46}\\},$
since $42$ can be justified regardless of the opponent move. However, the last
two moves cannot be collapsed. The player cannot initially select
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>in this case the opponent would win by choosing
$C_{0}^{\prime}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}40},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}41},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}43},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>∎

######  Example .

r1=x; y=1; || r2=y; x=r2;
$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{R}\,\smash{{x}\,0}$31$\mathsf{W}\smash{{y}\,1}$35$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,0}$33$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,0}$37$\mathsf{W}\smash{{x}\,1}$38
$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{R}\,\smash{{x}\,0}$31$\mathsf{W}\smash{{y}\,1}$35$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,0}$33$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,0}$37$\mathsf{W}\smash{{x}\,1}$38
$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{R}\,\smash{{x}\,0}$31$\mathsf{W}\smash{{y}\,1}$35$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,0}$33$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,0}$37$\mathsf{W}\smash{{x}\,1}$38

Figure 2. AE-order for $P_{3}$

We now consider the proof that $P_{3}$ is well-justified to read all ones,
given in Figure 2. The previous strategy does not work, since the goal
configuration is not acyclically justified.

The player chooses
$C_{1}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30}\\},$
$C_{2}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and finally
$C_{3}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}34},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}38},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}32},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>As in the previous example, the first two player moves can be collapsed, but
not the last two. We show the first two player moves separately to make the
opponent choices clear. The opponent can choose $C_{1}^{\prime}$ to include
any events except
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>(and therefore
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}36}$);
there is no acyclically justified configuration that includes
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>For this reason events
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>are gray in the top configuration of Figure 2. The opponent option to include
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>C_{1}^{\prime}$ prevents the player from selecting
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>C_{1}$. The $(\mathsf{R}\,\smash{{x}\,1})$ cannot be justified in this case.
However, $(\mathsf{R}\,\smash{{y}\,1})$ can be justified regardless of the
opponent’s choice. Thus
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>can be included in $C_{1}$ (or $C_{2}$, as shown).

Once the player has won the round including
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>the opponent is no longer at liberty to include
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>choice has been made. Thus the player may include
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>in the next round.

This reasoning holds even if the write to $y$ is conditional, as in the
following variation:

r1=x; if(r1<2){y=1;} || r2=y; x=r2;
$\mathsf{init}$$\mathsf{R}\,\smash{{x}\,2}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{R}\,\smash{{y}\,0}$$\mathsf{R}\,\smash{{y}\,1}$$\mathsf{R}\,\smash{{y}\,2}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{W}\smash{{x}\,1}$$\mathsf{W}\smash{{x}\,2}$

As before, there is no acyclically justified configuration of the event
structure that reads a value other than $0$ for $x$. Thus the player can
choose an initially choose a configuration containing
$(\mathsf{R}\,\smash{{y}\,1})$, and play proceeds as before. ∎

######  Example .

As noted in the introduction, configuration $C_{1}$ of $P_{1}$ fails to be
well-justified. We provide a proof in §5. Intuitively, the player is unable to
select
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>C_{1}$, because the opponent can choose
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>C^{\prime}_{0}$. ∎

In the process of revising the Java Memory Model, Pugh [2004] developed a set
of twenty _causality test cases_. Using hand calculation, we tested our
semantics against nineteen of these cases. (TC9 is based on the idea that an
execution should be allowed if there exists an augmentation, such as thread
inlining, that allows it. This is a non-goal for our semantics; therefore, we
do not consider TC9.)

Our semantics agrees with sixteen of the test cases and disagrees with three:
TC3, TC7 and TC11. In §7, we discuss TC7, which best elucidates the issues.

Also by hand calculation, we found that our semantics gives the desired
results for all examples in Batty et al. [2015, §4] and all but one in Ševčík
[2008, §5.3]: redundant-write-after-read-elimination—this counterexample
applies to any sensible non-coherent semantics.

y=x; || if(y){x=y;} else {x=1;}
$\mathsf{init}$a$\mathsf{R}\,\smash{{x}\,0}$b$\mathsf{R}\,\smash{{x}\,1}$c$\mathsf{R}\,\smash{{y}\,0}$d$\mathsf{R}\,\smash{{y}\,1}$e$\mathsf{W}\smash{{y}\,0}$f$\mathsf{W}\smash{{y}\,1}$g$\mathsf{W}\smash{{x}\,1}$h$\mathsf{R}\,\smash{{y}\,0}$i$\mathsf{R}\,\smash{{y}\,1}$j$\mathsf{W}\smash{{x}\,0}$k$\mathsf{W}\smash{{x}\,1}$l
$\mathsf{init}$a$\mathsf{R}\,\smash{{x}\,0}$b$\mathsf{R}\,\smash{{x}\,1}$c$\mathsf{R}\,\smash{{y}\,0}$d$\mathsf{R}\,\smash{{y}\,1}$e$\mathsf{W}\smash{{y}\,0}$f$\mathsf{W}\smash{{y}\,1}$g$\mathsf{W}\smash{{x}\,1}$h$\mathsf{R}\,\smash{{y}\,0}$i$\mathsf{R}\,\smash{{y}\,1}$j$\mathsf{W}\smash{{x}\,0}$k$\mathsf{W}\smash{{x}\,1}$l
$\mathsf{init}$a$\mathsf{R}\,\smash{{x}\,0}$b$\mathsf{R}\,\smash{{x}\,1}$c$\mathsf{R}\,\smash{{y}\,0}$d$\mathsf{R}\,\smash{{y}\,1}$e$\mathsf{W}\smash{{y}\,0}$f$\mathsf{W}\smash{{y}\,1}$g$\mathsf{W}\smash{{x}\,1}$h$\mathsf{R}\,\smash{{y}\,0}$i$\mathsf{R}\,\smash{{y}\,1}$j$\mathsf{W}\smash{{x}\,0}$k$\mathsf{W}\smash{{x}\,1}$l
$\mathsf{init}$a$\mathsf{R}\,\smash{{x}\,0}$b$\mathsf{R}\,\smash{{x}\,1}$c$\mathsf{R}\,\smash{{y}\,0}$d$\mathsf{R}\,\smash{{y}\,1}$e$\mathsf{W}\smash{{y}\,0}$f$\mathsf{W}\smash{{y}\,1}$g$\mathsf{W}\smash{{x}\,1}$h$\mathsf{R}\,\smash{{y}\,0}$i$\mathsf{R}\,\smash{{y}\,1}$j$\mathsf{W}\smash{{x}\,0}$k$\mathsf{W}\smash{{x}\,1}$l

Figure 3. AE-order for Ševčík §5.3.2

######  Example .

We consider the redundant-read-elimination counterexample of [Ševčík 2008,
§5.3.2], given in Figure 3. TC18 of [Pugh 2004] is similar. The question is
whether there is a well-justified configuration that includes event
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Starting from the empty set, the maximal acyclically justified configurations
are
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}b},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}f},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}d},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}d},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}h}\\},$
both of which include
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>with label $(\mathsf{W}\smash{{x}\,1})$. Therefore the player can choose
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Having secured
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>with label $(\mathsf{W}\smash{{y}\,1})$, the player can subsequently add
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>with label $(\mathsf{R}\,\smash{{y}\,1})$. At this point, the player has two
possible extensions, depending on the choice between
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>Both choices are _AE-justified_ , but only the choice of
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>can be extended to a _justified_ configuration, which is therefore _well-
justified_ : The AE-justified configuration
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}e},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>cannot be extended to include an event labeled $(\mathsf{W}\smash{{x}\,1})$,
which is necessary to justify
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>with label $(\mathsf{R}\,\smash{{x}\,1})$.

This example shows the importance of limiting the power of the opponent at
each step. If we were to allow the opponent to choose configurations using AE-
justification, rather than acyclic justification, then the opponent could
choose
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}e},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>to extend the empty set, disabling the players initial choice of
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>In this case, one can prevent the attack by limiting the opponent to well-
justification rather than AE-justification. By adding another variable,
however, one can construct an example in which well-justification gives the
opponent additional power over acyclic justification. ∎

##  4\. Data-race-free event structures

We say that $\textnormal{{ES}}^{\prime}$ is an augmentation of ES if it has
same events, conflict and labels, and possibly more order. Formally,
$(E,{\leq^{\prime}},{\mathrel{\\#}},\lambda)$ is an augmentation of
$(E,{\leq},{\mathrel{\\#}},\lambda)$ if ${\leq}\subseteq{\leq^{\prime}}$.

It is straightforward to show that justification, acyclic justification and
well-justification are all reflected by augmentation. For example, if
$\textnormal{{ES}}^{\prime}$ augments ES and $C$ is a well-justified
configuration of $\textnormal{{ES}}^{\prime}$ then $C$ is a well-justified
configuration of ES.

A _sequential_ memory event structure is one where, for any events $d$ and
$e$, either $d\leq e$, $e\leq d$ or $d\mathrel{\\#}e$. A _sequentially
consistent_ configuration of a memory event structure is a justified
configuration of a sequential augmentation of it. That is, a configuration $C$
of ES is sequentially consistent if there exists an augmentation
$\textnormal{{ES}}^{\prime}$ of ES such that $\textnormal{{ES}}^{\prime}$ is
sequential and $C$ is a justified configuration of
$\textnormal{{ES}}^{\prime}$.

Note that in a sequential memory event structure, if $d$ justifies $e$ then
$d\leq e$. It follows that any justified configuration of a sequential memory
event structure is well-justified, and hence that any sequentially consistent
configuration of a memory event structure is well-justified.

The converse is not true. There are well-justified configurations that are not
sequentially consistent, due to data races. For example, the program (w=1; ||
y=(w<=x); || z=(x<=w); || x=1;) has semantics with configuration:

$\mathsf{init}$$\mathsf{R}\,\smash{{w}\,1}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{R}\,\smash{{w}\,0}$$\mathsf{W}\smash{{w}\,1}$$\mathsf{W}\smash{{x}\,1}$$\mathsf{W}\smash{{y}\,0}$$\mathsf{W}\smash{{z}\,0}$

This is acyclically justified, and hence well-justified, but not sequentially
consistent. In this section, we shall show that such data races are the only
source of configurations which are well-justified but not sequentially
consistent.

In a memory event structure, define concurrent events $d$ and $e$ to be a
_read-write race_ whenever there is some $c\sim e$ such that $d$ justifies
$c$, as shown on the left below. Define concurrent events $d$ and $e$ to be a
_write-write race_ whenever there is some $b\sim c$ such that $d$ justifies
$b$ and $e$ justifies $c$, as shown on the right below.

Define a configuration to be _data-race-free_ when it contains no read-write
or write-write races. Recall that $\sim$ is reflexive; thus, we may also have
$c=e$ in the left diagram and $b=c$ in the right.

We state the theorem generally for any memory event structure that is read-
enabled and commutative. The prototypical example, given in §3, satisfies both
these criteria.

$c$$d$$e$

A memory event structure is _read-enabled_ whenever, for any read event $e$
there exists some $c\leq e\sim d$ such that $c$ justifies $d$, as shown on the
right. Any event structure that is the semantics of a program is read enabled.
Read enabledness ensures that every read operation in a program can be
satisfied by some preceding write. This is true because of the $\mathsf{init}$
event which justifies reading $0$ on every variable and, therefore, is in
read-write conflict with every read. For example, if $e$ is
$(\mathsf{R}\,\smash{{x}\,1})$, then it suffices to take $c$ to be
$\mathsf{init}{}$, since $\mathsf{init}{}$ justifies
$(\mathsf{R}\,\smash{{x}\,0})$, which is in primitive conflict with
$(\mathsf{R}\,\smash{{x}\,1})$.

A memory event structure is _commutative_ whenever $c\sim d$ and $d$ justifies
$e$ implies there exists $b\sim e$ where $c$ justifies $b$, that is:

$c$$d$$e$ implies $c$$d$$e$$b$

If read and write actions are disjoint, then it follows immediately that any
event structure that is the semantics of a program will be commutative, since
read is defined as a sum over all possible values. Commutativity ensures that
all writes can be read from.

Read-modify-write operators such as swap and fetch-and-add are commutative,
since these always write. Compare-and-set (CAS) is commutative if we interpret
a failed CAS as both read and write (of the old value), but not if we consider
a failed CAS only as a read. For example, if failed CAS is considered a read,
then $(\texttt{CAS}\,{x}\,{0}\,{1})$ generates the following event structure
for bit register $x$, where $(\mathsf{RMW}\,\smash{{x}\,0\,1})$ denotes a
successful CAS and $(\mathsf{R}\,\smash{{x}\,1})$ denotes a failed CAS.

$\mathsf{init}$$\mathsf{RMW}\,\smash{{x}\,0\,1}$$\mathsf{R}\,\smash{{x}\,1}$

The $(\mathsf{RMW}\,\smash{{x}\,0\,1})$ event may justify some other read of
$x$; however, the minimal conflicting event $(\mathsf{R}\,\smash{{x}\,1})$ is
a plain read, which justifies nothing. We leave weakening commutativity as
future work.

######  Theorem  (DRF).

In any commutative read-enabled memory event structure, if all sequentially
consistent configurations are data-race-free, then all well-justified
configurations are sequentially consistent.

###### Proof.

Define a configuration $C$ to be _pre-justified_ if every read action $e\in C$
is justified by a write action $d\in C$ where $d\leq e$. It is routine to show
that any pre-justified configuration is sequentially consistent. The core
lemma of the proof follows [Lochbihler 2013], which is that if $C$ is pre-
justified, and $C$ justifies $D$, then $D$ is pre-justified. After this, the
proof is routine: we first show that if $C$ is pre-justified and
$C\lesssim^{*}D$ then $D$ is pre-justified; then that if $C$ is pre-justified
and $C\sqsubseteq^{*}D$ then $D$ is pre-justified. The result follows, since
$\emptyset$ is trivially pre-justified. This proof has been mechanized in
Agda. ∎

##  5\. Invariants

While there is no formal definition of “thin-air read” [Batty et al. 2015],
the examples point to a failure of inductive reasoning, typically due to a
cycle in the union of the causal and data dependency orders. In order to
establish that these forms of thin-air read are impossible, it is sufficient
to show that is possible to reason inductively. In this section, we show that
well-justification enables inductive reasoning.

We consider a limited form of invariant reasoning, which is strong enough to
capture non-temporal safety properties, such as type safety. Given a suitable
notion of formula, $\phi$, we show that if, in every configuration of ES, the
_read_ events satisfy $\phi$, then, in every configuration of ES, _all_ events
satisfy $\phi$. Significantly, the result can be applied without reasoning
about well-justification.

To keep the setting as simple as possible, we consider logics over labels
rather than events. In order to establish the result, we must restrict
attention to logics that are subset closed. This allows the expression of
certain safety properties such as $x\mathord{\neq}1$, but not liveness
properties such as $x\mathord{=}1$. For a label set $\Sigma$, a _program
logic_ $(\Phi,{\vDash})$ consists of:

  * •

a set $\Phi$ (the _formulae_), and

  * •

a binary relation $\vDash$ between $\mathcal{P}(\Sigma)$ and $\Phi$
(_satisfaction_).

A formula $\phi$ is _subset closed_ whenever $A\subseteq B\vDash\phi$ implies
$A\vDash\phi$. It is _satisfiable_ whenever $A\vDash\phi$ for some $A$. It
_respects justification_ whenever $A$ justifies $B$ and $A\vDash\phi$ implies
$B\vDash\phi$.

For any configuration $C$, let $\Sigma(C)$ be the labels of $C$:

$\Sigma(C)=\\{\lambda(e)\mid e\in C\\}$

A formula $\phi$ is an _invariant_ of a memory event structure whenever
$\Sigma(C)\cap R\vDash\phi$ implies $\Sigma(C)\vDash\phi$ for any
configuration $C$ (recalling that $R$ is the set of all read actions).

A formula $\phi$ is a _tautology_ of a memory event structure whenever
$\Sigma(C)\vDash\phi$ for any well-justified configuration $C$.

######  Theorem .

For any satisfiable, subset-closed $\phi$ which respects justification, if
$\phi$ is an invariant of ES then $\phi$ is a tautology of ES.

###### Proof.

Mechanized in Agda. ∎

In the remainder of this section, we consider an example logic. Let
$\mathsf{T}$ be a set of _type names_ , ranged over by $\tau$. The set $\Phi$
of formulae is generated by the following BNF.

$\phi,\,\allowbreak\psi\;\mathrel{\mathord{\vcentcolon}\mkern-1.0mu\mathord{\vcentcolon}\mathord{{=}}}\;\mathord{{x}\mathord{\neq}{v}}\;\mathrel{|}\;\mathord{{x}\mathord{:}{\tau}}\;\mathrel{|}\;\mathord{\mathsf{true}}\;\mathrel{|}\;\mathord{\mathsf{false}}\;\mathrel{|}\;\phi\mathbin{\land}\psi\;\mathrel{|}\;\phi\mathbin{\lor}\psi$

Given a semantics $V_{\tau}\subseteq V$ for each type $\tau$, let $\vDash$ be
the obvious satisfaction relation generated by the following rules for the
atoms.

  * •

$A\vDash\mathord{{x}\mathord{\neq}{v}}$ when for any $a\in A$, if
$a=(\mathsf{R}\,\smash{{x}\,w})$ or $a=(\mathsf{W}\smash{{x}\,w})$, then
$w\neq v$.

  * •

$A\vDash\mathord{{x}\mathord{:}{\tau}}$ when for any $a\in A$, if
$a=(\mathsf{R}\,\smash{{x}\,v})$ or $a=(\mathsf{W}\smash{{x}\,v})$, then $v\in
V_{\tau}$.

Note that the logic is satisfiable and subset closed and thus satisfies the
criteria of Theorem 5.

Suppose that we attempt to show that
$\phi_{1}=(\mathord{{x}\mathord{\neq}{1}}\mathbin{\land}\mathord{{y}\mathord{\neq}{1}})$
is a tautology for $P_{1}$. Recall the event structure for this program, given
in the introduction.

(y=x; || x=y;)
$\mathsf{init}$10$\mathsf{R}\,\smash{{x}\,1}$12$\mathsf{R}\,\smash{{x}\,0}$11$\mathsf{W}\smash{{y}\,0}$15$\mathsf{W}\smash{{y}\,1}$16$\mathsf{R}\,\smash{{y}\,0}$13$\mathsf{R}\,\smash{{y}\,1}$14$\mathsf{W}\smash{{x}\,0}$17$\mathsf{W}\smash{{x}\,1}$18

Note that any configuration which includes write events $16$ or $18$, must
also include read events $12$ or $14$. Thus, if the read events satisfy
$\phi_{1}$ then the write events satisfy $\phi_{1}$, and so $\phi_{1}$ is
invariant for $P_{1}$. Thus, by Theorem 5, $\phi_{1}$ is a tautology for
$P_{1}$.

For $P_{3}$, instead, $\phi_{1}$ fails. Recall the event structure for this
program, also given in the introduction.

(r=x; y=1; || x=y;)
$\mathsf{init}$30$\mathsf{R}\,\smash{{x}\,1}$32$\mathsf{R}\,\smash{{x}\,0}$31$\mathsf{W}\smash{{y}\,1}$35$\mathsf{W}\smash{{y}\,1}$36$\mathsf{R}\,\smash{{y}\,0}$33$\mathsf{R}\,\smash{{y}\,1}$34$\mathsf{W}\smash{{x}\,0}$37$\mathsf{W}\smash{{x}\,1}$38

The configuration
$\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}30},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}31},\,\allowbreak{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>fails to satisfy $\phi_{1}$ even though its only read event
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>satisfies $\phi_{1}$.

These examples can be adapted to show reasoning using types. Let $0$ be the
unique value of type Unit. Then $P_{1}$ satisfies the typing
$\mathord{{x}\mathord{:}{\textsf{Unit}}}\mathbin{\land}\mathord{{y}\mathord{:}{\textsf{Unit}}}$,
but $P_{2}$ does not.

##  6\. Fencing

In §3, we noted that a memory alphabet includes _synchronized justification_ ,
such as lock release and acquire; however, we have not made any use of
synchronization up to now. In this section, we develop a notion of fencing, in
which synchronized justifications contribute to causal order.

We model lock-based synchronization in a very simple setting. We assume that
there is only one, statically allocated lock and that lock release always
occurs in the same thread as the previous acquire. The latter assumption
ensures that each release causally follows the corresponding acquire.

The memory alphabet from §3 is modified to include acquire and release
actions, which are considered both read and write actions. (We comment on this
design in §9.)

$\displaystyle\Sigma$ $\displaystyle=R\cup W$ $\displaystyle R$
$\displaystyle=\\{(\mathsf{R}\,\smash{{x}\,v}),\mathsf{Aq},\mathsf{Rl}\mid
x\in X,v\in V\\}$ $\displaystyle W$
$\displaystyle=\\{(\mathsf{W}\smash{{x}\,v}),\mathsf{Aq},\mathsf{Rl}\mid x\in
X,v\in V\\}\cup\\{\mathsf{init}\\}$

The semantics of locking actions are as follows.

$\displaystyle\mathcal{T}\llbracket\texttt{acq}\text{{;}}T\rrbracket ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}\mathsf{Aq}\bullet\mathcal{T}\llbracket
T\rrbracket ρ$
$\displaystyle\mathcal{T}\llbracket\texttt{rel}\text{{;}}T\rrbracket ρ$
$\displaystyle\mathrel{\smash{\overset{\scriptscriptstyle\vartriangle}{=}}}\mathsf{Rl}\bullet\mathcal{T}\llbracket
T\rrbracket ρ$

The justification relation, $J$, now includes lock actions:

$\displaystyle J$
$\displaystyle=\\{(\mathsf{init},(\mathsf{R}\,\smash{{x}\,0})),((\mathsf{W}\smash{{x}\,v}),(\mathsf{R}\,\smash{{x}\,v}))\mid
x\in X,v\in V\\}$
$\displaystyle\quad\cup\\{(\mathsf{init},\mathsf{Aq}),(\mathsf{Aq},\mathsf{Rl}),(\mathsf{Rl},\mathsf{Aq})\\}$

The synchronized justification relation, $K$, is restricted to lock actions.

$\displaystyle K$
$\displaystyle=\\{(\mathsf{init},\mathsf{Aq}),(\mathsf{Aq},\mathsf{Rl}),(\mathsf{Rl},\mathsf{Aq})\\}$

Recall from §3 that event $d$ _justifies_ event $e$ whenever

$(\lambda(d),\lambda(e))\in J$,

$d$ does not follow $e$,

$d$ is not in conflict with $e$, and

there is no intervening $b$ between $d$ and $e$ that justifies an event in
primitive conflict with $e$.

We say event $d$ _synchronously justifies_ event $e$ whenever $d$ justifies
$e$ and $(\lambda(d),\lambda(e))\in K$.

A _fenced_ memory event structure is one where, for any events $d$ and $e$, if
$d$ synchronously justifies $e$ then $d\leq e$.

A _well-fenced_ configuration of a memory event structure is a well-justified
configuration of a fenced augmentation of it. That is, a configuration $C$ of
ES is well-fenced if there exists a augmentation $\textnormal{{ES}}^{\prime}$
of ES such that $\textnormal{{ES}}^{\prime}$ is fenced and $C$ is a justified
configuration of $\textnormal{{ES}}^{\prime}$.

To show that a configuration is well-fenced, the player must first augment the
event structure so that it is fenced. Then the inductive argument for well-
justification proceeds as before.

For example, consider the following program, $P_{5}$.

acq; x=1; x=0; rel; || acq; r=x; rel; ($P_{5}$)
$\mathsf{init}$50$\mathsf{Aq}$51$\mathsf{W}\smash{{x}\,1}$53$\mathsf{W}\smash{{x}\,0}$56$\mathsf{Rl}$57$\mathsf{Aq}$52$\mathsf{R}\,\smash{{x}\,0}$54$\mathsf{R}\,\smash{{x}\,1}$55$\mathsf{Rl}$58$\mathsf{Rl}$59

Whereas the second thread can read $1$ in a well-justified configuration, this
is not possible in a well-fenced configuration. There are two possible
fencings. One includes the augmentation
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}57}\leq{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and the other includes
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}58}\leq{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}59}\leq{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>In either case,
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>can be justified, but
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>cannot. Therefore, there is no well-fenced configuration that includes
${\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>
Note that any sequential memory event structure is fenced. It follows that any
sequential augmentation of a memory event structure is a fenced augmentation
of it, and hence that any sequentially consistent configuration is a well-
fenced configuration.

Now, if every justification is synchronized (that is $J=K$) we have that every
well-fenced configuration is sequentially consistent, but in general this is
not true. In particular, if there is no synchronization (that is
$K=\emptyset$) then every well-justified configuration is well-fenced.

Fortunately, the proof of the DRF Theorem for well-fenced configurations
follows directly from the DRF theorem for well-justified configurations: we
just use DRF on each fencing.

######  Theorem  (DRF).

In any commutative read-enabled memory event structure, if all sequentially
consistent configurations are data-race-free, then all well-fenced
configurations are sequentially consistent.

###### Proof.

Follows directly from Theorem 4. ∎

##  7\. Limitations

As we noted in §3, one possible goal for a memory model is that an execution
should be allowed if there exists an augmentation, such as thread inlining,
that allows it. A related goal is that an execution should be allowed if it is
allowed for a subset of threads. These are non-goals for our semantics, which,
indeed, fails to validate them.

Both adding new threads and reducing causal order afford greater flexibility
in choosing configurations. The additional flexibility can be exploited by the
player, validating additional executions. But it can also be exploited by the
opponent, eliminating executions that would be possible without the additional
flexibility. Consider a variant of the program given in Example 3, which is
similar to TC9 from [Pugh 2004]:

r1=x; if(r1<2){y=1;} || x=2; || r2=y; x=r2; (TC9′)
$\mathsf{init}$$\mathsf{W}\smash{{x}\,2}$$\mathsf{R}\,\smash{{x}\,2}$$\mathsf{R}\,\smash{{x}\,1}$$\mathsf{R}\,\smash{{x}\,0}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{W}\smash{{y}\,1}$$\mathsf{R}\,\smash{{y}\,0}$$\mathsf{R}\,\smash{{y}\,1}$$\mathsf{R}\,\smash{{y}\,2}$$\mathsf{W}\smash{{x}\,0}$$\mathsf{W}\smash{{x}\,1}$$\mathsf{W}\smash{{x}\,2}$

Relative to Example 3, we have added a thread that writes $2$ to $x$. To
forbid configurations that include $(\mathsf{R}\,\smash{{y}\,1})$, it is
sufficient for the opponent to chose a configuration that includes
$(\mathsf{W}\smash{{x}\,2})$ and $(\mathsf{R}\,\smash{{x}\,2})$; clearly such
a configuration can be acyclically justified. This opponent move is
unavailable, however, if the new thread is removed or if it is inlined after
either of the other threads; in this case, $(\mathsf{R}\,\smash{{y}\,1})$ is
possible, following the reasoning of Example 3.

Of the remaining nineteen test cases from [Pugh 2004], our semantics disagrees
with TC3, TC7 and TC11. In all cases, the reason is the same. We discuss TC7,
which best elucidates the issues.

r=z; y=x; || z=y; x=1; (TC7)
$\mathsf{init}$a$\mathsf{R}\,\smash{{z}\,1}$c$\mathsf{R}\,\smash{{z}\,0}$b$\mathsf{R}\,\smash{{x}\,1}$g$\mathsf{R}\,\smash{{x}\,0}$f$\mathsf{W}\smash{{y}\,0}$l$\mathsf{W}\smash{{y}\,1}$m$\mathsf{R}\,\smash{{x}\,1}$i$\mathsf{R}\,\smash{{x}\,0}$h$\mathsf{W}\smash{{y}\,0}$n$\mathsf{W}\smash{{y}\,1}$o$\mathsf{R}\,\smash{{y}\,0}$d$\mathsf{R}\,\smash{{y}\,1}$e$\mathsf{W}\smash{{z}\,0}$j$\mathsf{W}\smash{{z}\,1}$k$\mathsf{W}\smash{{x}\,1}$p$\mathsf{W}\smash{{x}\,1}$q

The question is whether all of the reads can be resolved to $1$. This fails
under our semantics: there is no well-justified configuration that includes
events $c$, $e$ and $i$, all of which read $1$. In order to well-justify such
a configuration, one must first resolve the conflict on $x$, then $y$ and
finally $z$. But this strategy fails immediately after resolving $x$.

Starting from the empty configuration, all acyclically justified
configurations can be extended to include either $p$ or $q$, and thus the
player can select a configuration that includes either $g$ or $i$. Suppose the
player selects $i$. Since configurations are downclosed, the player must also
select $c$; however $c$ is not acyclically justified when the opponent selects
$p$. Symmetrically, $b$ is not acyclically justified when the opponent selects
$q$. Thus the player cannot resolve the conflict on $y$.

The failure of TC7 indicates a failure to validate the reordering of
independent reads. To see this, consider the program in which the first thread
is rewritten.

y=x; r=z; || z=y; x=1;
$\mathsf{init}$${}^{a^{\prime}}$$\mathsf{R}\,\smash{{x}\,1}$${}^{c^{\prime}}$$\mathsf{R}\,\smash{{x}\,0}$${}^{b^{\prime}}$$\mathsf{W}\smash{{y}\,1}$${}^{h^{\prime}}$$\mathsf{W}\smash{{y}\,0}$${}^{f^{\prime}}$$\mathsf{R}\,\smash{{z}\,1}$${}^{m^{\prime}}$$\mathsf{R}\,\smash{{z}\,0}$${}^{l^{\prime}}$$\mathsf{R}\,\smash{{z}\,1}$${}^{o^{\prime}}$$\mathsf{R}\,\smash{{z}\,0}$${}^{n^{\prime}}$$\mathsf{R}\,\smash{{y}\,0}$${}^{d^{\prime}}$$\mathsf{R}\,\smash{{y}\,1}$${}^{e^{\prime}}$$\mathsf{W}\smash{{z}\,0}$${}^{j^{\prime}}$$\mathsf{W}\smash{{z}\,1}$${}^{k^{\prime}}$$\mathsf{W}\smash{{x}\,1}$${}^{p^{\prime}}$$\mathsf{W}\smash{{x}\,1}$${}^{q^{\prime}}$

In this case, the player can choose $c^{\prime}$, then $e^{\prime}$, then
$o^{\prime}$, as required.

We now sketch a proposal to address this issue. On sets of events, define $C$
is _compatible_ with $D$ whenever there is no $c\in C$ and $d\in D$ such that
$c\mathrel{\\#_{\mu}}d$. Define $C$ is _consistent_ whenever $C$ is compatible
with $C$.

######  Proposal .

Modify Definitions 3 and 3 to range over consistent sets, rather than
configurations.

A configuration $C$ is _alt-well-justified_ whenever $C$ is justified and
there exists a consistent set $D$ such that
$\emptyset\sqsubseteq^{*}D\supseteq C$.

By this proposal, the definition of alt-AE-justifies is as follows: On
consistent sets, $C$ _alt-AE-justifies_ $D$ whenever for any
$C\lesssim^{*}C^{\prime}$ there exists a
$C^{\prime}\lesssim^{*}C^{\prime\prime}$ such that $C^{\prime\prime}$
justifies $D$.

The configuration of TC7 that always reads $1$ is alt-well-justified. Starting
from the empty set,
$C_{1}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is alt-AE-justified, since every consistent set that extends $\emptyset$ (via
$\lesssim^{*}$) can be further extended to include either $p$ or $q$, both
labeled $(\mathsf{W}\smash{{x}\,1})$. Although $g$ and $i$ are in conflict,
they are not in primitive conflict, and therefore may both be included in a
consistent set—this is the key difference between well- and alt-well-
justification. From $C_{1}$,
$C_{2}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}i},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is alt-AE-justified, since we can always extend to include either $m$ or $o$,
both labeled $(\mathsf{W}\smash{{y}\,1})$. From $C_{2}$,
$C_{3}=\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}i},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}e},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color<EMAIL_ADDRESS>is alt-AE-justified, since we can always extend to include $k$, labeled
$(\mathsf{W}\smash{{z}\,1})$. Thus $\emptyset\sqsubseteq^{*}C_{3}$ and
therefore, since writes do not require justification,
$\emptyset\sqsubseteq^{*}\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}g},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}m},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}i},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}o},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}e},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}k},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}q},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c}\\}\supseteq\\{{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}a},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}i},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}o},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}e},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}k},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}q},{\color[rgb]{0.3,0.3,0.3}\definecolor[named]{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@color@gray@fill{0.3}c}\\},$
as required.

By hand calculation, alt-well-justification agrees with all nineteen test
cases; therefore, the definition looks quite promising. The question of
whether DRF holds for alt-well-justification remains open. The inductive
structure of the proof of DRF relies on the fact that configurations are down
closed. Since consistent sets are not necessarily down closed, the proof
strategy fails.

##  8\. Related work

Our model is inspired by the Java Memory Model, first described by Manson et
al. [2005] and explored by Ševčík [2008]. Lochbihler [2013] provides
mechanized proofs, in addition to an encyclopedic survey and history.

The use of universal quantification over configurations in the definition of
AE-justification is novel in this work. Prior definitions for Java-like
languages are purely existential in their quantification over possible
executions [Manson et al. 2005; Cenciarelli et al. 2007; Jagadeesan et al.
2010]. This leads to differences between our model the JMM, such as the
execution of Example 3, which is allowed in our model, but disallowed by the
JMM [Ševčík 2008, §5.3.2].

Batty et al. [2015] describe the problem of thin-air executions and provide a
detailed review of the literature. They show the limitations of syntactic
notions of dependency, as defined, for example, in C++ [Boehm and Adve 2008;
Batty et al. 2011]. In particular, for C++ they show that there is no per-
candidate-execution condition that precludes thin-air reads while allowing
sufficient optimization. This problem is avoided in hardware models, such as
[Alglave 2010; Alglave et al. 2014], which are not subject to compiler
optimization and therefore can encode the specific notion of dependency
provided by the hardware at hand.

Event structures have appeared in other attempts to formalize relaxed memory
semantics:

  * •

Our first attempt to model relaxed memory using labeled prime event structures
was presented at a workshop in Cambridge [Jeffrey and Riely 2014]. Our
proposal was to allow configurations that are _relaxed justified_ : Define a
_pre-configuration_ to be a $\leq$-downclosed set of events. A pre-
configuration is _relaxed justified_ when it has a total order such that any
non-initial event has a justifier that precedes it in the total order. A
justified configuration is _relaxed justified_ when it is included in a
relaxed justified pre-configuration. We abandoned this approach after Sezgin
[2014] discovered that the program (y=x+1; || x=y;) may generate any integer
under this model. This example is since referred to as the Random Number
Generator (RNG).

  * •

Pichon-Pharabod and Sewell [2016] defined a semantics for C/C++ relaxed
atomics using event structures to model the state of a single thread, with the
goal of providing an semantic model of single-threaded optimization.
_Deordering_ allows removal causal order between events of a thread that are
not causally related; for example, replacing r=x;y=1 with r=x || y=1.
_Merging_ allows collapsing redundant reads into a single event; for example,
replacing r1=x;r2=x;$C$ with r1=x;$C^{\prime}$, where $C^{\prime}$ is derived
from $C$ by replacing occurrences of r2 by r1. Kang et al. [2017] observe that
this model is not robust with respect to all of the relaxations permitted
under hardware models.

  * •

Castellan [2016] presented a semantics for relaxed memory using event
structures and a restricted form of interleaving. In this work, the _open_
semantics of processes is as one expects for an event structure, with parallel
processes unordered by causality. In the _closed_ semantics, all events on the
same memory cell are related by either conflict or causality. Although
interleaving is only required for events on the same memory cell, the process