Transcript Problems of a More Complex Driver For Continuous Data Acquisition

Synthesizing Device Drivers
Roumen Kaiabachev and Walid Taha
Department of Computer Science, Rice University
Operating systems depend on device drivers to communicate with attached hardware.
A device driver is a collection of subroutines written in a low-level language that
interact both with the operating system and the actual device.
Driver Development is Hard
Why? Driver code executes in the
operating system trusted kernel.
When driver code crashes, the
whole system is usually taken
down.
How? We want to use high level
declarative specifications to
generate device drivers which
model operating system
processes and correctly
communicate with the
hardware. We are building
infrastructure in the form of a
domain-specific language (DSL)
which will provide the formal
theory and software
engineering medium for
development of device drivers.
Buffering. Data acquired
continuously is buffered until the
application can process it. Data is
transferred in the background from a
small hardware buffer on the device
to a second, larger buffer in computer
memory.
Page locking. Memory accessed from
an interrupt-service routine (ISR) or as
part of a direct memory access transfer
must be "page-locked" to prevent pages
from being swapped out.
Atomic device access. The device can be accessed from both the ISR
and from a user process calling device code. These device accesses can
be concurrent. We have to guarantee the ISR an atomic access until it is
done unless it is interrupted by a higher priority interrupt.
The Windows 2000
Architecture
 Cyclone – statically typed safe dialect of C
 Devil – DSL, high-level definition of bit-mapped I/O
 NDL – DSL, state-machine-based model of device
resources and common device driver operations
 BLAST – software model checking
In a previous study, we wrote a tiny device driver in
each of the tools to see how much and to what extent
they can help. There were several useful techniques to
take.
Resource tracking. It is not
allowed to start an acquisition
at the same time another is
already running. Also, it is
invalid to read data or stop an
acquisition if none is running.
Wait strategy. There are a
number of ways the driver
can wait when requested
data is not yet available:
polling, yielding, sleeping,
and waiting for an interrupt.
We Studied a Number of Existing Tools
Acknowledgements:
This work is supported
by National
Instruments,
Schlumberger, and a
Texas ATP grant
Problems of a More Complex Driver For Continuous Data Acquisition
Buffer overflow. There is a condition when the buffer can overflow.
Bad parameters. The user could give wrong parameters to the device.
Handling device reset. The driver should support a reset function that
stops any ongoing acquisition and returns the device to an initial state.
We are Designing and Implementing a DSL,
RIDL that solves the problems of the driver.
We will use state to tackle
We will use types for safe locking and will
explicitly model an interrupt scheduler
(constraints will be applied from defined
scheduling requirements).
We will use Devil-like interface checking for
RIDL will also use a Blast-like approach to
guarantee that certain user-specified states
cannot be reached.
Handling Other Driver
Problems
We will expand RIDL to
handle other interesting
device driver paradigms
and make it a useful tool
for driver writers.