From 5eb37672a5a8772dc41d78e03ffad77e1d1e875b Mon Sep 17 00:00:00 2001
From: Peizhao Ou
Date: Wed, 15 Apr 2015 17:36:11 0700
Subject: [PATCH] changes

correctnessmodel/writeup/formalization.tex  39 +++++++++++++++++
1 file changed, 33 insertions(+), 6 deletions()
diff git a/correctnessmodel/writeup/formalization.tex b/correctnessmodel/writeup/formalization.tex
index fc22c7e..0aff8cd 100644
 a/correctnessmodel/writeup/formalization.tex
+++ b/correctnessmodel/writeup/formalization.tex
@@ 109,12 +109,12 @@ ordering points, we believe that in realworld data structures, store operations
of ordering points are ordered by happensbefore 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 happensbefore 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{happensbefore} 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 happensbefore relation on
+$o$ and $l''$. When it finishes generating $H$, we have a finite steps of
+transform taken on the happensbefore 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?
+
+

2.17.1