changes
authorPeizhao Ou <peizhaoo@uci.edu>
Tue, 14 Apr 2015 01:07:07 +0000 (18:07 -0700)
committerPeizhao Ou <peizhaoo@uci.edu>
Tue, 14 Apr 2015 01:07:07 +0000 (18:07 -0700)
correctness-model/writeup/formalization.tex

index 2cc4564..b973eb5 100644 (file)
@@ -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 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}
@@ -120,45 +120,55 @@ Y \in \textit{LoadOps}\xspace
 \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]
-\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
-\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
-\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}