{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:49Z","timestamp":1767927829416,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Cache-coherence protocols have been one of the greatest challenges in formal verification of hardware, due to their central complication of executing multiple memory-access transactions concurrently within a distributed message-passing system. In this paper, we introduce Hemiola, a framework embedded in Coq that guides the user to design protocols that never experience inconsistent interleavings while handling transactions concurrently. The framework provides a DSL, where any protocol designed in the DSL always satisfies the serializability property, allowing a user to verify the protocol assuming that transactions are executed one-at-a-time. Hemiola also provides a novel invariant proof method, for protocols designed in Hemiola, that only requires considering execution histories without interleaved memory accesses. We used Hemiola to design and prove hierarchical MSI and MESI protocols as case studies. We also demonstrated that the case-study protocols are hardware-synthesizable, by using a compilation\/synthesis toolchain targeting FPGAs.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_16","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"317-339","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Hemiola: A DSL and\u00a0Verification Tools to\u00a0Guide Design and\u00a0Proof of\u00a0Hierarchical Cache-Coherence Protocols"],"prefix":"10.1007","author":[{"given":"Joonwon","family":"Choi","sequence":"first","affiliation":[]},{"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[]},{"family":"Arvind","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"16_CR1","unstructured":"7 Series FPGAs Configurable Logic Block - User Guide, September 2016. https:\/\/www.xilinx.com\/support\/documentation\/user_guides\/ug474_7Series_CLB.pdf"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Banks, C.J., Elver, M., Hoffmann, R., Sarkar, S., Jackson, P., Nagarajan, V.: Verification of a lazy cache coherence protocol against a weak memory model. In: FMCAD 2017, Austin, TX, pp. 60\u201367 (2017) http:\/\/dl.acm.org\/citation.cfm?id=3168451.3168470","DOI":"10.23919\/FMCAD.2017.8102242"},{"key":"16_CR3","unstructured":"Bernstein, P.A., Hadzilacos, V., Goodman, N.: Concurrency Control and Recovery in Database Systems. Addison-Wesley Longman Publishing Co., Inc. (1987)"},{"key":"16_CR4","doi-asserted-by":"publisher","unstructured":"Bourgeat, T., Pit-Claudel, C., Chlipala, A., Arvind: The essence of Bluespec: a core language for rule-based hardware design. In: PLDI, New York, NY, USA, pp. 243\u2013257 (2020). https:\/\/doi.org\/10.1145\/3385412.3385965","DOI":"10.1145\/3385412.3385965"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/978-3-642-39799-8_14","volume-title":"Computer Aided Verification","author":"T Braibant","year":"2013","unstructured":"Braibant, T., Chlipala, A.: Formal verification of hardware synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 213\u2013228. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_14"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/BFb0036900","volume-title":"Automata, Languages and Programming","author":"SD Brookes","year":"1983","unstructured":"Brookes, S.D., Rounds, W.C.: Behavioural equivalence relations induced by programming logics. In: Diaz, J. (ed.) ICALP 1983. LNCS, vol. 154, pp. 97\u2013108. Springer, Heidelberg (1983). https:\/\/doi.org\/10.1007\/BFb0036900"},{"key":"16_CR7","unstructured":"Chen, X.: Verification of hierarchical cache coherence protocols for futuristic processors. Ph.D. thesis, USA (2008)"},{"issue":"1","key":"16_CR8","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s10703-010-0092-y","volume":"36","author":"X Chen","year":"2010","unstructured":"Chen, X., Yang, Y., Gopalakrishnan, G., Chou, C.T.: Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols. Form. Methods Syst. Des. 36(1), 37\u201364 (2010). https:\/\/doi.org\/10.1007\/s10703-010-0092-y","journal-title":"Form. Methods Syst. Des."},{"key":"16_CR9","unstructured":"Choi, J.: Structural design and proof of hierarchical cache-coherence protocols. Ph.D. thesis (2021). https:\/\/hdl.handle.net\/1721.1\/130759"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Choi, J., Vijayaraghavan, M., Sherman, B., Chlipala, A., Arvind: Kami: a platform for high-level parametric hardware specification and its modular verification. In: Proc. ACM Program. Lang. 1(ICFP), 24:1\u201324:30 (2017). https:\/\/doi.org\/10.1145\/3110268","DOI":"10.1145\/3110268"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C-T Chou","year":"2004","unstructured":"Chou, C.-T., Mannava, P.K., Park, S.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 382\u2013398. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_27"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"DL Dill","year":"1996","unstructured":"Dill, D.L.: The Mur $$\\phi $$ verification system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 390\u2013393. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_86"},{"issue":"2","key":"16_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1023\/A:1022969405325","volume":"22","author":"R Joshi","year":"2003","unstructured":"Joshi, R., Lamport, L., Matthews, J., Tasiran, S., Tuttle, M., Yu, Y.: Checking cache-coherence protocols with TLA+. Form. Methods Syst. Des. 22(2), 125\u2013131 (2003). https:\/\/doi.org\/10.1023\/A:1022969405325","journal-title":"Form. Methods Syst. Des."},{"key":"16_CR14","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)"},{"issue":"12","key":"16_CR15","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun. ACM 18(12), 717\u2013721 (1975). https:\/\/doi.org\/10.1145\/361227.361234","journal-title":"Commun. ACM"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Matthews, O., Bingham, J., Sorin, D.J.: Verifiable hierarchical protocols with network invariants on parametric systems. In: FMCAD 2016, pp. 101\u2013108. FMCAD Inc, Austin (2016)","DOI":"10.1109\/FMCAD.2016.7886667"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Matthews, O., Sorin, D.J.: Architecting hierarchical coherence protocols for push-button parametric verification. MICRO 2017, pp. 477\u2013489 (2017). https:\/\/doi.org\/10.1145\/3123939.3123971","DOI":"10.1145\/3123939.3123971"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/3-540-48153-2_17","volume-title":"Correct Hardware Design and Verification Methods","author":"KL McMillan","year":"1999","unstructured":"McMillan, K.L.: Verification of infinite state systems by compositional model checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 219\u2013237. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_17"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.: Modular specification and verification of a cache-coherent interface. FMCAD 2016, pp. 109\u2013116. FMCAD Inc, Austin (2016). http:\/\/dl.acm.org\/citation.cfm?id=3077629.3077651","DOI":"10.1109\/FMCAD.2016.7886668"},{"key":"16_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, USA (1993)"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-030-53291-8_12","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2020","unstructured":"McMillan, K.L., Padon, O.: Ivy: a multi-modal verification tool for distributed algorithms. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 190\u2013202. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_12"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Moore, J. Strother.: An ACL2 proof of write invalidate cache coherence. In: Hu, Alan J.., Vardi, Moshe Y.. (eds.) CAV 1998. LNCS, vol. 1427, pp. 29\u201338. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0028728, http:\/\/dl.acm.org\/citation.cfm?id=647767.733778","DOI":"10.1007\/BFb0028728"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Nikhil, R.: Bluespec system verilog: efficient, correct RTL from high level specifications, pp. 69\u201370 (2004). https:\/\/doi.org\/10.1109\/MEMCOD.2004.1459818","DOI":"10.1109\/MEMCOD.2004.1459818"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"O\u2019Leary, J., Talupur, M., Tuttle, M.R.: Protocol verification using flows: an industrial experience. In: FMCAD 2009, pp. 172\u2013179 (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351126","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Oswald, N., Nagarajan, V., Sorin, D.J.: HieraGen: automated generation of concurrent, hierarchical cache coherence protocols. In: ISCA 2020, pp. 888\u2013899 (2020). https:\/\/doi.org\/10.1109\/ISCA45697.2020.00077","DOI":"10.1109\/ISCA45697.2020.00077"},{"key":"16_CR26","doi-asserted-by":"publisher","unstructured":"Oswald, N., Nagarajan, V., Sorin, D.J.: ProtoGen: automatically generating directory cache coherence protocols from atomic specifications. In: ISCA 2018, Piscataway, NJ, USA, pp. 247\u2013260 (2018) https:\/\/doi.org\/10.1109\/ISCA.2018.00030","DOI":"10.1109\/ISCA.2018.00030"},{"issue":"6","key":"16_CR27","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/2980983.2908118","volume":"51","author":"O Padon","year":"2016","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. SIGPLAN Not. 51(6), 614\u2013630 (2016). https:\/\/doi.org\/10.1145\/2980983.2908118","journal-title":"SIGPLAN Not."},{"key":"16_CR28","volume-title":"The Theory of Database Concurrency Control","author":"C Papadimitriou","year":"1986","unstructured":"Papadimitriou, C.: The Theory of Database Concurrency Control. Computer Science Press Inc., USA (1986)"},{"key":"16_CR29","doi-asserted-by":"publisher","unstructured":"Park, S., Dill, D.L.: Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In: SPAA 1996, pp. 288\u2013296. ACM, New York (1996). https:\/\/doi.org\/10.1145\/237502.237573","DOI":"10.1145\/237502.237573"},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Ros, A., Kaxiras, S.: Complexity-effective multicore coherence. In: PACT 2012, pp. 241\u2013252. Association for Computing Machinery, New York (2012). https:\/\/doi.org\/10.1145\/2370816.2370853","DOI":"10.1145\/2370816.2370853"},{"key":"16_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-319-11936-6_24","volume-title":"Automated Technology for Verification and Analysis","author":"D Sethi","year":"2014","unstructured":"Sethi, D., Talupur, M., Malik, S.: Using flow specifications of parameterized cache coherence protocols for verifying deadlock freedom. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 330\u2013347. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_24"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Talupur, M., Tuttle, M.R.: Going with the flow: parameterized verification using message flows. In: FMCAD 2008 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.14"},{"key":"16_CR33","unstructured":"Vijayaraghavan, M.: Modular verification of hardware systems. Ph.D. thesis (2016). http:\/\/hdl.handle.net\/1721.1\/106096"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Vijayaraghavan, M., Chlipala, A., Arvind, Dave, N.: Modular deductive verification of multiprocessor hardware designs. In: Kroening, D., P\u0103s\u0103reanu, C. (eds.) CAV 2015. LNCS, vol. 9207, pp. 109\u2013127. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21668-3_7","DOI":"10.1007\/978-3-319-21668-3_7"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Zhang, M., Bingham, J.D., Erickson, J., Sorin, D.J.: PVCoherence: designing flat coherence protocols for scalable verification. In: HPCA 2014, pp. 392\u2013403 (2014). https:\/\/doi.org\/10.1109\/HPCA.2014.6835949","DOI":"10.1109\/HPCA.2014.6835949"},{"key":"16_CR36","doi-asserted-by":"publisher","unstructured":"Zhang, M., Lebeck, A.R., Sorin, D.J.: Fractal coherence: scalably verifiable cache coherence. In: MICRO 2010, USA, pp. 471\u2013482 (2010). https:\/\/doi.org\/10.1109\/MICRO.2010.11","DOI":"10.1109\/MICRO.2010.11"},{"key":"16_CR37","doi-asserted-by":"publisher","unstructured":"Zhang, S., Wright, A., Bourgeat, T., Arvind, A.: Composable building blocks to open up processor design. In: MICRO 2018, pp. 68\u201381 (2018). https:\/\/doi.org\/10.1109\/MICRO.2018.00015","DOI":"10.1109\/MICRO.2018.00015"},{"key":"16_CR38","doi-asserted-by":"publisher","unstructured":"Zhao, L., Iyer, R., Makineni, S., Newell, D., Cheng, L.: NCID: a non-inclusive cache, inclusive directory architecture for flexible and efficient cache hierarchies. In: CF 2010, New York, NY, USA, pp. 121\u2013130 (2010). https:\/\/doi.org\/10.1145\/1787275.1787314","DOI":"10.1145\/1787275.1787314"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:21:45Z","timestamp":1659687705000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}