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 an trace as a \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. Given two operations $X$ and $Y$ that are
  16 both ordering points, the \textit{modification order} edges are as follows:
  17
  18 \squishcount
  19 \item {\bf Reads-From:} $X \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  20
  21 \item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
  22
  23 \item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \  A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
  24
  25 \item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \  B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
  26
  27 \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$.
  28 \countend
  29
  30
  31
  32 \mypara{\bf Generating the Reordering:}
  33 The \TOOL checker first builds an execution graph where the nodes are
  34 method calls and the edges represent the
  35 $\reltext{opo}$ ordering of the ordering points of the methods that
  36 correspond to the source and destination nodes.  Assuming the absence
  37 of cycles in the execution graph,
  38 the $\reltext{opo}$ ordering is used to generate the sequential history.
  39 The \TOOL checker
  40 topologically sorts the graph to generate the equivalent sequential
  41 execution.