{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:46:50Z","timestamp":1767926810722,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540417910","type":"print"},{"value":"9783540452515","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45251-6_4","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T01:53:28Z","timestamp":1186883608000},"page":"43-71","source":"Crossref","is-referenced-by-count":10,"title":["Proofs of Correctness of Cache-Coherence Protocols"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Stoy","sequence":"first","affiliation":[]},{"given":"Xiaowei","family":"Shen","sequence":"additional","affiliation":[]},{"family":"Arvind","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,16]]},"reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1145\/151646.151651","volume":"15","author":"Y. Afek","year":"1993","unstructured":"Yehuda Afek, Geoffrey Brown, and Michael Merritt. Lazy Caching. ACM Transactions on Programming Languages and Systems, 15(1):182\u2013205, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"[ADH+99]_Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark Tuttle, and Yuan Yu. Cache coherence verification with TLA+. In World Congress on Formal Methods in the Development of Computing Systems, Industrial Panel, Toulouse, France, September 1999.","DOI":"10.1007\/3-540-48118-4_62"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Sarita V. Adve and Kourosh Gharachorloo. Shared Memory Consistency Models: A Tutorial. IEEE Computer, pages 66\u201376, December 1996.","DOI":"10.1109\/2.546611"},{"key":"4_CR4","unstructured":"James K. Archibald. The Cache Coherence Problem in Shared-Memory Multiprocessors. PhD Dissertation, Department of Computer Science, University of Washington, February 1987."},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF01783663","volume":"4","author":"G. M. Brown","year":"1990","unstructured":"Geoffrey M. Brown. Asynchronous Multicaches. Distributed Computing, 4:31\u201336, 1990.","journal-title":"Distributed Computing"},{"issue":"2","key":"4_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR7","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. MIT Press, 1999."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Anne E. Condon, Mark D. Hill, Manoj Plakal, and Daniel J. Sorin. Using Lamport Clocks to Reason About Relaxed Memory Models. In Proceedings of the 5th International Symposium on High-Performance Computer Architecture, 1999.","DOI":"10.1109\/HPCA.1999.744379"},{"key":"4_CR9","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. A tutorial introduction to PVS. Presented at WIFT\u2019 95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. Available, with specification les, at http:\/\/www.csl.sri.com\/wift-tutorial.html ."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Giorgio Delzanno. Automatic Verification of Parameterized Cache Co-herence Protocols. Technical Report DISI-TR-00-1, DISI, University of Genoa, January 2000. Available at http:\/\/www.disi.unige.it\/person\/DelzannoG\/papers .","DOI":"10.1007\/10722167_8"},{"key":"4_CR11","unstructured":"Formal Systems (Europe) Limited. Fdr2. Web site. See http:\/\/www.formal.demon.co.uk\/FDR2.html ."},{"key":"4_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems","author":"T. A. Henzinger","year":"1999","unstructured":"Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. In Proceedings of the 11th International Conference on Computer-aided Verification (CAV), pages 301\u2013315. Springer-Verlag, 1999. Lecture Notes in Computer Science 1633."},{"key":"4_CR13","unstructured":"C.N. Ip and D.L. Dill. Better Verification Through Symmetry. In Proceedings of the 11th International Symposium on Computer Hardware Description Languages and Their Applications, pages 87\u2013100, April 1993."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"C.N. Ip and D.L. Dill. Efficient Verification of Symmetric Concurrent Systems. In International Conference on Computer Design: VLSI in Computers and Processors, October 1993.","DOI":"10.1109\/ICCD.1993.393375"},{"key":"4_CR15","unstructured":"[KPS93]David R. Kaeli, Nancy K. Perugini, and Janice M. Stone. Literature Survey of Memory Consistency Models. Research Report 18843 (k82385), IBM Research Devision, 1993."},{"key":"4_CR16","unstructured":"Leslie Lamport. How to write a proof. In Global Analysis in Modern Mathematics, pages 311\u2013321. Publish or Perish, Houston, Texas, U.S.A., February 1993. A symposium in honor of Richard Palais\u2019 sixtieth birthday."},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR18","unstructured":"Leslie Lamport. The Module Structure of TLA+. Technical Note 1996-002a, Compaq Systems Research Center, September 1996."},{"key":"4_CR19","unstructured":"Leslie Lamport. The Operators of TLA+. Technical Note 1997-006a, Compaq Systems Research Center, June 1997."},{"key":"4_CR20","unstructured":"Ranko Lazic. A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, Oxford University Computing Laboratory, 1999."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. PhD Dissertation, Carnegie Mellon University, May 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Fong Pong and Michel Dubois. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, 6, August 1995.","DOI":"10.1109\/71.406955"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Seungjoon Park and David L. Dill. Protocol Verification by Aggregation of Distributed Transactions. In International Conference on Computer-Aided Verification, July 1996.","DOI":"10.1007\/3-540-61474-5_78"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Seungjoon Park and David L. Dill. Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions. In Proceedings of the 8th ACM Symposium on Parallel Algorithms and Architectures, June 1996.","DOI":"10.1145\/237502.237573"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Fong Pong and Michel Dubois. Formal Verification of Delayed Consistency Protocols. In Proceedings of the 10th International Parallel Processing Symposium, April 1996.","DOI":"10.1109\/IPPS.1996.508048"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"[PNAD95]Fong Pong, Andreas Nowatzyk, Gunes Aybay, and Michel Dubois. Verifying Distributed Directory-based Cache Coherence Protocols: S3.mp, a Case Study. In Proceedings of the European Conference on Parallel Computing, 1995.","DOI":"10.1007\/BFb0020472"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Manoj Plakal, Daniel J. Sorin, Anne E. Condon, and Mark D. Hill. Lamport Clocks: Verifying a Directory Cache-Coherence Protocol. In Proceedings of the 10th ACM Symposium on Parallel Algorithms and Architectures, 1998.","DOI":"10.1145\/277651.277672"},{"key":"4_CR28","unstructured":"A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997."},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Xiaowei Shen, Arvind, and Larry Rodolph. CACHET: An Adaptive Cache Coherence Protocol for Distributed Shared-Memory Systems. In Proceedings of the 13th ACM International Conference on Supercomputing, June 1999.","DOI":"10.1145\/305138.305187"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Xiaowei Shen, Arvind, and Larry Rudolph. Commit-Reconcile & Fences (CRF): A New Memory Model for Architects and Compiler Writers. In Proceedings of the 26th International Symposium on Computer Architecture, May 1999.","DOI":"10.1145\/307338.300992"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Ulrich Stern and David L. Dill. Automatic Verification of the SCI Cache Coherence Protocol. In Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.","DOI":"10.1007\/3-540-60385-9_2"},{"key":"4_CR32","unstructured":"Xiaowei Shen. Design and Verification of Adaptive Cache Coherence Protocols. PhD thesis, Massachusetts Institute of Technology, February 2000."},{"key":"4_CR33","unstructured":"Joseph E. Stoy. Web sites concerning Cachet, TLA in PVS, and cache protocol verification using FDR. See http:\/\/web.comlab.ox.ac.uk\/oucl\/work\/joe.stoy\/ ."}],"container-title":["Lecture Notes in Computer Science","FME 2001: Formal Methods for Increasing Software Productivity"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45251-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T19:48:29Z","timestamp":1556740109000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45251-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417910","9783540452515"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-45251-6_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}