{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:52Z","timestamp":1725551272755},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540001164"},{"type":"electronic","value":"9783540361268"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36126-x_18","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:55:19Z","timestamp":1269899719000},"page":"292-309","source":"Crossref","is-referenced-by-count":1,"title":["A Specification and Verification Framework for Developing Weak Shared Memory Consistency Protocols"],"prefix":"10.1007","author":[{"given":"Prosenjit","family":"Chatterjee","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ganesh","family":"Gopalakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,11,5]]},"reference":[{"key":"18_CR1","unstructured":"The ASCI White Computer http:\/\/www.llnl.gov\/asci\/ ."},{"key":"18_CR2","unstructured":"The Sun MAJC Microarchitecture http:\/\/www.sun.com\/microelectronics\/MAJC\/ ."},{"key":"18_CR3","unstructured":"The IBM Power4 Microarchitecture http:\/\/www-1.ibm.com\/servers\/eserver\/pseries\/hardware\/whitepapers\/power4.html ."},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"L.A. Barroso, K. Gharachoroloo, R. McNamara, A. Nowatzyk, S. Qadeer, B. Sano, S. Smith, R. Stets, and B. Verghese, \u201cPiranha: A scalable architecture based on single-chip multiprocessing,\u201d in 27th International Symposium on Computer Architecture (ISCA), June 2000.","DOI":"10.1145\/339647.339696"},{"issue":"8","key":"18_CR5","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1109\/2.707614","volume":"31","author":"M. D. Hill","year":"1998","unstructured":"Mark D. Hill, \u201cMultiprocessors should support simple memory-consistency models,\u201d IEEE Computer, vol. 31, no. 8, pp. 28\u201334, 1998.","journal-title":"IEEE Computer"},{"key":"18_CR6","volume-title":"The SPARC Architecture Manual-Version 9","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":"18_CR7","unstructured":"Intel, The IA-64 Architecture Software Developer\u2019s Manual Vol. 2 rev. 1.1: Itanium (TM); System Architecture, Intel, 2000, Volume 2, Chapter 13, \u201cCoherence and MP Ordering.\u201d http:\/\/developer.intel.com\/design\/ia-64\/downloads\/24531802.htm ."},{"issue":"12","key":"18_CR8","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. V. Adve","year":"1996","unstructured":"Sarita V. Adve and Kourosh Gharachorloo, \u201cShared memory consistency models: A tutorial,\u201d Computer, vol. 29, no. 12, pp. 66\u201376, Dec. 1996.","journal-title":"Computer"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"M. Ahamad, R. A. Bazzi, R. John, P. Kohli, and G. Neiger, \u201cThe power of processor consistency (extended abstract),\u201d in Proc. of the 5th ACM Annual Symp. on Parallel Algorithms and Architectures (SPAA\u201993), June 1993, pp. 251\u2013260.","DOI":"10.1145\/165231.165264"},{"issue":"29","key":"18_CR10","first-page":"690","volume":"9","author":"L. Leslie","year":"1979","unstructured":"Leslie Lamport, \u201cHow to make a multiprocessor computer that correctly executes multiprocess programs,\u201d IEEE Transactions on Computers, vol. 9, no. 29, pp. 690\u2013691, 1979.","journal-title":"IEEE Transactions on Computers"},{"key":"18_CR11","unstructured":"Leslie Lamport, \u201cThe wildfire challenge problem,\u201d http:\/\/research.microsoft.com\/users\/lamport\/tla\/wildfire-challenge.html ."},{"key":"18_CR12","unstructured":"Gil Neiger, \u201c 2001, http:\/\/www.cs.utah.edu\/mpv\/papers\/neiger\/fmcad2001.pdf ."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"Anne Condon, Mark Hill, Manoj Plakal, and David Sorin, \u201dUsing lamport clocks to reason about relaxed memory models,\u201c in Proceedings of the Fifth International Symposium On High Performance Computer Architecture (HPCA-5), Jan. 1999.","DOI":"10.1109\/HPCA.1999.744379"},{"issue":"2","key":"18_CR14","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport, \u201cThe existence of refinement mappings,\u201d Theoretical Computer Science, vol. 82, no. 2, pp. 253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Rajeev Alur, Ken McMillan, and Doron Peled, \u201cModel-checking of correctness conditions for concurrent objects,\u201d in 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, July 1996, pp. 219\u2013228.","DOI":"10.1109\/LICS.1996.561322"},{"key":"18_CR16","unstructured":"Hemanthkumar Sivaraj, \u201cParallel and distributed model checking,\u201d M.S. thesis, School of Computing, University of Utah, 2002, In progress."},{"issue":"2","key":"18_CR17","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, \u201cParallelizing the Vlunp verifier,\u201d Formal Methods in System Design, vol. 18, no. 2, pp. 117\u2013129, 2001, (Journal version of their CAV 1997 paper).","journal-title":"Formal Methods in System Design"},{"key":"18_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BFb0028767","volume-title":"Computer Aided Verification98","author":"R. Nalumasu","year":"1998","unstructured":"Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, \u201cThe \u2018test model-checking\u2019 approach to the verification of formal memory models of multiprocessors,\u201d in Computer Aided Verification98, Alan J. Hu and Moshe Y. Vardi, Eds., Vancouver, BC, Canada, June\/July 1998, vol. 1427 of Lecture Notes in Computer Science, pp. 464\u2013476, Springer-Verlag."},{"key":"18_CR19","unstructured":"Seungjoon Park, Computer Assisted Analysis of Multiprocessor Memory Systems, Ph.D. thesis, Stanford University, jun 1996, Department of Computer Science."},{"key":"18_CR20","unstructured":"Prosenjit Chatterjee, \u201d Tool available at http:\/\/www.cs.utah.edu\/formalverification\/ESGtool ."},{"issue":"5","key":"18_CR21","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann, \u201cThe model checker spin,\u201d IEEE Transactions on Software Engineering, vol. 23, no. 5, pp. 279\u2013295, May 1997, Special issue on Formal Methods in Software Practice.","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"7","key":"18_CR22","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Leslie Lamport, \u201cTime, clocks, and the ordering of events in a distributed program,\u201d Communications of the ACM, vol. 21, no. 7, pp. 558\u2013565, 1978.","journal-title":"Communications of the ACM"},{"key":"18_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"1871","DOI":"10.1007\/3-540-48118-4_62","volume-title":"World Congress on Formal Methods","author":"H. Akhiani","year":"1999","unstructured":"Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark Tuttle, and Yuan Yu, \u201cCache coherence verification with tla+,\u201d in World Congress on Formal Methods, 1999, vol. LNCS 1709, pp. 1871\u20131872."},{"key":"18_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"Computer Aided Verification99","author":"T. Henzinger","year":"1999","unstructured":"Thomas Henzinger, Shaz Qadeer, and Sriram Rajamani, \u201cVerifying sequential consistency on shared-memory multiprocessor systems,\u201d in Computer Aided Verification99, Nicolas Halbwachs and Doron Peled, Eds., Trento, Italy, July 1999, vol. 1633 of Lecture Notes in Computer Science, pp. 301\u2013315, Springer-Verlag."},{"key":"18_CR25","unstructured":"Shaz Qadeer, \u201dVerifying sequential consistency on shared-memory multiprocessors by model checking,\u201c Tech. Rep., SRC, Dec. 2001, Research Report 176."},{"issue":"12","key":"18_CR26","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s004460050056","volume":"12","author":"M. Merritt","year":"1999","unstructured":"Michael Merritt, \u201cGuest editorial: Special issue on shared memory systems,\u201d Distributed Computing, vol. 12, no. 12, pp. 55\u201356, 1999.","journal-title":"Distributed Computing"},{"key":"18_CR27","unstructured":"Jason F. Cantin, Mikko H. Lipasti, and James E. Smith, \u201cDynamic verification of cache coherence protocol,\u201d in Workshop on Memory Performance Issues, in conjunction with ISCA, June 2001."},{"key":"18_CR28","volume-title":"Reasoning About Parallel Architectures","author":"W. W. Collier","year":"1992","unstructured":"W. W. Collier, Reasoning About Parallel Architectures, Prentice-Hall, Englewood Cliffs, NJ, 1992."},{"key":"18_CR29","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1007\/3-540-45591-4_135","volume-title":"Proc. of the workshop FMPPTA (Formal Methods for Parallel Programming: Theory and Applications), Cancun, Mexico","author":"R. Ghughal","year":"2000","unstructured":"Rajnish Ghughal and Ganesh Gopalakrishnan, \u201cVerification methods for weaker shared memory consistency models,\u201d in Proc. of the workshop FMPPTA (Formal Methods for Parallel Programming: Theory and Applications), Cancun, Mexico. LNCS # 1800, Jos\u00e9 Rolim et al., Ed., May 2000, pp. 985\u2013992."},{"key":"18_CR30","unstructured":"Rajnish Ghughal, \u201cTest model-checking approach to verification of formal memory models,\u201d M.S. thesis, Department of Computer Science, University of Utah, 1999, Also available from http:\/\/www.cs.utah.edu\/formal_verification ."},{"key":"18_CR31","unstructured":"Christoph Scheurich, Access Ordering and Coherence in Shared Memory Multiprocessors, Ph.D. thesis, University of Southern California, May 1989."},{"key":"18_CR32","volume-title":"Tech. Rep. #1412","author":"D. Sorin","year":"2000","unstructured":"D. Sorin, M. Plakal, A. E. Condon, M. D. Hill, M. M. Martin, and D. A. Wood, \u201cSpecifying and verifying a broadcast and a multicast snooping cache coherence protocol,\u201d Tech. Rep. #1412, Computer Sciences Department, U. Wisconsin, Madison, Mar. 2000."},{"key":"18_CR33","unstructured":"Prosenjit Chatterjee, \u201cFormal specification and verification of memory consistency models of shared memory multiprocessors,\u201d M.S. thesis, Department of Computer Science, University of Utah, 2002, Also available from http:\/\/www.cs.utah.edu\/formal_verification"},{"key":"18_CR34","unstructured":"Leslie Lamport, \u201cHow to make a correct multiprocess program execute correctly on a multiprocessor,\u201d Tech. Rep., Digital Equipment Corporation, Systems Research Center, Feb. 1993."},{"key":"18_CR35","unstructured":"Richard L. Sites, Alpha Architecture Reference Manual, Digital Press, 1992."},{"key":"18_CR36","doi-asserted-by":"crossref","unstructured":"K. Gharachorloo, D. E. Lenoski, J. Laudon, P. Gibbons, A. Gupta, and J. L. Hennessy, \u201cMemory consistency and event ordering in scalable shared-memory multiprocessors,\u201d in Proc. of the 17th Annual Int\u2019l Symp. on Computer Architecture (ISCA\u201990), May 1990, pp. 15\u201326.","DOI":"10.1145\/325164.325102"},{"key":"18_CR37","unstructured":"R. J. Lipton and J. S. Sandberg, \u201cPram: A scalable shared memory,\u201d Tech. Rep. CS-TR-180-88, Dept. of Computer Science, Princeton University, Sept. 1988."},{"key":"18_CR38","doi-asserted-by":"crossref","unstructured":"P. W. Hutto and M. Ahamad, \u201cSlow memory: Weakening consistency to enhance concurrency in distributed shared memories,\u201d in Proc. of the 10th Int\u2019l Conf. on Distributed Computing Systems (ICDCS-10), May 1990, pp. 302\u2013311.","DOI":"10.1109\/ICDCS.1990.89297"},{"key":"18_CR39","doi-asserted-by":"crossref","unstructured":"Prosenjit Chatterjee and Ganesh Gopalakrishnan, \u201cTowards a formal model of shared memory consistency for intel itanium,\u201d in International Conference on Computer Aided Design, Austin, USA, 2001.","DOI":"10.1109\/ICCD.2001.955081"},{"key":"18_CR40","unstructured":"A. Singhal, D. Broniarczyk, F Cerauskis, J. Price, L. Yuan, C. Cheng, D. Doblar, S. Fosth, N. Agarwal, K. Harvey, E. Hangersten, and B. Liencres, \u201cGigaplane: A high performance bus for large smps,\u201d in Proc. of the 4th Annual Symposium on High Performance Interconnects at Stanford University, 1996, pp. 41\u201352."},{"key":"18_CR41","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BFb0028767","volume-title":"Computer Aided Verification","author":"R. Nalumasu","year":"1998","unstructured":"Ratan Nalumasu, Rajnish Ghughal, Abdel Mokkedem, and Ganesh Gopalakrishnan, \u201cThe \u2018test model-checking\u2019 approach to the verification of formal memory models of multiprocessors,\u201d in Computer Aided Verification, Alan J. Hu and Moshe Y. Vardi, Eds., Vancouver, BC, Canada, June 1998, vol. 1427 of Lecture Notes in Computer Science, pp. 464\u2013476, Springer-Verlag."},{"key":"18_CR42","unstructured":"http:\/\/www.cs.utah.edu\/~prosen\/fmcad02.html ."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36126-X_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:26:58Z","timestamp":1558985218000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36126-X_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540001164","9783540361268"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/3-540-36126-x_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}