-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:
+However, while maintaining the \moc relation, we can weaken some
+constraints, e.g. eliminating some \textit{happens-before} edges, to generate a
+history that is consistent with the union of \hb and \moc relation. For
+instance, in the above example, we do not necessarily have to maintain the
+intra-thread order in both threads because they are independent operations and
+the later operation is a load.
+
+To be specific, in order to make the sequential history intuitive, we want to
+keep the happens-before edges from store to store, from load to store 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 that is consistent with the dependency between
+operations on the same location. However, a correctness model with these
+intuitions still does not work in C/C++ in general. Consider the following
+example: