@techreport{chandrasekaran2007programming,
author = {Chandrasekaran, Prakash and Conway, Christopher and Joy, Joseph and Rajamani, Sriram},
title = {Programming Asynchronous Layers with CLARITY},
year = {2007},
month = {June},
abstract = {Asynchronous systems components are hard to write, hard to reason about, and—not coincidentally—hard to mechanically verify. In order to achieve high performance, asynchronous code is often written in an event-driven style that introduces non-sequential control flow and persistent heap data to track pending operations. As a result, existing sequential verification and static analysis tools are ineffective on event-driven code. We describe clarity, a programming language that enables analyzable design of asynchronous components. clarity has three novel features: (1) Nonblocking function calls which allows 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, which encapsulate common interactions between asynchronous components and make high-level coordination protocols explicit. (3) Linearity annotations, which 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 effective program analysis—most checking is done using simple sequential analysis. We describe our experience in developing a network device driver with clarity. We are able to mechanically verify several properties of the clarity driver that are well beyond the reach of current analysis technology applied to equivalent C code.},
publisher = {Association for Computing Machinery, Inc.},
url = {http://approjects.co.za/?big=en-us/research/publication/programming-asynchronous-layers-with-clarity/},
number = {MSR-TR-2007-80},
}