Vault(ID:8202/)





References:
  • De Line, R. and M. Faehndrich. Enforcing high-level protocols in low-level software. In Proceedings of the ACM Conference on Programming Language Design and Implementation (PLDI), pages 59-69, Snowbird, Utah, June 2001. view details
  • Conway, Christopher L. and Edwards, Stephen A. "NDL: A Domain-Specific Language for Device Drivers" LCTES?04, June 11?13, 2004, Washington, DC, USA. view details Extract: Introduction
    Device drivers are critical, low-level systems code. Traditionally, they have been written in C due to its eciency and  exibility. Unfortunately, sophisticated device interaction protocols and C's lack of type safety make driver code complex and prone to failure. Indeed, device drivers have been noted as a major source of faults in operating system code [2]. However, no other high-level language is widely accepted for device programming.

    To address this challenge, we introduce NDL1, a domain-specific language for device drivers. The language includes direct support for the semantics of device drivers, leading to shorter, more maintainable driver code. NDL can be used to write drivers for a wide variety of devices in a platformneutral fashion. The compiler is designed to be readily ported to a broad class of operating systems.

    In this paper, we demonstrate the features that make NDL device drivers simple and concise and show that the NDL compiler produces code which is only marginally less e- cient than the equivalent C. Throughout this paper, we will illustrate the use of NDL using examples from the driver for an NE2000-compatible Ethernet adapter. Extract: Related Work
    Related Work
    A variety of approaches have been suggested to improve the reliability of low-level software and device driver software in particular. Crary and Morrissett [3] propose typed assembly language as a compiler target for preserving type information from higher-level languages. Unfortunately, C, the most common systems programming language, is not much more strongly typed than a traditional assembly language; there is little the compiler can do to improve the type safety of C code.
    Deline and Faehndrich [4] use a similar typing system in the C-like programming language VAULT. The use of variables is controlled through type guards that describe when an operation on a variable is valid. In order for the compiler to accept the program, it must respect the type guards' access specifications and types must match at program join points. VAULT has shown some success in preventing common programmer errors, but its limitations on alias types prevent it from being generally applicable to device driver development.
    Holzmann [5] and Ball and Rajamani [1] have addressed the use of static analysis in the verification of traditional C systems software. Static analyses can find subtle bugs and increase confidence in the code, but the types of detectable errors are restricted and the quality of the analysis depends on programmer-written property specifications.
    A group at the University of Rennes has done perhaps the most work on domain-specific languages for device drivers. Thibault et al.'s GAL [8] is a domain-specific language for X Windows video drivers. Their compiler combines a partial evaluation framework with a language tailored to video driver operations to produce driver code that is nearly 90% smaller than the equivalent C code and just as fast. This work is promising, but the methodology may not be applicable to a wider variety of device drivers.
    Also at Rennes, Merillon et al. [6] developed Devil, an interface definition language designed to be a more general solution for device driver development. A Devil specification describes hardware components such as I/O ports and memory-mapped registers. The specification is compiled into a set of C macros for device manipulation; the macros are called from traditional C driver code, allowing the driver programmer to avoid writing the lowest-level code by hand. This approach prevents certain common programming errors, but it does not specify the protocol for using the device, and it does not provide the type safety of a higher-level solution. Nevertheless, portions of NDL borrow liberally from Devil's interface definition syntax.
    O'Nils and Janstch [7] and Wang et al. [9] have also developed tools for device driver synthesis, but they are primarily concerned with hardware/software codesign for embedded systems. NDL provides a more  exible tool for a wider range of devices. Extract: NDL
    NDL
    NDL is a language for device driver development that provides high-level constructs for device programming, describing the driver in terms of its operational interface. Its declarations are designed to closely resemble the specification document for the device it controls. An NDL driver is typically composed of a set of register definitions, protocols for accessing those registers, and a collection of device functions. The compiler translates register definitions and access protocols into an abstract representation of the device interface. Device functions are then translated into a series of operations on that interface.
    Device drivers are systems-level code that interact directly with the operating system. The NDL compiler generates C that makes appropriate operating system calls. Platformspeci fic functions are provided through compiler libraries and device templates; platform dependencies are minimal.
    NDL's main abstraction is a representation of the state of the peripheral device being controlled. Internally, devices can be in a variety of states, e.g., receiving data, waiting for a certain condition, or having encountered an error.
    From software, this state can be fairly awkward to access. At its simplest, it is spread out across bits in I/O memory packed carefully into bytes. Typically it is even more complicated, often consisting of an address and data register pair that provide indirect access to internal device registers. In both cases, NDL provides an abstraction layer that provides transparent access to this state information.
    For example, a typical sequence of I/O memory accesses
    in C might be coded
    outb(E8390_NODMA + E8390_PAGE0 + E8390_START,
    nic_base + NE_CMD);
    outb(count & 0xff, nic_base + EN0_RCNTLO);
    outb(count >> 8, nic_base + EN0_RCNTHI);
    Bit flags are combined and the integer count is shifted and masked to force its value into a disjoint register format. The write operations are a series of low-level I/O calls, using prede fined o sets on the device's base address. The equivalent NDL code uses a simple assignment syntax:
    start = true;
    dmaState = DISABLED;
    remoteDmaByteCount = count;
    NDL also provides a mechanism for describing groups of mutually exclusive states and procedures for switching among them. As a result, with a single line of NDL code the programmer is able to e ect a state transition that would require many I/O operations in an equivalent C program.
    Copying large amounts of data to and from bu ers is another frequent device operation. There are common idioms for a bu er-to-bu er copy in C, but they are complicated by the need to support compatible devices with di erent data bus widths in the same driver. NDL treats bu er copying as a special case of assignment. The following fragment reads count bytes read from the FIFO dataport (defined elsewhere) and placed in the array buffer using the appropriate I/O operations.
    var buffer: byte[count];
    buffer = dataport; Extract: Vault
    Deline and Faehndrich [4] use a similar typing system in
    the C-like programming language VAULT. The use of variables
    is controlled through type guards that describe when
    an operation on a variable is valid. In order for the compiler
    to accept the program, it must respect the type guards' access
    specifications and types must match at program join
    points. VAULT has shown some success in preventing common
    programmer errors, but its limitations on alias types
    prevent it from being generally applicable to device driver
    development.