{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:08:11Z","timestamp":1790075291308,"version":"4.0.1"},"reference-count":88,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,6,8]]},"abstract":"<jats:p>\n                    Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed implementation. We present the first comprehensive investigation of global protocol implementability modulo network architectures. We propose a set of network-parametric Coherence Conditions, and exhibit sufficient assumptions under which it precisely characterizes implementability. We further reduce these assumptions to a minimal set of operational axioms describing insert and remove behavior of individual message buffers. Our reduction immediately establishes that five commonly studied asynchronous network architectures, namely peer-to-peer FIFO, mailbox, senderbox, monobox and bag, are instances of our networkparametric result. We use our characterization to derive optimal complexity results for implementability modulo networks, relationships between classes of implementable global protocols, and symbolic algorithms for deciding implementability modulo networks. We implement the latter in the first network-parametric tool S\n                    <jats:sc>prout<\/jats:sc>\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mrow>\n                            <mml:mo form=\"prefix\" stretchy=\"true\">(<\/mml:mo>\n                            <mml:mi mathvariant=\"double-struck\">A<\/mml:mi>\n                            <mml:mo form=\"postfix\" stretchy=\"true\">)<\/mml:mo>\n                          <\/mml:mrow>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , and show that it achieves network generality without sacrificing performance and modularity.\n                  <\/jats:p>","DOI":"10.1145\/3808319","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"1812-1838","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Implementability of Global Distributed Protocols Modulo Network Architectures"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0173-4498","authenticated-orcid":false,"given":"Elaine","family":"Li","sequence":"first","affiliation":[{"name":"New York University, New York City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4051-5968","authenticated-orcid":false,"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[{"name":"New York University, New York City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSTTCS.2013.213"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1214326"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_10"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-41157-1_7"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_3_1_7_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2021.14"},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_23"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290342"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2023.6"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3678232.3678258"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8_20"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-016-0379-X"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_20"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17715-6_15"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-39570-8_8"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.07.005"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3503221.3508404"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.6"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2024.22"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-014-0218-8"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00022-9"},{"key":"e_1_3_1_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_3_1_25_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(4:33)2023"},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/357195.357200"},{"key":"e_1_3_1_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP46215.2023.10179477"},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74407-8_12"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2005.25"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27755-2_15"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2005.09.007"},{"key":"e_1_3_1_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2018.12.002"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632398"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.22"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571248"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","unstructured":"Cinzia Di Giusto \u00c9tienne Lozes and Pascal Urso. 2025. On the Impact of the Communication Model on Realisability. CoRR abs\/2512.05609 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2512.05609 10.48550\/ARXIV.2512.05609 arXiv:2512.05609","DOI":"10.48550\/ARXIV.2512.05609"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","unstructured":"Cinzia Di Giusto \u00c9tienne Lozes and Pascal Urso. 2025. Realisability and Complementability of Multiparty Session Types. CoRR abs\/2507.17354 (2025). https:\/\/doi.org\/10.48550\/ARXIV.2507.17354 10.48550\/ARXIV.2507.17354 arXiv:2507.17354","DOI":"10.48550\/ARXIV.2507.17354"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-18(2:16)2022"},{"key":"e_1_3_1_41_2","doi-asserted-by":"crossref","unstructured":"Jonas Kastberg Hinrichsen Jules Jacobs and Robbert Krebbers. 2024. Multris: Functional Verification of Multiparty Message Passing in Separation Logic. (2024). https:\/\/jihgfee.github.io\/papers\/multris_manuscript.pdf","DOI":"10.1145\/3689762"},{"key":"e_1_3_1_42_2","unstructured":"Andrew K. Hirsch and Deepak Garg. 2021. Pirouette: Higher-Order Typed Functional Choreographies. CoRR abs\/2111.03484 (2021). arXiv:2111.03484 https:\/\/arxiv.org\/abs\/2111.03484"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498684"},{"key":"e_1_3_1_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33518-1_37"},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49665-7_24"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_7"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2020.9"},{"key":"e_1_3_1_49_2","volume-title":"ITU-T Recommendation Z.120","author":"Union International Telecommunication","year":"2011","unstructured":"International Telecommunication Union. 2011. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). ITU-T Recommendation Z.120. International Telecommunication Union, Geneva. https:\/\/www.itu.int\/rec\/T-REC-Z.120-201102-I\/en"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/3607856"},{"key":"e_1_3_1_51_2","unstructured":"Shun Kashiwa Gan Shen Soroush Zare and Lindsey Kuper. 2023. Portable Efficient and Practical Library-Level Choreographic Programming. arXiv:2311.11472 [cs.PL] https:\/\/arxiv.org\/abs\/2311.11472"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.8.2.9"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","DOI":"10.1145\/3335772.3335934"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180157"},{"key":"e_1_3_1_55_2","unstructured":"Languages Systems and Data Lab UC Santa Cruz. [n. d.]. ChoRus: Choreographic Programming in Rust. https:\/\/lsducsc.github.io\/ChoRus\/introduction.html. Accessed: 2025-07-10."},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","unstructured":"Elaine Li. 2026. Sprout(A): A Network-Parametric Verifier for Symbolic Multiparty Protocols. https:\/\/doi.org\/10.5281\/zenodo.19600644 10.5281\/zenodo.19600644","DOI":"10.5281\/zenodo.19600644"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/3720493"},{"key":"e_1_3_1_59_2","unstructured":"Elaine Li Felix Stutz Thomas Wies and Damien Zufferey. 2025. Characterizing Implementability of Global Protocols with Infinite States and Data. arXiv:2411.05722 [cs.PL] https:\/\/arxiv.org\/abs\/2411.05722"},{"key":"e_1_3_1_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-98682-6_16"},{"key":"e_1_3_1_61_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ITP.2025.15"},{"key":"e_1_3_1_62_2","doi-asserted-by":"publisher","unstructured":"Elaine Li and Thomas Wies. 2026. Implementability of Global Distributed Protocols modulo Network Architectures. CoRR abs\/2602.10320 (2026). https:\/\/doi.org\/10.48550\/ARXIV.2602.10320 10.48550\/ARXIV.2602.10320 arXiv:2602.10320","DOI":"10.48550\/ARXIV.2602.10320"},{"key":"e_1_3_1_63_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2003.08.002"},{"key":"e_1_3_1_64_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2019.28"},{"key":"e_1_3_1_65_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428202"},{"key":"e_1_3_1_66_2","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044482816-3\/50020-4"},{"key":"e_1_3_1_67_2","doi-asserted-by":"publisher","DOI":"10.1017\/9781108981491"},{"key":"e_1_3_1_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45841-7_43"},{"key":"e_1_3_1_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48340-3_8"},{"key":"e_1_3_1_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-017-0420-8"},{"key":"e_1_3_1_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/3178372.3179495"},{"key":"e_1_3_1_72_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:17)2017"},{"key":"e_1_3_1_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30561-0_15"},{"key":"e_1_3_1_74_2","doi-asserted-by":"publisher","DOI":"10.1109\/FPL.2016.7577359"},{"key":"e_1_3_1_75_2","unstructured":"Object Management Group. [n. d.]. Unified Modeling Language (UML) Website. https:\/\/www.uml.org\/. Accessed: 2025-07-10."},{"key":"e_1_3_1_76_2","unstructured":"Giuseppe De Palma Saverio Giallorenzo Jacopo Mauro Matteo Trentin and Gianluigi Zavattaro. 2024. Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications. arXiv:2406.09099 [cs.PL] https:\/\/arxiv.org\/abs\/2406.09099"},{"key":"e_1_3_1_77_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814"},{"key":"e_1_3_1_78_2","doi-asserted-by":"publisher","DOI":"10.1145\/2089116.2089122"},{"key":"e_1_3_1_79_2","doi-asserted-by":"publisher","unstructured":"Gan Shen Shun Kashiwa and Lindsey Kuper. 2023. HasChor: Functional Choreographic Programming for All (Functional Pearl). CoRR abs\/2303.00924 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.00924 10.48550\/ARXIV.2303.00924 arXiv:2303.00924","DOI":"10.48550\/ARXIV.2303.00924"},{"key":"e_1_3_1_80_2","volume-title":"Ph. D. Dissertation","author":"Stutz Felix","year":"2024","unstructured":"Felix Stutz. 2024. Implementability of Asynchronous Communication Protocols \u2013 The Power of Choice. Ph. D. Dissertation. Kaiserslautern University of Technology, Germany. https:\/\/kluedo.ub.rptu.de\/frontdoor\/index\/index\/docId\/8077"},{"key":"e_1_3_1_81_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2016.11.005"},{"key":"e_1_3_1_82_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704872"},{"key":"e_1_3_1_83_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_1_84_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECOOP.2024.41"},{"key":"e_1_3_1_85_2","unstructured":"Web Services Choreography Working Group. 2005. Web Services Choreography Description Language Version 1.0. W3C Candidate Recommendation. World Wide Web Consortium (W3C). Available at http:\/\/www.w3.org\/TR\/2005\/CR-ws-cdl-10-20051109\/."},{"key":"e_1_3_1_86_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-51060-1_6"},{"key":"e_1_3_1_87_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-05119-2_3"},{"key":"e_1_3_1_88_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428216"},{"key":"e_1_3_1_89_2","doi-asserted-by":"publisher","DOI":"10.1051\/ITA\/1987210200991"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808319","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:50:15Z","timestamp":1790074215000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":88,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808319"],"URL":"https:\/\/doi.org\/10.1145\/3808319","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-14","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}