changes

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

diff --git a/correctness-model/writeup/formalization.tex b/correctness-model/writeup/formalization.tex
new file mode 100644 (file)
index 0000000..aecb783
--- /dev/null
+++ b/correctness-model/writeup/formalization.tex
@@ -0,0 +1,92 @@
+\mysection{Formalization of Correctness Model}\label{sec:formalization}
+
+Unlike the SC memory model, applying linearizability can be complicated under
+C/C++ by the fact that the C/C++ memory model allows atomic loads to read from
+atomic stores that appear later in the trace and that it is in general
+impossible to produce a sequential history that preserves program order for the
+C/C++ memory model. Intuitively however, we can weaken some constraints, e.g.
+the \textit{happens-before} edges in some cases, to generate a reordering of
+ordering points such that they yield a sequential history that is consistent
+with the specification. We formalize our approach as follow.
+
+We represent a trace as an \textit{execution graph}, where each node represents
+each API method call with a set of ordering points, and edges 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:
+
+\squishcount
+
+\item {\bf Modification Order (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 (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$.
+\countend
+
+\vspace{0.3cm}
+
+Intuitively, if method $A$ 
+
+In order to relax the contraints on the original execution graph, we define an
+action \textit{tranform} that can be performed on the graph as follow:
+
+\mypara{{\bf Hoisting loads:}} $ \forall X, Y, X \in
+\textit{OrderingPoints}\xspace \wedge Y \in \textit{OrderingPoints}\xspace \wedge
+address(X)\not=address(Y) \wedge
+X \relation{hb} Y \wedge Y \in \textit{LoadOps}\xspace
+\Rightarrow \forall Z, Z
+$.
+
+
+\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}
+\Else
+\State results += \Call {WeakenOrderParams}{$c$} \label{line:weakenOrderParams}
+\EndIf
+\EndWhile
+\State inputParams := results \label{line:tmpOutputAsInput}
+\EndFor
+\State \Return{results} \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}
+\end{figure}
+
+
+
+\mypara{\bf Generating the Reordering:}
+The \TOOL checker first builds an execution graph where the nodes are
+method calls and the edges represent the
+$\reltext{opo}$ ordering of the ordering points of the methods that
+correspond to the source and destination nodes.  Assuming the absence
+of cycles in the execution graph, 
+the $\reltext{opo}$ ordering is used to generate the sequential history.
+The \TOOL checker 
+topologically sorts the graph to generate the equivalent sequential
+execution.