\subsection{Symbolic Devices}

Drivers interact with devices according to well-defined, narrow
interfaces.  For PCI device drivers, this interface is comprised of
I/O memory accessed via normal loads and stores, port I/O
instructions, bus operations, DMA memory, and interrupts.  Drivers
using other buses, such as SPI and \itwoc, use functions provided by
the bus for similar operations.

% From Matt - I cut the following paragraph as we seem to cover this
% in the subsequent sections.

%To provide symbolic hardware, \see\ provides symbolic data of the
%appropriate size each time the driver performs a read operation using
%memory or port I/O.  Similarly, the VMM treats the contents of DMA
%memory, indicated through DMA mapping functions, as symbolic.  The VMM
%does not insert symbolic interrupts; instead, \Arch\ invokes the
%driver's interrupt handler each time control passes from the driver to
%the kernel. For buses such as \itwoc\ that use I/O wrapper functions,
%\Arch\ rewrites the wrappers to return symbolic data.

\Arch\ provides a symbolic device for the driver under test, while at
the same time emulating the other devices in the system. A symbolic
device provides three key behaviors. First, it can be {\em
  discovered}, so the kernel loads the appropriate driver. Second, it
provides methods to read from and write to the device and return
symbolic data from reads. Third, it supports interrupts and DMA, if
needed.  \Arch\ currently supports 5 buses on Linux: PCI (and its
variants), \itwoc\ (including SMBus), Serial Peripheral Interface
(SPI), General Purpose I/O (GPIO), and Platform;\footnote{The
  ``platform bus'' is a Linux-specific term that encompasses many
  embedded devices.  Linux's ARM implementation, for example, supports
  a variety of SoCs, each with its own set of integrated devices.  The
  drivers for these devices are often of the ``platform'' type.} and
the PCI bus on FreeBSD.

\paragraph{Device Discovery.}
%\fixme{Julia: this section is rather technical -- can it be simplified
%  and/or can we provide an example}

When possible, \Arch\ creates symbolic devices in the \see\ virtual
machine and lets existing bus code discover the new device and load
the appropriate driver.  For some buses, such as \itwoc, the kernel or
another driver normally creates a statically configured device object
during initialization. For such devices, we created a small kernel
module, consisting of 715 lines of code, that creates the desired
symbolic device.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% one reviewer wanted to know why we don't do USB.  Here's an example
% response that's way too long

%We believe SymDrive
%would work with USB, but would require a more effort to implement a
%symbolic bus.  USB device drivers interface with other drivers lower
%in a stack.  The host controller interface driver communicates with
%the hardware, and modern operating systems typically only need one
%such driver for USB 1.0, 2.0, and 3.0.  Supplying symbolic data at
%this level of abstraction is not practical, because it would need to
%pass through the host controller driver, and likely generate many
%uninteresting paths.

%To address this issue, we would need to write a symbolic bus similar
%to the one used by SymDrive's I2C support.  I2C provides a similar,
%high-level communication interface with the device, implemented in
%Linux's i2c-core and one of the various chip-specific drivers,
%e.g. PIIX4.  We've not done a similar implementation for USB because
%of time constraints.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%For example, \Arch\ uses \see's symbolic
%hardware plugin to create a virtual PCI device with the desired I/O
%memory configuration and PCI identifiers, both easily found in
%driver source code. This device triggers the PCI code in Linux to load the
%driver.

% Edited to add that a number of drivers also create these devices.
% For example, many PCI-E video cards have thermal monitoring
% features, and these temperature sensors are often I2C, so the video
% card driver then creates the corresponding I2C device.

\Arch\ can make the device configuration space symbolic after loading
the driver by returning symbolic data from PCI bus functions with the
\tf (similar to \see's NDIS driver support).  PCI devices use this
region of I/O memory for plug-and-play information, such as the vendor
and device identifiers.  If this data is symbolic, the device ID will
be symbolic and cause the driver to execute different paths for each
of its supported devices. Other buses have similar configuration data,
such as ``platform data'' on the SPI bus. A developer can copy this
data from the kernel source and provide it when creating the device
object, or make it symbolic for additional code coverage.

\paragraph{Symbolic I/O.}
Most Linux and FreeBSD drivers do a mix of programmed I/O and DMA.
\Arch\ supports two forms of programmed I/O. For drivers that perform
I/O through hardware instructions, such as \codesm{inb}, or through
memory-mapped I/O, \Arch\ directs \see\ to ignore write operations,
because they do not return values that influence driver execution, and
to return symbolic data from reads. The \tf\ overrides bus I/O functions,
such as those used in \itwoc\ drivers, to function analogously.

\paragraph{Symbolic Interrupts.}
After a driver registers an interrupt handler, the \tf\ invokes the
interrupt handler on every transition from the driver into the kernel.
This model represents a trade-off between realism and simplicity: it
ensures the interrupt handler is called often enough to keep the
driver executing successfully, but may generate spurious interrupts
when the driver does not expect them.

\paragraph{Symbolic DMA.}
When a driver invokes a DMA mapping function, such as
\codesm{dma\_alloc\_coherent}, the \tf\ uses a new \see\ opcode to make
the memory act like a memory-mapped I/O region: each read returns a
new symbolic value and writes have no effect. Discarding writes to DMA
memory reflects the ability of the device to write the data via DMA at
any time.  The driver should not assume that data written here will be
available subsequently. When the driver unmaps the memory, the
\tf\ directs \see\ to revert the region to normal symbolic data, so
writes are seen by subsequent reads.
