Experience with a Language for
Writing Coherence Protocols


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.


Postscript



Randy Wang    (rywang.public@gmail.com)