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.
  36
  37 First of all, we represent a trace as an \textit{execution graph}, where each
  38 node represents each API method call with a set of ordering points, and edges
  39 between nodes are derived from the \textit{happens-before} edges and the
  40 \textit{modification order} edges between ordering points. We define
  41 \textit{opo} as the \textit{ordering point order} relation between ordering
  42 point.  Given two operations $X$ and $Y$ that are both ordering points, the
  43 \textit{modification order} edges are as follow:
  44
  45 \squishcount
  46
  47 \item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
  48
  49 \item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
  50
  51 \item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  52
  53 \item {\bf Modification Order (read-read):} $A \xrightarrow{mo} B \ \wedge \  A \xrightarrow{rf} X \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  54 \countend
  55
  56 \vspace{0.3cm}
  57
  58 Intuitively, if method $A$ has an information flow to method $B$, we want method
  59 $B$ to see the effects before method $A$. In C/C++11, on the other hand, we want
  60 method $A$ to have \code{release} semantics while method $B$ to have
  61 \code{acquire} semantics so that they establish the happens-before relationship.
  62 For example, for a concurrent queue, we want a dequeuer synchronizes with the
  63 corresponding enqueuer so that when the dequeuer obtains a reference to an
  64 object, it can read the fully initialized value of that object. To some degree
  65 this can also avoid data races. When it comes to C/C++11 data structures, the
  66 ordering points of method calls should have release/acquire semantics on stores
  67 and loads.
  68
  69 In order to relax the contraints on the original execution graph, we will have
  70 to disregard some happens-before edges. To make our model intuitive, we want to
  71 keep the happens-before edges from stores to stores and from load operations to
  72 store operations because that can ensure information is only flowing from
  73 earlier store operations. Besides, we also want to keep the happens-before edges
  74 between operations on the same memory location since otherwise the generated
  75 history will become very counter-intuitive. However, such a model does not work
  76 in C/C++ in general.  Consider the following example:
  77
  78 Consider the following example:
  79
  80 {
  81 \footnotesize
  82 \begin{verbatim}
  83 Thrd 1:     Thrd 2:     Thrd 3:     Thrd 4:
  84 x = 1;      y = 2;      r1 = x;     r3 = y;
  85 y = 1;      x = 2;      r2 = x;     r4 = y;
  86 \end{verbatim}
  87 }
  88
  89
  90 We define an action \textit{tranform} that can be performed on the graph as
  91 follow:
  92
  93 \mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in
  94 \textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
  95 address(X)\not=address(Y) \wedge
  96 X \relation{hb} Y \wedge Y \in \textit{LoadOps}\xspace
  97 \Rightarrow \forall Z, Z
  98 $.
  99
 100
 101 \begin{figure}[!htbp]
 102 \begin{algorithmic}[1]
 103 \Function{InferParams}{testcases, initialParams}
 104 \State inputParams := initialParams
 105 \If{inputParams is empty}
 106 \State inputParams := the weakest parameters \label{line:startWithRelaxed}
 107 \EndIf
 108 \ForAll{test case $t$ in testcases}
 109 \State candidates := inputParams \label{line:setOfCandidates}
 110 \State results := \{\}
 111 \While{candidates is not empty}
 112 \State Candidate $c$ := pop from candidates
 113 \State run \cdschecker with $c$ and check SC \label{line:findSCViolation}
 114 \If{$\exists$ SC violation $v$}
 115 \State \Call {StrengthenParam}{$v$, $c$, candidates} \label{line:callStrengthenParam}
 116 \Else
 117 \State results += \Call {WeakenOrderParams}{$c$} \label{line:weakenOrderParams}
 118 \EndIf
 119 \EndWhile
 120 \State inputParams := results \label{line:tmpOutputAsInput}
 121 \EndFor
 122 \State \Return{results} \label{line:finalResults}
 123 \EndFunction
 124
 125 \Procedure{StrengthenParam}{v, c, candidates}
 126 \While{$\exists$ a fix $f$ for violation $v$}
 127 \State possible\_repairs := strengthen $c$ with fix $f$ \label{line:strengthenParam}
 128 \State candidates += possible\_repairs \label{line:possibleFixes}
 129 \EndWhile
 130 \EndProcedure
 131
 132 \end{algorithmic}
 133 \caption{\label{fig:algorithmfence}Algorithm for inferring order parameters}
 134 \end{figure}
 135
 136
 137
 138 \mypara{\bf Generating the Reordering:}
 139 The \TOOL checker first builds an execution graph where the nodes are
 140 method calls and the edges represent the
 141 $\reltext{opo}$ ordering of the ordering points of the methods that
 142 correspond to the source and destination nodes.  Assuming the absence
 143 of cycles in the execution graph,
 144 the $\reltext{opo}$ ordering is used to generate the sequential history.
 145 The \TOOL checker
 146 topologically sorts the graph to generate the equivalent sequential
 147 execution.