{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:45:10Z","timestamp":1773193510928,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R006865\/1"],"award-info":[{"award-number":["EP\/R006865\/1"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,3,30]]},"DOI":"10.1145\/3676641.3715999","type":"proceedings-article","created":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:47:32Z","timestamp":1743094052000},"page":"437-450","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Formalising CXL Cache Coherence"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-7822-8407","authenticated-orcid":false,"given":"Chengsong","family":"Tan","sequence":"first","affiliation":[{"name":"Kaihong, Shenzhen, China"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, London, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19835-9_5"},{"key":"e_1_3_2_1_2_1","volume-title":"A Programming Model for Disaggregated Memory over CXL","author":"Assa Gal","year":"2024","unstructured":"Gal Assa, Michal Friedman, and Ori Lahav. A Programming Model for Disaggregated Memory over CXL, 2024. https:\/\/arxiv.org\/pdf\/2407.16300."},{"key":"e_1_3_2_1_3_1","unstructured":"Thomas Bourgeat. Specification and verification of sequential machines in rule-based hardware languages. PhD thesis MIT 2023. ."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_3"},{"key":"e_1_3_2_1_5_1","volume-title":"CCIX Consortium Enables Next Generation Compute Architectures with the Availability of Base Specification 1.0","author":"CCIX Consortium","year":"2018","unstructured":"CCIX Consortium. CCIX Consortium Enables Next Generation Compute Architectures with the Availability of Base Specification 1.0, 2018. https:\/\/bwnews.pr\/4ePcMLM."},{"key":"e_1_3_2_1_6_1","volume-title":"Intel's Omni-Path InfiniBand-killer debuts at sizzling 100 Gb\/sec","author":"Chirgwin Richard","year":"2015","unstructured":"Richard Chirgwin. Intel's Omni-Path InfiniBand-killer debuts at sizzling 100 Gb\/sec, 2015. https:\/\/bit.ly\/omnipath."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_16"},{"key":"e_1_3_2_1_8_1","volume-title":"New Industry High-Speed Interconnect From Intel","author":"Cutress Ian","year":"2019","unstructured":"Ian Cutress. CXL Specification 1.0 Released: New Industry High-Speed Interconnect From Intel, 2019. https:\/\/bit.ly\/cxl-spec."},{"key":"e_1_3_2_1_9_1","first-page":"l31","article-title":"Compute Express Link Specification","volume":"1","author":"CXL Consortium","year":"2023","unstructured":"CXL Consortium. Compute Express Link Specification, Revision 3.1, 2023. https:\/\/bit.ly\/cxl31.","journal-title":"Revision 3"},{"key":"e_1_3_2_1_10_1","volume-title":"An Introduction to the Compute Express Link (CXL) Interconnect","author":"Sharma Debendra Das","year":"2023","unstructured":"Debendra Das Sharma, Robert Blankenship, and Daniel Berger. An Introduction to the Compute Express Link (CXL) Interconnect, 2023. https:\/\/arxiv.org\/pdf\/2306.11227."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591267"},{"key":"e_1_3_2_1_12_1","volume-title":"AMD's Infinity Fabric will be the foundation for all of its chips from 2017 onwards","author":"Goto Hiroshige","year":"2017","unstructured":"Hiroshige Goto. AMD's Infinity Fabric will be the foundation for all of its chips from 2017 onwards, 2017. https:\/\/bit.ly\/infinityfabric."},{"key":"e_1_3_2_1_13_1","first-page":"287","volume-title":"2022 USENIX Annual Technical Conference (USENIX ATC","author":"Gouk Donghyun","year":"2022","unstructured":"Donghyun Gouk, Sangwon Lee, Miryeong Kwon, and Myoungsoo Jung. Direct access, High-Performance memory disaggregation with DirectCXL. In 2022 USENIX Annual Technical Conference (USENIX ATC , pages 287--294, Carlsbad, CA, July 2022. USENIX Association."},{"key":"e_1_3_2_1_14_1","volume-title":"Memory Processor Interface","author":"Grossi Thibault","year":"2023","unstructured":"Thibault Grossi. Memory Processor Interface 2023, Focus on CXL, 2024. https:\/\/bit.ly\/yole_cxl."},{"key":"e_1_3_2_1_15_1","volume-title":"The Sketch and Explore library","author":"Haftmann Florian","year":"2023","unstructured":"Florian Haftmann. The Sketch and Explore library, 2023. https:\/\/bit.ly\/sketch_explore."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_17_1","volume-title":"Intel Ultra Path Interconnect","year":"2020","unstructured":"Intel. Intel Ultra Path Interconnect, 2020. https:\/\/bit.ly\/ultrapath."},{"key":"e_1_3_2_1_18_1","volume-title":"Orchestrating memory disaggregation with Compute Express Link","year":"2024","unstructured":"Intel. Orchestrating memory disaggregation with Compute Express Link, 2024. https:\/\/intel.ly\/48j1JIv."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3575693.3578835"},{"key":"e_1_3_2_1_20_1","volume-title":"Introduction to InfiniBand","author":"Mellanox Technologies Inc.","year":"2003","unstructured":"Mellanox Technologies Inc. Introduction to InfiniBand, 2003. https:\/\/bit.ly\/infiniband."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-01764-3"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow Lawrence C. Paulson and Markus Wenzel. Isabelle\/ HOL - A Proof Assistant for Higher-Order Logic volume 2283 of Lecture Notes in Computer Science. Springer 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_23_1","first-page":"247","volume-title":"ISCA","author":"Oswald Nicolai","year":"2018","unstructured":"Nicolai Oswald, Vijay Nagarajan, and Daniel J. Sorin. ProtoGen: Automatically Generating Directory Cache Coherence Protocols from Atomic Specifications. In ISCA, pages 247--260. IEEE Computer Society, 2018."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/HPCA53966.2022.00061"},{"key":"e_1_3_2_1_25_1","series-title":"EPiC Series in Computing","first-page":"1","volume-title":"PAAR@IJCAR","author":"Paulson Lawrence C.","year":"2010","unstructured":"Lawrence C. Paulson. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In PAAR@IJCAR, volume 9 of EPiC Series in Computing, pages 1--10. EasyChair, 2010."},{"key":"e_1_3_2_1_26_1","volume-title":"PCIE specification library","author":"PCIE Consortium","year":"2023","unstructured":"PCIE Consortium. PCIE specification library, 2023. https:\/\/pcisig.com\/specifications."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/248621.248624"},{"key":"e_1_3_2_1_28_1","volume-title":"Hardware makers unite to challenge Intel with Gen-Z spec","author":"Shah Agam","year":"2016","unstructured":"Agam Shah. Hardware makers unite to challenge Intel with Gen-Z spec, 2016. https:\/\/bit.ly\/gen-z-spec."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_4"},{"issue":"4","key":"e_1_3_2_1_30_1","first-page":"8","article-title":"opens up a new era of acceleration enablement","volume":"62","author":"Stuecheli Jeffrey","year":"2018","unstructured":"Jeffrey Stuecheli, William J. Starke, John D. Irish, L. Baba Arimilli, Daniel M. Dreps, Bart Blaner, Curt Wollbrink, and Brian Allison. IBM POWER9 opens up a new era of acceleration enablement: OpenCAPI. IBM J. Res. Dev., 62(4\/5):8:1--8:8, 2018.","journal-title":"OpenCAPI. IBM J. Res. Dev."},{"key":"e_1_3_2_1_31_1","volume-title":"GitHub repository for formalisation of CXL.cache","author":"Tan Chengsong","year":"2025","unstructured":"Chengsong Tan. GitHub repository for formalisation of CXL.cache, 2025. Accessed: 2025-02-05."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/FormaliSE66629.2025.00010"},{"key":"e_1_3_2_1_33_1","volume-title":"Compute Express Link (CXL): Exploring Coherent Memory and Innovative Use Cases. https:\/\/bit.ly\/cxlwebinar","author":"Tavallaei Siamak","year":"2020","unstructured":"Siamak Tavallaei, Kurt Lender, and Robert Blankenship. Compute Express Link (CXL): Exploring Coherent Memory and Innovative Use Cases. https:\/\/bit.ly\/cxlwebinar, 2020."},{"key":"e_1_3_2_1_34_1","unstructured":"Jon Worrel. Nvidia NVLINK 2.0 arrives in IBM servers next year 2016. https:\/\/bit.ly\/nvlink."}],"event":{"name":"ASPLOS '25: 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems","location":"Rotterdam Netherlands","acronym":"ASPLOS '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGOPS ACM Special Interest Group on Operating Systems","SIGARCH ACM Special Interest Group on Computer Architecture"]},"container-title":["Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676641.3715999","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3676641.3715999","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T11:07:13Z","timestamp":1755774433000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3676641.3715999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":34,"alternative-id":["10.1145\/3676641.3715999","10.1145\/3676641"],"URL":"https:\/\/doi.org\/10.1145\/3676641.3715999","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}