{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,12]],"date-time":"2026-03-12T01:01:51Z","timestamp":1773277311942,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,12,5]],"date-time":"2015-12-05T00:00:00Z","timestamp":1449273600000},"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-1117147"],"award-info":[{"award-number":["CCF-1117147"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["HR0011-13-3-0002"],"award-info":[{"award-number":["HR0011-13-3-0002"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,12,5]]},"DOI":"10.1145\/2830772.2830782","type":"proceedings-article","created":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T13:38:13Z","timestamp":1452519493000},"page":"26-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["CCICheck"],"prefix":"10.1145","author":[{"given":"Yatin A.","family":"Manerkar","sequence":"first","affiliation":[{"name":"Princeton University"}]},{"given":"Daniel","family":"Lustig","sequence":"additional","affiliation":[{"name":"Princeton University"}]},{"given":"Michael","family":"Pellauer","sequence":"additional","affiliation":[{"name":"NVIDIA"}]},{"given":"Margaret","family":"Martonosi","sequence":"additional","affiliation":[{"name":"Princeton University"}]}],"member":"320","published-online":{"date-parts":[[2015,12,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2003.1199067"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/285930.285996"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0161-5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481839.1481842"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_25"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2627752"},{"key":"e_1_3_2_1_8_1","unstructured":"AMD \"Revision guide for AMD family 10h processors \" August 2011. {Online}. Available: http:\/\/developer.amd.com\/wordpress\/media\/2012\/10\/41322.pdf  AMD \"Revision guide for AMD family 10h processors \" August 2011. {Online}. Available: http:\/\/developer.amd.com\/wordpress\/media\/2012\/10\/41322.pdf"},{"key":"e_1_3_2_1_9_1","unstructured":"AMD \"AMD64 architecture programmer's manual \" 2013.  AMD \"AMD64 architecture programmer's manual \" 2013."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCA.2006.26"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.155"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.21"},{"key":"e_1_3_2_1_13_1","unstructured":"E. M. Clarke O. Grumberg H. Hiraishi S. Jha D. E. Long K. L. McMillan and L. A. Ness \"Verification of the futurebus+ cache coherence protocol \" in International Conference on Computer Hardware Description Languages and their Applications (CHDL) 1993 pp. 15--30.   E. M. Clarke O. Grumberg H. Hiraishi S. Jha D. E. Long K. L. McMillan and L. A. Ness \"Verification of the futurebus+ cache coherence protocol \" in International Conference on Computer Hardware Description Languages and their Applications (CHDL) 1993 pp. 15--30."},{"key":"e_1_3_2_1_15_1","unstructured":"Digital Equipment Corporation \"Alpha architecture reference manual \" 1992.   Digital Equipment Corporation \"Alpha architecture reference manual \" 1992."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"M. Dubois C. Scheurich and F. Briggs \"Memory access buffering in multiprocessors \" ISCA 1986.   M. Dubois C. Scheurich and F. Briggs \"Memory access buffering in multiprocessors \" ISCA 1986.","DOI":"10.1145\/17356.17406"},{"key":"e_1_3_2_1_17_1","unstructured":"M. Elver \"TSO-CC specification \" 2015. {Online}. Available: http:\/\/homepages.inf.ed.ac.uk\/s0787712\/res\/research\/tsocc\/tso-cc spec.pdf  M. Elver \"TSO-CC specification \" 2015. {Online}. Available: http:\/\/homepages.inf.ed.ac.uk\/s0787712\/res\/research\/tsocc\/tso-cc spec.pdf"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"M. Elver and V. Nagarajan \"TSO-CC: consistency directed cache coherence for TSO \" in HPCA 2014.  M. Elver and V. Nagarajan \"TSO-CC: consistency directed cache coherence for TSO \" in HPCA 2014.","DOI":"10.1109\/HPCA.2014.6835927"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2745404.2744921"},{"key":"e_1_3_2_1_20_1","unstructured":"K. Gharachorloo A. Gupta and J. Hennessy \"Two techniques to enhance the performance of memory consistency models \" International Conference on Parallel Processing (ICPP) 1991.  K. Gharachorloo A. Gupta and J. Hennessy \"Two techniques to enhance the performance of memory consistency models \" International Conference on Parallel Processing (ICPP) 1991."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/325164.325102"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"S. Hangal D. Vahia C. Manovit and J.-Y. J. Lu \"Tsotool: A program for verifying memory systems using the memory consistency model \" in ISCA 2004.   S. Hangal D. Vahia C. Manovit and J.-Y. J. Lu \"Tsotool: A program for verifying memory systems using the memory consistency model \" in ISCA 2004.","DOI":"10.1145\/1028176.1006710"},{"key":"e_1_3_2_1_24_1","unstructured":"Intel \"Intel Itanium architecture software developer's manual revision 2.3 \" 2010. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf  Intel \"Intel Itanium architecture software developer's manual revision 2.3 \" 2010. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf"},{"key":"e_1_3_2_1_25_1","unstructured":"Intel \"Intel 64 and IA-32 architectures software developer's manual \" 2013. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf  Intel \"Intel 64 and IA-32 architectures software developer's manual \" 2013. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/manuals\/64-ia-32-architectures-software-developer-manual-325462.pdf"},{"key":"e_1_3_2_1_26_1","unstructured":"Intel \"Intel Xeon processor E3-1200 v3 product family specification update \" April 2015. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/specification-updates\/xeon-e3-1200v3-specupdate.pdf  Intel \"Intel Xeon processor E3-1200 v3 product family specification update \" April 2015. {Online}. Available: http:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/documents\/specification-updates\/xeon-e3-1200v3-specupdate.pdf"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/224170.224398"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/143365.143540"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2014.38"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"D. Lustig M. Pellauer and M. Martonosi \"Verifying correct microarchitectural enforcement of memory consistency models \" IEEE Micro (Top Picks of 2014) vol. 35 no. 3 2015.  D. Lustig M. Pellauer and M. Martonosi \"Verifying correct microarchitectural enforcement of memory consistency models \" IEEE Micro (Top Picks of 2014) vol. 35 no. 3 2015.","DOI":"10.1109\/MM.2015.47"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_36"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.58"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"crossref","unstructured":"K. McMillan \"Parameterized verification of the FLASH cache coherence protocol by compositional model checking \" in Correct Hardware Design and Verification Methods (CHARME) 2001.   K. McMillan \"Parameterized verification of the FLASH cache coherence protocol by compositional model checking \" in Correct Hardware Design and Verification Methods (CHARME) 2001.","DOI":"10.1007\/3-540-44798-9_17"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.70243"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_27"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2370816.2370853"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993520"},{"key":"e_1_3_2_1_39_1","volume-title":"Ed. Morgan & Claypool Publishers","author":"Sorin D.","year":"2011"},{"key":"e_1_3_2_1_40_1","unstructured":"SPARC \"SPARC architecture manual version 9 \" 1994.   SPARC \"SPARC architecture manual version 9 \" 1994."},{"key":"e_1_3_2_1_41_1","volume-title":"LogiCal Project","year":"2004"},{"key":"e_1_3_2_1_42_1","unstructured":"The diy development team A don't (diy) tutorial version 5.01 2012. {Online}. Available: http:\/\/diy.inria.fr\/doc\/index.html  The diy development team A don't (diy) tutorial version 5.01 2012. {Online}. Available: http:\/\/diy.inria.fr\/doc\/index.html"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Y. Yang G. Gopalakrishnan G. Lindstrom and K. Slind \"Analyzing the Intel Itanium memory ordering rules using logic programming and SAT \" in Correct Hardware Design and Verification Methods (CHARME) 2003.  Y. Yang G. Gopalakrishnan G. Lindstrom and K. Slind \"Analyzing the Intel Itanium memory ordering rules using logic programming and SAT \" in Correct Hardware Design and Verification Methods (CHARME) 2003.","DOI":"10.1007\/978-3-540-39724-3_9"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"crossref","unstructured":"M. Zhang J. Bingham J. Erickson and D. Sorin \"PVCoherence: Designing at coherence protocols for scalable verification \" in HPCA 2014.  M. Zhang J. Bingham J. Erickson and D. Sorin \"PVCoherence: Designing at coherence protocols for scalable verification \" in HPCA 2014.","DOI":"10.1109\/HPCA.2014.6835949"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2010.11"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/L-CA.2010.18"}],"event":{"name":"MICRO-48: The 48th Annual IEEE\/ACM International Symposium of Microarchitecture","location":"Waikiki Hawaii","acronym":"MICRO-48","sponsor":["IEEE Computer Society TC-uARCH","SIGMICRO ACM Special Interest Group on Microarchitectural Research and Processing"]},"container-title":["Proceedings of the 48th International Symposium on Microarchitecture"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2830772.2830782","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2830772.2830782","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:39Z","timestamp":1750225719000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2830772.2830782"}},"subtitle":["using \u00b5hb graphs to verify the coherence-consistency interface"],"short-title":[],"issued":{"date-parts":[[2015,12,5]]},"references-count":44,"alternative-id":["10.1145\/2830772.2830782","10.1145\/2830772"],"URL":"https:\/\/doi.org\/10.1145\/2830772.2830782","relation":{},"subject":[],"published":{"date-parts":[[2015,12,5]]},"assertion":[{"value":"2015-12-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}