\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.
