Teapot: A domain-specific language for writing cache coherence protocols

In this paper, we describe Teapot, a domain-specific language for writing cache coherence protocols. Cache coherence is of concern when parallel and distributed systems make local replicas of shared data to improve scalability and performance. In both distributed shared memory systems and distributed file systems, a coherence protocol maintains agreement among the replicated copies as the underlying data are modified by programs running on the system. Cache coherence protocols are notoriously difficult to implement, debug, and maintain. Moreover, protocols are not off-the-shelf, reusable components, because their details depend on the requirements of the system under consideration. The complexity of engineering coherence protocols can discourage users from experimenting with new, potentially more efficient protocols. We have designed and implemented Teapot, a domain-specific language that attempts to address this complexity. Teapot's language constructs, such as a state-centric control structure and continuations, are better suited to expressing protocol code than those of a typical systems programming language. Teapot also facilitates automatic verification of protocols, so hard to find protocol bugs, such as deadlocks, can be detected and fixed before encountering them on an actual execution. We describe the design rationale of Teapot, present an empirical evaluation of the language using two case studies, and relate the lessons that we learned in building a domain-specific language for systems programming.