Verification of FLASH cache coherence protocol by aggregation of distributed transactions

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verification of FLASH cache coherence protocol by aggregation of distributed transactions

Full text

Pdf (1.14 MB)

Source

ACM Symposium on Parallel Algorithms and Architectures archive
Proceedings of the eighth annual ACM symposium on Parallel algorithms and architectures table of contents

Padua, Italy

Pages: 288 - 296

Year of Publication: 1996

ISBN:0-89791-809-6

Authors

Seungjoon Park	Computer Systems Laboratory, Stanford University
David L. Dill	Computer Systems Laboratory, Stanford University

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGARCH: ACM Special Interest Group on Computer Architecture

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 4, Downloads (12 Months): 30, Citation Count: 8

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/237502.237573 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	James Archibald , Jean Loup Baer, An economical solution to the cache coherence problem, Proceedings of the 11th annual international symposium on Computer architecture, p.355-362, January 1984
	2	L. Censier and P. Feautrier. A new solution to coherence problems in multicache systems. IEEE Transactzons on Computers, 27(12):1112-1118, December 1978.
	3	David L. Dill , Andreas J. Drexler , Alan J. Hu , C. Han Yang, Protocol Verification as a Hardware Design Aid, Proceedings of the 1991 IEEE International Conference on Computer Design on VLSI in Computer & Processors, p.522-525, October 11-14, 1992
	4	David L Dill , Seungjoon Park , Andreas G. Nowatzyk, Formal specification of abstract memory models, Proceeding of the 1993 symposium on Research on integrated systems, p.38-52, February 1993, Seattle, Washington, United States
	5	Ásgeir Th. Eiríksson , Kenneth L. McMillan, Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study, Proceedings of the 7th International Conference on Computer Aided Verification, p.367-380, July 03-05, 1995
	6	Phillip B. Gibbons , Michael Merritt , Kourosh Gharachorloo, Proving sequential consistency of high-performance shared memories (extended abstract), Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.292-303, July 21-24, 1991, Hilton Head, South Carolina, United States [doi>10.1145/113379.113406]
	7	Mark Heinrich. The FLASH Protocol. Internal document, Stanford University FLASH Group, 1993.
	8	J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
	9	Leslie Lamport. How to make a multiprocessor computer that correctly executes multiprocessor programs. IEEE Transactions on Computers, 28(9):690- 691, September 1979.
	10	Daniel Lenoski , James Laudon , Kourosh Gharachorloo , Anoop Gupta , John Hennessy, The directory-based cache coherence protocol for the DASH multiprocessor, Proceedings of the 17th annual international symposium on Computer Architecture, p.148-159, May 28-31, 1990, Seattle, Washington, United States
	11	Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
	12	Seungjoon Park , David L. Dill, An executable specification, analyzer and verifier for RMO (relaxed memory order), Proceedings of the seventh annual ACM symposium on Parallel algorithms and architectures, p.34-41, June 24-26, 1995, Santa Barbara, California, United States [doi>10.1145/215399.215413]
	13	Seungjoon Park , David L. Dill, Protocol Verification by Aggregation of Distributed Transactions, Proceedings of the 8th International Conference on Computer Aided Verification, p.300-310, August 03, 1996
	14	Fong Pong , Michel Dubois, The verification of cache coherence protocols, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.11-20, June 30-July 02, 1993, Velen, Germany [doi>10.1145/165231.165233]
	15	W. C. Yen and W. L. Yen. Data coherence problem in a multicache system. IEEE Transactions on Computers, 34(1), January 1985.

CITED BY 8

	Rajnish Ghughal , Abdel Mokkedem , Ratan Nalumasu , Ganesh Gopalakrishnan, Using “test model-checking” to verify the Runway-PA8000 memory model, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.231-239, June 28-July 02, 1998, Puerto Vallarta, Mexico
	David Lie , Andy Chou , Dawson Engler , David L. Dill, A simple method for extracting models for protocol code, ACM SIGARCH Computer Architecture News, v.29 n.2, p.192-203, May 2001
	Andy Chou , Benjamin Chelf , Dawson Engler , Mark Heinrich, Using meta-level compilation to check FLASH protocol code, ACM SIGOPS Operating Systems Review, v.34 n.5, p.59-70, Dec. 2000
	Phillip B. Gibbons , John L. Bruno , Steven Phillips, Post-mortem black-box correctness tests for basic parallel data structures, Proceedings of the eleventh annual ACM symposium on Parallel algorithms and architectures, p.44-53, June 27-30, 1999, Saint Malo, France
	Manoj Plakal , Daniel J. Sorin , Anne E. Condon , Mark D. Hill, Lamport clocks: verifying a directory cache-coherence protocol, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.67-76, June 28-July 02, 1998, Puerto Vallarta, Mexico
	Andy Chou , Benjamin Chelf , Dawson Engler , Mark Heinrich, Using meta-level compilation to check FLASH protocol code, ACM SIGPLAN Notices, v.35 n.11, p.59-70, Nov. 2000
	Daniel J. Sorin , Manoj Plakal , Anne E. Condon , Mark D. Hill , Milo M. K. Martin , David A. Wood, Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol, IEEE Transactions on Parallel and Distributed Systems, v.13 n.6, p.556-578, June 2002
	Murali Talupur , Mark R. Tuttle, Going with the flow: parameterized verification using message flows, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon