From 6d9ef2b895306c8351d5f08a07dc7e630a3100f8 Mon Sep 17 00:00:00 2001 From: Peizhao Ou Date: Mon, 13 Apr 2015 18:07:07 -0700 Subject: [PATCH] changes --- correctness-model/writeup/formalization.tex | 80 ++++++++++++--------- 1 file changed, 45 insertions(+), 35 deletions(-) diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex index 2cc4564..b973eb5 100644 --- 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 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} -- 2.34.1