Proving sequential consistency of high-performance shared memories (extended abstract)

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Proving sequential consistency of high-performance shared memories (extended abstract)

Full text

Pdf (1.28 MB)

Source

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

Hilton Head, South Carolina, United States

Pages: 292 - 303

Year of Publication: 1991

ISBN:0-89791-438-4

Authors

Phillip B. Gibbons	AT&T Bell Laboratories, Murray Hill, NJ
Michael Merritt	AT&T Bell Laboratories, Murray Hill, NJ
Kourosh Gharachorloo	Stanford University, Stanford, CA

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): 2, Downloads (12 Months): 21, Citation Count: 30

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/113379.113406 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.

	ABM89	Y. Afek , G. Brown , M. Merritt, A lazy cache algorithm, Proceedings of the first annual ACM symposium on Parallel algorithms and architectures, p.209-222, June 18-21, 1989, Santa Fe, New Mexico, United States [doi>10.1145/72935.72958]
	AH90a	S.V. Adve and M. D. Hill. Implementing sequential consistency in cache-based systems. In 1990 International Conference on Parallel Processing, pages I47-I50, August 1990.
	AH90b	Sarita V. Adve , Mark D. Hill, Weak ordering—a new definition, Proceedings of the 17th annual international symposium on Computer Architecture, p.2-14, May 28-31, 1990, Seattle, Washington, United States
	AL88	M. Abadi and L. Lamport. The existence of refinement mappings. In Third Annual Symposium on Logic in Computer Science, pages 165-175, July 1988. Also available as a Digital Systems Research Center technical report.
	DS90	Michel Dubois , Christoph Scheurich, Memory Access Dependencies in Shared-Memory Multiprocessors, IEEE Transactions on Software Engineering, v.16 n.6, p.660-673, June 1990 [doi>10.1109/32.55094]
	DSB86	M. Dubois , C. Scheurich , F. Briggs, Memory access buffering in multiprocessors, Proceedings of the 13th annual international symposium on Computer architecture, p.434-442, June 02-05, 1986, Tokyo, Japan
	GG91	Kourosh Gharachorloo , Phillip B. Gibbons, Detecting violations of sequential consistency, Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.316-326, July 21-24, 1991, Hilton Head, South Carolina, United States [doi>10.1145/113379.113408]
	GGH91	Kourosh Gharachorloo , Anoop Gupta , John Hennessy, Performance evaluation of memory consistency models for shared-memory multiprocessors, Proceedings of the fourth international conference on Architectural support for programming languages and operating systems, p.245-257, April 08-11, 1991, Santa Clara, California, United States
	GLL+90	Kourosh Gharachorloo , Daniel Lenoski , James Laudon , Phillip Gibbons , Anoop Gupta , John Hennessy, Memory consistency and event ordering in scalable shared-memory multiprocessors, Proceedings of the 17th annual international symposium on Computer Architecture, p.15-26, May 28-31, 1990, Seattle, Washington, United States
	GMG91	P. B. Gibbons, M. Merritt, and K. Gharachorloo. Proving sequential consistency of high-performance shared memories. Technical report, ATL:T Bell Laboratories, May 1991. Full version.
	Goo89	J.R. Goodman. Cache consistency and sequential consistency. Technical report no. 61, SCI Committee, March 1989.
	HA90	P. Hutto and M. Ahamad. Slow memory: Weakening consistency to enhance concurrency in distributed memories. In l Olh Annual International Conference on Distributed Computing Systems, pages 302-309. IEEE Computer Society Press, 1990.
	HW87	M. P. Herlihy , J. M. Wing, Axioms for concurrent objects, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.13-26, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41627]
	Lam79	Leslie Lamport. How to make a multiprocessor that correctly executes multiprocess programs. IEEE Transactions on Computers, C-28:690-691, 1979.
	LLG+90	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
	LS88	R. Lipton and J. Sandberg. Pram: A scalable shared memory. Technical Report CS- TR-180-88, Princeton University, September 1988.
	LT87	Nancy A. Lynch , Mark R. Tuttle, Hierarchical correctness proofs for distributed algorithms, Proceedings of the sixth annual ACM Symposium on Principles of distributed computing, p.137-151, August 10-12, 1987, Vancouver, British Columbia, Canada [doi>10.1145/41840.41852]
	Lyn88	N. Lynch. I/O automata: A model for discrete event systems. In 22nd Annual Conference on Information Science and Systems. Princeton University, March 1988. Also MIT technical report number MIT/LCS/TM- 351.
	Mer90	M. Merritt, Completeness theorems for automata, Proceedings on Stepwise refinement of distributed systems: models, formalisms, correctness, p.544-560, May 1990, Mook, The Netherlands
	Mil80	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	SS88	Dennis Shasha , Marc Snir, Efficient and correct execution of parallel programs that share memory, ACM Transactions on Programming Languages and Systems (TOPLAS), v.10 n.2, p.282-312, April 1988 [doi>10.1145/42190.42277]

CITED BY 30

	John Howard , Shmuel Katz, Reconciliations, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.14-21, August 14-17, 1994, Los Angeles, California, United States
	Alan Fekete , M. Frans Kaashoek , Nancy Lynch, Implementing sequentially consistent shared objects using broadcast and point-to-point communication, Journal of the ACM (JACM), v.45 n.1, p.35-69, Jan. 1998
	Hagit Attiya , Jennifer L. Welch, Sequential consistency versus linearizability, ACM Transactions on Computer Systems (TOCS), v.12 n.2, p.91-122, May 1994
	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
	S. V. Adve , J. K. Aggarwal, A Unified Formalization of Four Shared-Memory Models, IEEE Transactions on Parallel and Distributed Systems, v.4 n.6, p.613-624, June 1993
	Phillip B. Gibbons , Michael Merritt, Specifying non-blocking shared memories (extended abstract), Proceedings of the fourth annual ACM symposium on Parallel algorithms and architectures, p.306-315, June 29-July 01, 1992, San Diego, California, United States
	Yehuda Afek , Geoffrey Brown , Michael Merritt, Lazy caching, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.1, p.182-205, Jan. 1993
	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
	Hagit Attiya , Roy Friedman, A correctness condition for high-performance multiprocessors (extended abstract), Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, p.679-690, May 04-06, 1992, Victoria, British Columbia, Canada
	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
	Roy Friedman, Implementing hybrid consistency with high-level synchronization operations, Proceedings of the twelfth annual ACM symposium on Principles of distributed computing, p.229-240, August 15-18, 1993, Ithaca, New York, United States
	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
	Mustaque Ahamad , Rida A. Bazzi , Ranjit John , Prince Kohli , Gil Neiger, The power of processor consistency, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.251-260, June 30-July 02, 1993, Velen, Germany
	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
	Hagit Attiya , Roy Friedman, Programming DEC-Alpha based multiprocessors the easy way (extended abstract), Proceedings of the sixth annual ACM symposium on Parallel algorithms and architectures, p.157-166, June 27-29, 1994, Cape May, New Jersey, United States
	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
	Fong Pong , Michel Dubois, Verification techniques for cache coherence protocols, ACM Computing Surveys (CSUR), v.29 n.1, p.82-126, March 1997
	Kourosh Gharachorloo , Phillip B. Gibbons, Detecting violations of sequential consistency, Proceedings of the third annual ACM symposium on Parallel algorithms and architectures, p.316-326, July 21-24, 1991, Hilton Head, South Carolina, United States
	Hagit Attiya , Soma Chaudhuri , Roy Friedman , Jennifer L. Welch, Shared memory consistency conditions for non-sequential execution: definitions and programming strategies, Proceedings of the fifth annual ACM symposium on Parallel algorithms and architectures, p.241-250, June 30-July 02, 1993, Velen, Germany
	Matteo Frigo , Victor Luchangco, Computation-centric memory models, Proceedings of the tenth annual ACM symposium on Parallel algorithms and architectures, p.240-249, June 28-July 02, 1998, Puerto Vallarta, Mexico
	Martha J. Kosa, Making operations of concurrent data types fast, Proceedings of the thirteenth annual ACM symposium on Principles of distributed computing, p.32-41, August 14-17, 1994, Los Angeles, California, United States
	Allon Adir , Hagit Attiya , Gil Shurek, Information-Flow Models for Shared Memory with an Application to the PowerPC Architecture, IEEE Transactions on Parallel and Distributed Systems, v.14 n.5, p.502-515, May 2003
	Jaehyuk Huh , Jichuan Chang , Doug Burger , Gurindar S. Sohi, Coherence decoupling: making use of incoherence, ACM SIGARCH Computer Architecture News, v.32 n.5, December 2004
	Seungjoon Park , David L. Dill, An Executable Specification and Verifier for Relaxed Memory Order, IEEE Transactions on Computers, v.48 n.2, p.227-235, February 1999
	Roy Friedman, Implementing hybrid consistency with high-level synchronization operations, Distributed Computing, v.9 n.3, p.119-129, December 1995
	Leslie Lamport, How to Make a Correct Multiprocess Program Execute Correctly on a Multiprocessor, IEEE Transactions on Computers, v.46 n.7, p.779-782, July 1997
	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
	M. Rasit Eskicioglu, A comprehensive bibliography of distributed shared memory, ACM SIGOPS Operating Systems Review, v.30 n.1, p.71-96, Jan. 1996
	Lisa Higham , Jalal Kawash, Implementing sequentially consistent programs on processor consistent platforms, Journal of Parallel and Distributed Computing, v.68 n.4, p.488-500, April, 2008
	Gérard Boudol , Gustavo Petri, Relaxed memory models: an operational approach, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA