{
\footnotesize
\begin{verbatim}
-Thrd 1: Thrd 2:
-x = 1; y = 1;
-r1 = y; r2 = x;
+ Thrd 1: Thrd 2:
+ x = 1; y = 1;
+ r1 = y; r2 = x;
\end{verbatim}
}
\textit{modification order} edges between ordering points. We define
\textit{opo} as the \textit{ordering point order} relation between ordering
point. Given two operations $X$ and $Y$ that are both ordering points, the
-\textit{modification order} edges are as follow:
+\textit{modification order consistency} edges are as follow:
\squishcount
-\item {\bf Modification Order (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
+\item {\bf Modification Order Consistency (write-write):} $X \xrightarrow{mo} Y \Rightarrow X \xrightarrow{opo} Y$.
-\item {\bf Modification Order (read-write):} $A \xrightarrow{mo} Y \ \wedge \ A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
+\item {\bf Modification Order Consistency (read-write):} $A \xrightarrow{mo} Y \ \wedge \ A \xrightarrow{rf} X \Rightarrow X \xrightarrow{opo} Y$.
-\item {\bf Modification Order (write-read):} $X \xrightarrow{mo} B \ \wedge \ B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
+\item {\bf Modification Order Consistency (write-read):} $X \xrightarrow{mo} B \ \wedge \ B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
-\item {\bf Modification Order (read-read):} $A \xrightarrow{mo} B \ \wedge \ A \xrightarrow{rf} X \ \wedge \ B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
+\item {\bf Modification Order Consistency (read-read):} $A \xrightarrow{mo} B \ \wedge \ A \xrightarrow{rf} X \ \wedge \ B \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.
\countend
\vspace{0.3cm}
{
\footnotesize
\begin{verbatim}
-Thrd 1: Thrd 2: Thrd 3: Thrd 4:
-x = 1; y = 2; r1 = x; r3 = y;
-y = 1; x = 2; r2 = x; r4 = y;
+ Thrd 1: Thrd 2: Thrd 3: Thrd 4:
+ x = 1; y = 2; r1 = x; r3 = y;
+ y = 1; x = 2; r2 = x; r4 = y;
\end{verbatim}
}
structures, and we believe that store operations are ordered. In terms of
ordering points, we believe that in real-world data structures, store operations
of ordering points are ordered by happens-before relation.
-\todo{argue why ordered stores are reasonable to concurrent data structures}
+\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:
\forall Z,
Z \in \textit{orderingPoints}\xspace \wedge
Z \relation{hb} X,
-Z \relation{hb} Y \wedge \neg X \relation{hb} Y
-$.
-
-Under these analysis and assumptions, we clearly define our correctness model as
-follow:
+Z \relation{hb} Y \wedge \neg X \relation{hb} Y $.
+
+Under these analysis and assumptions, we present Lemma~\ref{seqHistoryExistence}.
+
+\begin{lemma} \label{seqHistoryExistence}
+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, there exists a sequential history
+that is consistent with the modification order consistency and the
+happens-before relation in terms of store to store operations, load to store
+operations and operations on the same memory location.
+\end{lemma}
+
+\begin{proof}
+To prove Lemma~\ref{seqHistoryExistence}, we present in
+Figure~\ref{fig:algorithmConsistentHistory} our constructive algorithm that
+generates a sequential history and prove that its output satisfies the
+condition. This algorithm topologically sort operations by \hb, and then it only
+moves up certain load operations (Line~\ref{line:moveUpLoads}); thus, the store
+to store and load to store \hb relation hold. Since load operations that read
+from the correct store is not moved (Line~\ref{line:loadSet}) and store
+operations are ordered by \hb relation, the write-write and write-read \mo
+consistency holds. By induction, moving up load operations will end up placing
+load operations between the store operation that they read from and the next
+store operation, and thus the read-read and read-write \mo consistency also
+holds. We then illustrates that the \hb relation between the same memory
+location also holds by contradiction. The only possibility of moving load
+operations across operations on the same location lies in
+Line~\ref{line:loadSet} where there exists an operation $o$ between
+$w'$
+and $r$, and $o$ is not moved up while some operation $r'$ in $l'$ is
+moved up, and $o$ happens before $r'$. If $o$ is a load operation, $o$ must
+read from $w$ otherwise $o$ will be moved up. Thus we have the relation: $w
+\relation{hb} w' \relation{hb} o \relation{hb} r'$, which contradicts
+the fact that $r$ reads from $w$. Likewise, if $o$ is a store operation, since
+store operations are ordered by \hb relation, we have the relation: $w
+\relation{hb} o \relation{hb} r'$ and this is a contradiciton similarly.
+Therefore, the generated sequential history by this algorithm satisfies the
+conditions in this Lemma.
+\end{proof}
\begin{figure}[!htbp]
\begin{algorithmic}[1]
-\Function{InferParams}{testcases, initialParams}
-\State inputParams := initialParams
-\If{inputParams is empty}
-\State inputParams := the weakest parameters \label{line:startWithRelaxed}
-\EndIf
-\ForAll{test case $t$ in testcases}
-\State candidates := inputParams \label{line:setOfCandidates}
-\State results := \{\}
-\While{candidates is not empty}
-\State Candidate $c$ := pop from candidates
-\State run \cdschecker with $c$ and check SC \label{line:findSCViolation}
-\If{$\exists$ SC violation $v$}
-\State \Call {StrengthenParam}{$v$, $c$, candidates} \label{line:callStrengthenParam}
+\Function{GenerateConsistentHistory}{trace}
+\State $H$ := topologically sort operations of trace by \hb
+\ForAll{load operation $r$ in $H$ in reverse order}
+\State $w$ := store operation that $r$ reads from
+\State $m$ := memory location of $r$
+\If{no store operations on $m$ between $w$ and $r$}
+\State continue
\Else
-\State results += \Call {WeakenOrderParams}{$c$} \label{line:weakenOrderParams}
+\State $w'$ := most recent store on $m$ before $r$
+\State \parbox[t]{\dimexpr\linewidth-\algorithmicindent}{$l'$ := set of \label{line:loadSet}
+load operations on $m$ between $w'$ and $r$\\
+that do not read from $w'$ (including $r$) \strut}
+\State move $l'$ (keep inner order) above $w$ and continue \label{line:moveUpLoads}
\EndIf
-\EndWhile
-\State inputParams := results \label{line:tmpOutputAsInput}
\EndFor
-\State \Return{results} \label{line:finalResults}
+\State \Return{$H$} \label{line:finalResults}
\EndFunction
-
-\Procedure{StrengthenParam}{v, c, candidates}
-\While{$\exists$ a fix $f$ for violation $v$}
-\State possible\_repairs := strengthen $c$ with fix $f$ \label{line:strengthenParam}
-\State candidates += possible\_repairs \label{line:possibleFixes}
-\EndWhile
-\EndProcedure
-
\end{algorithmic}
-\caption{\label{fig:algorithmfence}Algorithm for inferring order parameters}
+\caption{\label{fig:algorithmConsistentHistory}Algorithm for generating a consistent sequential history}
\end{figure}
-\todo{prove that our correctness model is composable}
+\begin{lemma} \label{equivalence}
+
+\end{lemma}
+
+\todo{formalize composability and show hat our correctness model is composable}
projects / cdsspec-compiler.git / commitdiff