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.
+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
\end{verbatim}
}
-
-We define an action \textit{tranform} that can be performed on the graph as
+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:
-\mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in
-\textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
+$ \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]
\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}
projects / cdsspec-compiler.git / blobdiff