changes

[cdsspec-compiler.git] / correctness-model / writeup / formalization.tex

diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex
index 2cc45642eea4f4b9829e7c95b6f07a849c5253f3..b973eb5a91e01d50cb94556ea4cb2e06ae786551 100644 (file)
--- a/correctness-model/writeup/formalization.tex
+++ b/correctness-model/writeup/formalization.tex
@@ -42,17 +42,17 @@ between nodes are derived from the \textit{happens-before} edges and the
 \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 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
 
 
 \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}
 \countend
 
 \vspace{0.3cm}


@@ -120,45 +120,55 @@ Y \in \textit{LoadOps}\xspace
 \forall Z,
 Z \in \textit{orderingPoints}\xspace \wedge 
 Z \relation{hb} X, 
 \forall Z,
 Z \in \textit{orderingPoints}\xspace \wedge 
 Z \relation{hb} X, 

-Z \relation{hb} Y \wedge \neg X \relation{hb} Y
-$.
+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 our algorithm to generate
+such a sequential history and prove that such an algorithm is feasible. We first
+topologically sort the operations by the \hb relation and have a sequential
+history $H$. By C/C++11, \hb is acyclic. Since every store / load operations
+have release / acquire semantics, every reads-from edge is also a \hb edge.
+Thus, a load operation can only read from an old store in $H$. We iterate the
+load operations on the same memory location from the end of $H$. For each load
+operation $X$ that reads from some store $Y$ on location $M$, if no store
+operation on $M$ exists between $X$ and $Y$ in $H$, any load operations on $M$
+before $X$ and after $Y$ cannot be \mo consistency ordered after $Y$ so $Y$ is
+ordered consistently; otherwise, if there exists
+
+
+\end{proof}

 
 

-Under these analysis and assumptions, we clearly define our correctness model as
-follow:

 
 \begin{figure}[!htbp]
 \begin{algorithmic}[1]
 
 \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 $r$ reads from
+\State $m$ := memory location of $r$
+\If{no store operations on $m$ between $w$ and $r$}
+\State continue

 \Else
 \Else

-\State results += \Call {WeakenOrderParams}{$c$} \label{line:weakenOrderParams}
+\State $w\prime$ := most recent store on $m$ before $r$
+\State $l\prime$ := set of load operations between $w\prime$ and $r$ \pushcode[2] that $w\prime$ is not \hb before

 \EndIf
 \EndIf

-\EndWhile
-\State inputParams := results \label{line:tmpOutputAsInput}

 \EndFor
 \EndFor

-\State \Return{results} \label{line:finalResults}
+\State \Return{$H$} \label{line:finalResults}

 \EndFunction
 \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}
 \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}
 \end{figure}
 
 \todo{prove that our correctness model is composable}