changes
[cdsspec-compiler.git] / correctness-model / writeup / formalization.tex
index aecb783..2cc4564 100644 (file)
@@ -1,21 +1,48 @@
 \mysection{Formalization of Correctness Model}\label{sec:formalization}
 
-Unlike the SC memory model, applying linearizability can be complicated under
-C/C++ by the fact that the C/C++ memory model allows atomic loads to read from
-atomic stores that appear later in the trace and that it is in general
-impossible to produce a sequential history that preserves program order for the
-C/C++ memory model. Intuitively however, we can weaken some constraints, e.g.
+Unlike the SC memory model, finding an appropriate correctness model for
+concurrent data structures under the C/C++11 memory model is challenging. For
+example, linearizability no longer fits C/C++ by the fact that the C/C++ memory
+model allows atomic loads to read from atomic stores that appear later in the
+trace and that it is in general impossible to produce a sequential history that
+preserves program order for the C/C++ memory model.
+
+Consider the following example:
+
+{
+\footnotesize
+\begin{verbatim}
+Thrd 1:              Thrd 2:
+x = 1;               y = 1;
+r1 = y;              r2 = x;
+\end{verbatim}
+}
+
+Suppose each operation in this example is the only operation of each method
+call, and shared variables \code{x} and \code{y} are both initilly \code{0}.
+Each store operation has \code{release} semantics and each load operation has
+\code{acquire} semantics. For the execution where both \code{r1} and \code{r2}
+obtain the old value \code{0}, we encounter a challenge of generating a
+sequential history. Since neither load operation reads
+from the corresponding store, they should be ordered before their corresponding
+store operation. On the other hand, both stores happen before the other load
+(intra-thread ordering), making it impossible to topologically sort the
+operations to generate a consistent sequential history.
+
+Intuitively however, we can weaken some constraints, e.g.
 the \textit{happens-before} edges in some cases, to generate a reordering of
 ordering points such that they yield a sequential history that is consistent
-with the specification. We formalize our approach as follow.
-
-We represent a trace as an \textit{execution graph}, where each node represents
-each API method call with a set of ordering points, and edges between nodes are
-derived from the \textit{happens-before} edges and the \textit{modification
-order} edges between ordering points. We define \textit{opo} as the
-\textit{ordering point order} relation between ordering point.  Given two
-operations $X$ and $Y$ that are both ordering points, the \textit{modification
-order} edges are as follow:
+with the specification. We formalize our approach as follow. The goal is to come
+up with a correctness model that is weaker than linearizability and SC and yet
+is composable.
+
+First of all, we represent a trace as an \textit{execution graph}, where each
+node represents each API method call with a set of ordering points, and edges
+between nodes are derived from the \textit{happens-before} edges and the
+\textit{modification order} edges between ordering points. We define
+\textit{opo} as the \textit{ordering point order} relation between ordering
+point.  Given two operations $X$ and $Y$ that are both ordering points, the
+\textit{modification order} edges are as follow:
 
 \squishcount
 
@@ -30,18 +57,74 @@ order} edges are as follow:
 
 \vspace{0.3cm}
 
-Intuitively, if method $A$ 
-
-In order to relax the contraints on the original execution graph, we define an
-action \textit{tranform} that can be performed on the graph as follow:
-
-\mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in
-\textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
+Intuitively, if method $A$ has an information flow to method $B$, we want method
+$B$ to see the effects before method $A$. In C/C++11, on the other hand, we want
+method $A$ to have \code{release} semantics while method $B$ to have
+\code{acquire} semantics so that they establish the happens-before relationship.
+For example, for a concurrent queue, we want a dequeuer synchronizes with the
+corresponding enqueuer so that when the dequeuer obtains a reference to an
+object, it can read the fully initialized value of that object. To some degree
+this can also avoid data races. When it comes to C/C++11 data structures, the
+ordering points of method calls should have release/acquire semantics on stores
+and loads.
+
+In order to relax the contraints on the original execution graph, we will have
+to disregard some happens-before edges. To make our model intuitive, we want to
+keep the happens-before edges from stores to stores and from load operations to
+store operations because that can ensure information is only flowing from
+earlier store operations. Besides, we also want to keep the happens-before edges
+between operations on the same memory location since otherwise the generated
+history will become very counter-intuitive. However, such a model does not work
+in C/C++ in general.  Consider the following example:
+
+Consider the following example:
+
+{
+\footnotesize
+\begin{verbatim}
+Thrd 1:     Thrd 2:     Thrd 3:     Thrd 4:
+x = 1;      y = 2;      r1 = x;     r3 = y;
+y = 1;      x = 2;      r2 = x;     r4 = y;
+\end{verbatim}
+}
+
+We encounter a challenge for the execution where the following holds:
+\path{r1 == 2 && r2 == 1 && r3 == 1 && r4 == 2}. For any total order that is
+consistent with the happens-before relation, that total order will be
+inconsistent with the modification order in either variable \code{x} or
+\code{y}. For example, if \code{y = 1} is ordered before \code{y = 2}, then
+\code{x = 1} is ordered before \code{x = 2} while \code{r1 = x} is ordered
+before \code{r2 = x}. As a result, we cannot possibly move up the second load
+operation \code{r2 = x} across \code{r1 = x} to generate a consistent sequential
+history. To solve this, one option is that allow loads to move up any operation
+including load and store operation on the same location. However, it is
+extremely conuter-intuitive for a later load operation to read an older value.
+By analysis, the problem here is that the store operations with different values
+to the same memory location are not ordered. This is actually a really rare case
+because it could be possible that only one store operation takes effect and all
+other store operations are useless. We believe that such case of blind stores
+from different threads is not the general pattern for concurrent data
+structures, and we believe that store operations are ordered. In terms of
+ordering points, we believe that in real-world data structures, store operations
+of ordering points are ordered by happens-before relation.
+\todo{argue why ordered stores are reasonable to concurrent data structures}
+
+We next define an action called \textit{tranform} that can be performed on the graph as
+follow:
+
+$ \forall X, Y, X \in \textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
 address(X)\not=address(Y) \wedge
-X \relation{hb} Y \wedge Y \in \textit{LoadOps}\xspace
-\Rightarrow \forall Z, Z
+X \relation{hb} Y \wedge
+Y \in \textit{LoadOps}\xspace
+\Rightarrow
+\forall Z,
+Z \in \textit{orderingPoints}\xspace \wedge 
+Z \relation{hb} X, 
+Z \relation{hb} Y \wedge \neg X \relation{hb} Y
 $.
 
+Under these analysis and assumptions, we clearly define our correctness model as
+follow:
 
 \begin{figure}[!htbp]
 \begin{algorithmic}[1]
@@ -78,15 +161,4 @@ $.
 \caption{\label{fig:algorithmfence}Algorithm for inferring order parameters}
 \end{figure}
 
-
-
-\mypara{\bf Generating the Reordering:}
-The \TOOL checker first builds an execution graph where the nodes are
-method calls and the edges represent the
-$\reltext{opo}$ ordering of the ordering points of the methods that
-correspond to the source and destination nodes.  Assuming the absence
-of cycles in the execution graph, 
-the $\reltext{opo}$ ordering is used to generate the sequential history.
-The \TOOL checker 
-topologically sorts the graph to generate the equivalent sequential
-execution.
+\todo{prove that our correctness model is composable}