correctness-model/writeup/formalization.tex

   1 \mysection{Formalization of Correctness Model}\label{sec:formalization}
   2
   3 Unlike the SC memory model, applying linearizability can be complicated under
   4 C/C++ by the fact that the C/C++ memory model allows atomic loads to read from
   5 atomic stores that appear later in the trace and that it is in general
   6 impossible to produce a sequential history that preserves program order for the
   7 C/C++ memory model. Intuitively however, we can weaken some constraints, e.g.
   8 the \textit{happens-before} edges in some cases, to generate a reordering of
   9 ordering points such that they yield a sequential history that is consistent
  10 with the specification. We formalize our approach as follow.
  11
  12 We represent a trace as an \textit{execution graph}, where each node represents
  13 each API method call with a set of ordering points, and edges between nodes are
  14 derived from the \textit{happens-before} edges and the \textit{modification
  15 order} edges between ordering points. We define \textit{opo} as the
  16 \textit{ordering point order} relation between ordering point.  Given two
  17 operations $X$ and $Y$ that are both ordering points, the \textit{modification
  18 order} edges are as follow:
  19
  20 \squishcount
  21
  22 \item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
  23
  24 \item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
  25
  26 \item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  27
  28 \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$.
  29 \countend
  30
  31 \vspace{0.3cm}
  32
  33 Intuitively, if method $A$
  34
  35 In order to relax the contraints on the original execution graph, we define an
  36 action \textit{tranform} that can be performed on the graph as follow:
  37
  38 \mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in
  39 \textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
  40 address(X)\not=address(Y) \wedge
  41 X \relation{hb} Y \wedge Y \in \textit{LoadOps}\xspace
  42 \Rightarrow \forall Z, Z
  43 $.
  44
  45
  46 \begin{figure}[!htbp]
  47 \begin{algorithmic}[1]
  48 \Function{InferParams}{testcases, initialParams}
  49 \State inputParams := initialParams
  50 \If{inputParams is empty}
  51 \State inputParams := the weakest parameters \label{line:startWithRelaxed}
  52 \EndIf
  53 \ForAll{test case $t$ in testcases}
  54 \State candidates := inputParams \label{line:setOfCandidates}
  55 \State results := \{\}
  56 \While{candidates is not empty}
  57 \State Candidate $c$ := pop from candidates
  58 \State run \cdschecker with $c$ and check SC \label{line:findSCViolation}
  59 \If{$\exists$ SC violation $v$}
  60 \State \Call {StrengthenParam}{$v$, $c$, candidates} \label{line:callStrengthenParam}
  61 \Else
  62 \State results += \Call {WeakenOrderParams}{$c$} \label{line:weakenOrderParams}
  63 \EndIf
  64 \EndWhile
  65 \State inputParams := results \label{line:tmpOutputAsInput}
  66 \EndFor
  67 \State \Return{results} \label{line:finalResults}
  68 \EndFunction
  69
  70 \Procedure{StrengthenParam}{v, c, candidates}
  71 \While{$\exists$ a fix $f$ for violation $v$}
  72 \State possible\_repairs := strengthen $c$ with fix $f$ \label{line:strengthenParam}
  73 \State candidates += possible\_repairs \label{line:possibleFixes}
  74 \EndWhile
  75 \EndProcedure
  76
  77 \end{algorithmic}
  78 \caption{\label{fig:algorithmfence}Algorithm for inferring order parameters}
  79 \end{figure}
  80
  81
  82
  83 \mypara{\bf Generating the Reordering:}
  84 The \TOOL checker first builds an execution graph where the nodes are
  85 method calls and the edges represent the
  86 $\reltext{opo}$ ordering of the ordering points of the methods that
  87 correspond to the source and destination nodes.  Assuming the absence
  88 of cycles in the execution graph,
  89 the $\reltext{opo}$ ordering is used to generate the sequential history.
  90 The \TOOL checker
  91 topologically sorts the graph to generate the equivalent sequential
  92 execution.