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