{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T10:11:45Z","timestamp":1725617505477},"reference-count":49,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NWO","award":["016.Veni.192.259"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism\u2014based on session types\u2014for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a distributed merge sort, a distributed load-balancing mapper, and a variant of the map-reduce model, using relatively simple specifications. Soundness of Actris is proved using a model of its protocol mechanism in the Iris framework. We mechanised the theory of Actris, together with tactics for symbolic execution of programs, as well as all examples in the paper, in the Coq proof assistant.<\/jats:p>","DOI":"10.1145\/3371074","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-30","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Actris: session-type based reasoning in separation logic"],"prefix":"10.1145","volume":"4","author":[{"given":"Jonas Kastberg","family":"Hinrichsen","sequence":"first","affiliation":[{"name":"IT University of Copenhagen, Denmark"}]},{"given":"Jesper","family":"Bengtson","sequence":"additional","affiliation":[{"name":"IT University of Copenhagen, Denmark"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"key-10.1145\/3371074-1","unstructured":"Pierre America and Jan J. M. M. Rutten. 1989. Solving Reflexive Domain Equations in a Category of Complete Metric Spaces. JCSS 39, 3 (1989), 343–375."},{"key":"key-10.1145\/3371074-2","doi-asserted-by":"crossref","unstructured":"Andrew W Appel. 2014. Program logics for certified compilers. Cambridge University Press.","DOI":"10.1017\/CBO9781107256552"},{"key":"key-10.1145\/3371074-3","unstructured":"Robert Atkey, Sam Lindley, and J. Garrett Morris. 2016. Conflation Confers Concurrency. In Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday (LNCS), Vol. 9600. 32–55."},{"key":"key-10.1145\/3371074-4","unstructured":"Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. PACMPL 1, ICFP (2017), 37:1–37:29."},{"key":"key-10.1145\/3371074-5","unstructured":"Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In ESOP, Vol. 11423 LNCS. 611–639."},{"key":"key-10.1145\/3371074-6","doi-asserted-by":"crossref","unstructured":"Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. LMCS 8, 4 (2012).","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"key-10.1145\/3371074-7","unstructured":"Ales Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal. 2019. Iron: Managing Obligations in Higher-Order Concurrent Separation Logic. PACMPL 3, POPL (2019), 65:1–65:30."},{"key":"key-10.1145\/3371074-8","doi-asserted-by":"crossref","unstructured":"Laura Bocchi, Kohei Honda, Emilio Tuosto, and Nobuko Yoshida. 2010. A Theory of Design-by-Contract for Distributed Multiparty Interactions. In CONCUR. 162–176.","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"key-10.1145\/3371074-9","unstructured":"Coq Development Team. 2019. The Coq Proof Assistant Reference Manual, Version 8.9. (2019). https:\/\/coq.inria.fr\/distrib\/ current\/refman\/"},{"key":"key-10.1145\/3371074-10","unstructured":"Andreea Costea, Wei-Ngan Chin, Shengchao Qin, and Florin Craciun. 2018. Automated Modular Verification for Relaxed Communication Protocols. In APLAS (LNCS), Vol. 11275. 284–305."},{"key":"key-10.1145\/3371074-11","doi-asserted-by":"crossref","unstructured":"Florin Craciun, Tibor Kiss, and Andreea Costea. 2015. Towards a Session Logic for Communication Protocols. In ICECCS. 140–149.","DOI":"10.1109\/ICECCS.2015.33"},{"key":"key-10.1145\/3371074-12","doi-asserted-by":"crossref","unstructured":"Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A Logic for Time and Data Abstraction. In ECOOP. 207–231.","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"key-10.1145\/3371074-13","doi-asserted-by":"crossref","unstructured":"Ornela Dardha, Elena Giachino, and Davide Sangiorgi. 2012. Session Types Revisited. In PPDP. 139–150.","DOI":"10.1145\/2370776.2370794"},{"key":"key-10.1145\/3371074-14","unstructured":"Jeffrey Dean and Sanjay Ghemawat. 2004. MapReduce: Simplified Data Processing on Large Clusters. In OSDI. 137–150."},{"key":"key-10.1145\/3371074-15","doi-asserted-by":"crossref","unstructured":"Adrian Francalanza, Julian Rathke, and Vladimiro Sassone. 2011. Permission-Based Separation Logic for Message-Passing Concurrency. LMCS 7, 3 (2011).","DOI":"10.2168\/LMCS-7(3:7)2011"},{"key":"key-10.1145\/3371074-16","unstructured":"Jafar Hamin and Bart Jacobs. 2019. Transferring Obligations Through Synchronizations. In ECOOP."},{"key":"key-10.1145\/3371074-17","unstructured":"Carl Hewitt, Peter Bishop, and Richard Steiger. 1973. A Universal Modular ACTOR Formalism for Artificial Intelligence. In IJCAI. 235–245."},{"key":"key-10.1145\/3371074-18","doi-asserted-by":"crossref","unstructured":"Jonas Kastberg Hinrichsen, Jesper Bengtson, and Robbert Krebbers. 2019. Coq Mechanization of Actris. Available online at https:\/\/gitlab.mpi- sws.org\/iris\/actris .","DOI":"10.1145\/3373096"},{"key":"key-10.1145\/3371074-19","doi-asserted-by":"crossref","unstructured":"Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In proceedings of ESOP. 122–138.","DOI":"10.1007\/BFb0053567"},{"key":"key-10.1145\/3371074-20","doi-asserted-by":"crossref","unstructured":"Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In POPL. 273–284.","DOI":"10.1145\/1328897.1328472"},{"key":"key-10.1145\/3371074-21","unstructured":"Raymond Hu, Dimitrios Kouzapas, Olivier Pernet, Nobuko Yoshida, and Kohei Honda. 2010. Type-Safe Eventful Sessions in Java. In ECOOP. 21–25."},{"key":"key-10.1145\/3371074-22","unstructured":"Keigo Imai, Nobuko Yoshida, and Shoji Yuen. 2019. Session-OCaml: A Session-Based Library with Polarities and Lenses. Science of Computer Programming 172 (2019), 135–159."},{"key":"key-10.1145\/3371074-23","doi-asserted-by":"crossref","unstructured":"Bart Jacobs and Frank Piessens. 2011. Expressive Modular Fine-Grained Concurrency Specification. In POPL. 271–282.","DOI":"10.1145\/1925844.1926417"},{"key":"key-10.1145\/3371074-24","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. RustBelt: Securing the Foundations of the Rust Programming Language. PACMPL 2, POPL (2018), 66:1–66:34."},{"key":"key-10.1145\/3371074-25","doi-asserted-by":"crossref","unstructured":"Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-Order Ghost State. In ICFP. 256–269.","DOI":"10.1145\/3022670.2951943"},{"key":"key-10.1145\/3371074-26","unstructured":"Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris From the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. JFP 28 (2018), e20."},{"key":"key-10.1145\/3371074-27","doi-asserted-by":"crossref","unstructured":"Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and Invariants as an Orthogonal Basis for Concurrent Reasoning. In POPL. 637–650.","DOI":"10.1145\/2775051.2676980"},{"key":"key-10.1145\/3371074-28","unstructured":"Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In CONCUR (LNCS), Vol. 4137. 233–247."},{"key":"key-10.1145\/3371074-29","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi, Benjamin C. Pierce, and David N. Turner. 1996. Linearity and the pi-Calculus. In POPL. 358–371.","DOI":"10.1145\/237721.237804"},{"key":"key-10.1145\/3371074-30","unstructured":"Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic. PACMPL 2, ICFP (2018), 77:1–77:30."},{"key":"key-10.1145\/3371074-31","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017a. The Essence of Higher-Order Concurrent Separation Logic. In ESOP. 696–723.","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"key-10.1145\/3371074-32","doi-asserted-by":"crossref","unstructured":"Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. 205–217.","DOI":"10.1145\/3093333.3009855"},{"key":"key-10.1145\/3371074-33","doi-asserted-by":"crossref","unstructured":"Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. 2019. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. Submitted for publication.","DOI":"10.1007\/978-3-030-44914-8_13"},{"key":"key-10.1145\/3371074-34","unstructured":"Julien Lange, Nicholas Ng, Bernardo Toninho, and Nobuko Yoshida. 2018. A Static Verification Framework for Message Passing in Go Using Behavioural Types. ICSE (2018), 1137–1148."},{"key":"key-10.1145\/3371074-35","unstructured":"William Mansky, Andrew W. Appel, and Aleksey Nogin. 2017. A Verified Messaging System. PACMPL 1, OOPSLA (2017), 87:1–87:28."},{"key":"key-10.1145\/3371074-36","unstructured":"Claude Marché, Christine Paulin-Mohring, and Xavier Urbain. 2004. The KRAKATOA Tool for Certification of JAVA\/JAVAC-ARD Programs Annotated in JML. JLP 58, 1-2 (2004), 89–106."},{"key":"key-10.1145\/3371074-37","doi-asserted-by":"crossref","unstructured":"Dimitris Mostrous and Vasco Thudichum Vasconcelos. 2014. Affine Sessions. In COORDINATION. 115–130.","DOI":"10.1007\/978-3-662-43376-8_8"},{"key":"key-10.1145\/3371074-38","unstructured":"Hiroshi Nakano. 2000. A Modality for Recursion. In LICS. 255–266."},{"key":"key-10.1145\/3371074-39","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski, Ruy Ley-Wild, Ilya Sergey, and Germán Andrés Delbianco. 2014. Communicating State Transition Systems for Fine-Grained Concurrent Resources. In ESOP. 290–310.","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"key-10.1145\/3371074-40","doi-asserted-by":"crossref","unstructured":"Kosuke Ono, Yoichi Hirai, Yoshinori Tanabe, Natsuko Noda, and Masami Hagiya. 2011. Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications. In SEFM. 350–365.","DOI":"10.1007\/978-3-642-24690-6_24"},{"key":"key-10.1145\/3371074-41","doi-asserted-by":"crossref","unstructured":"Wytse Oortwijn, Stefan Blom, and Marieke Huisman. 2016. Future-based Static Analysis of Message Passing Programs. In PLACES. 65–72.","DOI":"10.4204\/EPTCS.211.7"},{"key":"key-10.1145\/3371074-42","unstructured":"Luca Padovani. 2014. Deadlock and Lock Freedom in the Linear 𝜋 -Calculus. In CSL. 72:1–72:10."},{"key":"key-10.1145\/3371074-43","unstructured":"Luca Padovani. 2017. A Simple Library Implementation of Binary Sessions. JFP 27, 2010 (2017), e4."},{"key":"key-10.1145\/3371074-44","unstructured":"Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming and Proving with Distributed Protocols. PACMPL 2, POPL (2018), 28:1–28:30."},{"key":"key-10.1145\/3371074-45","doi-asserted-by":"crossref","unstructured":"Kasper Svendsen and Lars Birkedal. 2014. Impredicative Concurrent Abstract Predicates. In ESOP. 149–168.","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"key-10.1145\/3371074-46","doi-asserted-by":"crossref","unstructured":"Samira Tasharofi, Peter Dinges, and Ralph E. Johnson. 2013. Why Do Scala Developers Mix the Actor Model with Other Concurrency Models?. In ECOOP. 302–326.","DOI":"10.1007\/978-3-642-39038-8_13"},{"key":"key-10.1145\/3371074-47","doi-asserted-by":"crossref","unstructured":"Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP. 909–936.","DOI":"10.1007\/978-3-662-54434-1_34"},{"key":"key-10.1145\/3371074-48","unstructured":"Tengfei Tu, Xiaoyu Liu, Linhai Song, and Yiying Zhang. 2019. Understanding Real-World Concurrency Bugs in Go. In ASPLOS. 865–878."},{"key":"key-10.1145\/3371074-49","doi-asserted-by":"crossref","unstructured":"Jules Villard, Étienne Lozes, and Cristiano Calcagno. 2009. Proving Copyless Message Passing. In APLAS. 194–209.","DOI":"10.1007\/978-3-642-10672-9_15"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371074","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T09:45:48Z","timestamp":1672566348000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371074"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":49,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371074"],"URL":"https:\/\/doi.org\/10.1145\/3371074","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}