+++ /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