S. Chandra, M. D. Dahlin, B. Richards, R. Y. Wang, T. E. Anderson, J. R.
Larus. Experience with a Language for Writing Coherence Protocols. Proc.
USENIX Conference on Domain-Specific Languages. October 1997.
In this paper, we describe our experience with Teapot, a domain-specific
language for addressing the cache coherence problem. The cache coherence problem
arises when parallel and distributed computing systems make local replicas of
shared data for reasons of scalability and performance. In both distributed
shared memory systems and distributed file systems, a coherence protocol
maintains agreement among the replicated copies when the underlying data are
modified by programs running on the system. Unfortunately, cache coherence
protocols are notoriously difficult to implement, debug, and maintain.
Furthermore, the details of the protocols depend on the requirements of the
system under consideration and are highly varied. This paper presents case
studies detailing the successes and shortcomings of using Teapot for writing
coherence protocols in two distinct systems. The first system, loosely coherent
memory (LCM), implements a particular flavor of distributed shared memory
suitable for data-parallel programming. The second system, the xFS distributed
file system, implements a high-performance, serverless file system. Our overall
experience with using Teapot has been positive. In particular, Teapot's language
features resulted in considerable simplifications in the protocol code for both
systems. Furthermore, Teapot's close coupling between implementation and formal
verification allowed us to achieve much higher confidence in our protocol
implementations than had previously been possible, reducing the time needed to
build the protocols. By using Teapot to solve real problems in complex systems,
we also discovered several shortcomings of the Teapot design. Most noticeably,
we found Teapot lacking in sup port for multithreaded environments, for
expressing actions that transcend several cache blocks, and for blocking system
calls. We conclude that domain-specific languages can be valuable in the
specific problem domain of cache coherence. Drawing on our experience, we also
provide guidelines for domain-specific languages in the broader context of
systems software.