Abstract
We address the problem of developing efficient cache coherence protocols implementing distributed shared memory (DSM) using message passing. A serious drawback of traditional approaches to this problem is that designers are required to state the desired coherence protocol at the level of asynchronous message interactions. We propose a method in which designers express the desired protocol at a high-level using rendezvous communication. These descriptions are much easier to understand and computationally more efficient to verify than asynchronous protocols due to their small state spaces. The rendezvous protocol can also be synthesized into efficient asynchronous protocols. We present our protocol refinement procedure, prove its soundness, and provide examples of its efficiency.
Supported in part by ARPA Order #13990 under SPAWAR Contract, #N0039-95-C0018 (Avalanche), DARPA under contract #DABT6396C0094 (UV).
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
G. N. Buckley and A. Silberschatz. An effective implementation for the generalized input-output construct of CSP. ACM TOPLAS, 5(2):223–235, April 1983.
J. B. Carter, C. Kuo, and R. Kuramkote. A comparison of software and hardware synchronization mechanisms for distributed shared memory multiprocessors. Technical Report UUCS-96-011, University of Utah, Salt Lake City, UT, USA, September 1996.
S. Chandra, B. Richards, and J. R. Larus. Teapot: Language support for writing memory coherency protocols. In SIGPLAN Conference on Programming Language Design and Implementation, May 1996.
Cray Research, Inc. CRAY T3D System Architecture Overview, hr-04033 edition, September 1993.
D. Dill, A.J. Drexler, A.J. Hu, and C.H. Yang. Protocol verification as a hardware design aid. In ICCD, pages 522–525, 1992.
A. Th. Eiriksson and K. McMillan. Using formal verification/analysis methods on the critical path in system design: A case study. In CAV, pages 367–380, 1995. Springer LNCS 939.
E. P. Gribomont. From synchronous to asynchronous communication. In C. Rattay, editor, Specification and Verification of Concurrent Systems, pages 368–383. Springer-Verilog, University of Stirling, Scotland, 1990.
J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Apporach. Morgan Kaufmann, 1996. Second Edition, Appendix E.
C. A. R. Hoare. Communicating sequential processes. CACM, 21(8):666–677, 1978.
G. J. Holzmann and D. Peled. The state of SPIN. In CAV, pages 385–389, New Brunswick, New Jersey, July 1996.
J. Kuskin and D. Ofelt et al. The Stanford FLASH multiprocessor. In 21st Annual International Symposium on Computer Architecture, pages 302–313, May 1994.
L. Lamport and F. B. Schneider. Pretending atomicity. In Research Report 44, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, May 1989.
D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M. S. Lam. The Stanford DASH multiprocessor. IEEE Computer, 25(3):63–79, March 1992.
R. J. Lipton. Reduction: A method of proving properties of parallel programs. CACM, 18(12):717–721, December 1975.
A. Nowatzyk, G. Aybay, M. Browne, E. Kelly, M. Parkin, B. Radke, and S. Vishin. The S3.mp scalable shared memory multiprocessor. In Proceedings of the 1995 International Conference on Parallel Processing, 1995.
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking and model checking. In CAV, pages 411–414, New Brunswick, NJ, USA, 1996.
S. Park and D. L. Dill. Protocol verification by aggregation of distributed transactions. In CAV, pages 300–309, New Brunswick, NJ, USA, July 1996. *** DIRECT SUPPORT *** A0008D07 00024
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nalumasu, R., Gopalakrishnan, G. (1998). Deriving efficient cache coherence protocols through refinement. In: Rolim, J. (eds) Parallel and Distributed Processing. IPPS 1998. Lecture Notes in Computer Science, vol 1388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-64359-1_748
Download citation
DOI: https://doi.org/10.1007/3-540-64359-1_748
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64359-3
Online ISBN: 978-3-540-69756-5
eBook Packages: Springer Book Archive