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

We next briefly summarize the key aspects of the C/C++ memory model.  The
memory model describes a set of atomic operations and the
corresponding allowed behaviors of programs that utilize them.  A more
detailed formal treatment of the memory model~\cite{c11popl} and a
more detailed informal description~\cite{cpp11spec,c11spec} are
available in the literature.  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{\small{memory\_order\_relaxed}} --
		weakest ordering

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

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

		\footnotetext{Consume is not broadly supported by compilers due to
      challenges associate with preserving data dependencies and is
      unlikely to provide significant performance gains on x86
      hardware. We take the same approach as many compilers and treat
      consumes as acquires.}
    
	\item[acquire:]
		\code{\small{memory\_order\_acquire}},
		\code{\small{memory\_order\_acq\_rel}}, and
		\code{\small{memory\_order\_seq\_cst}} --
		a load-acquire may form release/acquire synchronization

	\item[seq-cst:]
		\code{\small{memory\_order\_seq\_cst}} --
		strongest 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$.

\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.
In general the modification orders for all objects cannot be combined
to form a consistent total ordering.




