changes

diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex
index b973eb5a91e01d50cb94556ea4cb2e06ae786551..fc22c7e64dbab26d16d258cd7d975d6a4be24778 100644 (file)
--- a/correctness-model/writeup/formalization.tex
+++ b/correctness-model/writeup/formalization.tex
@@ -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
+moves up certain load operations (Line~\ref{line:moveUpLoads}); thus, the store
+to store and load to store \hb relation hold. Since load operations that read
+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
+store operation, and thus the read-read and read-write \mo consistency also
+holds. We then illustrates that the \hb relation between the same memory
+location also holds by contradiction. The only possibility of moving load
+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}[1]
 \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[2] 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}