\section{C/C++ Memory Model}\label{sec:memorymodel}

We next briefly summarize key aspects of the C/C++ memory model.  The memory model describes a series of atomic operations and the
corresponding allowed behaviors of programs that utilize them.

Any operation on an atomic object will have one of six \textit{memory orders},
each of which falls into one or more of the following categories.

\begin{description}

	\item[relaxed:]
		\code{memory\_order\_relaxed} --
		weakest memory ordering

	\item[release:]
		\code{memory\_order\_release},
		\code{memory\_order\_acq\_rel}, and
		\code{memory\_order\_seq\_cst} --
		a store-release may form release/consume or release/acquire synchronization

	\item[consume:\footnotemark{}]
		\code{memory\_order\_consume} --
		a load-consume may form release/consume synchronization

		\footnotetext{Consume is not broadly supported by compilers at
      this point due to specifying data dependencies. We treat consumes as acquires.}
    
	\item[acquire:]
		\code{memory\_order\_acquire},
		\code{memory\_order\_acq\_rel}, and
		\code{memory\_order\_seq\_cst} --
		a load-acquire may form release/acquire synchronization

	\item[seq-cst:]
		\code{memory\_order\_seq\_cst} --
		strongest memory ordering

\end{description}

\subsection{Relations}\label{sec:model-relations}

The C/C++ memory model expresses program behavior in the form
of binary relations or orderings. The following subsections will briefly
summarize the relevant relations. Much of this discussion resembles the preferred model from the 
formalization in \cite{c11popl}.

\mypara{\bf Sequenced-Before:}
The order of program operations within a single thread of execution establishes an intra-thread
\textit{sequenced-before} (\reltext{sb}) relation.
Note that while some operations in C/C++ provide no
intra-thread ordering---the equality operator (\code{==}), for example---we
ignore this detail and assume that \reltext{sb} totally orders all operations in
a thread.

\mypara{\bf Reads-From:}
The \textit{reads-from} (\reltext{rf}) relation consists of store-load pairs $(X, Y)$
such that $Y$ reads its value from the effect of $X$---or $X \relation{rf} Y$. In the
C/C++ memory model, this relation is non-trivial, as a given load operation may
read from one of many potential stores in the program execution.

\mypara{\bf Synchronizes-With:}
The \textit{synchronizes-with} (\reltext{sw}) relation captures
synchronization that occurs when certain atomic operations interact across two
threads. For instance, release/acquire synchronization occurs between a pair of
atomic operations on the same object: a store-release $X$ and a load-acquire
$Y$. If $Y$ reads from $X$, then $X$ synchronizes with $Y$---or $X
\relation{sw} Y$. Synchronization also occurs between consecutive unlock and
lock operations on the same mutex, between thread creation and the first event
in the new thread, and between the last action of a thread and the completion of
a thread-join operation targeting that thread.

\mypara{\bf Happens-Before:}
In \TOOL, we avoid consume operations, and so the \textit{happens-before}
(\reltext{hb}) relation is simply the transitive closure of \reltext{sb} and
\reltext{sw}.

The \reltext{hb} relation restricts the stores that loads can read
from.  For example, if we have two stores $X$ and $Y$ and
a load $Z$ to the same memory location and $X \relation{hb} Y
\relation{hb} Z$, then $Z$ cannot read from $X$.

\mypara{\bf Sequential Consistency:}
All seq-cst operations in a program execution form a
total ordering (\reltext{sc}) so that, for instance, a seq-cst load may not read
from a seq-cst store prior to the most recent store (to the same location) in
the \reltext{sc} ordering, nor from any store that happens before that store.
The \reltext{sc} order must be consistent with \reltext{hb}.

\mypara{\bf Modification Order:}
Each atomic object in a program execution has an associated \textit{modification order}
(\reltext{mo})---a total order of all stores to that object---which
informally represents a memory-coherent ordering in which those stores may be observed by
the rest of the program.
Note that
in general the modification orders for all objects cannot be combined
to form a consistent total ordering. We use $X \relation{mo} Y$ to represent the
fact that $X$ is modification ordered before $Y$.