\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 an trace as a \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. Given two operations $X$ and $Y$ that are
both ordering points, the \textit{modification order} edges are as follows:

\squishcount
\item {\bf Reads-From:} $X \xrightarrow{rf} Y \Rightarrow X \xrightarrow{opo} Y$.

\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



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