+++ /dev/null
-\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.
-
-
projects / cdsspec-compiler.git / blobdiff