-\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{argue why ordered stores are reasonable to concurrent data structures}
-
-We next define an action called \textit{tranform} that can be performed on the graph as
-follow:
-
-$ \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 \in \textit{orderingPoints}\xspace \wedge
-Z \relation{hb} X,
-Z \relation{hb} Y \wedge \neg X \relation{hb} Y
-$.
-
-Under these analysis and assumptions, we clearly define our correctness model as
-follow:
+\path{r1 == 2 && r2 == 1 && r3 == 1 && r4 == 2}. Operation \code{y = 1} has an
+\moc edge to operation \code{y = 2}, and operation \code{x = 2} also has
+an edge to operation \code{x = 1}. As a result, there exists a cycle in the
+union of the \moc and \hb relation.
+
+To solve this, one option is to allow load operations to move up any operation
+including load and store operations on the same location. However, this can be
+extremely conuter-intuitive for a later load operation in \hb relation to read
+an older value than its previous load operation. Actually, the problem here is
+that the store operations with different values to the same memory location are
+not ordered by \hb relation. This is 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 a case of blind store operations is
+not the general pattern for concurrent data structures implementation. Instead,
+we believe that store operations to the same memory location should be ordered
+by \hb relation.
+
+We first define two categories of memory operations as follow:
+\begin{eqnarray*}
+s \in \StoreOp &=& \{store\} \times \Address \times \Value \cup \\
+&&\{rmw\} \times \Address \times \Value \\
+l \in \LoadOp &=& \{load\} \times \Address.
+\end{eqnarray*}
+
+We next define a \textit{relaxing operation} --- $r(x, y)$ on relation $R$ ($(x,
+y) \in R$), and it generates a new relation, denoted as relation $R_{r(x, y)}$
+(or $R_r$ for short) which is defined as follow:
+
+$ R_{r(x, y)} = \{ (a, b) \mid [ (a, b) \in R \wedge \neg [ (a, b) == (x, y)
+\wedge \movable(x, y) ]] \vee [ b == y \wedge (a, x) \in R \wedge \movable(x, y) ]$,
+where $ \movable(x, y) = \{ \Address(x) \not= \Address(y) \wedge y \in \LoadOp \}$.
+
+We also define a \textit{transform operation} --- $T$ on relation $R$, as a
+finite number of relaxing operations, $r1, r2,..., rn$ that are cumulatively
+operated on $R$, as follow:
+
+$R_T = R_{r1r2...rn} = (((R_{r1})_{r2})...)_{rn}$ .
+
+Furthermore, we define a special \textit{transform operation} $UT$ on relation
+$R$, where any further \textit{relaxing operation} $r$ on $R_{UT}$
+
+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 \hb relation, there exists a sequential history that is consistent with the
+\moc relation and the \hb relation in terms of store to store, load to store 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 such a history satisfies the
+condition. The algorithm first topologically sort operations by \hb, and then it
+only moves up certain load operations (Line~\ref{line:moveUpLoads}); thus, the
+\hb relation in terms of store to store and load to store holds. 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
+\moc relation in terms of write-write and write-read operations 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 \moc relation in terms of read-read and read-write operations also holds. As
+a result, the \moc relation 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}