changes

diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex
index fc22c7e64dbab26d16d258cd7d975d6a4be24778..0aff8cdd14cce9205ba77343566aecb22d5d6f5c 100644 (file)
--- a/correctness-model/writeup/formalization.tex
+++ b/correctness-model/writeup/formalization.tex
@@ -109,12 +109,12 @@ ordering points, we believe that in real-world data structures, store operations
 of ordering points are ordered by happens-before relation.
 \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:
+We next define a \textit{relaxing action} that takes input a relation $R$
+and outputs a new relation $R'$. We denote $R_r$ as the new relation after
+taking a relaxing action $r$ on relation $R$. 
 
-$ \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
+$ \forall X, Y, address(X)\not=address(Y) \wedge
+X \relation{R} Y \wedge
 Y \in \textit{LoadOps}\xspace
 \Rightarrow
 \forall Z,
@@ -122,6 +122,9 @@ Z \in \textit{orderingPoints}\xspace \wedge
 Z \relation{hb} X, 
 Z \relation{hb} Y \wedge \neg X \relation{hb} Y $.
 
+We denote \textit{hb}$_r$ as the happens-before relation after taking a relaxing action
+$r$.
+
 Under these analysis and assumptions, we present Lemma~\ref{seqHistoryExistence}.
 
 \begin{lemma} \label{seqHistoryExistence}
@@ -185,7 +188,31 @@ that do not read from $w'$ (including $r$)  \strut}
 \end{figure}
 
 \begin{lemma} \label{equivalence}
-
+For any legal C/C++11 execution, where store / load operations have release /
+acquire semantics and store operations to the same memory location are ordered
+by \textit{happens-before} relation, the sequential history $H$ generated by the
+algorithm in Figure~\ref{fig:algorithmConsistentHistory} is equivalent to some
+topological sorting of the operations by \mo consistency and \hb relation after
+finite steps of actions (\textit{transform}).
 \end{lemma}
 
+\begin{proof}
+In the algorithm showed in Figure~\ref{fig:algorithmConsistentHistory}, during
+each iteration it can have a set of load operations $l'$
+(Line~\ref{line:loadSet}) to be moved up across the most recent store operation
+$w'$. For any load opeartion $l''$ in the set $l'$, as showed in the proof of
+Lemma~\ref{seqHistoryExistence}, no other operation on the same memory location
+exists between $w'$ and $l''$. When $l''$ moves across an operation $o$ that
+happens before $l''$, we make a transform $t$ on the happens-before relation on
+$o$ and $l''$. When it finishes generating $H$, we have a finite steps of
+transform taken on the happens-before graph, denoted as $T$. We also denote that
+\textit{hb}$_T$ as the happens before relation after $T$. 
+\end{proof}
+
 \todo{formalize composability and show hat our correctness model is composable}
+1. Should we still assume that store operations to the same memory location are
+ordered?
+2. Or is it safe to assume that variables from two release/acquire consistent
+objects should be disjoint?
+
+