|
Conference on Domain-Specific Languages, 1997
Experience with a Language for Writing Coherence Protocols
Satish Chandra and James R. Larus, University of Wisconsin, Madison; Michael Dahlin, University of Texas, Austin; Bradley Richards, Vassar College; Randolph Y. Wang and Thomas E. Anderson, University of California, Berkeley
Abstract
In this paper we describe our experience
with Teapot [7], a domain-specific language for writing cache
coherence protocols. Cache coherence is of concern when parallel and
distributed computing 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. Unfortunately, protocols are not off-the-shelf
items, as their details depend on the requirements of the system under
consideration. This paper presents case studies detailing the successes
and shortcomings of using Teapot for writing coherence protocols in two
systems. The first system, loosely coherent memory (LCM) [16], implements
a particular type of distributed shared memory suitable for data-parallel
programming. The second system, the xFS distributed file system
[9], implements a high-performance, serverless file system.
Our overall experience with Teapot has been very
positive. In particular, Teapot's language features resulted in considerable
simplifications in the protocol source code for both systems. Furthermore,
Teapot's close coupling between implementation and formal verification
helped to achieve much higher confidence in our protocol implementations
than previously possible and reduced the time 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 handling blocking system calls.
We believe that domain-specific languages are valuable tools for writing
cache coherence protocols.
- View the full text of this paper in
HTML form and
PDF form.
- If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
- To become a USENIX Member, please see our Membership Information.
|
Need help? Use our Contacts page.
Technical Program