乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T23:08:15Z","timestamp":1740179295304,"version":"3.37.3"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"Villum Fonden","award":["25804"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,10,8]]},"abstract":"We introduce Multris, a separation logic for verifying functional correctness of programs that combine multiparty message-passing communication with shared-memory concurrency. The foundation of our work is a novel concept of multiparty protocol consistency, which guarantees safe communication among a set of parties, provided each party adheres to its prescribed protocol. Our concept of protocol consistency is inspired by the bottom-up approach for multiparty session types. However, by considering it in the context of separation logic instead of a type system, we go further in terms of generality by supporting new notions of implicit transfer of knowledge and implicit transfer of resources. We develop tactics for automatically verifying protocol consistency and for reasoning about message-passing operations in Multris. We evaluate Multris on a range of examples, including the well-known two- and three-buyer protocols, as well as a new verification benchmark based on Chang and Roberts's ring leader election protocol. To ensure the reliability of our work, we prove soundness of Multris w.r.t. a low-level channel semantics using the Iris framework in Coq.<\/jats:p>","DOI":"10.1145\/3689762","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T07:23:04Z","timestamp":1728372184000},"page":"1446-1474","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Multris: Functional Verification of Multiparty Message Passing in Separation Logic"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6143-9031","authenticated-orcid":false,"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus N, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1976-3182","authenticated-orcid":false,"given":"Jules","family":"Jacobs","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1185-5237","authenticated-orcid":false,"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"volume-title":"Semantics of Types for Mutable State. Ph. D. Dissertation","author":"Ahmed Amal","key":"e_1_2_1_1_1","unstructured":"Amal Ahmed. 2004. Semantics of Types for Mutable State. Ph. D. Dissertation. Princeton University."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(89)90027-5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel. 2001. Foundational Proof-Carrying Code. In LICS. https:\/\/doi.org\/10.1109\/LICS.2001.932501 10.1109\/LICS.2001.932501","DOI":"10.1109\/LICS.2001.932501"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Andrew W. Appel Paul-Andr\u00e9 Melli\u00e8s Christopher D. Richards and J\u00e9r\u00f4me Vouillon. 2007. A very modal model of a modern major general type system. In POPL. https:\/\/doi.org\/10.1145\/1190216.1190235 10.1145\/1190216.1190235","DOI":"10.1145\/1190216.1190235"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Lars Birkedal Kristian St\u00f8vring and Jacob Thamsborg. 2010. The category-theoretic solution of recursive metric-space equations. TCS https:\/\/doi.org\/10.1016\/j.tcs.2010.07.010 10.1016\/j.tcs.2010.07.010","DOI":"10.1016\/j.tcs.2010.07.010"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Laura Bocchi Kohei Honda Emilio Tuosto and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_12 10.1007\/978-3-642-15375-4_12","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454041"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Ernest Chang and Rosemary Roberts. 1979. An improved algorithm for decentralized extrema-finding in circular configurations of processes. CACM https:\/\/doi.org\/10.1145\/359104.359108 10.1145\/359104.359108","DOI":"10.1145\/359104.359108"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"Florin Craciun Tibor Kiss and Andreea Costea. 2015. Towards a Session Logic for Communication Protocols. In ICECCS. https:\/\/doi.org\/10.1109\/ICECCS.2015.33 10.1109\/ICECCS.2015.33","DOI":"10.1109\/ICECCS.2015.33"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"Thomas Dinsdale-Young Mike Dodds Philippa Gardner Matthew J. Parkinson and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP. https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24 10.1007\/978-3-642-14107-2_24","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Adrian Francalanza Julian Rathke and Vladimiro Sassone. 2011. Permission-Based Separation Logic for Message-Passing Concurrency. LMCS https:\/\/doi.org\/10.2168\/LMCS-7(3:7)2011 10.2168\/LMCS-7(3:7)2011","DOI":"10.2168\/LMCS-7(3:7)2011"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607859"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371074"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jesper Bengtson and Robbert Krebbers. 2022. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. LMCS https:\/\/doi.org\/10.46298\/lmcs-18(2:16)2022 10.46298\/lmcs-18(2:16)2022","DOI":"10.46298\/lmcs-18(2:16)2022"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Jules Jacobs and Robbert Krebbers. 2024. Coq Mechanization of \u201cMultris: Functional Verification of Multiparty Message Passing in Separation Logic\u201d. https:\/\/doi.org\/10.5281\/zenodo.13380561 10.5281\/zenodo.13380561","DOI":"10.5281\/zenodo.13380561"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"Jonas Kastberg Hinrichsen Dani\u00ebl Louwrink Robbert Krebbers and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. https:\/\/doi.org\/10.1145\/3437992.3439914 10.1145\/3437992.3439914","DOI":"10.1145\/3437992.3439914"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR. https:\/\/doi.org\/10.1007\/3-540-57208-2_35 10.1007\/3-540-57208-2_35","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In POPL. https:\/\/doi.org\/10.1145\/1328438.1328472 10.1145\/1328438.1328472","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","unstructured":"Kohei Honda Nobuko Yoshida and Marco Carbone. 2016. Multiparty Asynchronous Session Types. JACM https:\/\/doi.org\/10.1145\/2827695 10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547638"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607856"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632889"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Lars Birkedal and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. https:\/\/doi.org\/10.1145\/2951913.2951943 10.1145\/2951913.2951943","DOI":"10.1145\/2951913.2951943"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. JFP https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Jacques-Henri Jourdan Ralf Jung Joseph Tassarotti Jan-Oliver Kaiser Amin Timany Arthur Chargu\u00e9raud and Derek Dreyer. 2018. MoSeL: A General Extensible Modal Framework for Interactive Proofs in Separation Logic. https:\/\/doi.org\/10.1145\/3236772 10.1145\/3236772","DOI":"10.1145\/3236772"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Ralf Jung Ales Bizjak Jacques-Henri Jourdan Derek Dreyer and Lars Birkedal. 2017. The Essence of Higher-Order Concurrent Separation Logic. In ESOP. https:\/\/doi.org\/10.1007\/978-3-662-54434-1_26 10.1007\/978-3-662-54434-1_26","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"Robbert Krebbers Amin Timany and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. https:\/\/doi.org\/10.1145\/3009837.3009855 10.1145\/3009837.3009855","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_17"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"\u00c9tienne Lozes and Jules Villard. 2012. Shared Contract-Obedient Endpoints. In ICE. https:\/\/doi.org\/10.4204\/EPTCS.104.3 10.4204\/EPTCS.104.3","DOI":"10.4204\/EPTCS.104.3"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","unstructured":"Dimitris Mostrous Nobuko Yoshida and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-00590-9_23 10.1007\/978-3-642-00590-9_23","DOI":"10.1007\/978-3-642-00590-9_23"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Nakano. 2000. A modality for recursion. In LICS. https:\/\/doi.org\/10.1109\/LICS.2000.855774 10.1109\/LICS.2000.855774","DOI":"10.1109\/LICS.2000.855774"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Wytse Oortwijn Stefan Blom and Marieke Huisman. 2016. Future-based Static Analysis of Message Passing Programs. In PLACES. https:\/\/doi.org\/10.4204\/EPTCS.211.7 10.4204\/EPTCS.211.7","DOI":"10.4204\/EPTCS.211.7"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","unstructured":"Alceste Scalas and Nobuko Yoshida. 2019. Less is more: multiparty session types revisited. POPL https:\/\/doi.org\/10.1145\/3290343 10.1145\/3290343","DOI":"10.1145\/3290343"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Thomas Somers and Robbert Krebbers. 2024. Verified Lock-Free Session Channels with Linking. https:\/\/doi.org\/10.1145\/3689732 10.1145\/3689732","DOI":"10.1145\/3689732"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In ESOP. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_9 10.1007\/978-3-642-54833-8_9","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_13"},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2024. A Logical Approach to Type Soundness. To appear in JACM","DOI":"10.1145\/3676954"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Dawit Legesse Tirore Jesper Bengtson and Marco Carbone. 2023. A Sound and Complete Projection for Global Types. In ITP (LIPIcs). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.28 10.4230\/LIPICS.ITP.2023.28","DOI":"10.4230\/LIPICS.ITP.2023.28"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Tengfei Tu Xiaoyu Liu Linhai Song and Yiying Zhang. 2019. Understanding Real-World Concurrency Bugs in Go. In ASPLOS. 865\u2013878. https:\/\/doi.org\/10.1145\/3297858.3304069 10.1145\/3297858.3304069","DOI":"10.1145\/3297858.3304069"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Aaron Turon Derek Dreyer and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. https:\/\/doi.org\/10.1145\/2500365.2500600 10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"Fangyi Zhou Francisco Ferreira Raymond Hu Rumyana Neykova and Nobuko Yoshida. 2020. Statically verified refinements for multiparty protocols. https:\/\/doi.org\/10.1145\/3428216 10.1145\/3428216","DOI":"10.1145\/3428216"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689762","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T22:12:31Z","timestamp":1728425551000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689762"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":47,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689762"],"URL":"https:\/\/doi.org\/10.1145\/3689762","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}