\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. The goal is to come
up with a correctness model that is weaker than linearizability and SC and yet
is composable.

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 consistency} edges are as follow:

\squishcount

\item {\bf Modification Order Consistency (write-write):} $X \xrightarrow{mo} Y \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 Consistency (write-read):} $X \xrightarrow{mo} B \ \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}

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 encounter a challenge for the execution where the following holds:
\path{r1 == 2 && r2 == 1 && r3 == 1 && r4 == 2}. For any total order that is
consistent with the happens-before relation, that total order will be
inconsistent with the modification order in either variable \code{x} or
\code{y}. For example, if \code{y = 1} is ordered before \code{y = 2}, then
\code{x = 1} is ordered before \code{x = 2} while \code{r1 = x} is ordered
before \code{r2 = x}. As a result, we cannot possibly move up the second load
operation \code{r2 = x} across \code{r1 = x} to generate a consistent sequential
history. To solve this, one option is that allow loads to move up any operation
including load and store operation on the same location. However, it is
extremely conuter-intuitive for a later load operation to read an older value.
By analysis, the problem here is that the store operations with different values
to the same memory location are not ordered. This is actually a really rare case
because it could be possible that only one store operation takes effect and all
other store operations are useless. We believe that such case of blind stores
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{explain why ordered stores are reasonable to concurrent data structures}

We next define a \textit{relaxing action} that takes input a relation $R$
and outputs a new relation $R'$. We denote $R_r$ as the new relation after
taking a relaxing action $r$ on relation $R$. 

$ \forall X, Y, address(X)\not=address(Y) \wedge
X \relation{R} Y \wedge
Y \in \textit{LoadOps}\xspace
\Rightarrow
\forall Z,
Z \in \textit{orderingPoints}\xspace \wedge 
Z \relation{hb} X, 
Z \relation{hb} Y \wedge \neg X \relation{hb} Y $.

We denote \textit{hb}$_r$ as the happens-before relation after taking a relaxing action
$r$.

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{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 $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
\EndFor
\State \Return{$H$} \label{line:finalResults}
\EndFunction
\end{algorithmic}
\caption{\label{fig:algorithmConsistentHistory}Algorithm for generating a consistent sequential history}
\end{figure}

\begin{lemma} \label{equivalence}
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, the sequential history $H$ generated by the
algorithm in Figure~\ref{fig:algorithmConsistentHistory} is equivalent to some
topological sorting of the operations by \mo consistency and \hb relation after
finite steps of actions (\textit{transform}).
\end{lemma}

\begin{proof}
In the algorithm showed in Figure~\ref{fig:algorithmConsistentHistory}, during
each iteration it can have a set of load operations $l'$
(Line~\ref{line:loadSet}) to be moved up across the most recent store operation
$w'$. For any load opeartion $l''$ in the set $l'$, as showed in the proof of
Lemma~\ref{seqHistoryExistence}, no other operation on the same memory location
exists between $w'$ and $l''$. When $l''$ moves across an operation $o$ that
happens before $l''$, we make a transform $t$ on the happens-before relation on
$o$ and $l''$. When it finishes generating $H$, we have a finite steps of
transform taken on the happens-before graph, denoted as $T$. We also denote that
\textit{hb}$_T$ as the happens before relation after $T$. 
\end{proof}

\todo{formalize composability and show hat our correctness model is composable}
1. Should we still assume that store operations to the same memory location are
ordered?
2. Or is it safe to assume that variables from two release/acquire consistent
objects should be disjoint?


