correctness-model/writeup/formalization.tex

   1 \mysection{Formalization of Correctness Model}\label{sec:formalization}
   2
   3 Unlike the SC memory model, finding an appropriate correctness model for
   4 concurrent data structures under the C/C++11 memory model is challenging. For
   5 example, linearizability no longer fits C/C++ by the fact that the C/C++ memory
   6 model allows atomic loads to read from atomic stores that appear later in the
   7 trace and that it is in general impossible to produce a sequential history that
   8 preserves program order for the C/C++ memory model.
   9
  10 Consider the following example:
  11
  12 {
  13 \footnotesize
  14 \begin{verbatim}
  15  Thrd 1:              Thrd 2:
  16  x = 1;               y = 1;
  17  r1 = y;              r2 = x;
  18 \end{verbatim}
  19 }
  20
  21 Suppose each operation in this example is the only operation of each method
  22 call, and shared variables \code{x} and \code{y} are both initilly \code{0}.
  23 Each store operation has \code{release} semantics and each load operation has
  24 \code{acquire} semantics. For the execution where both \code{r1} and \code{r2}
  25 obtain the old value \code{0}, we encounter a challenge of generating a
  26 sequential history. Since neither load operation reads
  27 from the corresponding store, they should be ordered before their corresponding
  28 store operation. On the other hand, both stores happen before the other load
  29 (intra-thread ordering), making it impossible to topologically sort the
  30 operations to generate a consistent sequential history.
  31
  32 Intuitively however, we can weaken some constraints, e.g.
  33 the \textit{happens-before} edges in some cases, to generate a reordering of
  34 ordering points such that they yield a sequential history that is consistent
  35 with the specification. We formalize our approach as follow. The goal is to come
  36 up with a correctness model that is weaker than linearizability and SC and yet
  37 is composable.
  38
  39 First of all, we represent a trace as an \textit{execution graph}, where each
  40 node represents each API method call with a set of ordering points, and edges
  41 between nodes are derived from the \textit{happens-before} edges and the
  42 \textit{modification order} edges between ordering points. We define
  43 \textit{opo} as the \textit{ordering point order} relation between ordering
  44 point.  Given two operations $X$ and $Y$ that are both ordering points, the
  45 \textit{modification order consistency} edges are as follow:
  46
  47 \squishcount
  48
  49 \item {\bf Modification Order Consistency (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
  50
  51 \item {\bf Modification Order Consistency (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
  52
  53 \item {\bf Modification Order Consistency (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  54
  55 \item {\bf Modification Order Consistency (read-read):} $A \xrightarrow{mo} B \ \wedge \  A \xrightarrow{rf} X \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  56 \countend
  57
  58 \vspace{0.3cm}
  59
  60 Intuitively, if method $A$ has an information flow to method $B$, we want method
  61 $B$ to see the effects before method $A$. In C/C++11, on the other hand, we want
  62 method $A$ to have \code{release} semantics while method $B$ to have
  63 \code{acquire} semantics so that they establish the happens-before relationship.
  64 For example, for a concurrent queue, we want a dequeuer synchronizes with the
  65 corresponding enqueuer so that when the dequeuer obtains a reference to an
  66 object, it can read the fully initialized value of that object. To some degree
  67 this can also avoid data races. When it comes to C/C++11 data structures, the
  68 ordering points of method calls should have release/acquire semantics on stores
  69 and loads.
  70
  71 In order to relax the contraints on the original execution graph, we will have
  72 to disregard some happens-before edges. To make our model intuitive, we want to
  73 keep the happens-before edges from stores to stores and from load operations to
  74 store operations because that can ensure information is only flowing from
  75 earlier store operations. Besides, we also want to keep the happens-before edges
  76 between operations on the same memory location since otherwise the generated
  77 history will become very counter-intuitive. However, such a model does not work
  78 in C/C++ in general.  Consider the following example:
  79
  80 Consider the following example:
  81
  82 {
  83 \footnotesize
  84 \begin{verbatim}
  85  Thrd 1:     Thrd 2:     Thrd 3:     Thrd 4:
  86  x = 1;      y = 2;      r1 = x;     r3 = y;
  87  y = 1;      x = 2;      r2 = x;     r4 = y;
  88 \end{verbatim}
  89 }
  90
  91 We encounter a challenge for the execution where the following holds:
  92 \path{r1 == 2 && r2 == 1 && r3 == 1 && r4 == 2}. For any total order that is
  93 consistent with the happens-before relation, that total order will be
  94 inconsistent with the modification order in either variable \code{x} or
  95 \code{y}. For example, if \code{y = 1} is ordered before \code{y = 2}, then
  96 \code{x = 1} is ordered before \code{x = 2} while \code{r1 = x} is ordered
  97 before \code{r2 = x}. As a result, we cannot possibly move up the second load
  98 operation \code{r2 = x} across \code{r1 = x} to generate a consistent sequential
  99 history. To solve this, one option is that allow loads to move up any operation
 100 including load and store operation on the same location. However, it is
 101 extremely conuter-intuitive for a later load operation to read an older value.
 102 By analysis, the problem here is that the store operations with different values
 103 to the same memory location are not ordered. This is actually a really rare case
 104 because it could be possible that only one store operation takes effect and all
 105 other store operations are useless. We believe that such case of blind stores
 106 from different threads is not the general pattern for concurrent data
 107 structures, and we believe that store operations are ordered. In terms of
 108 ordering points, we believe that in real-world data structures, store operations
 109 of ordering points are ordered by happens-before relation.
 110 \todo{explain why ordered stores are reasonable to concurrent data structures}
 111
 112 We next define a \textit{relaxing action} that takes input a relation $R$
 113 and outputs a new relation $R'$. We denote $R_r$ as the new relation after
 114 taking a relaxing action $r$ on relation $R$.
 115
 116 $ \forall X, Y, address(X)\not=address(Y) \wedge
 117 X \relation{R} Y \wedge
 118 Y \in \textit{LoadOps}\xspace
 119 \Rightarrow
 120 \forall Z,
 121 Z \in \textit{orderingPoints}\xspace \wedge
 122 Z \relation{hb} X,
 123 Z \relation{hb} Y \wedge \neg X \relation{hb} Y $.
 124
 125 We denote \textit{hb}$_r$ as the happens-before relation after taking a relaxing action
 126 $r$.
 127
 128 Under these analysis and assumptions, we present Lemma~\ref{seqHistoryExistence}.
 129
 130 \begin{lemma} \label{seqHistoryExistence}
 131 For any legal C/C++11 execution, where store / load operations have release / acquire
 132 semantics and store operations to the same memory location are ordered by
 133 \textit{happens-before} relation, there exists a sequential history
 134 that is consistent with the modification order consistency and the
 135 happens-before relation in terms of store to store operations, load to store
 136 operations and operations on the same memory location.
 137 \end{lemma}
 138
 139 \begin{proof}
 140 To prove Lemma~\ref{seqHistoryExistence}, we present in
 141 Figure~\ref{fig:algorithmConsistentHistory} our constructive algorithm that
 142 generates a sequential history and prove that its output satisfies the
 143 condition. This algorithm topologically sort operations by \hb, and then it only
 144 moves up certain load operations (Line~\ref{line:moveUpLoads}); thus, the store
 145 to store and load to store \hb relation hold. Since load operations that read
 146 from the correct store is not moved (Line~\ref{line:loadSet}) and store
 147 operations are ordered by \hb relation, the write-write and write-read \mo
 148 consistency holds. By induction, moving up load operations will end up placing
 149 load operations between the store operation that they read from and the next
 150 store operation, and thus the read-read and read-write \mo consistency also
 151 holds. We then illustrates that the \hb relation between the same memory
 152 location also holds by contradiction. The only possibility of moving load
 153 operations across operations on the same location lies in
 154 Line~\ref{line:loadSet} where there exists an operation $o$ between
 155 $w'$
 156 and $r$, and $o$ is not moved up while some operation $r'$ in $l'$ is
 157 moved up, and $o$ happens before $r'$. If $o$ is a load operation, $o$ must
 158 read from $w$ otherwise $o$ will be moved up. Thus we have the relation: $w
 159 \relation{hb} w' \relation{hb} o \relation{hb} r'$, which contradicts
 160 the fact that $r$ reads from $w$. Likewise, if $o$ is a store operation, since
 161 store operations are ordered by \hb relation, we have the relation: $w
 162 \relation{hb} o \relation{hb} r'$ and this is a contradiciton similarly.
 163 Therefore, the generated sequential history by this algorithm satisfies the
 164 conditions in this Lemma.
 165 \end{proof}
 166
 167 \begin{figure}[!htbp]
 168 \begin{algorithmic}[1]
 169 \Function{GenerateConsistentHistory}{trace}
 170 \State $H$ := topologically sort operations of trace by \hb
 171 \ForAll{load operation $r$ in $H$ in reverse order}
 172 \State $w$ := store operation that $r$ reads from
 173 \State $m$ := memory location of $r$
 174 \If{no store operations on $m$ between $w$ and $r$}
 175 \State continue
 176 \Else
 177 \State $w'$ := most recent store on $m$ before $r$
 178 \State  \parbox[t]{\dimexpr\linewidth-\algorithmicindent}{$l'$ := set of \label{line:loadSet}
 179 load operations on $m$ between $w'$ and $r$\\
 180 that do not read from $w'$ (including $r$)  \strut}
 181 \State move $l'$ (keep inner order) above $w$ and continue \label{line:moveUpLoads}
 182 \EndIf
 183 \EndFor
 184 \State \Return{$H$} \label{line:finalResults}
 185 \EndFunction
 186 \end{algorithmic}
 187 \caption{\label{fig:algorithmConsistentHistory}Algorithm for generating a consistent sequential history}
 188 \end{figure}
 189
 190 \begin{lemma} \label{equivalence}
 191 For any legal C/C++11 execution, where store / load operations have release /
 192 acquire semantics and store operations to the same memory location are ordered
 193 by \textit{happens-before} relation, the sequential history $H$ generated by the
 194 algorithm in Figure~\ref{fig:algorithmConsistentHistory} is equivalent to some
 195 topological sorting of the operations by \mo consistency and \hb relation after
 196 finite steps of actions (\textit{transform}).
 197 \end{lemma}
 198
 199 \begin{proof}
 200 In the algorithm showed in Figure~\ref{fig:algorithmConsistentHistory}, during
 201 each iteration it can have a set of load operations $l'$
 202 (Line~\ref{line:loadSet}) to be moved up across the most recent store operation
 203 $w'$. For any load opeartion $l''$ in the set $l'$, as showed in the proof of
 204 Lemma~\ref{seqHistoryExistence}, no other operation on the same memory location
 205 exists between $w'$ and $l''$. When $l''$ moves across an operation $o$ that
 206 happens before $l''$, we make a transform $t$ on the happens-before relation on
 207 $o$ and $l''$. When it finishes generating $H$, we have a finite steps of
 208 transform taken on the happens-before graph, denoted as $T$. We also denote that
 209 \textit{hb}$_T$ as the happens before relation after $T$.
 210 \end{proof}
 211
 212 \todo{formalize composability and show hat our correctness model is composable}
 213 1. Should we still assume that store operations to the same memory location are
 214 ordered?
 215 2. Or is it safe to assume that variables from two release/acquire consistent
 216 objects should be disjoint?
 217
 218