The verification of cache coherence protocols

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The verification of cache coherence protocols

Full text

Pdf (1.05 MB)

Source

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

Velen, Germany

Pages: 11 - 20

Year of Publication: 1993

ISBN:0-89791-599-2

Authors

Fong Pong
Michel Dubois

Sponsors

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
SIGARCH: ACM Special Interest Group on Computer Architecture
European Comp Soc : European Computer Society

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 15, Citation Count: 6

Additional Information:

references cited by index terms collaborative colleagues peer to peer

Tools and Actions:	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/165231.165233 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, Cache coherence protocols: evaluation using a multiprocessor simulation model, ACM Transactions on Computer Systems (TOCS), v.4 n.4, p.273-298, Nov. 1986 [doi>10.1145/6513.6514]
	2	J.-L. Baer and C. Girault "A Petri Net Model for a Solution to the Cache Coherence Problem "'Proc. of the 1st Conf. on Supercomputing Systems, 1985, pp. 680-689.
	3	G.V. Bochmann "Combining Assertions and States For the Validation of Process Communication ", Proc. of the IFIP, 1978.
	4	G.V. Bochmann and J. Gecsei "A Unified Method for the Specification and Verification of Protocols ", Proc. of the IFIP, 1977, Toronto.
	5	G.V. Bochmann and C.A. Sunshine "Formal Methods in Communication Protocol Design ", IEEE Trans. on Communications, Vol. COM-28, No. 4, Apr. 1980, pp. 624-631.
	6	L.M. Censier and P. Feautrier "A new solution to coherence problems in multicache systems "', IEEE Trans. on Comp., C-27.12, Dec. 1978, pp. 1112-1118.
	7	Yoshiaki Kakuda , Yasushi Wakahara , Masamitsu Norigoe, An Acyclic Expansion Algorithm for Fast Protocol Validation, IEEE Transactions on Software Engineering, v.14 n.8, p.1059-1070, August 1988 [doi>10.1109/32.7616 ]
	8	G.J. Holzmann "Algorithms for Automated Protocol Verification ", AT#&T Technical Journal, Jan./Feb., 1990.
	9	K.L. McMillan and J. Schwalbe "Formal Verification of the Gigamax Cache Consistency Protocol ", Proc. of the ISSM lnt' l Conf. on Par. and Dist. Comp., Oct. 1991.
	10	Katie Tarnay, Protocol Specification and Testing, Perseus Publishing, 1991
	11	P. Zaftropulo, C.H. West, H.Rudin, et al. "Towards Analyzing and Synthesizing Protocols ", IEEE Trans. on Communications, Vol. COM-28, No. 4, Apr. 1980, pp. 651- 660.
	12	E Pong and M. Dubois, "'The Verification of Cache Coherence Protocols," U.S.C. Tech. Rep. CENG-92-20, Nov. 1992.
	13	R. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	14	E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
	15	Larry Rudolph , Zary Segall, Dynamic decentralized cache schemes for mimd parallel processors, Proceedings of the 11th annual international symposium on Computer architecture, p.340-347, January 1984
	16	A.K. Nanda and L. N. Bhuyan "A Formal Specification and Verification Technique for Cache Coherence Protocols ", Proc. of the 1992 Int. Conf. on Par. Proc., pp. 1-22-I- 26.

CITED BY 6

	Seungjoon Park , David L. Dill, Verification of FLASH cache coherence protocol by aggregation of distributed transactions, Proceedings of the eighth annual ACM symposium on Parallel algorithms and architectures, p.288-296, June 24-26, 1996, Padua, Italy
	Fong Pong , Michel Dubois, Formal verification of complex coherence protocols using symbolic state models, Journal of the ACM (JACM), v.45 n.4, p.557-587, July 1998
	Fong Pong , Michel Dubois, A New Approach for the Verification of Cache Coherence Protocols, IEEE Transactions on Parallel and Distributed Systems, v.6 n.8, p.773-787, August 1995
	Phillip B. Gibbons , Ephraim Korach, On testing cache-coherent shared memories, Proceedings of the sixth annual ACM symposium on Parallel algorithms and architectures, p.177-188, June 27-29, 1994, Cape May, New Jersey, United States
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999