\mysection{Motivating Example}
\label{sec:example}

We will use the read-copy update (RCU)~\cite{rcu} implementation in
Figure~\ref{fig:rcuexample} as a running example.  RCU data structures
are useful for usage scenarios with large numbers of reads and
relatively few updates.  RCU based data structures scale to large
numbers of readers because read operations do not contain any
low-level store operations and thus do not generate coherence traffic to invalidate cache lines.
Lines~\ref{line:rcuBegin} through~\ref{line:rcuEnd} contain
the code for the RCU implementation, and
Lines~\ref{line:testcaseBegin} through~\ref{line:testcaseEnd} show a
test case for the implementation.

The RCU implementation maintains a shared pointer
(Line~\ref{line:rcuSharedData})
\code{node} to reference the data shared by readers and
updaters. A reader loads the shared pointer (Line~\ref{line:rcuReadLoad}) to read
the shared data, while an updater allocates a new struct
(Line~\ref{line:rcuUpdateAlloc}), loads the shared pointer
(Line~\ref{line:rcuUpdateLoad}), and then attempts a compare and swap (CAS) operation to update the shared pointer.  This process repeats until the CAS is successful.

\begin{figure}[h]
\vspace{-.2cm}
\begin{lstlisting}[xleftmargin=6.0ex]
#define mo_acquire memory_order_acquire
#define mo_acq_rel memory_order_acq_rel
struct Node {/*@ \label{line:rcuBegin} @*/
	int data ;
	int version;
};

class RCU {
	atomic<Node*> node;/*@ \label{line:rcuSharedData} @*/
	public:
	RCU() {
		Node *n = new Node;
		n->data= 0;
		n->version = 0;
		atomic_init(&node, n);	
	}
	void read(int *data, int *version) {
		Node *res = node.load(mo_acquire);/*@ \label{line:rcuReadLoad} @*/
		*data = res->data;
		*version = res->version;
	}
	void update(int data) {
		bool succ = false;
		Node *newNode = new Node;/*@ \label{line:rcuUpdateAlloc} @*/
		Node *prev = node.load(mo_acquire);/*@ \label{line:rcuUpdateLoad} @*/
		do {
			newNode->data = data;
			newNode->version = prev->version + 1;
			succ = node.compare_exchange_strong(prev,/*@ \label{line:rcuUpdateCAS} @*/
				newNode, mo_acq_rel, mo_acquire);/*@ \label{line:rcuUpdateCASMO} @*/
		} while (!succ);
	}
};/*@ \label{line:rcuEnd} @*/

RCU x, y; // Define two RCU objects/*@ \label{line:testcaseBegin} @*/
int r1, r2, v1, v2;
void thrd_1() { // Thread 1/*@ \label{line:thrd1} @*/
	x.update(1);
	y.read(&r1, &v1); // r1 == 0
}
void thrd_2() { // Thread 2/*@ \label{line:thrd2} @*/
	y.update(1);
	x.read(&r2, &v2); // r2 == 0
}/*@ \label{line:testcaseEnd} @*/
\end{lstlisting}
\vspace{-.2cm}
\caption{\label{fig:rcuexample}C++11 read-copy update example}
\vspace{-.3cm}
\end{figure}

\begin{figure}[t]
        \centering
\vspace{-.3cm}
	\resizebox{\columnwidth}{!}{
		\includegraphics[scale=0.33]{figures/rcuhistory}
	}
  \vspace{-.4cm}
		\caption{\label{fig:rcuhistory}History of a possible execution of two RCU objects}
\vspace{-.4cm}
\end{figure}

This implementation uses low-level atomic operations provided by
C/C++ to implement the RCU mechanism. For example, in
Line~\ref{line:rcuUpdateCAS}, the \code{update} method uses a CAS
operation to update the \code{node}. The memory
order parameters attached to the atomic operations ensure that memory
accesses that were performed before the \code{update} operation must
occur before memory accesses that were performed after the \code{read}
operation.

\mysubsection{Consistency Model}
\label{sec:exampleMotivation}

In the example code, two threads, Thread~1 and Thread~2, each update
one of the RCU objects \code{x} and \code{y}, respectively, and then
access the object updated by the other thread.  Under the C/C++
memory model, this example admits an execution in which both Thread~1
and Thread~2 read the initial value 0.

Figure~\ref{fig:rcuhistory} shows a possible order for this
execution in which the model checker processes statements in the order shown in
the
execution labeled Original Trace\footnote{Note that the C/C++ memory
model does not include any notion of a trace.  We merely use the term
trace to refer to the order in which \TOOL prints the execution.},
which is an interleaving of the invocation and response events of
API methods indicated by \lq\lq\_i\rq\rq and \lq\lq\_r\rq\rq,
respectively.

This trace is rather counter-intuitive because it orders 
Thread~1's \code{update} event before Thread~2's \code{read} event,
yet Thread~2's \code{read} event does not observe the updated value.
However, under the C/C++11 memory model, this is allowed since a load
is allowed to read a value that is written by an old store.

It is important to note that it is impossible to produce a sequential history
for this example that preserves program order and produces the observed
behavior.  This means that traditional notions of correctness that relate
concurrent executions to sequential executions that were developed for
the SC memory model cannot directly be applied to the C/C++11 memory
model.

This example leads to the following conclusion --- if we want to
define the behavior of concurrent executions by relating them to
equivalent sequential histories, then we must give up on preserving
program order.

We note that for this example, if we give up on program order, we
produce the sequential history in Figure~\ref{fig:rcuhistory}
labeled Reordered Trace.  The data structure operations in this
sequential history have behavior that is consistent with the observed
behaviors in the example execution.

\mysubsection{Synchronization Properties}

A correct RCU data structure ensures the property that the invocation
event of an \code{update} operation happens-before the response event
of the subsequent
\code{read} operation. Informally, all operations that appear before the \code{update} operation must appear to occur before the operations that appear after the \code{read} operation.  While these
semantics follow naturally for SC, for relaxed memory models we must
ensure that neither the compiler nor the processor performs
reorderings that violate these semantics. Therefore, when a reader
reads the fields of the
\code{node}, 
data races are eliminated since the \code{read} operation synchronizes with the \code{update} operation.


In the C/C++11 memory model, the transitive closure of
\textit{sequence-before} and \textit{synchronizes-with} relations form the
\textit{happens-before} relation in the absence of operations with the \code{consume} memory order.  Since every time an \code{update} operation finishes, a CAS operation to
\code{node} with release semantics is executed, and the subsequent \code{read}
loads the \code{node} reference with acquire semantics, the \code{read} operation synchronizes
with the \code{update} operation, providing the necessary synchronization properties.
Some RCU implementations may use consume semantics instead of acquire semantics,
however we do not use consume for the following two reasons: (1) most existing
C/C++ compilers do not support consume semantics and thus acquire does not
involve extra overhead and (2) using consume semantics provides a more complex interface to 
clients that may require them to explicitly declare dependences throughout the code.


