Title

Teapot: Language Support for Writing Memory Coherence Protocols

Document Type

Conference Proceeding

Publication Date

5-1-1996

Publication Title

Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation (PLDI)

Conference or Event

ACM SIGPLAN 1996 conference on Programming language design and implementation (PLDI)

Department

Mathematics and Computer Science

Abstract

Recent shared-memory parallel computer systems offer the exciting possibility of customizing memory coherence protocols to fit an application's semantics and sharing patterns. Custom protocols have been used to achieve message-passing performance---while retaining the convenient programming model of a global address space---and to implement high-level language constructs. Unfortunately, coherence protocols written in a conventional language such as C are difficult to write, debug, understand, or modify. This paper describes Teapot, a small, domain-specific language for writing coherence protocols. Teapot uses continuations to help reduce the complexity of writing protocols. Simple static analysis in the Teapot compiler eliminates much of the overhead of continuations and results in protocols that run nearly as fast as hand-written C code. A Teapot specification can be compiled both to an executable coherence protocol and to input for a model checking system, which permits the specification to be verified. We report our experiences coding and verifying several protocols written in Teapot, along with measurements of the overhead incurred by writing a protocol in a higher-level language.

pp.

237-248