edits

[cdsspec-compiler.git] / correctness-model / writeup / evaluation.tex

\mysection{Evaluation}\label{sec:evaluation}

We have implemented \TOOL.  Our evaluation focuses on the following
questions: (1) How expressive is \TOOL for specifying
the correctness properties of real-world concurrent data structures? (2) How easy is it
to use \TOOL? (3) What
is the performance of \TOOL? (4) How effective was \TOOL
in finding bugs?

In order to evaluate \TOOL, we have gathered a contention
free lock, two types of concurrent queues, and a work stealing
deque~\cite{ppoppworkstealing}.  As C/C++11 is relatively new
there are no C/C++11 implementations for many concurrent data
structures, thus we ported several data structures.  The Linux
kernel's reader-writer spinlock and the Michael Scott queue were originally ported
for the \cdschecker benchmark suite.  We also ported an RCU
implementation and Cliff Click's hashtable from its Java
implementation~\cite{clickhashtable}.  We report execution times on an 
Intel Core i7 3770.

\mysubsection{Expressiveness}\label{sec:expressiveness}

In this section, we evaluate the expressiveness of \TOOL by reporting
our experiences writing specifications for a range of concurrent data
structures.

\mypara{\bf Lockfree hashtable:} We ported Cliff Click's hashtable,
which supports simultaneous lookups and updates by multiple threads as
well as concurrent table resizing.  The implementation uses an array
of atomic variables to store the key/value slots, and uses
acquire/release synchronization to establish the synchronization
between hashtable accesses.

Hashtable updates consist of two CAS operations --- one to claim
the key slot and one to update the value.  When a \code{put} method
invocation successfully updates both the key and value, the
update is visible to other threads.  Thus, both CAS operations are
ordering points for the \code{put} method, and we annotate both of
them as potential ordering points. The \code{get} method is ordered after
an invocation of the \code{put} only if it sees both the key and
value updates.  Thus we annotate an ordering point for the
key read only if the key is null.  We also
annotate an ordering point for the value read if
it reads the value slot. The test driver has two threads both of
which update and read the value for the same key.

\mypara{\bf RCU:} As discussed in the example, this is a
synchronization mechanism used in the Linux kernel that allows concurrent reads
and updates. We ran this benchmark with four threads, two update the data
structure and two read the data structure.

\mypara{\bf Chase-Lev Deque:} This is a bug-fixed version of a published C11 adaptation
of the Chase-Lev deque~\cite{ppoppworkstealing}.
It maintains a top and bottom index to a shared array of
references. In terms of synchronization,
when pushing an item into the sequential deque,
we attach a unique ID tag to that element. When stealing or taking an item, we
use that tag as the ID of the method call. Thus, we have (push, steal) or
(push, take) pairs that have the same method call ID.
In our test driver, one thread 
pushes 3 items and takes 2 items while the other one steals 1
item.

\mypara{\bf Linux Reader-Writer Lock:} A reader-writer lock allows either
multiple concurrent readers or one exclusive writer. We can abstract
it with a boolean \code{writer\_lock} representing
whether the writer lock is held and an integer \code{reader\_cnt}
representing the number of threads that are reading.
We test this benchmark with a single lock that
protects shared variables. We have two threads that read and write
the shared variables under the protection of a read lock and a write
lock.

\mypara{\bf MCS Lock:} This benchmark is an implementation of
the Mellor-Crummey and Scott lock~\cite{mcs-lock,
  mcs-lock-url}.  This lock queues waiting threads in a FIFO.
Our test driver utilizes two
threads that read and write shared variables with the protection of
the lock.

\mypara{\bf M\&S Queue:} This benchmark is an adaptation of the
Michael and Scott lock free queue~\cite{lockfreequeue} to the C/C++
memory model.  We ran with two threads, one of which enqueues and the
other of which dequeues an item.

\mypara{\bf SPSC Queue:} This is a lock-free single-producer,
single-consumer queue. 
We used a test driver that has two
threads --- one enqueues a value and the other  dequeues
it.

\mypara{\bf MPMC Queue:} This is a multiple-producer, multiple-consumer
queue. Producers call \code{write\_prepare} to obtain a free
slot, update the slot, and call \code{write\_publish} to
publish it. Consumers call \code{read\_fetch} to obtain
a valid slot, read the slot, and call \code{read\_consume}
to free it. The specification focuses on the synchronization
properties which require \code{write\_publish} to synchronize with
\code{read\_fetch} to ensure the data integrity and
\code{read\_consume} to synchronize with \code{write\_prepare} to
ensure that slots are not prematurely recycled.  The test driver
contains two threads, each of which enqueue and dequeue
an item.

\subsection{Ease of Use} In addition to expressiveness, it is also important for
specification languages to be easy to use. In our experience using \TOOL
to specify the real-world data
structures in our benchmark set, we found that \TOOL was easy to use. \TOOL specifications have only three 
parts --- equivalent sequential data structures, ordering points, and
synchronization properties, and we explain the reasons as follows. (1) Specifying
sequential data structures is easy and straightforward, and developers can often
just use an off-the-shelf implementation from a library.
(2) When developers specify ordering points, they
only need to know what operations order methods without needing to specify
the subtle reasoning about the corner cases involving
interleavings and reorderings introduced by relaxed memory models. Take the
Michael \& Scott queue as an example, we can easily order enqueuers with the
point when \code{enqueue} loads the \code{tail} pointer right before inserting the new
node.
(3) For synchronization, the fact that we allow specifying
synchronization at the abstraction of methods makes it easy. For example, we only used 
36 lines to specify synchronization in a total 1,033 lines of
code (omitting blanks and comments).

\begin{figure}[!htb]
\vspace{-.2cm}
{\footnotesize
        \centering

        \resizebox{\columnwidth}{!}{
        \begin{tabular}{lrrr}
                \hline
                Benchmark & \# Executions & \# Feasible & Total Time (s) \\
                \hline
                Chase-Lev Deque & 1,365 & 232 & 0.15 \\
                SPSC Queue & 19 & 15 & 0.01 \\
                RCU & 1269 & 756 & 0.11 \\ 
                Lockfree Hashtable & 30,941 & 25,731 & 11.39 \\ 
                MCS Lock & 19,501 & 13,546 & 2.62 \\
                MPMC Queue & 170,220 & 93,224 & 45.63 \\ % 1r2w
                M\&S Queue & 168 & 114 & 0.05 \\
                Linux RW Lock & 148,053 & 405 & 13.06 \\
                % Results from: 2014-03-25-13:26
                % Flags: -y -m 2 -u 3
                \hline
        \end{tabular}
        }
\vspace{-.1cm}
        \caption{\label{fig:benchmark_results} Benchmark results}
\vspace{-.3cm}
}
\end{figure}

\mysubsection{Performance}\label{sec:performance} 

Figure~\ref{fig:benchmark_results} presents performance results for
\TOOL on our benchmark set.  We list the number of
the total executions that \cdschecker has explored, the number of the feasible
executions that we checked the specification for, and the time the benchmark
took to complete.  All of our benchmarks complete within one minute
and most take less than 3 seconds to complete.

\mysubsection{Finding Bugs}\label{sec:findbugs}

\begin{figure}[!htb]
\vspace{-.2cm}
{\footnotesize
        \centering
        
        \resizebox{\columnwidth}{!}{
        \begin{tabular}{l|ccccc|c}
                \hline
                Benchmark & \# Injection & \# DR & \# UL & \# Correctness & \# Sync & Rate\\
                \hline
                Chase-Lev Deque & 10 & 0 & 2 & 3 & 2 & 70\%\\
                SPSC Queue & 2 & 2 & 0 & 0 & 0 & 100\%\\
                RCU & 3 & 0 & 0 & 1 & 2 & 100\%\\
                Lockfree Hashtable & 5 & 0 & 0 & 0 & 2 & 40\%\\
                MCS Lock & 4 & 0 & 0 & 0 & 4 & 100\%\\
                MPMC Queue & 6 & 0 & 0 & 0 & 2 & 33\%\\ 
                M\&S Queue & 11 & 0 & 6 & 3 & 0 & 82\%\\
                Linux RW Lock & 8 & 0 & 0 & 0 & 8 & 100\%\\
                \hline
                Total & 49 & 2 & 8 & 7 & 20 & 76\%\\
                \hline
                
                % Results from: 2014-03-25-17:08
                % Flags: -y -m 2 -u 3
        \end{tabular}
        }
\vspace{-.2cm}
        \caption{\label{fig:injection_results} Bug injection detection results}
\vspace{-.2cm}
}
\end{figure}

The next component of the evaluation examines the effectiveness of \TOOL for finding bugs.

\mypara{\bf New Bugs:} In the M\&S queue benchmark used
in~\cite{cdschecker}, the dequeue interface does not differentiate
between dequeuing the integer zero and returning that no item is
available, and it passed our initial specification.  However, after
modifying the dequeue interface to match that in the original paper,
\TOOL is able to find a new bug that \cdschecker did not find.  The
original test driver for this benchmark performed the enqueues first
to make it easy to write assertions that are valid for all executions.
\TOOL allows specification assertions to capture the behavior of the specific execution
and thus is able to discover the given bug.

\mypara {\bf Injected Bugs:} To further evaluate \TOOL,
we injected bugs in our benchmarks by weakening the ordering
parameter of the atomic operations. These include
changing \code{release}, \code{acquire}, \code{acq\_rel} and
\code{seq\_cst} to \code{relaxed}. We weakened one operation per
each trial, and covered all of the atomic operations that our
tests exercise.  While this injection strategy may not
reproduce all types of errors that developers make, it does
simulate errors that are caused by misunderstanding the
complicated semantics of relaxed memory models.

This fault injection strategy will introduce one of two types of bugs.
The first type is a specification-independent bug, which can be
detected by the underlying \cdschecker infrastructure which includes
internal data races and uninitialized loads. The second type is a
specification-dependent bug, which passes the built-in checks 
but violates the \TOOL specification.  These include
failed assertions and synchronization violations.  We
classifying bugs as follows. If \cdschecker reports a data
race or an uninitialized load, \TOOL reports the error and stops.
If not, \TOOL continues to check the
execution against the specification.  It first
checks for violations of the preconditions and postconditions and then for
violations of the synchronization specification.

Figure~\ref{fig:injection_results} shows the results of the injection
detection.  The column \textit{DR} represents data races, \textit{UL} represents
uninitialized loads, \textit{correctness} represents a failed precondition or
postcondition, and
\textit{sync} represents a synchronization violation. The detection rate is the
number of injections for which we detected a bug divided by the total
number of injections.

\mypara{\bf Linux Reader-Writer Lock:} Our initial specification for this
benchmark did not allow \code{write\_trylock} to spuriously fail.
However, when we checked this benchmark against that specification,
\TOOL checker reports a correctness violation. We then analyzed the code
and found that \code{write\_trylock} first subtracts a bias from the
\code{lock} variable to attempt to acquire the lock, and restores that
bias if the attempt to acquire the lock fails.  In the scenario where
two \code{write\_trylock} are racing for the lock before the lock is
released, one \code{write\_trylock} can first decrement the lock
variable, the lock can be released by the original holder, and then
the second \code{write\_trylock} can attempt to acquire the lock.
Even though the history indicates that the lock is unlocked, it
still holds a transient value due to the partially completed first
\code{write\_trylock} invocation.  Thus, the second
\code{write\_trylock} invocation will also fail.  As the second
\code{write\_trylock} serializes after both the first unsuccessful
\code{write\_trylock} and the \code{unlock} operation,
the sequential specification would force it to succeed.  We then modified  
the specification
of \code{write\_trylock} to allow spurious failures so that our correctness
model fits this data structure.  This shows
\TOOL can help developers iteratively refine the
specifications of their data structures. By analyzing the \TOOL
diagnostic report, developers can better understand
any inconsistencies between the specification and the
implementation.

\mypara{\bf MCS Lock:} Three of the weakened
operations are not detected because they cause the execution
to fail to terminate (and hit a trace bound).  We 
reviewed the code and found that weakening any of those three 
operations makes the lock spin forever.

\mypara{\bf M\&S Queue:} Our test driver does not cause
an enqueue or dequeue thread to help another
enqueue thread update the tail pointer, which corresponds to two of the
undetected injections.

\mypara{\bf Lockfree Hashtable:} Our experiment only focuses on the two
primitive methods, \code{get} and \code{put} without triggering the
\code{resize}. We were able to successfully check all executions from a  test driver for the lockfree hash table that generates executions that have no program order preserving sequential histories.

\mypara{\bf MPMC Queue:} The undetected injections in this benchmark are
primarily due to the limitation of our test driver. One
synchronization property of this benchmark is
that \code{read\_consume} should synchronize with the
next \code{write\_prepare} to ensure that a slot cannot be reused
before the consumer has finished with the slot.  Our test driver is
unable to reach this case so those injections are not detected.

From our experiments on concurrent data structures, we can see that
\TOOL checker can help detect incorrect memory orderings,
help developers refine data structure specifications,
and help determine whether strong memory orderings are really
necessary. Since \TOOL checker is a unit testing tool, it is limited
to small-scale tests to explore common usage scenarios of the data
structures. As a unit testing tool, \TOOL was able to find 100\% of
injections for many data structures and to find 76\% of the injections
on average. For our 49 injections, 10 of them were detected by checks
in \cdschecker, and 27 additional injections were detected by
\TOOL. This shows that by writing specifications, we detect
significantly more fault injections.