--- /dev/null
+\mysection{Introduction}\label{sec:introduction}
+
+Concurrent data structure design can improve scalability by supporting
+multiple simultaneous operations, reducing memory coherence traffic, and reducing the time taken by an
+individual data structure operation. Researchers have developed many concurrent
+data structure designs with these goals~\cite{rcu,
+lockfreequeue}. Concurrent data structures often use sophisticated techniques
+including low-level atomic instructions (e.g., compare and
+swap), careful reasoning about the order of loads and
+stores, and fine-grained locking. For example, while the standard Java hash
+table implementation can limit scalability to a handful of cores,
+more sophisticated concurrent hash tables can scale to many hundreds of
+cores~\cite{javaConcurrentHashMap}.
+
+The C/C++ standard committee extended the C and C++ languages with
+support for low-level atomic operations in the C/C++11
+standard~\cite{cpp11spec, c11spec, boehmpldi} to enable developers to
+write portable implementations of concurrent data structures. To support the relaxations typically performed by compilers and processors,
+the
+C/C++ memory model provides weaker semantics than sequential
+consistency~\cite{scmemorymodel} and as a result, correctly using
+these operations is challenging. Developers must not only
+reason about potential interleavings, but also about how the processor
+and compiler might reorder memory operations. Even experts make
+subtle errors when reasoning about such memory models.
+
+Researchers have developed tools for exploring the behavior of code
+under the C/C++ model including \cdschecker~\cite{cdschecker}, {\sc
+Cppmem}~\cite{c11popl}, and Relacy~\cite{relacy}. These tools explore
+behaviors that are allowed under the C/C++ memory model. While these
+tools can certainly be useful for exploring executions, they can be
+challenging to use for testing as they don't provide support (other
+than assertions) for specifying the behavior of data structures.
+Using assertions can be challenging as different interleavings or
+reorderings legitimately produce different behaviors, and it can be
+very difficult to code assertions to check the output of a test case under for an
+arbitrary (unknown) execution.
+
+This paper presents \TOOL, a specification language and specification
+checking tool that is designed to be used in conjunction with model
+checking tools. We have implemented it as a plugin for
+the \cdschecker model checker.
+
+\mysubsection{Background on Linearizability}
+
+Researchers have developed several techniques for specifying
+correctness properties of concurrent data structures written for strong memory
+models. While these techniques cannot handle the behaviors typically
+exhibited by relaxed data structure implementations, they provide insight into
+intuitive approaches to specifying concurrent data structure behavior.
+
+One approach for specifying the correctness of concurrent data
+structures is in terms of equivalent sequential executions of either
+the concurrent data structure or a simplified sequential version. The
+problem then becomes how do we map a concurrent execution to an equivalent
+sequential execution? A common criterion is {\it
+ linearizability} --- linearizability simply states that a concurrent
+operation can be viewed as taking effect at some time between its
+invocation and its return (or response)~\cite{linearizableref}.
+
+An {\it equivalent sequential data structure} is a sequential version
+of a concurrent data structure that can be used to express correctness
+properties by relating executions of the original concurrent data
+structure with executions of the equivalent sequential data structure.
+The equivalent sequential data structure is often simpler, and in
+many cases one can simply use existing well-tested implementations from the
+STL library.
+
+An execution {\it history} is a total order of method invocations and
+responses. A {\it sequential history} is one where all invocations are
+followed by the corresponding responses immediately. A concurrent
+execution is correct if its behavior is consistent with its equivalent
+sequential history replayed on the equivalent sequential data
+structure. A concurrent object is linearizable if for all executions:
+\begin{enumerate}
+\item Each method call appears to take effect instantaneously at some
+ point between its invocation and response.
+
+\item The invocations and responses can be reordered to yield a
+ sequential history under the rule that an invocation cannot be
+ reordered before the preceding responses.
+
+\item The concurrent execution yields the same behavior as
+ the sequential history.
+\end{enumerate}
+
+A weaker variation of linearization is {\it sequential
+consistency}\footnote{It is important to note that the term sequential
+consistency in the literature is applied to both the consistency model
+that data structures expose clients to as well as the guarantees that
+the underlying memory system provides for load and store operations.}.
+Sequential consistency only requires that there exist a sequential
+history that is consistent with the {\it program order} (the intra-thread
+order). This ordering does not need to be consistent with the order
+that the operations were actually issued in.
+
+Line-Up~\cite{lineup}, Paraglider~\cite{VechevMCLinear}, and
+VYRD~\cite{vyrd} leverage linearizability to test concurrent data
+structures. {\bf Unfortunately, efficient implementations of many
+common data structures, e.g., RCU~\cite{rcu}, MS
+Queue~\cite{lockfreequeue}, ..., for the C/C++ memory model are
+neither linearizable nor sequentially consistent! Thus previous tools
+cannot check such data structures under the C/C++ memory model.}
+
+\mysubsection{New Challenges from the C/C++ Memory Model}
+\label{sec:introNewChallenges}
+
+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:
+
+\squishcount
+\item {\bf Relaxed Executions Break Existing Data Structure Consistency Models:}
+C/C++ data structures often expose clients to weaker (non-SC)
+behaviors to gain performance. A common guarantee is to provide
+happens-before synchronization between operations that implement
+updates and the operations that read those updates. These data
+structures often do not guarantee that different threads observe updates in the
+same order --- in other words the data structures may expose clients
+to weaker consistency models than sequential consistency. For
+example, even when one uses the relatively strong \code{acquire}
+and \code{release} memory orderings in C++, it is possible for two
+different threads to observe two stores happening in
+different orders, i.e., executions can fail the IRIW test.
+Thus many data structure legitimately admit executions for which there
+are no sequential histories that preserve program order.
+
+Like many other relaxed memory models, the C/C++ memory model does
+not include a total order over all memory operations, thus even
+further complicating the application of traditional approaches to correctness,
+e.g., linearization cannot be applied. In
+particular the approaches that relate the behaviors of concurrent data
+structures to analogous sequential data structures break down due to
+the absence of a total ordering of the memory operations. While many
+of the dynamic tools~\cite{cdschecker,relacy} for exploring the
+behavior of code under relaxed models do as a practical matter
+print out an execution in some order, this order is to some degree arbitrary as relaxed memory models
+generally make it possible for a data structure operation to see the
+effects of operations that appear later in any such an order (e.g., a load
+can read from a store that appears later in the order). Instead of a total order, the C/C++
+memory model is formulated as a graph of memory operations
+with several partial orders defined in this graph.
+
+\item {\bf Constraining Reorderings (Specifying Synchronization Properties):}
+Synchronization\footnote{Synchronization here is not mutual exclusion,
+ but rather a lower-level property that captures which stores must be
+ visible to a thread. In other words, it constrains which
+ reorderings can be performed by a processor or compiler.} in C/C++
+ provides an ordering between memory operations to different
+ locations. Concurrent data structures must establish
+ synchronization or they potentially expose their users to highly
+ non-intuitive behavior that is likely to break client code. For
+ example, consider the case of a concurrent queue that does not
+ establish synchronization between enqueue and dequeue operations. Consider the
+ following sequence of operations: (1) thread A initializes the fields of a new
+ object X; (2) thread A enqueues the reference to X in such a queue
+ (3) thread B dequeues the reference to X; (4) thread B reads the
+ fields of X through the dequeued reference. In (4), thread B could fail to see the
+ initializing writes from (1).
+ This surprising behavior could occur if the compiler or CPU could
+ reorder the initializing writes to be executed after the enqueue
+ operation. If the fields are non-atomic, such loads are considered
+ data races and violate the data race free requirement of the C/C++
+ language standard and thus the program has no semantics.
+
+The C/C++ memory model formalizes synchronization in terms of a {\it
+ happens-before} relation. The C/C++ happens-before relationship
+is a partial order over memory accesses. If memory access {\it x}
+happens before memory access {\it y}, it means that the effects of
+{\it x} must be ordered before the effects of {\it y}.
+\countend
+
+\begin{figure}
+ \centering
+\vspace{-.3cm}
+ \includegraphics[scale=0.35]{figures/specworkflow}
+\vspace{-.4cm}
+ \caption{\label{fig:specworkflow} \TOOL system overview}
+\vspace{-.4cm}
+\end{figure}
+
+\mysubsection{Specification Language and Tool Support}
+
+Figure~\ref{fig:specworkflow} presents an overview of the \TOOL system. After
+implementing a concurrent data structure, developers annotate their code
+with a \TOOL specification. To test their implementation,
+developers compile the data structure with the \TOOL specification
+compiler to extract the specification and generate a program that is instrumented with specification checks.
+ Then, developers compile the instrumented program with a
+standard C/C++ compiler. Finally, developers run the binary under
+the \TOOL checker. \TOOL
+then exhaustively explores the behaviors of the specific unit test and
+generates diagnostic reports for any executions that violate the specification.
+
+\mysubsection{Contributions}
+
+This paper makes the following contributions:
+
+\begin{itemize}
+\item {\bf Specification Language:} It introduces a specification
+ language that enables developers to write specifications of
+ concurrent data structures developed for a relaxed memory model in a
+ simple fashion that captures the key correctness properties. Our
+ specification language is the first to our knowledge that supports concurrent data
+ structures that use C/C++ atomic operations.
+
+\item {\bf A Technique to Relate Concurrent Executions to Sequential Executions:} It presents an approach to order the memory operations for the
+ C/C++ model, which lacks a definition of a trace and for which one
+ generally cannot even construct a total order of atomic operations
+ that is consistent with the program order. The generated
+ sequential execution by necessity does not always maintain program order.
+
+\item {\bf Synchronization Properties:} It presents constructs
+ for specifying the happens before relations that a data structure
+ should establish and tool support for checking these properties and
+ exposing synchronization related bugs.
+
+\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.
+
+\item {\bf Evaluation:} It shows that the \TOOL specification language can express key correctness properties for a
+set of real-world concurrent data structures, that our tool can detect
+ bugs, and that our tool can unit test real world data structures
+ with reasonable performance.
+\end{itemize}
+
projects / cdsspec-compiler.git / blobdiff