XGitUrl: http://plrg.eecs.uci.edu/git/?p=cdsspeccompiler.git;a=blobdiff_plain;f=correctnessmodel%2Fwriteup%2Fformalization.tex;h=5d10f43db2ba4a9af4622b3d8f2dc1802a707e92;hp=aecb783bbdc3808453289fe1cf47c23f6cb47a47;hb=e8942c527bf582229e12d9a922a099dd168375d6;hpb=f7207fbf6086300565ee3f30c220fd37a891eb4e
diff git a/correctnessmodel/writeup/formalization.tex b/correctnessmodel/writeup/formalization.tex
index aecb783..5d10f43 100644
 a/correctnessmodel/writeup/formalization.tex
+++ b/correctnessmodel/writeup/formalization.tex
@@ 1,21 +1,46 @@
\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
+(intrathread 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{happensbefore} 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{happensbefore} 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:
+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{happensbefore} 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,10 +55,40 @@ 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:
+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 happensbefore 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 happensbefore edges. To make our model intuitive, we want to
+keep the happensbefore 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 happensbefore edges
+between operations on the same memory location since otherwise the generated
+history will become very counterintuitive. 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 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