correctness-model/writeup/.#introduction.tex.1.26

   1 \mysection{Introduction}\label{sec:introduction}
   2
   3 Concurrent data structure design can improve scalability by supporting
   4 multiple simultaneous operations, reducing memory coherence traffic, and reducing the time taken by an
   5 individual data structure operation.  Researchers have developed many concurrent
   6 data structure designs with these goals~\cite{rcu,
   7 lockfreequeue}.  Concurrent data structures often use sophisticated techniques
   8 including low-level atomic instructions (e.g., compare and
   9 swap), careful reasoning about the order of loads and
  10 stores, and fine-grained locking.    For example, while the standard Java hash
  11 table implementation can limit scalability to a handful of cores,
  12 more sophisticated concurrent hash tables can scale to many hundreds of
  13 cores~\cite{javaConcurrentHashMap}.
  14
  15 The C/C++ standard committee extended the C and C++ languages with
  16 support for low-level atomic operations in the C/C++11
  17 standard~\cite{cpp11spec, c11spec, boehmpldi} to enable developers to
  18 write portable implementations of concurrent data structures.  To support the relaxations typically performed by compilers and processors,
  19 the
  20 C/C++ memory model provides weaker semantics than sequential
  21 consistency~\cite{scmemorymodel} and as a result, correctly using
  22 these operations is challenging.  Developers must not only
  23 reason about potential interleavings, but also about how the processor
  24 and compiler might reorder memory operations.  Even experts make
  25 subtle errors when reasoning about such memory models.
  26
  27 Researchers have developed tools for exploring the behavior of code
  28 under the C/C++ model including \cdschecker~\cite{cdschecker}, {\sc
  29 Cppmem}~\cite{c11popl}, and Relacy~\cite{relacy}.  These tools explore
  30 behaviors that are allowed under the C/C++ memory model.  While these
  31 tools can certainly be useful for exploring executions, they can be
  32 challenging to use for testing as they don't provide support (other
  33 than assertions) for specifying the behavior of data structures.
  34 Using assertions can be challenging as different interleavings or
  35 reorderings legitimately produce different behaviors, and it can be
  36 very difficult to code assertions to check the output of a test case under for an
  37 arbitrary (unknown) execution.
  38
  39 This paper presents \TOOL, a specification language and specification
  40 checking tool that is designed to be used in conjunction with model
  41 checking tools.  We have implemented it as a plugin for
  42 the \cdschecker model checker.
  43
  44 \mysubsection{Background on Linearizability}
  45
  46 Researchers have developed several techniques for specifying
  47 correctness properties of concurrent data structures written for strong memory
  48 models.  While these techniques cannot handle the behaviors typically
  49 exhibited by relaxed data structure implementations, they provide insight into
  50 intuitive approaches to specifying concurrent data structure behavior.
  51
  52 One approach for specifying the correctness of concurrent data
  53 structures is in terms of equivalent sequential executions of either
  54 the concurrent data structure or a simplified sequential version.  The
  55 problem then becomes how do we map a concurrent execution to an equivalent
  56 sequential execution?  A common criterion is {\it
  57   linearizability} --- linearizability simply states that a concurrent
  58 operation can be viewed as taking effect at some time between its
  59 invocation and its return (or response)~\cite{linearizableref}.
  60
  61 An {\it equivalent sequential data structure} is a sequential version
  62 of a concurrent data structure that can be used to express correctness
  63 properties by relating executions of the original concurrent data
  64 structure with executions of the equivalent sequential data structure.
  65 The equivalent sequential data structure is often simpler, and in
  66 many cases one can simply use existing well-tested implementations from the
  67 STL library.
  68
  69 An execution {\it history} is a total order of method invocations and
  70 responses. A {\it sequential history} is one where all invocations are
  71 followed by the corresponding responses immediately. A concurrent
  72 execution is correct if its behavior is consistent with its equivalent
  73 sequential history replayed on the equivalent sequential data
  74 structure. A concurrent object is linearizable if for all executions:
  75 \begin{enumerate}
  76 \item Each method call appears to take effect instantaneously at some
  77   point between its invocation and response.
  78
  79 \item The invocations and responses can be reordered to yield a
  80   sequential history under the rule that an invocation cannot be
  81   reordered before the preceding responses.
  82
  83 \item The concurrent execution yields the same behavior as
  84   the sequential history.
  85 \end{enumerate}
  86
  87 A weaker variation of linearization is {\it sequential
  88 consistency}\footnote{It is important to note that the term sequential
  89 consistency in the literature is applied to both the consistency model
  90 that data structures expose clients to as well as the guarantees that
  91 the underlying memory system provides for load and store operations.}.
  92 Sequential consistency only requires that there exist a sequential
  93 history that is consistent with the {\it program order} (the intra-thread
  94 order).  This ordering does not need to be consistent with the order
  95 that the operations were actually issued in.
  96
  97 Line-Up~\cite{lineup}, Paraglider~\cite{VechevMCLinear}, and
  98 VYRD~\cite{vyrd} leverage linearizability to test concurrent data
  99 structures.  {\bf Unfortunately, efficient implementations of many
 100 common data structures, e.g., RCU~\cite{rcu}, MS
 101 Queue~\cite{lockfreequeue}, ..., for the C/C++ memory model are
 102 neither linearizable nor sequentially consistent! Thus previous tools
 103 cannot check such data structures under the C/C++ memory model.}
 104
 105 \mysubsection{New Challenges from the C/C++ Memory Model}
 106 \label{sec:introNewChallenges}
 107
 108 The C/C++ memory model brings the following two key challenges that prevent the application of previous approaches to checking concurrent data structures to this setting:
 109
 110 \squishcount
 111 \item {\bf Relaxed Executions Break Existing Data Structure Consistency Models:}
 112 C/C++ data structures often expose clients to weaker (non-SC)
 113 behaviors to gain performance.  A common guarantee is to provide
 114 happens-before synchronization between operations that implement
 115 updates and the operations that read those updates.  These data
 116 structures often do not guarantee that different threads observe updates in the
 117 same order --- in other words the data structures may expose clients
 118 to weaker consistency models than sequential consistency.  For
 119 example, even when one uses the relatively strong \code{acquire}
 120 and \code{release} memory orderings in C++, it is possible for two
 121 different threads to observe two stores happening in
 122 different orders, i.e., executions can fail the IRIW test.
 123 Thus many data structure legitimately admit executions for which there
 124 are no sequential histories that preserve program order.
 125
 126 Like many other relaxed memory models, the C/C++ memory model does
 127 not include a total order over all memory operations, thus even
 128 further complicating the application of traditional approaches to correctness,
 129 e.g., linearization cannot be applied.  In
 130 particular the approaches that relate the behaviors of concurrent data
 131 structures to analogous sequential data structures break down due to
 132 the absence of a total ordering of the memory operations.  While many
 133 of the dynamic tools~\cite{cdschecker,relacy} for exploring the
 134 behavior of code under relaxed models do as a practical matter
 135 print out an execution in some order, this order is to some degree arbitrary as relaxed memory models
 136 generally make it possible for a data structure operation to see the
 137 effects of operations that appear later in any such an order (e.g., a load
 138 can read from a store that appears later in the order).  Instead of a total order, the C/C++
 139 memory model is formulated as a graph of memory operations
 140 with several partial orders defined in this graph.
 141
 142 \item {\bf Constraining Reorderings (Specifying Synchronization Properties):}
 143 Synchronization\footnote{Synchronization here is not mutual exclusion,
 144   but rather a lower-level property that captures which stores must be
 145   visible to a thread.  In other words, it constrains which
 146   reorderings can be performed by a processor or compiler.} in C/C++
 147   provides an ordering between memory operations to different
 148   locations.  Concurrent data structures must establish
 149   synchronization or they potentially expose their users to highly
 150   non-intuitive behavior that is likely to break client code.  For
 151   example, consider the case of a concurrent queue that does not
 152   establish synchronization between enqueue and dequeue operations. Consider the
 153   following sequence of operations: (1) thread A initializes the fields of a new
 154   object X; (2) thread A enqueues the reference to X in such a queue
 155   (3) thread B dequeues the reference to X; (4) thread B reads the
 156   fields of X through the dequeued reference. In (4), thread B could fail to see the
 157   initializing writes from (1).
 158   This surprising behavior could occur if the compiler or CPU could
 159   reorder the initializing writes to be executed after the enqueue
 160   operation.  If the fields are non-atomic, such loads are considered
 161   data races and violate the data race free requirement of the C/C++
 162   language standard and thus the program has no semantics.
 163
 164 The C/C++ memory model formalizes synchronization in terms of a {\it
 165   happens-before} relation.  The C/C++ happens-before relationship
 166 is a partial order over memory accesses.  If memory access {\it x}
 167 happens before memory access {\it y}, it means that the effects of
 168 {\it x} must be ordered before  the effects of {\it y}.
 169 \countend
 170
 171 \begin{figure}
 172         \centering
 173 \vspace{-.3cm}
 174         \includegraphics[scale=0.35]{figures/specworkflow}
 175 \vspace{-.4cm}
 176                 \caption{\label{fig:specworkflow} \TOOL system overview}
 177 \vspace{-.4cm}
 178 \end{figure}
 179
 180 \mysubsection{Specification Language and Tool Support}
 181
 182 Figure~\ref{fig:specworkflow} presents an overview of the \TOOL system. After
 183 implementing a concurrent data structure, developers annotate their code
 184 with a \TOOL specification. To test their implementation,
 185 developers compile the data structure with the \TOOL specification
 186 compiler to extract the specification and generate a program that is instrumented with specification checks.
 187  Then, developers compile the instrumented program with a
 188 standard C/C++ compiler. Finally, developers run the binary under
 189 the \TOOL checker. \TOOL
 190 then exhaustively explores the behaviors of the specific unit test and
 191 generates diagnostic reports for any executions that violate the specification.
 192
 193 \mysubsection{Contributions}
 194
 195 This paper makes the following contributions:
 196
 197 \begin{itemize}
 198 \item {\bf Specification Language:} It introduces a specification
 199   language that enables developers to write specifications of
 200   concurrent data structures developed for a relaxed memory model in a
 201   simple fashion that captures the key correctness properties.  Our
 202   specification language is the first to our knowledge that supports concurrent data
 203   structures that use C/C++ atomic operations.
 204
 205 \item {\bf A Technique to Relate Concurrent Executions to Sequential Executions:}  It presents an approach to order the memory operations for the
 206   C/C++ model, which lacks a definition of a trace and for which one
 207   generally cannot even construct a total order of atomic operations
 208   that is consistent with the program order.  The generated
 209   sequential execution by necessity does not always maintain program order.
 210
 211 \item {\bf Synchronization Properties:} It presents constructs
 212   for specifying the happens before relations that a data structure
 213   should establish and tool support for checking these properties and
 214   exposing synchronization related bugs.
 215
 216 \item {\bf Tool for Checking C/C++ Data Structures Against Specifications:} \TOOL is the first tool to our knowledge that can check concurrent data structures that exhibit relaxed behaviors against specifications that are specified in terms intuitive sequential executions.
 217
 218 \item {\bf Evaluation:} It shows that the \TOOL specification language can express key correctness properties for a
 219 set of real-world concurrent data structures, that our tool can detect
 220   bugs, and that our tool can unit test real world data structures
 221   with reasonable performance.
 222 \end{itemize}
 223