correctness-model/writeup/memorymodel.tex

   1 \section{C/C++ Memory Model}\label{sec:memorymodel}
   2
   3 We next briefly summarize the key aspects of the C/C++ memory model.  The
   4 memory model describes a set of atomic operations and the
   5 corresponding allowed behaviors of programs that utilize them.  A more
   6 detailed formal treatment of the memory model~\cite{c11popl} and a
   7 more detailed informal description~\cite{cpp11spec,c11spec} are
   8 available in the literature.  Any operation on an atomic object will
   9 have one of six \textit{memory orders}, each of which falls into one
  10 or more of the following categories.
  11
  12 \begin{description}
  13
  14         \item[relaxed:]
  15                 \code{\small{memory\_order\_relaxed}} --
  16                 weakest ordering
  17
  18         \item[release:]
  19                 \code{\small{memory\_order\_release}},
  20                 \code{\small{memory\_order\_acq\_rel}}, and
  21                 \code{\small{memory\_order\_seq\_cst}} --
  22                 a store-release may form release/consume or release/acquire synchronization
  23
  24         \item[consume:\footnotemark{}]
  25                 \code{\small{memory\_order\_consume}} --
  26                 a load-consume may form release/consume synchronization
  27
  28                 \footnotetext{Consume is not broadly supported by compilers due to
  29       challenges associate with preserving data dependencies and is
  30       unlikely to provide significant performance gains on x86
  31       hardware. We take the same approach as many compilers and treat
  32       consumes as acquires.}
  33
  34         \item[acquire:]
  35                 \code{\small{memory\_order\_acquire}},
  36                 \code{\small{memory\_order\_acq\_rel}}, and
  37                 \code{\small{memory\_order\_seq\_cst}} --
  38                 a load-acquire may form release/acquire synchronization
  39
  40         \item[seq-cst:]
  41                 \code{\small{memory\_order\_seq\_cst}} --
  42                 strongest ordering
  43
  44 \end{description}
  45
  46 \subsection{Relations}\label{sec:model-relations}
  47
  48 The C/C++ memory model expresses program behavior in the form
  49 of binary relations or orderings. The following subsections will briefly
  50 summarize the relevant relations. Much of this discussion resembles the preferred model from the
  51 formalization in \cite{c11popl}.
  52
  53 \mypara{\bf Sequenced-Before:}
  54 The order of program operations within a single thread of execution establishes an intra-thread
  55 \textit{sequenced-before} (\reltext{sb}) relation.
  56 Note that while some operations in C/C++ provide no
  57 intra-thread ordering---the equality operator (\code{==}), for example---we
  58 ignore this detail and assume that \reltext{sb} totally orders all operations in
  59 a thread.
  60
  61 \mypara{\bf Reads-From:}
  62 The \textit{reads-from} (\reltext{rf}) relation consists of store-load pairs $(X, Y)$
  63 such that $Y$ reads its value from the effect of $X$---or $X \relation{rf} Y$. In the
  64 C/C++ memory model, this relation is non-trivial, as a given load operation may
  65 read from one of many potential stores in the program execution.
  66
  67 \mypara{\bf Synchronizes-With:}
  68 The \textit{synchronizes-with} (\reltext{sw}) relation captures
  69 synchronization that occurs when certain atomic operations interact across two
  70 threads. For instance, release/acquire synchronization occurs between a pair of
  71 atomic operations on the same object: a store-release $X$ and a load-acquire
  72 $Y$. If $Y$ reads from $X$, then $X$ synchronizes with $Y$---or $X
  73 \relation{sw} Y$.
  74
  75 \mypara{\bf Happens-Before:}
  76 In \TOOL, we avoid consume operations, and so the \textit{happens-before}
  77 (\reltext{hb}) relation is simply the transitive closure of \reltext{sb} and
  78 \reltext{sw}.
  79
  80 The \reltext{hb} relation restricts the stores that loads can read
  81 from.  For example, if we have two stores $X$ and $Y$ and
  82 a load $Z$ to the same memory location and $X \relation{hb} Y
  83 \relation{hb} Z$, then $Z$ cannot read from $X$.
  84
  85 \mypara{\bf Sequential Consistency:}
  86 All seq-cst operations in a program execution form a
  87 total ordering (\reltext{sc}) so that, for instance, a seq-cst load may not read
  88 from a seq-cst store prior to the most recent store (to the same location) in
  89 the \reltext{sc} ordering, nor from any store that happens before that store.
  90 The \reltext{sc} order must be consistent with \reltext{hb}.
  91
  92 \mypara{\bf Modification Order:}
  93 Each atomic object in a program execution has an associated \textit{modification order}
  94 (\reltext{mo})---a total order of all stores to that object---which
  95 informally represents a memory-coherent ordering in which those stores may be observed by
  96 the rest of the program.
  97 In general the modification orders for all objects cannot be combined
  98 to form a consistent total ordering.
  99
 100
 101
 102