+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:
projects / cdsspec-compiler.git / commitdiff