--- /dev/null
+\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.
projects / cdsspec-compiler.git / blobdiff