Programming Asynchronous Layers with CLARITY
Chennai Mathematical Institute.
Asynchronous systems programming is usually done in an event-driven style, which is tailored for performance rather than analyzability. Such programs have non-sequential control flow 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 ineective in analyzing asynchronous systems components. We propose a programming language, CLARITY, which enables analyzable design of asynchronous components. CLARITY has three novel features: (1) A nonblocking function call enables writing event driven code in sequential style. If a blocking construct is encountered during the execution of such a call, the call returns, and the remaining part of the computation is automatically queued for later execution. (2) A set of high-level coordination primitives, or coords, encap- sulate common interactions between asynchronous compo- nents, and make high-level coordination protocols explicit. (3) Code annotations delegate protocol obligations to exactly one thread at each asynchronous function call, making the behavior of an operation with respect to each coord effectively sequential.
We demonstrate how these language features enable both a more intuitive expression of program logic as well as more eective 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.
This is joint work with Christopher L. Conway, Joseph Joy and Sriram Rajamani.