{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:08:18Z","timestamp":1750306098772,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,14]],"date-time":"2017-10-14T00:00:00Z","timestamp":1507939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-142-1167"],"award-info":[{"award-number":["CCF-142-1167"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,14]]},"DOI":"10.1145\/3123939.3123971","type":"proceedings-article","created":{"date-parts":[[2017,11,20]],"date-time":"2017-11-20T14:31:12Z","timestamp":1511188272000},"page":"477-489","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Architecting hierarchical coherence protocols for push-button parametric verification"],"prefix":"10.1145","author":[{"given":"Opeoluwa","family":"Matthews","sequence":"first","affiliation":[{"name":"Duke University and University of Michigan"}]},{"given":"Daniel J.","family":"Sorin","sequence":"additional","affiliation":[{"name":"Duke University"}]}],"member":"320","published-online":{"date-parts":[[2017,10,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"International Symposium On High Performance Computer Architecture (HPCA).","author":"Alameldeen Alaa R","year":"2003","unstructured":"Alaa R Alameldeen and David A Wood . 2003 . Variability in architectural simulations of multi-threaded workloads . In International Symposium On High Performance Computer Architecture (HPCA). Alaa R Alameldeen and David A Wood. 2003. Variability in architectural simulations of multi-threaded workloads. In International Symposium On High Performance Computer Architecture (HPCA)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_2"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/339647.339696"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2013.6522350"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2155620.2155647"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1454115.1454128"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2024716.2024718"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/582034.582041"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30494-4_27"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679392"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_55"},{"key":"e_1_3_2_1_13_1","unstructured":"Sylvain Conchon Amit Goel Sava Krstic Alain Mebsout and Fatiha Za\u00c4\u015bdi. 2012. German's Protocol http:\/\/cubicle.lri.fr\/examples\/german.ctc.cub.html.  Sylvain Conchon Amit Goel Sava Krstic Alain Mebsout and Fatiha Za\u00c4\u015bdi. 2012. German's Protocol http:\/\/cubicle.lri.fr\/examples\/german.ctc.cub.html."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2010.31"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/645461.654859"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_3"},{"key":"e_1_3_2_1_17_1","first-page":"2","article-title":"The Intel Pentium M Processor: Microarchitecture and Performance","volume":"7","author":"Gochman Simcha","year":"2003","unstructured":"Simcha Gochman , Ronny Ronen , Ittai Anati , Ariel Berkovits , Tsvika Kurts , Alon Naveh , Ali Saeed , Zeev Sperber , and Robert C Valentine . 2003 . The Intel Pentium M Processor: Microarchitecture and Performance . Intel Technology Journal 7 , 2 . Simcha Gochman, Ronny Ronen, Ittai Anati, Ariel Berkovits, Tsvika Kurts, Alon Naveh, Ali Saeed, Zeev Sperber, and Robert C Valentine. 2003. The Intel Pentium M Processor: Microarchitecture and Performance. Intel Technology Journal 7, 2.","journal-title":"Intel Technology Journal"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088149.1088181"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/520549.822785"},{"key":"e_1_3_2_1_20_1","unstructured":"Glenn Hinton Dave Sager Mike Upton Darrell Boggs Doug Carmean Alan Kyker and Patrice Roussel. 2001. The microarchitecture of the Pentium\u00ae 4 processor. In Intel Technology Journal.  Glenn Hinton Dave Sager Mike Upton Darrell Boggs Doug Carmean Alan Kyker and Patrice Roussel. 2001. The microarchitecture of the Pentium\u00ae 4 processor. In Intel Technology Journal."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1378533.1378536"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.121510"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2209249.2209269"},{"key":"e_1_3_2_1_24_1","volume-title":"Verifiable Hierarchical Protocols with Network Invariants on Parametric Systems. In International Conference on Formal Methods in Computer-Aided Design (FMCAD).","author":"Matthews Opeoluwa","year":"2016","unstructured":"Opeoluwa Matthews , Jesse Bingham , and Daniel Sorin . 2016 . Verifiable Hierarchical Protocols with Network Invariants on Parametric Systems. In International Conference on Formal Methods in Computer-Aided Design (FMCAD). Opeoluwa Matthews, Jesse Bingham, and Daniel Sorin. 2016. Verifiable Hierarchical Protocols with Network Invariants on Parametric Systems. In International Conference on Formal Methods in Computer-Aided Design (FMCAD)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2014.6835967"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/43.875327"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA.2015.7056032"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1399504.1360617"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1148882.1148884"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-031-01733-9","volume-title":"A primer on memory consistency and cache coherence. Synthesis Lectures on Computer Architecture","author":"Sorin Daniel J","year":"2011","unstructured":"Daniel J Sorin , Mark D Hill , and David A Wood . 2011. A primer on memory consistency and cache coherence. Synthesis Lectures on Computer Architecture ( 2011 ). Daniel J Sorin, Mark D Hill, and David A Wood. 2011. A primer on memory consistency and cache coherence. Synthesis Lectures on Computer Architecture (2011)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2596669"},{"volume-title":"Going with the Flow: Parameterized Verification Using Message Flows. In International Conference on Formal Methods in Computer-Aided Design (FMCAD).","author":"Talupur Murali","key":"e_1_3_2_1_32_1","unstructured":"Murali Talupur and Mark R. Tuttle . 2008 . Going with the Flow: Parameterized Verification Using Message Flows. In International Conference on Formal Methods in Computer-Aided Design (FMCAD). Murali Talupur and Mark R. Tuttle. 2008. Going with the Flow: Parameterized Verification Using Message Flows. In International Conference on Formal Methods in Computer-Aided Design (FMCAD)."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1147\/rd.461.0005"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/2665671.2665733"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541982"},{"key":"e_1_3_2_1_38_1","unstructured":"Deborah A Wallach. 1992. PHD: A hierarchical cache coherent protocol. Ph.D. Dissertation. Massachusetts Institute of Technology.  Deborah A Wallach. 1992. PHD: A hierarchical cache coherent protocol. Ph.D. Dissertation. Massachusetts Institute of Technology."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/30350.30378"},{"volume-title":"International Symposium On High Performance Computer Architecture (HPCA).","author":"Zhang Meng","key":"e_1_3_2_1_40_1","unstructured":"Meng Zhang , Jesse D. Bingham , John Erickson , and Daniel J. Sorin . 2014. PVCoherence: Designing flat coherence protocols for scalable verification . In International Symposium On High Performance Computer Architecture (HPCA). Meng Zhang, Jesse D. Bingham, John Erickson, and Daniel J. Sorin. 2014. PVCoherence: Designing flat coherence protocols for scalable verification. In International Symposium On High Performance Computer Architecture (HPCA)."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2010.11"}],"event":{"name":"MICRO-50: The 50th Annual IEEE\/ACM International Symposium on Microarchitecture","sponsor":["SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing","IEEE-CS\\DATC IEEE Computer Society"],"location":"Cambridge Massachusetts","acronym":"MICRO-50"},"container-title":["Proceedings of the 50th Annual IEEE\/ACM International Symposium on Microarchitecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3123939.3123971","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3123939.3123971","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3123939.3123971","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:31Z","timestamp":1750217431000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3123939.3123971"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10,14]]},"references-count":39,"alternative-id":["10.1145\/3123939.3123971","10.1145\/3123939"],"URL":"https:\/\/doi.org\/10.1145\/3123939.3123971","relation":{},"subject":[],"published":{"date-parts":[[2017,10,14]]},"assertion":[{"value":"2017-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}