\section{Testing Device Drivers}
\label{section:testing}

The second major component of \Arch\ is a {\em \tf} used to determine
whether a symbolically executing driver is behaving
correctly. Symbolic execution can detect whether a driver will perform
an illegal operation, such as reference an invalid address, on any
execution path through a function.  However, this proof does not
provide any general correctness guarantees: a ``hello world'' program
will not crash but will also not bring up an Ethernet interface
properly.

Thus, achieving high-quality driver code requires both
\textit{validating} and \textit{verifying} its operation to the extent
practical.  \textit{Validation} establishes that the driver is solving
the right problem and demonstrates that the driver does what it is
supposed to do, such as initializing a data structure or registering
with the kernel.  In contrast, \textit{verification} establishes that
the implementation follows the rules to solve the problem.  It ensures
the absence of known bugs such as memory or lock leaks and null
pointer dereferences.  With \Arch, we seek to ensure both driver
verification and validation takes place.  In the interests of
simplicity, we will refer to these two processes collectively as
``testing'' in this section.

Executing both the driver and the kernel symbolically provide only a
limited degree of validation and verification. The kernel contains
relatively little error checking code because it trusts drivers to
operate correctly; incorrect behavior by a driver often manifests as a
resource leak or a malfunctioning device, rather than as an illegal
operation detectable by symbolic execution.

\subsection{Testing with Specifications}

To support the above-mentioned use cases, \Arch\ provides developers
the means to specify a set of conditions that all drivers of a
particular class must enforce.  The \tf\ checks these specifications
as \Arch\ executes the driver.  For example, all network drivers must
call the \codesm{register\_netdev} function during initialization,
unless initialization fails.  No network driver should claim
initialization was successful and fail to call this function.
Symbolic execution by itself can never catch these kinds of bugs,
because of their domain-specific nature. Similarly, normal testing has
difficulty verifying these conditions, because they must hold across
{\em all possible} execution paths, not just the one that occurred
during testing.

The \tf\ is comprised of (i) a set of call outs into test code, where
conditions can be checked, (ii) an API library of code to check common
conditions, and (iii) checks for specific conditions on specific
interfaces.  The \tf\ interposes call outs on all interfaces between
the driver and kernel and allows tests to execute whenever control
passes between the kernel and the driver, in either direction. While
this allows tests to be developed independently of driver code, it
limits the framework for testing conditions that are visible at the
driver/kernel interface. The \tf\ executes symbolically, so it
evaluates conditions along each branch of execution independently.

\paragraph{Test-framework call outs} 
The \tf\ invokes a test function before and after every call into the
driver. Each function in the driver/kernel interface provides a unique
test function. Before entering the driver, test code can establish
preconditions, and when leaving the driver, test code can verify
postconditions that must hold.

\paragraph{Test-framework API}

The \tf\ provides an API library containing utility code for common
classes of tests. Using this API, checks can remain small and readily
understandable.  The API provides four classes of functions, which we
describe more in Section~\ref{sec:test-framework}.  First, the API
provides basic supporting functions to querying the current driver's
bus and class. This allows checks that apply only to certain classes
of drivers, such as PCI network drivers.  Second, the API provides a
function to report current execution context, indicating whether
blocking is safe. Third, the API provides methods to record state
variables, such as whether the driver has completed
initialization. Finally, the API provides an object tracker, which
records the state of memory regions (\eg, how was it allocated and how
big is it?) or locks (\eg, is it initialized?).

With this API, writing additional tests is straightforward.  For
example, verifying that a custom allocator is paired with a custom
free routine needs only a single call to the \tf\ API to tell it about
the allocation.  The \tf\ will then automatically support all drivers
that use the new allocator, and the drivers themselves require no
changes.

\paragraph{Test-framework checks}
The \tf\ API library provides a number of common checks, similar to
checking for illegal operations. For example, it verifies that all
objects that are freed were first allocated, and that locks released
were first acquired. However, we expect driver developers to use the
API to develop their own tests.

