add write up
[cdsspec-compiler.git] / writeup / introduction.tex
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++ memory 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 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 Specifying the Correctness of Concurrent Data Structures}
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 \squishcount
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 \countend
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 exists 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}, etc., 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 specifying the 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 structures 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 \squishlist
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 capture 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 (a) constructs
212   for specifying the happens before relations that a data structure
213   should establish, and (b) 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:}
217 \TOOL is the first tool to our knowledge that can check concurrent data
218 structures that exhibit relaxed behaviors against specifications that are
219 specified in terms of intuitive sequential executions.
220
221 \item {\bf Evaluation:} It shows that the \TOOL specification language can express key correctness properties for a
222 set of real-world concurrent data structures, that our tool can detect
223   bugs, and that our tool can unit test real world data structures
224   with reasonable performance.
225 \squishend
226