\mysection{Formalization of Correctness Model}\label{sec:formalization}
Unlike the SC memory model, finding an appropriate correctness model for
concurrent data structures under the C/C++11 memory model is challenging. For
example, linearizability no longer fits 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.
Consider the following example:
{
\footnotesize
\begin{verbatim}
Thrd 1: Thrd 2:
x = 1; y = 1;
r1 = y; r2 = x;
\end{verbatim}
}
Suppose each operation in this example is the only operation of each method
call, and shared variables \code{x} and \code{y} are both initilly \code{0}.
Each store operation has \code{release} semantics and each load operation has
\code{acquire} semantics. For the execution where both \code{r1} and \code{r2}
obtain the old value \code{0}, we encounter a challenge of generating a
sequential history. Since neither load operation reads
from the corresponding store, they should be ordered before their corresponding
store operation. On the other hand, both stores happen before the other load
(intra-thread ordering), making it impossible to topologically sort the
operations to generate a consistent sequential history.
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.
First of all, 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$ has an information flow to method $B$, we want method
$B$ to see the effects before method $A$. In C/C++11, on the other hand, we want
method $A$ to have \code{release} semantics while method $B$ to have
\code{acquire} semantics so that they establish the happens-before relationship.
For example, for a concurrent queue, we want a dequeuer synchronizes with the
corresponding enqueuer so that when the dequeuer obtains a reference to an
object, it can read the fully initialized value of that object. To some degree
this can also avoid data races. When it comes to C/C++11 data structures, the
ordering points of method calls should have release/acquire semantics on stores
and loads.
In order to relax the contraints on the original execution graph, we will have
to disregard some happens-before edges. To make our model intuitive, we want to
keep the happens-before edges from stores to stores and from load operations to
store operations because that can ensure information is only flowing from
earlier store operations. Besides, we also want to keep the happens-before edges
between operations on the same memory location since otherwise the generated
history will become very counter-intuitive. However, such a model does not work
in C/C++ in general. Consider the following example:
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;
\end{verbatim}
}
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.