Programming Asynchronous Layers with CLARITY

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.