--- /dev/null
+\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.
+
+
+
+
projects / cdsspec-compiler.git / blobdiff