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}

-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,
@@ -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?
+
+