Experience with a Language for Writing Coherence Protocols

Satish Chandra, Michael Dahlin, Bradley Richards, Randolph Y. Wang, Thomas E. Anderson and James R Larus

EECS Department
University of California, Berkeley
Technical Report No. UCB/CSD-98-998
1998

http://www2.eecs.berkeley.edu/Pubs/TechRpts/1998/CSD-98-998.pdf

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 support 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.


BibTeX citation:

@techreport{Chandra:CSD-98-998,
    Author = {Chandra, Satish and Dahlin, Michael and Richards, Bradley and Wang, Randolph Y. and Anderson, Thomas E. and Larus, James R},
    Title = {Experience with a Language for Writing Coherence Protocols},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {1998},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/1998/5563.html},
    Number = {UCB/CSD-98-998},
    Abstract = {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. <p>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 support 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.}
}

EndNote citation:

%0 Report
%A Chandra, Satish
%A Dahlin, Michael
%A Richards, Bradley
%A Wang, Randolph Y.
%A Anderson, Thomas E.
%A Larus, James R
%T Experience with a Language for Writing Coherence Protocols
%I EECS Department, University of California, Berkeley
%D 1998
%@ UCB/CSD-98-998
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/1998/5563.html
%F Chandra:CSD-98-998