From 5eb37672a5a8772dc41d78e03ffad77e1d1e875b Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Wed, 15 Apr 2015 17:36:11 -0700 Subject: [PATCH] changes --- correctness-model/writeup/formalization.tex | 39 +++++++++++++++++---- 1 file changed, 33 insertions(+), 6 deletions(-) diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex index fc22c7e..0aff8cd 100644 --- 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? + + -- 2.17.1