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.
Also appeared as University of California Technical Report CSD-98-998.
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 dis
tributed computing systems make local replicas of shared data for
reasons of scalability and perfor mance. 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 imple ment,
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 suc cesses 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 dis covered 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.