author Peizhao Ou Thu, 16 Apr 2015 00:36:11 +0000 (17:36 -0700) committer Peizhao Ou Thu, 16 Apr 2015 00:36:11 +0000 (17:36 -0700)

index fc22c7e..0aff8cd 100644 (file)
@@ -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}

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
\Rightarrow
\forall Z,
\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 $. 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}
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}
\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}

\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}
\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?
+
+