author Peizhao Ou Wed, 15 Apr 2015 00:38:06 +0000 (17:38 -0700) committer Peizhao Ou Wed, 15 Apr 2015 00:38:06 +0000 (17:38 -0700)

index b973eb5..fc22c7e 100644 (file)
@@ -12,9 +12,9 @@ Consider the following example:
{
\footnotesize
\begin{verbatim}
-Thrd 1:              Thrd 2:
-x = 1;               y = 1;
-r1 = y;              r2 = x;
+ Thrd 1:              Thrd 2:
+ x = 1;               y = 1;
+ r1 = y;              r2 = x;
\end{verbatim}
}

@@ -82,9 +82,9 @@ 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;
+ 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}
}

@@ -107,7 +107,7 @@ 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}
+\todo{explain 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:
@@ -134,35 +134,48 @@ operations and operations on the same memory location.
\end{lemma}

\begin{proof}
-
-To prove Lemma~\ref{seqHistoryExistence}, we present our algorithm to generate
-such a sequential history and prove that such an algorithm is feasible. We first
-topologically sort the operations by the \hb relation and have a sequential
-history $H$. By C/C++11, \hb is acyclic. Since every store / load operations
-have release / acquire semantics, every reads-from edge is also a \hb edge.
-Thus, a load operation can only read from an old store in $H$. We iterate the
-load operations on the same memory location from the end of $H$. For each load
-operation $X$ that reads from some store $Y$ on location $M$, if no store
-operation on $M$ exists between $X$ and $Y$ in $H$, any load operations on $M$
-before $X$ and after $Y$ cannot be \mo consistency ordered after $Y$ so $Y$ is
-ordered consistently; otherwise, if there exists
-
-
+To prove Lemma~\ref{seqHistoryExistence}, we present in
+Figure~\ref{fig:algorithmConsistentHistory} our constructive algorithm that
+generates a sequential history and prove that its output satisfies the
+condition. This algorithm topologically sort operations by \hb, and then it only
+from the correct store is not moved (Line~\ref{line:loadSet}) and store
+operations are ordered by \hb relation, the write-write and write-read \mo
+consistency holds. By induction, moving up load operations will end up placing
+load operations between the store operation that they read from and the next
+holds. We then illustrates that the \hb relation between the same memory
+operations across operations on the same location lies in
+Line~\ref{line:loadSet} where there exists an operation $o$ between
+$w'$
+and $r$, and $o$ is not moved up while some operation $r'$ in $l'$ is
+moved up, and $o$ happens before $r'$. If $o$ is a load operation, $o$ must
+read from $w$ otherwise $o$ will be moved up. Thus we have the relation: $w +\relation{hb} w' \relation{hb} o \relation{hb} r'$, which contradicts
+the fact that $r$ reads from $w$. Likewise, if $o$ is a store operation, since
+store operations are ordered by \hb relation, we have the relation: $w +\relation{hb} o \relation{hb} r'$ and this is a contradiciton similarly.
+Therefore, the generated sequential history by this algorithm satisfies the
+conditions in this Lemma.
\end{proof}

-
\begin{figure}[!htbp]
\begin{algorithmic}
\Function{GenerateConsistentHistory}{trace}
\State $H$ := topologically sort operations of trace by \hb
\ForAll{load operation $r$ in $H$ in reverse order}
-\State $w$ := store operation $r$ reads from
+\State $w$ := store operation that $r$ reads from
\State $m$ := memory location of $r$
\If{no store operations on $m$ between $w$ and $r$}
\State continue
\Else
-\State $w\prime$ := most recent store on $m$ before $r$
-\State $l\prime$ := set of load operations between $w\prime$ and $r$ \pushcode that $w\prime$ is not \hb before
+\State $w'$ := most recent store on $m$ before $r$
+\State  \parbox[t]{\dimexpr\linewidth-\algorithmicindent}{$l'$ := set of \label{line:loadSet}
+load operations on $m$ between $w'$ and $r$\\
+that do not read from $w'$ (including $r$)  \strut}
+\State move $l'$ (keep inner order) above $w$ and continue \label{line:moveUpLoads}
\EndIf
\EndFor
\State \Return{$H$} \label{line:finalResults}
@@ -171,4 +184,8 @@ ordered consistently; otherwise, if there exists
\caption{\label{fig:algorithmConsistentHistory}Algorithm for generating a consistent sequential history}
\end{figure}

-\todo{prove that our correctness model is composable}
+\begin{lemma} \label{equivalence}
+
+\end{lemma}
+
+\todo{formalize composability and show hat our correctness model is composable}