From: Peizhao Ou Date: Wed, 15 Apr 2015 00:38:16 +0000 (-0700) Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/spec-checker-compiler X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=ccad1a6eb845e0e2e7f1e8395c3d32cc569306fc;hp=7f557a3891c3ec8f7a8ffc5461299d50428be247 Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/spec-checker-compiler --- diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex index 2cc4564..fc22c7e 100644 --- a/correctness-model/writeup/formalization.tex +++ b/correctness-model/writeup/formalization.tex @@ -12,9 +12,9 @@ Consider the following example: { \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} } @@ -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} @@ -82,9 +82,9 @@ Consider the following example: { \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} } @@ -107,7 +107,7 @@ from different threads is not the general pattern for concurrent data 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: @@ -120,45 +120,72 @@ 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 -$. - -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} diff --git a/correctness-model/writeup/paper.tex b/correctness-model/writeup/paper.tex index d65f512..00e607d 100644 --- a/correctness-model/writeup/paper.tex +++ b/correctness-model/writeup/paper.tex @@ -81,6 +81,18 @@ \usepackage{algpseudocode} +\usepackage[utf8]{inputenc} +\usepackage[english]{babel} + +\newtheorem{theorem}{Theorem} +\newtheorem{corollary}{Corollary}[theorem] +\newtheorem{lemma}[theorem]{Lemma} + +\newcommand{\hb}[0]{\textit{hb}\xspace} +\newcommand{\mo}[0]{\textit{mo}\xspace} + +\newcommand{\pushcode}[1][1]{\hskip\dimexpr#1\algorithmicindent\relax} + %% Not used yet % \usepackage{times} % \usepackage{latexsym}