Asynchronous systems programs are usually written in an event-driven style which is tailored for performance rather than analyzability. Such programs have non-sequential control ow and make heavy use of heap data structures to store and retrieve state related to pending operations. As a result, existing tools that analyze sequential programs are ine ective in analyzing asynchronous systems components. We describe clarity, a programming language that enables analyzable design of asynchronous components. clarity has three novel features: (1) Nonblocking function calls that allow event-driven code to be written in a sequential style. If a blocking statement is encountered during the execution of such a call, the call returns and the remainder of the operation is automatically queued for later execution. (2) Coords, a set of high-level coordination primitives, encapsulate common interactions between asynchronous components and make high-level coordination protocols explicit. (3) Linearity annotations delegate coord protocol obligations to exactly one thread at each asynchronous function call, transforming a concurrent analysis problem into a sequential one. We demonstrate how these language features enable both a more intuitive expression of program logic and more e ective program analysis most checking is done using simple sequential analysis. We describe our experience in developing, testing, and analyzing a network device driver using clarity. 1.

Device drivers are difficult to write and error-prone. They are usually written in C, a fairly low-level language with minimal type safety and little support for device semantics. As a result, they have become a major source of instability in operating system code.This paper presents NDL, a language for device drivers. NDL provides high-level abstractions of device resources and constructs tailored to describing common device driver operations. We show that NDL allows for the coding of a semantically correct driver with a code size reduction of more than 50% and a minimal impact on performance.