changes

[cdsspec-compiler.git] / correctness-model / writeup / .#memorymodel.tex.1.1

diff --git a/correctness-model/writeup/.#memorymodel.tex.1.1 b/correctness-model/writeup/.#memorymodel.tex.1.1
new file mode 100644 (file)
index 0000000..f60d9da
--- /dev/null
+++ b/correctness-model/writeup/.#memorymodel.tex.1.1
@@ -0,0 +1,101 @@
+\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$.
+
+
+
+