{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:22:33Z","timestamp":1742397753640},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_10","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"123-136","source":"Crossref","is-referenced-by-count":14,"title":["Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking"],"prefix":"10.1007","author":[{"given":"Prosenjit","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Hemanthkumar","family":"Sivaraj","sequence":"additional","affiliation":[]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Sarita V. Adve and Kourosh Gharachorloo. Shared memory consistency models: A tutorial. Computer, 29(12):66\u201376, December 1996.","DOI":"10.1109\/2.546611"},{"key":"10_CR2","unstructured":"http:\/\/research.microsoft.com\/users\/lamport\/tla\/wildfire-challenge.html\n                    \n                  ."},{"key":"10_CR3","unstructured":"Gil Neiger, 2001. \n                    http:\/\/www.cs.utah.edu\/mpv\/papers\/neiger\/fmcad2001.pdf\n                    \n                  ."},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Prosenjit Chatterjee and Ganesh Gopalakrishnan. Towards a formal model of shared memory consistency for intel itanium. In ICCD, pages 515\u2013518, 2001.","DOI":"10.1109\/ICCD.2001.955081"},{"key":"10_CR5","unstructured":"Mpv: Workshop on specification and verification of shared memory systems, 2001. \n                    http:\/\/www.cs.utah.edu\/mpv\/\n                    \n                  ."},{"key":"10_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"CAV","author":"T. Henzinger","year":"1999","unstructured":"Thomas Henzinger, Shaz Qadeer, and Sriram Rajamani. Verifying sequential consistency on shared-memory multiprocessor systems. In CAV, LNCS 1633, pages 301\u2013315, 1999."},{"key":"10_CR7","unstructured":"Shaz Qadeer. Verifying sequential consistency on shared-memory multiprocessors by model checking. Technical report, SRC, December 2001. Research Report 176."},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Anne Condon and Alan J. Hu. Automatable verification of sequential consistency. In Symposium on Parallel Algorithms and Architectures (SPAA), July 2001.","DOI":"10.1145\/378580.378604"},{"issue":"12","key":"10_CR9","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s004460050056","volume":"12","author":"M. Merritt","year":"1999","unstructured":"Michael Merritt. Guest editorial: Special issue on shared memory systems. Distributed Computing, 12(12): 55\u201356, 1999.","journal-title":"Distributed Computing"},{"key":"10_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/BFb0028767","volume-title":"CAV","author":"R. Nalumasu","year":"1998","unstructured":"Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan. The \u2018test model-checking\u2019 approach to the verification of formal memory models of multiprocessors. In CAV, LNCS 1427, pages 464\u2013476, 1998."},{"key":"10_CR11","volume-title":"Technical Report #1412","author":"D. Sorin","year":"2000","unstructured":"D. Sorin et.al. Specifying and verifying a broadcast and a multicast snooping cache coherence protocol. Technical Report #1412, CS Department, U. Wisconsin, Madison, March 2000."},{"key":"10_CR12","unstructured":"Seungjoon Park. Computer Assisted Analysis of Multiprocessor Memory Systems. PhD thesis, Stanford University, jun 1996. Department of Computer Science."},{"key":"10_CR13","volume-title":"The SPARC Architecture Manual-Version","author":"D. L. Weaver","year":"1994","unstructured":"David L. Weaver and Tom Germond. The SPARC Architecture Manual-Version 9. P T R, Prentice-Hall, Englewood Cliffs, NJ 07632, USA, 1994."},{"key":"10_CR14","unstructured":"Prosenjit Chatterjee. Formal specification and verification of memory consistency models of shared memory multiprocessors. Master\u2019s thesis, Univ Utah, School of Computing, 2002."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Anne Condon, Mark Hill, Manoj Plakal, and David Sorin. Using lamport clocks to reason about relaxed memory models. In Proceedings of HPCA-5, January 1999.","DOI":"10.1109\/HPCA.1999.744379"},{"key":"10_CR16","unstructured":"A. Singhal et.al. Gigaplane: A high performance bus for large smps. In Proc. 4th Annual Symp on High Performance Interconnects, Stanford University, pages 41\u201352, 1996."},{"key":"10_CR17","unstructured":"The Ultra Enterprise 10000 Server, \n                    http:\/\/www.sun.com\/servers\/highend\/10000\/"},{"issue":"2","key":"10_CR18","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1008771324652","volume":"18","author":"U. Stern","year":"2001","unstructured":"Ulrich Stern and David Dill. Parallelizing the Muro verifier. Formal Methods in System Design, 18(2):117\u2013129, 2001. (Journal version of their CAV 1997 paper).","journal-title":"Formal Methods in System Design"},{"key":"10_CR19","volume-title":"About Parallel Architectures","author":"W. W. Collier","year":"1992","unstructured":"W. W. Collier. Reasoning About Parallel Architectures. Prentice-Hall, Englewood Cliffs, NJ, 1992."},{"key":"10_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1007\/3-540-45591-4_135","volume-title":"Proc. FMPPTA","author":"R. Ghughal","year":"2000","unstructured":"Rajnish Ghughal and Ganesh Gopalakrishnann. Verification methods for weaker shared memory consistency models. In Jose Rolim et al. (Eds.), editor, Proc. FMPPTA, pages 985\u2013992, May 2000. LNCS 1800."},{"key":"10_CR21","unstructured":"Jason F. Cantin, Mikko H. Lipasti, and James E. Smith. Dynamic verification of cache coherence protocol. In ?, June 2001. Workshop on Memory Performance Issues, in conjunction with ISCA."},{"key":"10_CR22","unstructured":"David L. Dill, Seungjoon Park, and Andreas Nowatzyk. Formal specification of abstract memory models. In Gaetano Borriello and Carl Ebeling, editors, Research on Integrated Systems, pages 38\u201352. MIT Press, 1993."},{"key":"10_CR23","unstructured":"P. Ladkin, L. Lamport, B. Olivier, and D. Roegel. Lazy caching in TLA. Distributed Computing, 1997."},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Jeremy Manson and William Pugh. Core semantics of multithreaded Java. In ACM Java Grande Conference, June 2001.","DOI":"10.1145\/376656.376806"},{"key":"10_CR25","unstructured":"Yue Yang, Ganesh Gopalakrishnan, and Gary Lindstrom. Formalizing the java memory model for multithreaded program correctness and optimization. Technical Report UUCS-02-011, University of Utah, School of Computing, 2002. Also at \n                    http:\/\/www.cs.utah.edu\/-yyang\/research\n                    \n                  ."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T19:36:18Z","timestamp":1550345778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}