correctness-model/writeup/.#memorymodel.tex.1.1

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