\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++ memory 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 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 Specifying the Correctness of Concurrent Data Structures}

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:
\squishcount
\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.
\countend

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 exists 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}, etc., 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 specifying the 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 structures 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:

\squishlist
\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 capture 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 (a) constructs
  for specifying the happens before relations that a data structure
  should establish, and (b) 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 of 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.
\squishend

