\section{Evaluation}
\label{section:evaluation}

The purpose of the evaluation is to verify that \Arch\ achieves its
goals: (i) usefulness, (ii) simplicity, and (iii) efficiency.

\subsection{Methodology}

% Next paragraph:
% 19 + 7 = \howmanydrivers = 26
% 13 + 4 + 5 + 4 = \howmanydrivers = 26

As shown in Table~\ref{fig:table-drivers}, we tested \Arch\ on
\howmanydrivers\ drivers in 11 classes from several Linux kernel
revisions (13 drivers from 2.6.29, 4 from 3.1.1, and 4 that normally
run only on Android-based phones) and from FreeBSD 9 (5 drivers).  Of
the \howmanydrivers\ drivers, we chose 19 as examples of a specific
bus or class and the remaining 7 because we found frequent patches to
them and thus expected to find bugs.

%\fixme{Julia: why some from each kernel?  relevance of having the
%  hardware?}

All tests took place on a machine running Ubuntu 10.10 x64 equipped
with a quad-core Intel 2.50GHz Intel Q9300 CPU and 8GB of memory.  All
results are obtained while running \Arch\ in a single-threaded mode,
as \Arch\ does not presently work with \see's multicore
support.\footnote{This limitation is an engineering issue and prevents
  \Arch\ from exploring multiple paths simultaneously. However,
  because \Arch's favor-success scheduling often explores a single
  path deeply rather than many paths at once, \see's multi-threaded
  mode would have little performance benefit.}

To test each driver, we carry out the following operations:

\begin{enumerate}
\item Run \ds\ over the driver and compile the output.
\item Define a virtual hardware device with the desired parameters and
  boot the \Arch\ virtual machine.
\item Load the driver with \codesm{insmod} and wait for initialization
  to complete successfully.  Completing this step entails executing at
  least one successful path and returning success, though it is likely
  that other failed paths also run and are subsequently discarded.
\item Execute a workload (optional).  We ensure all network drivers
  attempt to transmit and that sound drivers attempt to play a sound.
\item Unload the driver.
\end{enumerate}

If \Arch\ reports warnings about too many paths from complex loops, we
annotate the driver code and repeat the operations.  For most drivers,
we run \ds\ over only the driver code. For drivers that have
fine-grained interactions with a library, such as sound drivers and
the pluto2 media driver, we run \ds\ over both the library and the
driver code. We annotated each driver at locations \Arch\ specified,
and tested each Linux driver with 49 checkers for a variety of common
bugs.  For FreeBSD drivers, we only used the operating system's
built-in test functionality.

\setlength{\tabcolsep}{5pt}
\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l|l||r|r|r|r|r}
\hline
% All annotations mentioned in comments are included
{\bf Driver} & {\bf Class} & {\bf Bugs} &{\bf LoC} & {\bf Ann} & {\bf Load} & {\bf Unld.} \\
\hline
\hline
\textit{akm8975}*  & Compass  & 4 &    629  & 0 &  0:22 & 0:08 \\
\textit{mmc31xx}*  & Compass  & 3 &    398  & 0 &  0:10 & 0:04 \\
tle62x0*           & Control  & 2 &    260  & 0 &  0:06 & 0:05 \\
me4000             & Data Ac. & 1 &  5,394  & 2 &  1:17 & 1:04 \\
phantom            & Haptic   & 0 &    436  & 0 &  0:16 & 0:13 \\
lp5523*            & LED Ctl. & 2 &    828  & 0 &  2:26 & 0:19 \\
apds9802*          & Light    & 0 &    256  & 1 &  0:31 & 0:21 \\
8139cp             & Net      & 0 &  1,610  & 1 &  1:51 & 0:37 \\
8139too            & Net      & 2 &  1,904  & 3 &  3:28 & 0:35 \\
be2net             & Net      & 7 &  3,352  & 2 &  4:49 & 1:39 \\
dl2k               & Net      & 1 &  1,985  & 5 &  2:52 & 0:35 \\
e1000              & Net      & 3 & 13,971  & 2 &  4:29 & 2:01 \\
et131x             & Net      & 2 &  8,122  & 7 &  6:14 & 0:47 \\
forcedeth          & Net      & 1 &  5,064  & 2 &  4:28 & 0:51 \\
ks8851*            & Net      & 3 &  1,229  & 0 &  2:05 & 0:13 \\
pcnet32            & Net      & 1 &  2,342  & 1 &  2:34 & 0:27 \\
\textit{smc91x}*   & Net      & 0 &  2,256  & 0 & 10:41 & 0:22 \\
pluto2             & Media    & 2 &    591  & 3 &  1:45 & 1:01 \\ % 591 used to have asterisk
econet             & Proto.   & 2 &    818  & 0 &  0:11 & 0:11 \\
ens1371            & Sound    & 0 &  2,112  & 5 & 27:07 & 4:48 \\ % 2,112 used to have asterisk
\textit{a1026}*    & Voice    & 1 &  1,116  & 1 &  0:34 & 0:03 \\
\hline
ed                 & Net      & 0 &  5,014  & 0 &  0:49 & 0:13 \\
re                 & Net      & 0 &  3,440  & 3 & 16:11 & 0:21 \\
rl                 & Net      & 0 &  2,152  & 1 &  2:00 & 0:08 \\
es137x             & Sound    & 1 &  1,688  & 2 & 57:30 & 0:09 \\
maestro            & Sound    & 1 &  1,789  & 2 & 17:51 & 0:27 \\

% Ensure bugs column totals \howmanybugs

\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Drivers tested.  Those in \textit{italics} run
  on Android-based phones, those followed by an asterisk are for
  embedded systems and do not use the PCI bus. Drivers above the line
  are for Linux and below the line are for FreeBSD.  Line counts come
  from  CLOC~\cite{clocutility}.  Times are in minute:second format, and are
  an average of three runs.}
\label{fig:table-drivers}
\vspace{-0.1in}
\end{table}

\subsection{Bug Finding}


\begin{table}[t!]
\footnotesize
\centering
\begin{tabular}{l||r|r||r|r|r}
\hline
               &            & {\bf Kernel /} & {\bf Cross}  &             &            \\
{\bf Bug Type} & {\bf Bugs} & {\bf Checker}  & {\bf EntPt} & {\bf Paths} & {\bf Ptrs} \\
\hline
\hline
Hardware Dep.     &  7 &  6 /  1 &  4 &  6 &  6 \\
API Misuse        & 15 &  7 /  8 &  6 &  5 &  1 \\
Race              &  3 &  3 /  0 &  3 &  2 &  3 \\
Alloc. Mismatch   &  3 &  0 /  3 &  3 &  0 &  3 \\
Leak              &  7 &  0 /  7 &  6 &  1 &  7 \\
Driver Interface  &  3 &  0 /  3 &  0 &  2 &  0 \\
Bad pointer       &  1 &  1 /  0 &  0 &  0 &  1 \\
\hline
{\bf Totals}      & 39 & 17 / 22 & 22 & 16 & 21 \\ % \howmanybugs - ensure totals match
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Summary of bugs found. For each category, we
  present the number of bugs found by kernel crash/warning or a checker
  and the number that crossed driver entry points (``Cross EntPt''),
  occurred only on specific paths, or required tracking pointer
  usage.}
\label{fig:table-bug-summary}
\vspace{-0.2in}
\end{table}
\setlength{\tabcolsep}{6pt}

% \howmanybugs
% 17 + 22 = 39 (see table above)

Across the \howmanydrivers\ drivers listed in
Table~\ref{fig:table-drivers}, we found the \howmanybugs\ distinct bugs
described in Table~\ref{fig:table-bug-summary}.  Of these bugs, \see\
detected 17 via a kernel warning or crash, and the checkers caught the
remaining 22. Although these bugs do not necessarily result in driver
crashes, they all represent issues that need addressing and are
difficult to find without visibility into driver/kernel interactions.

% \howmanybugs
% 22 / 39 = 56%
% 16 / 39 = 41%
% 21 / 39 = 54%

These results show the value of symbolic execution. Of the
\howmanybugs\ bugs, 56\% spanned multiple driver invocations. For
example, the akm8975 compass driver calls \codesm{request\_irq} before
it is ready to service interrupts.  If an interrupt occurs immediately
after this call, the driver will crash, since the interrupt handler
dereferences a pointer that is not yet initialized. In addition, 41\%
of the bugs occurred on a unique path through a driver other than one
that returns success, and 54\% involved pointers and pointer
properties that may be difficult to detect statically.

%\fixme{Julia: why is [path sensitivity] a problem for static analysis}
%\fixme{Julia: hard to judge based on one example.  Ref. to results?}

\paragraph{Bug Validation.}
Of the \howmanybugs\ bugs found, at least 17 were fixed between the
2.6.29 and 3.1.1 kernels, which indicates they were significant enough
to be addressed. We were unable to establish the current status of 7
others because of significant driver changes.  We have submitted bug
reports for 5 unfixed bugs in mainline Linux drivers, all of which
have been confirmed as genuine by kernel developers.  The remaining
bugs are from drivers outside the main Linux kernel that we have not
yet reported.

\subsection{Developer Effort}

One of the goals of \Arch\ is to minimize the effort to test a
driver. The effort of testing comes from three sources: (i) annotations to
prepare the driver for testing, (ii) testing time, and (iii) updating
code as kernel interfaces change.

To measure the effort of applying \Arch\ to a new driver, we tested
the \codesm{phantom} haptic driver from scratch. The total time to
complete testing was 1h:45m, despite having no prior experience with
the driver and not having the hardware.  In this time, we configured
the symbolic hardware, wrote a user-mode test program that passes
symbolic data to the driver's entry points, and executed the driver
four times in different configurations. Of this time, overhead of
\Arch\ compared to testing with a real device was an additional pass
during compilation to run \ds, which takes less than a minute, and 38
minutes to execute.  Although not a large driver, this test
demonstrates \Arch's usability from the developer's perspective.

\paragraph{Annotations.}
The only per-driver coding \Arch\ requires is annotations on loops
that slow testing and annotations that prioritize specific
paths. Table~\ref{fig:table-drivers} lists the number of annotation
sites for each driver. Of the \howmanydrivers\ drivers, only 6
required more than two annotations, and 9 required no annotations. In
all cases, \Arch\ printed a warning indicating where an annotation
would benefit testing.

\paragraph{Testing time.}
Symbolic execution can be much slower than normal execution. Hence, we
expect it to be used near the end of development, before submitting a
patch, or on periodic scans through driver code.  We report the time
to load, initialize, and unload a driver (needed for detecting
resource leaks) in Table~\ref{fig:table-drivers}.  Initialization time
is the minimum time for testing, and thus presents a lower bound.

Overall, the time to initialize a driver is roughly proportional to
the size of the driver.  Most drivers initialize in 5 minutes or less,
although the ens1371 sound driver required 27 minutes, and the
corresponding FreeBSD es137x driver required 58 minutes.  These two
results stem from the large amount of device interaction these drivers
perform during initialization.  Excluding these results, execution is
fast enough to be performed for every patch, and with a cluster could
be performed on every driver affected by a collateral
evolution~\cite{padioleau:coccinelle:eurosys:2008}.


%\fixme{Julia: If a
%  maintainer receives 10 patches per day, then he may have to wait 5
%  hours?  If he did static analysis on the code affected by the
%  changes, would it take 5h to analyze the results?  (Admittedly this
%  is a worst case)}.

\paragraph{Kernel evolution.}
Near the end of development, we upgraded \Arch\ from Linux 2.6.29 to
Linux 3.1.1. If much of the code in \Arch\ was specific to the kernel
interface, porting \Arch\ would be a large effort. However, \Arch's
use of static analysis and code generation minimized the effort to
maintain tests as the kernel evolves: the only changes needed were to
update a few checkers whose corresponding kernel functions had
changed. The remainder of the system, including \ds\ and the \tf, were
unchanged.  The number of lines of code changed was less than 100.

Furthermore, porting \Arch\ to a new operating system is not
difficult.  We also ported the \Arch\ infrastructure, checkers
excluded, to FreeBSD 9.  The entire process took three person-weeks.
The FreeBSD implementation largely shares the same code base as the
Linux version, with just a few OS-specific sections.  This result
confirms that the techniques \Arch\ uses are compatible across
operating systems.


\subsection{Coverage}

% Basic block coverage
%8139too      & 80\% &
%a1026        & 76\% &
%apds9802     & 85\% &
%econet       & 36\% &
%ens1371      & 56\% &
%lp5523       & out of date &
%me4000       & 61\% &
%mmc31xx      & 83\% &
%phantom      & 81\% &
%pluto2       & 76\% &
%tle62x0      & out of date &

\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l||rr|rr}
\hline
                &  { \bf Touched} &                 & \multicolumn{2}{|c}{\bf Time} \\
{\bf Driver}    &  { \bf Funcs. } & {\bf Coverage}  & { \bf CPU } & { \bf Latency } \\
\hline
\hline
8139too         &  93\% & 83\% &   2h36m &   1h00m \\
a1026           &  95\% & 80\% &     15m &     13m \\
apds9802        &  85\% & 90\% &     14m &      7m \\
econet          &  51\% & 61\% &     42m &     26m \\
ens1371         &  74\% & 60\% &  *8h23m &  *2h16m \\
lp5523          &  95\% & 83\% &     21m &      5m \\
me4000          &  82\% & 68\% & *26h57m & *10h25m \\
mmc31xx         & 100\% & 83\% &     14m &     26m \\
phantom         &  86\% & 84\% &     38m &     32m \\
pluto2          &  78\% & 90\% &     19m &      6m \\
tle62x0         & 100\% & 85\% &     16m &     12m \\
\hline
es137x          &  97\% & 70\% &   1h22m &     58m \\
rl              &  84\% & 71\% &     13m &     10m \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Code coverage.}
\label{fig:table-drivers-coverage}
\vspace{-0.2in}
\end{table}

While \Arch\ primarily uses symbolic execution to simulate the device,
a second benefit is higher code coverage than standard
testing. Table~\ref{fig:table-drivers-coverage} shows coverage results
for one driver of each class, and gives the fraction of functions
executed (``Touched Funcs.'') and the fraction of basic blocks {\em
  within} those functions (``Coverage'').\footnote{* Drivers with an
  asterisk ran unattended, and their total execution time is not
  representative of the minimum.} In addition, the table gives the
total CPU time to run the tests on a single machine (CPU) and the
latency of the longest run if multiple machines are used (Latency). In
all cases, we ran drivers multiple times and merged the coverage
results. We terminated each run once it reached a steady state and
stopped testing the driver once coverage did not meaningfully improve
between runs.

Overall, \Arch\ executed a large majority (80\%) of driver functions
in most drivers, and had high coverage (80\% of basic blocks) in those
functions. These results are below 100\% for two reasons. First, we
could not invoke all entry points in some drivers. For example, econet
requires user-mode software to trigger additional driver entry points
that \Arch\ is unable to call on its own.  In other cases, we simply
did not spend enough time understanding how to invoke all of a
driver's code, as some functionality requires the driver to be in a
specific state that is difficult to realize, even with symbolic
execution.  Second, of the functions \Arch\ did execute, additional
inputs or symbolic data from the kernel were needed to test all
paths. Following \see's relaxed consistency model by making more of
the kernel API symbolic could help improve coverage.

As a comparison, we tested the 8139too driver on a real network card
using \codesm{gcov} to measure coverage with the same set of tests.
We loaded and unloaded the driver, and ensured that transmit, receive,
and all ethtool functions executed.  Overall, these tests executed
77\% of driver functions, and covered 75\% of the lines in the
functions that were touched, as compared to 93\% of functions and 83\%
of code for \Arch.  Although not directly comparable to the other
coverage results due to differing methodologies, this result shows
that \Arch\ can provide coverage better than running the driver on
real hardware.

\subsection{Patch Testing}
The second major use of \Arch\ is to verify driver patches similar to
a code reviewer. For this use, we seek high coverage in every function
modified by the patch in addition to the testing described
previously. We evaluate \Arch's support for patch testing by applying
all the patches between the  3.1.1 and 3.4-rc6 kernel
releases that applied to the 8139too (net), ks8851 (net) and lp5523
(LED controller) drivers, of which there were 4, 2, and 6,
respectively.  The other drivers either lacked recent patches,
had only trivial patches, or required upgrading the kernel, so we
did not consider them.

In order to test the functions affected by a patch, we used
favor-success scheduling to fast-forward execution to a patched
function and then enabled high coverage mode.  The results, shown in
Table~\ref{fig:table-patch-coverage}, demonstrate that \Arch\ is able
to quickly test patches as they are applied to the kernel, by allowing
developers to test nearly all the changed code without any device
hardware. \Arch\ was able to execute 100\% of the functions touched by
all 12 patches across the 3 drivers, and an average of 98\% of the
code in each function touched by the patch. In addition, tests took an
average of only 12 minutes to complete.

% 6m = (total run time / number of runs).  This number is less than
% parallel time since there were six runs in all.
% 98\% = (touched basic blocks in functions of interest) /
%        (bb's in functions of interest)

\begin{table}[t!]
\centering
\footnotesize
\begin{tabular}{l||rr|rr}
\hline
                &  { \bf Touched} &                 & \multicolumn{2}{|c}{\bf Time} \\
{\bf Driver}    &  { \bf Funcs. } & {\bf Coverage}  & { \bf Serial } & { \bf Parallel } \\
\hline
\hline
8139too         &  100\% &  96\% &      9m &      5m \\
ks8851          &  100\% & 100\% &     16m &      8m \\
lp5523          &  100\% &  97\% &     12m &     12m \\
\end{tabular}
\vspace{-0.1in}
\caption{\small \bf Patched code coverage.}
\label{fig:table-patch-coverage}
\vspace{-0.2in}
\end{table}

% We have been unable to author patches for all of the bugs as the
% solutions in some cases appear to be complex, and some of the bugs
% are from out-of-tree drivers without a clear patch submission
% process.  In the case of one bug, developers confirmed it as
% genuine, but were unable to suggest a proper patch.

\paragraph{Execution tracing.}
Execution tracing provides an alternate means to verify patches by
comparing the behavior of a driver before and after applying the
patch. We used tracing to verify that \Arch\ can distinguish between
patches that change the driver/device interactions and those that do
not, such as a collateral evolution.  We tested five patches to the
8139too network driver that refactor the code, add a feature, or
change the driver's interaction with the hardware.  We executed the
original and patched drivers and record the hardware interactions.
Comparing the traces of the before and after-patch drivers, differing
I/O operations clearly identify the patches that added a feature or
changed driver/device interactions, including which functions
changed. As expected, there were no differences in the refactoring
patches.

We also apply tracing to compare the behavior of drivers for the same
device across operating systems. Traces of the Linux 8139too driver
and the FreeBSD rl driver show differences in how these devices
interact with the same hardware that could lead to incorrect behavior.
In one case, the Linux \codesm{8139too} driver incorrectly treats one
register as 4 bytes instead of 1 byte, while in the other, the \codesm{rl}
FreeBSD driver uses incorrect register offsets for a particular
supported chipset.  Developers fixed the Linux bug independently after
we discovered it, and we validated the FreeBSD bug with a FreeBSD
kernel developer.  We do not include these bugs in the
previous results as they were not identified automatically by \Arch.

These bugs demonstrate a new capability to find hardware-specific bugs
by comparing independent driver implementations. While we manually
compared the traces, it may be possible to automate this
process.

\subsection{Comparison to other tools.}
We compare \Arch\ against other driver testing/bug-finding tools to
demonstrate its usefulness, simplicity, and efficiency.

\paragraph{\see.}
In order to demonstrate the value of \Arch's additions to \see, we
executed the 8139too driver with only annotations to the driver source
guiding path exploration but without the \tf\ or \ds\ to prioritize
relevant paths.  In this configuration, \see\ executes using
\textit{strict consistency}, wherein the only source of symbolic data
is the hardware, and maximizes coverage with the MaxTbSearcher plugin.
This mode is the default when a developer does not write API-specific
plugins; results improve greatly when these plugins are
available~\cite{ckc12}.  We ran \see\ until it ran out of memory to
store paths and started thrashing after 23 minutes.

During this test, only 33\% of the functions in the driver were
executed, with an average coverage of 69\%.  In comparison, \Arch\
executed 93\% of functions with an average coverage of 83\% in
2\textonehalf\ hours. With \see\ alone, the driver did not complete
initialization and did not attempt to transmit packets.  In addition,
\see's annotations could not be made on the driver source, but must be
made on the binary instead. Thus, annotations must be regenerated
every time a driver is compiled.

Adding more RAM and running the driver longer would likely have
allowed the driver to finish executing the initialization routine.
However, many uninteresting paths would remain, as \see\ has no
automatic way to prune them.  Thus, the developer would still have
considerable difficulty invoking other driver entry points, since
\see\ would continue to execute failing execution paths.

In order for \see\ to achieve higher coverage in this driver, we would
need a plugin to implement a relaxed consistency model.  However, the
8139too driver (v3.1.1) calls 73 distinct kernel functions, which
would require developer effort to code corresponding functions in the
plugin.

%Running
%\see\ without API-aware plugins is analogous to running \Arch\ with
%FreeBSD, since \Arch\ has no API-specific knowledge of FreeBSD's
%operation aside from the short list of kernel functions which return
%non-standard error values.

% Maybe in related work or separate ``limitations of static tools''
% section
\paragraph{Static-analysis tools.} Static analysis tools are able to
find many driver bugs, but require a large effort to implement a model
of operating system behavior. For example, Microsoft's Static Driver
Verifier (SDV) requires 39,170 lines of C code to implement an
operating system model~\cite{microsoft10}.  \Arch\ instead relies on
models only for the I/O bus implementations, which together account
for 715 lines of code for 5 buses.  \Arch\ supports FreeBSD with only
491 lines of OS-specific code, primarily for the \tf, and can check
drivers with the debugging facilities already included in the OS.  

In addition, SDV achieves much of its speed through simplifying its
analysis, and consequently its checkers are unable to represent
arbitrary state. Thus, it is difficult to check complex properties
such as whether a variable has matched allocation/free calls across
different entry points.

\paragraph{Kernel debug support.} Most kernels provide debugging to
aid kernel developers, such as tools to detect deadlock, track memory
leaks, or uncover memory corruption. Some of the \tf\ checkers are
similar to debug functionality built into Linux.  Compared to the
Linux leak checker, kmemleak, the \tf\ allows testing a single driver
for leaks, which can be drowned out when looking at a list of leaks
across the entire kernel. Furthermore, writing checkers for \Arch\ is
much simpler: the Linux 3.1.1 kmemleak module is 1,113 lines, while,
the \tf\ object tracker, including a complete hash table
implementation, is only 722 lines yet provides more precise results.
