Get 20M+ Full-Text Papers For Less Than $1.50/day. Subscribe now for You or Your Team.

Learn More →

Multiparty GV: functional multiparty session types with certified deadlock freedom

Multiparty GV: functional multiparty session types with certified deadlock freedom Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom JULES JACOBS, Radboud University Nijmegen, The Netherlands STEPHANIE BALZER, Carnegie Mellon University, USA ROBBERT KREBBERS, Radboud University Nijmegen, The Netherlands Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels. Representatives of the GV (Wadler’s łGood Variationž) session type family are of particular appeal because they not only assert session fidelity but also deadlock freedom, inspired by a Curry-Howard correspondence to linear logic. A restriction of current versions of GV, however, is the focus on binary sessions, limiting concurrent interactions within a session to two participants. This paper introduces Multiparty GV (MPGV), a functional language with multiparty session types, allowing concurrent interactions among several participants. MPGV upholds the strong guarantees of its ancestor GV, including deadlock freedom, despite session interleaving and delegation. MPGV has a novel redirecting construct for modular programming with first-class endpoints, thanks to which we give a type-preserving translation from binary session types to MPGV to show that MPGV is strictly more general than binary GV. All results in this paper have been mechanized using the Coq proof assistant. CCS Concepts: • Software and its engineering → Concurrent programming languages. Additional Key Words and Phrases: Session types, message-passing concurrency, deadlock freedom ACM Reference Format: Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. Proc. ACM Program. Lang. 6, ICFP, Article 107 (August 2022), 30 pages. https://doi.org/10.1145/3547638 1 INTRODUCTION Session types are a type discipline for message-passing concurrency. Originally developed in the context of process calculi by Honda [1993]; Honda et al. [1998], they were later generalized to object-oriented [Dezani-Ciancaglini et al. 2006] and functional languages [Gay and Vasconcelos 2010] leading to implementations in mainstream languages like Haskell [Pucella and Tov 2008; Imai et al. 2010; Lindley and Morris 2016a], Scala [Scalas and Yoshida 2016], OCaml [Padovani 2017; Imai et al. 2019], and Rust [Jespersen et al. 2015; Kokke 2019; Chen et al. 2022]. A particularly exciting development is the GV (łGood Variationž) session type family, pioneered by Gay and Vasconcelos [2010], later coined GV and refined by Wadler [2012], and further developed by e.g., Lindley and Morris [2015, 2016b, 2017]; Fowler et al. [2019, 2021]; Kokke and Dardha [2021b]; Jacobs et al. [2022a]. The GV family combines session types with functional programming by treating session-typed channels as first-class data, similar to references in ML. Channels can be stored in data structures (like lists), captured by closures, and sent along channels (even when contained in Authors’ addresses: Jules Jacobs, Radboud University Nijmegen, The Netherlands, mail@julesjacobs.com; Stephanie Balzer, Carnegie Mellon University, USA, balzers@cs.cmu.edu; Robbert Krebbers, Radboud University Nijmegen, The Netherlands, mail@robbertkrebbers.nl. This work is licensed under a Creative Commons Attribution 4.0 International License. © 2022 Copyright held by the owner/author(s). 2475-1421/2022/8-ART107 https://doi.org/10.1145/3547638 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:2 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers data structures, thus generalizing delegation). Similarly, the SILL family of session type languages [Toninho et al. 2013; Pfenning and Griffith 2015 ; Toninho 2015] integrates a process language via a contextual monad with an unrestricted functional language. Aside from a tight integration with functional programming, a key strength of GV and SILL representatives is that they do not only guarantee type safety (łwell-typed programs cannot get stuck due to illegal operationsž), but also deadlock freedom or global progress (łwell-typed programs cannot end up waiting for each otherž). This result follows from adopting a session initialization pattern based on cut, inspired by the Curry-Howard correspondence between linear logic and the session-typed 𝜋 -calculus [Caires and Pfenning 2010; Wadler 2012]. Such a pattern combines session creation and thread spawning to avoid deadlocks. The family of session types based on the pioneering work by Honda [1993]; Honda et al. [1998], in contrast, separates session creation from thread (process) spawning and thus does not prevent deadlocks. A cut-based initialization pattern also seamlessly integrates with channels as first-class data. The restriction of interactions to two participants, present in GV, SILL, and session types based on the pioneering work by Honda [1993]; Honda et al. [1998], led to the development of multiparty session types [Honda et al. 2008, 2016]. Multiparty session types allow an arbitrary but statically determined number of participants (łrolesž) to engage in a session. The key ingredient of multiparty session types is a global type that defines a protocol from the perspective of the entire session, from which local types for each participant can be generated. A global type not only increases expressivity but also establishes deadlock freedom for a system consisting of a single session. The development of GV-style session types and multiparty session types has mostly happened independently of each other. There exists no system that combines the flexibility of functional programming with the expressivity of multiparty session types. This paper introduces Multiparty GV (MPGV)Ða linear lambda calculus with first-class multiparty sessions and dynamic thread and channel initialization. Deadlock freedom is guaranteed purely by linear type checking and an 𝑛 -ary łforkž inspired by a cut-based initialization pattern. MPGV complements linear sessions with standard unrestricted functional types and language features, such as general recursive functions and algebraic data types. The integration of multiparty session types into a GV-style functional language brings a number of challenges: Deadlock freedom. Although global types guarantee deadlock freedom for a single multiparty session, global types alone cannot guarantee deadlock freedom for interleaved multiparty sessions. To establish deadlock freedom in the presence of dynamic session spawning and session delegation, where participants can engage in several multiparty sessions simultaneously, Kobayashi-style or ł ders/prioritiesž [ Kobayashi 1997, 2002, 2006] have been used to rule out cyclic dependencies among channel actions. The resulting interaction type systems [Coppo et al. 2013; Bettini et al. 2008; Coppo et al. 2016] are complementary in terms of expressivity compared to GV. They are more powerful in the sense that they allow cyclic communication topologies within and between sessions. However, well-typed programs in GV cannot be translated into these systems because orders/priorities are static and sessions are not first-class data. In this paper we take the GV approach to deadlock freedomÐMPGV features an 𝑛 -ary łforkž that combines the creation of 𝑛 threads and multiparty session for 𝑛 participants. While this makes the MPGV type system and operational semantics simple, proving that it in fact guarantees deadlock freedom is challenging. To handle dynamic thread and channel creation, direct-style deadlock freedom proofs of GV (like those by Lindley and Morris [2015]; Fowler et al. [2021]; Jacobs et al. [2022a]) crucially rely on the communication topology remaining acyclic during program execution. For multiparty session types this is not the caseÐthe communication topology between sessions is acyclic, but the communication topology within a session is not. The key insight of our work is Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:3 to represent the cyclic communication topology within sessions as an acyclic graph at the logical level, without needing central coordination in the operational semantics. Participant redirecting. Binary session types specify the types of data that is being sent and received, while local multiparty session types also specify the participants names to/from whom that data is received. These names make programming with first-class sessions non modular since the exact participants are fixed in type signatures. Suppose that one has library functions 𝑓 and 𝑔 such that 𝑓 returns a session of a certain session type, and 𝑔 expects an argument with that same session type, but with different participant names. We introduce a łredirectingž construct, which allows an endpoint to be passed to functions where different participant names are expected. Using this construct, we give a type-preserving translation from binary session types into MPGV, showing that MPGV restricted to two participants per session is at least as expressive as GV. Mechanization. The complexities of session types, especially in the multiparty setting, and the existence of published broken proofsÐincluding the failure of subject reduction for several multiparty systems [Scalas and Yoshida 2019a]Ðgave the impetus for mechanization. Whereas there exists extensive work on mechanizing the meta-theory of binary session types [Thiemann 2019; Rouvoet et al. 2020; Hinrichsen et al. 2021; Tassarotti et al. 2017; Goto et al. 2016; Ciccone and Padovani 2020; Castro-Perez et al. 2020; Gay et al. 2020], deadlock freedom for binary session types has only recently been mechanized by Jacobs et al. [2022a]. For multiparty session types, the only mechanization is Zooid by Castro-Perez et al. [2021], which mechanizes the trace semantics of a single multiparty session and proves that it conforms to its global type. In the spirit of this line of work, we provide a full mechanization of all our results in the Coq proof assistant. Contributions and outline. Our main contribution is MPGVÐthe first deadlock-free linear lambda calculus with first-class multiparty sessions, dynamic thread and channel initialization, and functional features like general recursive functions and algebraic data types. Concretely: • We explain the key ideas behind MPGV in the context of new and existing examples (ğ2 ). • We formalize the type system and operational semantics of MPGV (ğ3 ). • We give a type-preserving embedding of GV-style binary session types into MPGV, using our new redirecting construct, showing that MPGV goes strictly beyond binary session types (ğ4 ). • We prove a combined partial deadlock and memory-leak freedom theorem for multiparty session types that also subsumes type safety and global progress (ğ5 and ğ7 ). • Inspired by Scalas and Yoshida [2019a], we extend MPGV with a more flexible notion of consis- tency that does not rely on global types (ğ6 ). • We mechanize all our results in the Coq proof assistant (ğ8 ). 2 MPGV BY EXAMPLE We introduce MPGV’s features, based on examples (ğ2.1 ś ğ2.8 ), and provide the main intuitions for how MPGV guarantees deadlock freedom for cyclic intra-session topologies (ğ2.9 ). 2.1 Global and Local Types Similar to original multiparty session types [Honda et al. 2008], sessions in MPGV can be described by a global type. A simple example of a global type is: 𝐺 ≜ [0 → 1]N.[1 → 2]N.[2 → 0]N.End. This global type says that participant 0 first sends a value of natural number type N to participant 1, then 1 sends a N to 2, then 2 sends a N to 0, and finally the protocol ends. The global type 𝐺 induces Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:4 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers local types for each participant 𝑝 via projections 𝐺 ⇂ 𝑝 : 𝐺 ⇂ 0 = ![1]N.?[2]N.End 𝐺 ⇂ 1 = ?[0]N.![2]N.End 𝐺 ⇂ 2 = ?[1]N.![0]N.End The local type ![𝑝 ]𝜏.𝐿 indicates that the next action should be sending a value 𝑣 of type 𝜏 to participant 𝑝 , to then continue with 𝐿 . Dually, ?[𝑝 ]𝜏.𝐿 indicates that the next action should be receiving a value 𝑣 of type 𝜏 from participant 𝑝 , to then continue with 𝐿 . Finally, End states that the protocol has finished and the participant’s endpoint should be closed. 2.2 Combined Session and Channel Initialization With our simple global type 𝐺 at hand, we now give a program that implements this global type: let 𝑐 : ![1]N.?[2]N.End = fork(service , service ) in 0 1 2 let 𝑐 : ?[2]N.End = send[1](𝑐 , 99) in 0 0 let (𝑐 ,𝑛 ) : End × N = receive[2](𝑐 ) in 0 0 close(𝑐 ) The fork operation simultaneously forks off 2 threads and creates 3 channel endpoints for the participants in the session. The fork returns endpoint 𝑐 with type 𝐺 ⇂ 0 = ![1]N.?[2]N.End, and runs functions service and service (shown below) in background threads. The main thread uses 1 2 send[1](𝑐 , 99) to send the message ł 99ž to participant 1 ( i.e., service ). As is common in functional 0 1 session-typed languages, the send and receive operations of MPGV return the endpoint back to us. The returned endpoint will be at a different type, because the step has been taken in the session type. For convenience, the above code let-binds the returned endpoint to the same name. The main thread then uses the operation receive[2](𝑐 ) and blocks to receive a message from endpoint 2 (i.e., service ). After the message has been received, it closes the endpoint using close. Similar to many multiparty session-type systems, MPGV uses numbers for participant names in send and receive to indicate which other participant the communication concerns. Note that also for receive it is necessary to indicate which participant to receive from, because multiple participants could send a message to the same participant simultaneously, and these messages may have different types. The endpoint returned from fork has participant number 0, and endpoints of the forked-off threads have participant numbers 1, 2, etc. The forked-off threads could be implemented as: service : (?[0]N.![2]N.End) → 1 service : (?[1]N.![0]N.End) → 1 1 2 service 𝑐 ≜ let (𝑐 ,𝑛 ) = receive[0](𝑐 ) in service 𝑐 ≜ let (𝑐 ,𝑛 ) = receive[1](𝑐 ) in 1 1 1 1 2 2 2 2 let 𝑐 = send[2](𝑐 ,𝑛 + 3) in let 𝑐 = send[0](𝑐 ,𝑛 + 4) in 1 1 2 2 close(𝑐 ) close(𝑐 )) 1 2 The arguments of fork are closures that take the endpoint (typed with local type𝐺 ⇂ 𝑝 ) as argument and return the unit value when done. The first forked-off thread service tries to receive a message from participant 0 (i.e., the main thread), increments the received number, and passes it on to endpoint 2 (i.e., service ). Similarly, the second forked-off thread service receives a number from 2 2 participant 1 (i.e., service ), increments it, and passes it to participant 0 (i.e., the main thread). Novel elements of MPGV. The 𝑛 -ary fork ensures that the communication topology between sessions remains acyclic. This is in contrast to original multiparty session-type systems [Honda et al. 2008], which use service names to create new sessions between already existing, concurrently running processes, selecting the participating processes non-deterministically in case there are several attempting to participate (see ğ9 for an in-depth discussion). By separating session creation from thread spawning in these original systems, cyclic communication topologies can be created, and hence interleaved sessions can deadlock. Inspired by binary session-typed lambda-calculi like GV [Wadler 2012; Lindley and Morris 2015] and multi-cut with coherence proofs [Carbone et al. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:5 2015, 2016, 2017], MPGV combines session creation with thread spawning, to maintain acyclicity of the communication topology and guarantee deadlock freedom. 2.3 Interleaving and First-Class Endpoints We now illustrate MPGV’s support for session interleaving and delegation. Similar to the original versions of GV by Gay and Vasconcelos [2010]; Wadler [2012], MPGV obtains delegation without the need for special language constructs since endpoints are first class. We modify the example from ğ2.2 , which performs its communication actions on 𝑐 locally, by letting the main thread fork off yet another thread to perform the communication: let 𝑐 : 𝐺 ⇂ 0 = fork(service , service ) in 0 1 2 ′ ′ let 𝑑 : 𝐺 ⇂ 0 = fork(𝑑𝜆 : 𝐺 ⇂ 1. let (𝑑 ,𝑥 ) : (![0]N.End) × (𝐺 ⇂ 0) = receive[0](𝑑 ) in 0 1 1 1 let 𝑥 : ?[2]N.End = send[1](𝑥, 99) in let (𝑥,𝑛 ) : End × N = receive[2](𝑥 ) in let 𝑑 : End = send[0](𝑑 ,𝑛 ) in 1 1 close(𝑥 ); close(𝑑 )) in let 𝑑 : ?[1]N.End = send[1](𝑑 ,𝑐 ) in 0 0 0 let (𝑑 ,𝑛 ) : End × N = receive[1](𝑑 ) in 0 0 close(𝑑 ) To type the second fork, we need to come up with a second global type that governs the communi- cation between the third forked-off thread and the main thread: 𝐺 ≜ [0 → 1](𝐺 ⇂ 0).[1 → 0]N.End where 𝐺 ⇂ 0 = ![1]N.?[2]N.End ′ ′ The projections are 𝐺 ⇂ 0 = ![1](𝐺 ⇂ 0).?[1]N.End and 𝐺 ⇂ 1 = ?[0](𝐺 ⇂ 0).![0]N.End. This global type shows that participant 0 (the main thread) of 𝐺 first delegates an endpoint with local type 𝐺 ⇂ 0 to participant 1 of 𝐺 (the third forked-off thread), which then sends a natural number back. In the code, the main thread sends endpoint 𝑐 , which the third forked-off thread receives as 𝑥 . The third forked-off thread then executes the communication according to local type 𝐺 ⇂ 0, and sends back a natural number to the main thread. Novel elements of MPGV. As demonstrated by the above example, MPGV’s session-typed endpoints are first class and can thus be sent over channels ( i.e., delegated) like any other data. MPGV not only allows sending single endpoints over channels, but also lists of endpoints (ğ2.8 ) or closures, which may capture endpoints. Data types that contain endpoints are treated linearly in order to protect type safety, whereas data types that cannot contain endpoints (e.g., lists of natural numbers) may be freely copied and discarded. MPGV guarantees deadlock freedom in the presence of interleaved sessions solely by linear typing and 𝑛 -ary fork, and without any extrinsic mechanisms like orders/priorities [Bettini et al. 2008; Coppo et al. 2013, 2016]. 2.4 Participant Redirecting In the example from ğ2.2 we have two threads service and service that were doing more or less the 1 2 same thing (adding 3 and 4, respectively). To obtain a language that enables modular programming, we would like to write a single function that generalizes both services that we could use for both threads in the fork operation. Let us try to make an attempt: service : N → (?[0]N.![1]N.End) → 1 service 𝑎 𝑐 ≜ let (𝑐,𝑛 ) = receive[0](𝑐 ) in let 𝑐 = send[1](𝑐,𝑛 + 𝑎 ) in close(𝑐 ) Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:6 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers The function service takes a natural number 𝑎 for the value that should be added. Unfortunately, service 3 and service 4 cannot readily be used because their types do not match up with 𝐺 ⇂ 1 = ?[0]N.![2]N.End and 𝐺 ⇂ 2 = ?[1]N.![0]N.End since the participant numbers are off. MPGV provides a redirect[𝜋 ](𝑐 ) operation that allows us to locally redirect participant numbers, making it possible for a programmer to pass endpoints to destinations where different participant numbers are expected in the type signature. The informal semantics of the redirect operation is that any send[𝑝 ] and receive[𝑝 ] operations on 𝑐 = redirect[𝜋 ](𝑐 ) get redirected to send[𝜋 (𝑝 )] and receive[𝜋 (𝑝 )] on 𝑐 . With MPGV’s redirect operation at hand, we can change the fork in the first line of the example in ğ2.2 into: fork(𝑐𝜆 . service 3 (redirect[0 ↦→ 0, 1 ↦→ 2](𝑐 )),𝑐𝜆 . service 4 (redirect[0 ↦→ 1, 1 ↦→ 0](𝑐 ))) 1 1 2 2 Novel elements of MPGV. Redirecting is a novel concept that has not been explored in multiparty session types to our knowledge. Redirecting is important for modularity because it allows composing a function 𝑓 with a function 𝑔 with compatible range and domain types even when participant numbers are at odds. Redirecting is also crucial for embedding binary sessions in MPGV; without redirecting, that would not be possible (see ğ4 ). 2.5 Choice and Recursive Session Types Similar to traditional (multiparty) session types, MPGV supports choice and recursion. For example: ′′ ′′ 𝐺 ≜ [0 → 1]{𝐴 : N.𝐺 , 𝐵 : string.End} In this global type, participant 0 sends participant 1 a choice label {,𝐴 𝐵 }. If the choice label is 𝐴 , then the payload of the message is of type N, and the protocol recursively loops back to the initial state. If the choice label is 𝐵 , then the payload of the message is of type string, and then the protocol ends. This gives the following local projections: ′′ ′′ ′′ ′′ 𝐺 ⇂ 0 ≜ ![1]{𝐴 : N.(𝐺 ⇂ 0), 𝐵 : string.End} 𝐺 ⇂ 1 ≜ ?[0]{𝐴 : N.(𝐺 ⇂ 1), 𝐵 : string.End} With choice, not all global types one can write down are valid: all the branches of a choice must have equal projections for participants that are neither the sender nor the receiver of the choice. This is to ensure that each participant always has enough information to determine the type of the next message that they should send or expect to receive [Honda et al. 2008, 2016]. MPGV supports recursive functions, which are crucial to provide implementations of recursive session types. 2.6 Two Buyer Protocol The two buyer protocol is a classic example from the literature [Honda et al. 2008] with two buyers (Alice and Bob) and a Seller. The protocol has the following global type in MPGV (we use symbolic participant identifiers for readability; one can take 𝑆 = 0, 𝐴 = 1, 𝐵 = 2): 𝐺 ≜ [𝐴 → 𝑆 ]string.[𝑆 → 𝐴 ]N. [𝑆 → 𝐵 ]N.[𝐴 → 𝐵 ]N. 𝑆𝐴𝐵 [𝐵 → 𝑆 ]{Yes : [𝑆 → 𝐵 ]date. End, No : End} This global protocol has the following projections for Alice, Bob, and Seller: 𝐺 ⇂ 𝐴 = ![𝑆 ]string.?[𝑆 ]N.![𝐵 ]N.End 𝑆𝐴𝐵 𝐺 ⇂ 𝐵 = ?[𝑆 ]N.?[𝐴 ]N.![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End} 𝑆𝐴𝐵 𝐺 ⇂ 𝑆 = ?[𝐴 ]string.![𝐴 ]N.![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End} 𝑆𝐴𝐵 The participants perform the following interactions: (1) Alice tells the Seller which item she wants to buy ([𝐴 → 𝑆 ]string). (2) The Seller tells both Alice and Bob how much the item costs ([𝑆 → 𝐴 ]N. [𝑆 → 𝐵 ]N). Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:7 (3) Alice tells Bob how much money she is willing to contribute to the purchase ([𝐴 → 𝐵 ]N). (4) Bob decides whether they can afford the item, and informs the Seller of his decision ( [𝐵 → 𝑆 ]{Yes : . . ., No : . . .}). (5) If Bob says Yes, the Seller sends Bob the date at which the item will be delivered and then ends the protocol ([𝑆 → 𝐵 ]date.End). (6) If Bob says No, the protocol ends immediately (End). A possible implementation of the Seller is as follows: seller : 𝐺 ⇂ 𝑆 → 1 𝑆𝐴𝐵 seller 𝑐 ≜ let (𝑐 ,𝑖𝑡𝑒𝑚 ) : (![𝐴 ]N.![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) × string = receive[𝐴 ](𝑐 ) in 𝑆 𝑆 let 𝑐 : ![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) = send[𝐴 ](𝑐 , cost(𝑖𝑡𝑒𝑚 )) in 𝑆 𝑆 let 𝑐 : ?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) = send[𝐵 ](𝑐 , cost(𝑖𝑡𝑒𝑚 )) in 𝑆 𝑆 match receive [𝐵 ](𝑐 ) with { ⟨Yes :𝑐 : ![𝐵 ]date.End⟩ ↦→ let 𝑐 : End = send[𝐵 ](𝑐 , date(𝑖𝑡𝑒𝑚 )) in close(𝑐 ) 𝑆 𝑆 𝑆 𝑆 ⟨No :𝑐 : End⟩ ↦→ close(𝑐 ) 𝑆 𝑆 In the case ⟨Yes :𝑐 ⟩, we have 𝑐 : ![𝐵 ]date.End, whereas in case ⟨No :𝑐 ⟩ we have 𝑐 : End, so the 𝑆 𝑆 𝑆 𝑆 type of the endpoint depends on which choice was made by Bob. Assuming that we also have functions alice : 𝐺 ⇂ 𝐴 → 1 and bob : 𝐺 ⇂ 𝐵 → 1 for Alice and Bob, we can run the two 𝑆𝐴𝐵 𝑆𝐴𝐵 buyer protocol with program seller (fork(alice, bob)). 2.7 Three Buyer Protocol and Session Delegation The two buyer example has been extended with delegation by Honda et al. [2008]. To help Alice and Bob, there is a fourth person, Carol. If Bob and Alice cannot afford the item together, then instead of replying No to the Seller, Bob will send the remainder of his session to Carol (i.e., delegation). Carol will then respond Yes to the Seller, if the three of them together have enough money. This is modeled by a separate session between Bob and Carol with global type: 𝐺 ≜ [𝐵 → 𝐶 ](N × ![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}).End 𝐶𝐵 Because Bob needs access to Carol, his function is parameterized by that endpoint 𝑐 as well as his own endpoint 𝑐 in the two buyer protocol between him, Alice, and the Seller: bob : 𝐺 ⇂ 𝐵 → 𝐺 ⇂ 𝐵 → 1 del 𝐶𝐵 𝑆𝐴𝐵 bob 𝑐 𝑐 ≜ let (𝑐 ,𝑐𝑜𝑠𝑡 ) : (?[𝐴 ]N.![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}) × N = receive[𝑆 ](𝑐 ) in del 𝐶 𝐵 𝐵 𝐵 let (𝑐 ,𝑐𝑜𝑛𝑡𝑟𝑖𝑏 ) : (![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}) × N = receive[𝐴 ](𝑐 ) in 𝐵 𝐴 𝐵 if 𝑐𝑜𝑠𝑡 − 𝑐𝑜𝑛𝑡𝑟𝑖𝑏 < 𝑚𝑎𝑥 then let 𝑐 : ?[𝑆 ]date.End = send[𝑆 ](𝑐 , ⟨𝑌𝑒𝑠 ⟩) in 𝐵 𝐵 let (𝑐 ,𝑑𝑎𝑡𝑒 ) : End × date = receive[𝑆 ](𝑐 ) in 𝐵 𝐵 close(𝑐 ) else let 𝑐 : End = send[𝐶 ](𝑐 , (𝑐𝑜𝑠𝑡 − 𝑐𝑜𝑛𝑡𝑟𝑖𝑏 − 𝑚𝑎𝑥 ,𝑐 )) in 𝐶 𝐶 𝐴 𝐵 𝐵 close(𝑐 ) In the else branch, Bob sends his endpoint 𝑐 over his connection to Carol, 𝑐 . We can run the three 𝐵 𝐶 buyer protocol with the following program, assuming that we have carol : 𝐺 ⇂ 𝐶 → 1: 𝐶𝐵 let 𝑐 : 𝐺 ⇂ 𝐵 = fork(carol) in 𝐶 𝐶𝐵 seller (fork(alice, bob 𝑐 )) del 𝐶 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:8 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝐴 𝐴 𝐴 { { { 𝐶 𝐶 𝐶 𝐶 𝑆 𝐵 𝑆 𝐵 𝑆 𝑆 𝐴 𝐴 𝐴 { { { 𝑆 𝐶 𝑆 𝐶 𝑆 𝐶 𝑆 𝐶 1 1 1 1 𝑆 𝑆 𝑆 𝐵 2 𝑆 𝐵 2 𝑆 𝑆 Fig. 1. Steps in three buyer protocol. Top: physical communication paths; bottom: logical connectivity. Depending on thread scheduling, operations can be executed in a different order. One possible execution is graphically depicted in the top row of Figure 1. In the left picture, we have the session between 𝐴 , 𝐵 , and 𝑆 , and the session between 𝐵 and 𝐶 . In our operational semantics, the participants are connected directly, and each participant has their own set of buffers in the heap, separate from the others. At some point Bob decides to send his session to Carol (second picture), so the connections of 𝐵 get moved to 𝐶 . Bob then ends his session with Carol (third picture). Alice ends her participation in the session (fourth picture). This deletes her buffers from the heap, even though the Seller and Carol may still be actively communicating. The global type ensures that whenever Alice is allowed to close her session, the other participants are guaranteed not to perform further communication with her. 2.8 Endpoints in Data Structures Because of the functional nature of MPGV, we can freely intermix sessions and data structures. We give an example of a department store, to which we can send several buyers in a list. The department store will then let the buyers interact by applying the 𝑠𝑒𝑙𝑙𝑒𝑟 function for us. To illustrate recursive protocols, the department store loops around and accepts new buyers: departmentstore : (𝜇𝑥. ?[𝐶 ]List(𝐺 ⇂ 𝑆 ).𝑥 ) → 1 𝑆𝐴𝐵 departmentstore 𝑐 ≜ let (𝑐 ,𝑒𝑑𝑛𝑝𝑜𝑖𝑛𝑡𝑠 ) = receive[𝐶 ](𝑐 ) in 𝐷 𝐷 𝐷 map seller 𝑒𝑑𝑛𝑝𝑜𝑖𝑛𝑡𝑠 ; departmentstore 𝑐 Given a function buyers : string → 𝐺 ⇂ 𝑆 that starts up the two or three buyers trying to buy 𝑆𝐴𝐵 an item of the given name and returns the seller’s endpoint to interact with them, we can start a department store and send buyers to it as follows: let store = fork(departmentstore) in let 𝑐 = buyers ł ℎ𝑎𝑡 ” in let 𝑐 = buyers ł 𝑐𝑜𝑤 ” in let store = send[𝐷 ](store, [𝑐 ;𝑐 ]) in 1 2 let 𝑐 = buyers ł 𝑔𝑒𝑔 ” in let 𝑐 = buyers ł 𝑏𝑜𝑤 ” in let store = send[𝐷 ](store, [𝑐 ;𝑐 ]) in . . . 3 4 Novel elements of MPGV. MPGV allows multiparty endpoints to be stored in data structures, and captured in closures, which can then be sent as messages. This is in contrast to earlier multiparty systems, where endpoints can either not be manipulated at all [Castro-Perez et al. 2021], or where Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:9 there is a separate syntactic category for endpoints, which cannot be mixed with data [Honda et al. 2008; Coppo et al. 2016; Bettini et al. 2008; Coppo et al. 2013]. 2.9 Deadlock Freedom of MPGV MPGV’s deadlock freedom proof is based on two key ideas: (1) local progress within a session is guaranteed by the global type, and (2) global progress between sessions is guaranteed by our 𝑛 -ary fork and linear typing, asserting that the communication topology between sessions remains acyclic (despite first-class endpoints). To reason about deadlock freedom we abstract a logical connectivity topology from the physical communication topology and prove that the logical connectivity topology remains acyclic. The logical topology of the three buyer protocol is depicted in the bottom row of Figure 1. It introduces a blue circle for each multiparty session, abstracting over the cyclic topology within a session and exposing the acyclicity of the logical topology. Figure 1 shows that the logical connectivity topology remains acyclic throughout the execution. This holds for any well-typed MPGV programÐ Figure 10 in ğ 7 shows how the logical topology is transformed and remains acyclic for each of the session operations. Novel elements of MPGV. Similar to binary variants of GV, MPGV ensures global progress and deadlock freedom for an entire program, solely by linear typing. In contrast, earlier multiparty systems either guarantee deadlock freedom only for a single session [Castro-Perez et al. 2021; Honda et al. 2008], or for multiple sessions if types are augmented with extrinsic orders/priorities [Coppo et al. 2016; Bettini et al. 2008; Coppo et al. 2013]. Moreover, our global progress and deadlock freedom theorems are mechanized in Coq (ğ5 ). 3 THE SEMANTICS OF MPGV 3.1 Syntax and Operational Semantics Each configuration in our small-step operational semantics consists of a thread pool and heap, which stores a vector of buffers for each endpoint: fin fin 𝜌 ∈ Cfg ≜ List Expr × Heap ℎ ∈ Heap ≜ Endpoint −⇀ (Participant −⇀ List (Label ×Val)) :: An endpoint 𝑐 ∈ Endpoint = (𝑠,𝑝 ) consists of a number 𝑠 ∈ Session identifying the session, and a number 𝑝 ∈ Participant identifying the participant number of the endpoint in the session. The operational semantics has three reduction relations. Firstly, 𝑒 { 𝑒 for pure reductions pure ′ ′ of expressions. Secondly, (𝑒,ℎ ) { (𝑒 ,ℎ ,𝑒®) for reductions of channel operations involving the head heap ℎ, with the option to spawn a list of new threads 𝑒® (a non-empty list for fork, and an empty ′ ′ list for the other operations). Thirdly, (𝑒,®ℎ ) { (𝑒® ,ℎ ) between configurations, which performs cfg { on some thread in the thread pool, and also handles evaluation contexts. The formal syntax head and operational semantics of MPGV can be found in Figure 2. We give an informal description of the semantics of the message-passing operations fork, send, receive, close, and redirect next. Fork. The fork operation fork(𝑣 , . . .,,𝑣 ) spawns 𝑛 threads and creates a new session between 1 𝑛 the 𝑛 + 1 endpoints. The session 𝑠 has (𝑛 + 1) × (𝑛 + 1) buffers in the heap ℎ for the 𝑛 + 1 endpoints, such that the buffer stored at ℎ(𝑠,𝑞 )(𝑝 ) queues messages sent from 𝑝 to 𝑞 . Session endpoints 𝑐 are represented as triples 𝑐 = #[(𝑠,𝑝 ), 𝜋 ] of a session address 𝑠 ∈ Session, endpoint number fin 𝑝 ∈ Participant, and translation vector 𝜋 : Participant −⇀ Participant, which is used for redirecting and initialized by fork to be the identity mapping. Each of the values 𝑣 passed as arguments to fork must be a closure that accepts an endpoint as its argument, so that the threads run function calls 𝑣 #[(𝑠,𝑖 ), id] for 𝑖 = 1..𝑛 . The fork returns endpoint #[(𝑠, 0), id]. A usage pattern is: let 𝑐 = fork((𝑐𝜆 . 𝑒 ), . . ., (𝑐𝜆 . 𝑒 )) in 𝑒 0 1 1 𝑛 𝑛 0 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:10 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Expressions, values, and evaluation contexts :: 𝑒 ∈ Expr = 𝑥 | () | 𝑛 | (𝑒,𝑒 ) | ⟨ℓ :𝑒 ⟩ | 𝜆𝑥. 𝑒 | rec 𝑓 𝑥. 𝑒 | 𝑒 𝑒 | fork(𝑒, . . .,𝑒 ) | send[𝑝 ](𝑒, ℓ :𝑒 ) | receive[𝑝 ](𝑒 ) | close(𝑒 ) | redirect[𝜋 ](𝑒 ) | let 𝑥 = 𝑒 in 𝑒 | let (𝑥 ,𝑥 ) = 𝑒 in 𝑒 | match 𝑒 with {⟨ℓ :𝑥 ⟩ ↦→ 𝑒 ; . . .} 1 2 ℓ ∈𝐼 𝑣 ∈Val ::= () | 𝑛 | (𝑣,𝑣 ) | ⟨ℓ :𝑣 ⟩ | 𝜆𝑥. 𝑒 | rec 𝑓 𝑥. 𝑒 | #[𝑐, 𝜋 ] 𝐾 ∈ Ctx ::= □ | (𝐾,𝑒 ) | (𝑣,𝐾 ) | 𝐾 𝑒 | 𝑣 𝐾 | let 𝑥 = 𝐾 in 𝑒 | · · · Data structures 𝑠 ∈ Session ≜ N 𝑐 ∈ Endpoint ≜ Session × Participant fin 𝑝,𝑞 ∈ Participant ≜ N 𝜋 ∈ Translation ≜ Participant −⇀ Participant fin fin ℓ ∈ Label ≜ N ℎ ∈ Heap ≜ Endpoint −⇀ (Participant −⇀ List (Label ×Val)) 𝜌 ∈ Cfg ≜ List Expr × Heap Small-step operational semantics (𝑒 ,ℎ) { (𝑒 ,ℎ,𝜖 ) (if 𝑒 { 𝑒 ) 1 head 2 1 pure 2 (fork(𝑣 , . . .,𝑣 ),ℎ) { (#[(𝑠, 0), id],ℎ ⊎ {(𝑠, 0) ↦→ 𝜖,®. . ., (𝑠,𝑛 ) ↦→ 𝜖®}, 1 𝑛 head [𝑣 #[(𝑠, 1), id], . . .,𝑣 #[(𝑠,𝑛 ), id]]) 1 𝑛 (send[𝑞 ](#[(𝑠,𝑝 ), 𝜋 ], ℓ :𝑣 ),ℎ) { (#[(𝑠,𝑝 ), 𝜋 ], push((𝑠, 𝜋 (𝑞 )),𝑝, ⟨ℓ :𝑣 ⟩ ,ℎ),𝜖 ) head (receive[𝑝 ](#[(𝑠,𝑞 ), 𝜋 ]),ℎ) { (⟨ℓ : (𝑣, #[(𝑠,𝑞 ), 𝜋 ])⟩ ,ℎ ,𝜖 ) head ⟨ ⟩ (if pop((𝑠,𝑞 ), 𝜋 (𝑝 ),ℎ) = ( ℓ :𝑣 ,ℎ )) (close(#[(𝑠,𝑝 ), 𝜋 ]),ℎ) { ((),ℎ\{(𝑠,𝑝 )},𝜖 ) head (redirect[𝜋 ](#[(𝑠,𝑝 ), 𝜋 ]),ℎ) { (#[(𝑠,𝑝 ), 𝜋 ◦ 𝜋 ],ℎ,𝜖 ) 1 2 head 2 1 ′ ′ ′ ′ (𝑒 ® ++ [𝐾 [ 𝑒 ]] ++ 𝑒 ® ,ℎ) { (𝑒 ® ++ [𝐾 [ 𝑒 ]] ++ 𝑒 ® ++ 𝑒,®ℎ ) (if (𝑒,ℎ ) { (𝑒 ,ℎ ,𝑒®)) 𝑎 𝑏 cfg 𝑎 𝑏 head Fig. 2. Syntax and operational semantics of MPGV (selected rules). Send. The send operation send[𝑞 ](𝑐, ℓ : 𝑣 ) sends the message ⟨ℓ :𝑣 ⟩ to 𝑞 via the endpoint 𝑐 = #[(𝑠,𝑝 ), 𝜋 ] by adding the message to the end of buffer (using the operation push((𝑠, 𝜋 (𝑞 )),𝑝, ⟨ℓ :𝑣 ⟩ ,ℎ) in Figure 2). The message is tagged with a label ℓ, which can influence the future actions allowed to be performed by the participant. We revisit this in detail when we introduce the typing rules. Our send operation is asynchronous. One can encode synchronous communication by inserting after each message 𝐴 → 𝐵 a dummy message 𝐵 → 𝐴 with type unit to enforce synchronization. Receive. The receive operation receive[𝑝 ](𝑐 ) receives a message from 𝑝 via endpoint 𝑐 = #[(𝑠,𝑞 ), 𝜋 ]. The receive operation takes the first message out of buffer (using the operation pop((𝑠,𝑞 ), 𝜋 (𝑝 ),ℎ) = (⟨ℓ :𝑣 ⟩ ,ℎ ) in Figure 2). If the buffer is empty, the operation blocks until a message becomes available. Close. The close operation close(𝑐 ) deletes all the buffers from which the endpoint 𝑐 = #[(𝑠,𝑞 ), 𝜋 ] receives messages, that is, it simply deletes entry ℎ((𝑠,𝑞 )) of the heap. fin Redirect. The redirecting operation 𝑐 = redirect[𝜋 ](𝑐 ) where 𝜋 ∈ Participant −⇀ Participant redirects messages so that send and receive operations to 𝑝 on 𝑐 are redirected to 𝜋 (𝑝 ) on 𝑐 . Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:11 Γ ⊥ Γ Γ ⊢ 𝑒 :𝜏 ⇒ = 𝜏 Γ ⊢ 𝑒 :𝜏 (⇒ =) ∈ {→,−◦} 1 2 1 1 1 2 2 2 1 Γ unr 𝑥 ∉ Γ {𝑥 ↦→ 𝜏 } ∪ Γ ⊢ 𝑥 :𝜏 Γ ∪ Γ ⊢ 𝑒 𝑒 :𝜏 1 2 1 2 2 Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 𝑥 ∉ Γ Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 Γ unr 𝑥 ∉ Γ 1 2 1 2 Γ ⊢ 𝜆𝑥. 𝑒 :𝜏 −◦ 𝜏 Γ ⊢ 𝜆𝑥. 𝑒 :𝜏 → 𝜏 1 2 1 2 Γ ∪ {𝑓 ↦→ (𝜏 → 𝜏 ),𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 Γ unr 𝑓 ,𝑥 ∉ Γ Γ ⊢ 𝑒 :𝜏 1 2 1 2 ℓ Γ ⊢ rec 𝑓 𝑥. 𝑒 :𝜏 → 𝜏 Γ ⊢ ⟨ℓ :𝑒 ⟩ :Σ . 𝜏 1 2 ℓ ∈𝐼 ℓ Γ ⊥ Γ Γ ⊢ 𝑒 :Σ . 𝜏 ∀ℓ ∈ 𝐼. Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 𝑥 ∉ Γ (𝐼 = ∅ =⇒ Γ = ∅) 1 2 1 ℓ ∈𝐼 ℓ 2 ℓ ℓ ℓ ℓ 2 2 Γ ∪ Γ ⊢ match 𝑒 with {⟨ℓ :𝑥 ⟩ ↦→ 𝑒 ; . . .} :𝜏 1 2 ℓ ℓ ℓ ∈𝐼 Γ ⊥ · · · ⊥ Γ consistent(𝐿 , 𝐿 , . . ., 𝐿 ) ∀𝑝 ∈ {1..𝑛 }. Γ ⊢ 𝑒 :𝐿 −◦ 1 Γ ⊢ 𝑒 :End 1 𝑛 0 1 𝑛 𝑝 𝑝 𝑝 Γ ∪ · · · ∪ Γ ⊢ fork(𝑒 , . . .,𝑒 ) :𝐿 Γ ⊢ close(𝑒 ) :1 1 𝑛 1 𝑛 0 Γ ⊥ Γ Γ ⊢ 𝑒 :![𝑝 ]{ℓ : 𝜏 . 𝐿 } Γ ⊢ 𝑒 :𝜏 Γ ⊢ 𝑒 :?[𝑝 ]{ℓ : 𝜏 . 𝐿 } 1 2 1 1 ℓ ℓ ℓ ∈𝐼 2 2 ℓ ℓ ℓ ℓ ∈𝐼 Γ ∪ Γ ⊢ send[𝑝 ](𝑒 , ℓ :𝑒 ) :𝐿 Γ ⊢ receive[𝑝 ](𝑒 ) :Σ . 𝜏 × 𝐿 1 2 1 2 ℓ ℓ ∈𝐼 ℓ ℓ Γ ⊢ 𝑒 :𝜋 (𝐿 ) Γ ⊢ redirect[𝜋 ](𝑒 ) :𝐿 Fig. 3. Selected MPGV typing rules. Operationally, this composes the translation vector of 𝑐 with 𝜋 : redirect[𝜋 ](#[(𝑠,𝑝 ), 𝜋 ]) = #[(𝑠,𝑝 ), 𝜋 ◦ 𝜋 ] 1 2 2 1 For details, see Figure 2. This operation is required to make multiparty sessions formally subsume binary sessions (ğ4 ), but is independently useful for modular programming with first-class endpoints (ğ2.4 ), because it allows the programmer to pass endpoints to destinations where different endpoint numbers are expected in the type signature. 3.2 Static Type System The functional layer of MPGV features base types, products, closures, sums, and equi-recursive types [Crary et al. 1999]. The message-passing layer of MPGV features multiparty sessions with n-ary choice. Formally the types of MPGV are given by: :: 𝜏 ∈ Type = 1 | N | 𝜏 × 𝜏 | 𝜏 −◦ 𝜏 | 𝜏 → 𝜏 | Σ . 𝜏 | 𝐿 ℓ ∈𝐼 ℓ (𝑐𝑜𝑖𝑑𝑛 ) :: 𝐿 ∈ LType = ![𝑝 ]{ℓ : 𝜏 . 𝐿 } | ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } | End ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) The functional types 𝜏 and local session types 𝐿 are mutually defined: functional types occur as messages in local types, and local types are functional types. To support equi-recursive types, we define Type and LType coinductively, allowing types to refer to themselves [Crary et al. 1999; Gay et al. 2020; Jacobs et al. 2022a; Castro-Perez et al. 2021; Keizer et al. 2021]. Mutually recursive functional types and local types can be constructed using corecursion in the meta logic (i.e., Coq), so Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:12 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers there is no explicit recursion operator. We use = to denote coinductive equivalence (i.e., bisimulation). The typing rules for MPGV’s judgment Γ ⊢ 𝑒 :𝜏 are displayed in Figure 3. 3.2.1 Unrestricted Types. We have linear function types 𝜏 −◦ 𝜏 , which must be used exactly once, 1 2 and whose lambda expressions can capture linear data. We also have unrestricted functions 𝜏 → 𝜏 , 1 2 which can be used any number of times (incl. zero times), but whose lambda expressions cannot capture linear data. We define the subset UType ⊆ Type of unrestricted types as: 𝜏 ˜ ∈ UType ::= 1 | N | 𝜏 ˜ × 𝜏 ˜ | 𝜏 → 𝜏 | Σ . 𝜏 ˜ ℓ ∈𝐼 ℓ (𝑐𝑜𝑖𝑑𝑛 ) Note that 𝜏 → 𝜏 is always unrestricted, even if 𝜏 and 𝜏 are restricted, because closures of 1 2 1 2 unrestricted function type cannot contain endpoints. To support linear and unrestricted types in the typing judgment, context disjointness Γ ⊥ Γ is 1 2 defined such that if Γ and Γ both contain variable 𝑥 , the two contexts must assign equal types 1 2 to 𝑥 (i.e., Γ (𝑥 ) = Γ (𝑥 )), and the type they assign to 𝑥 must be an unrestricted type. This ensures 1 2 that the union operation Γ ∪ Γ on contexts is well-defined whenever it is used in the typing rules 1 2 (for instance, if Γ = {𝑥 : N;𝑦 : N} and Γ = {𝑦 : N}, then Γ ∪ Γ = {𝑥 : N;𝑦 : N}). A context is 1 2 1 2 unrestricted if all its types are unrestricted. 3.2.2 Local Types. Local types describe the protocol that an endpoint 𝑐 must follow: • If 𝑐 : ![𝑝 ]{ℓ : 𝜏 . 𝐿 } then the next action on 𝑐 has to be send[𝑝 ](𝑐, ℓ :𝑣 ), and 𝑣 : 𝜏 and the ℓ ℓ ℓ ∈𝐼 ℓ continuation type 𝐿 of 𝑐 is determined by the sent label ℓ ∈ 𝐼 . • If 𝑐 : ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } then the next action on 𝑐 has to be receive[𝑝 ](𝑐 ), and the received label ℓ ℓ ℓ ∈𝐼 ℓ ∈ 𝐼 determines the type 𝜏 of the value received and the next type 𝐿 of 𝑐 . ℓ ℓ • If 𝑐 : End then the next action on 𝑐 must be close(𝑐 ). Due to linear typing of endpoints, we must use each endpoint variable exactly once. Like in other session typed languages, this is necessary for type safety. For the typing rule of redirect (if 𝑒 : 𝜋 (𝐿 ), then redirect[𝜋 ](𝑒 ) : 𝐿 ), we define the action of a renaming 𝜋 (not necessarily injective) on local types: 𝜋 (![𝑝 ]{ℓ : 𝜏 . 𝐿 } ) ≜ ![𝜋 (𝑝 )]{ℓ : 𝜏 . 𝜋 (𝐿 )} ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝜋 (?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ) ≜ ?[𝜋 (𝑝 )]{ℓ : 𝜏 . 𝜋 (𝐿 )} ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝜋 (End) ≜ End 3.2.3 Global Types and Projections. The typing rule for fork (Figure 3) requires a session’s local types 𝐿 , . . ., 𝐿 to be consistent. Consistency means, for instance, that if participant 𝑝 sends a value 0 𝑛 of type 𝜏 to participant 𝑞 , then 𝑞 is expecting to receive a value of type 𝜏 from 𝑝 at that point in the protocol. Traditionally, consistency is defined by the existence of a global type that governs the communication between all participants in a session. Global types are of the form: 𝐺 ∈ GType ::= [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝐺 } | End 1 2 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) A global type [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝐺 } expresses that the first action in the protocol is for participant 1 2 ℓ ℓ ℓ ∈𝐼 𝑝 to send a message to 𝑝 , such that if the label in the message is chosen to be ℓ, then the payload 1 2 of the message has to have type 𝜏 , and then the global protocol continues as 𝐺 . Note that łglobalž ℓ ℓ in our use of łglobal typež means global with respect to a session, not the whole programÐeach different session started by a fork can have its own global type. Local types can be extracted from global types by a projection judgment 𝐺 ⇂ 𝑝 = 𝐿 , indicating that participant 𝑝 ’s local type is 𝐿 if the global type is 𝐺 . The judgment is coinductively defined in Figure 4. The first two rules state how the sender and receiver of a message in the global type are Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:13 𝑟 ≠ 𝑞 ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 𝑟 ≠ 𝑝 ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ ℓ ℓ ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· [𝑟 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } [𝑝 → 𝑟 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝑟 ∉ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 𝑟 guards 𝐺 𝐼 ≠ ∅ 𝑟 ∉ participants(𝐺 ) ℓ ℓ ·· ····················································································· ·· ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = 𝐿 𝐺 ⇂ 𝑟 = End ℓ ℓ ℓ ∈𝐼 𝑟 ∈ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝑟 guards 𝐺 𝑟 guards [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } 𝑟 guards [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 Fig. 4. Coinductive projection rules (dotted line) and inductive guardedness rules (solid line). projected. The third rule states how other participants not involved in the message are projected. For participants not involved in the message, we require that participant to guard the rest of the global type, which means that the participant occurs in the global type at finite depth along every branch. The fourth rule states that if a participant does not occur in the global type, then it projects to End. Our projection rules are similar to those of Zooid [Castro-Perez et al. 2021]. Traditionally, consistency consistent(𝐿 , . . ., 𝐿 ) is expressed in terms of a global type 𝐺 such 0 𝑛 that 𝐺 ⇂ 0 = 𝐿 , . . .,𝐺 ⇂ 𝑛 = 𝐿 , and 𝐺 ⇂ 𝑚 = End for 𝑚 > 𝑛 . In ğ6 we develop, inspired by Scalas 0 𝑛 and Yoshida [2019a], a more permissive notion of consistency that is independent of a global type, permitting deadlock-free scenarios for which no appropriate global type can be found. ğ6.2 then shows that the traditional notion of consistency based on global types implies our new notion. 4 TRANSLATION FROM BINARY TO MULTIPARTY We show that a GV-style binary session-typed language falls out as a special mode of use of our multiparty language MPGV by giving a type-preserving translation of binary channel operations into MPGV. We consider this an important benchmark, because whereas traditional multiparty systems do support such a translationÐthe output of the translation does not necessarily fall into the fragment of the language where the type system ensures deadlock freedom if whole programs instead of single sessions are considered. There are two main obstacles in existing systems: (1) after translation, participant numbers do not match up, and (2) in systems such as Coppo et al. [2013]; Bettini et al. [2008]; Coppo et al. [2016], deadlock-freedom mechanisms such as orders/priorities prevent programs from being translated because these orders are absent in the source program, so after translation one must come up with an order on sessions. The latter is not always possible if sessions are used in a different orders in different branches of a conditional. Finally, translation of an expressive language such as GV requires the target language to support storing endpoints in data structures, as GV supports this. MPGV overcomes all these obstacles. We start by giving a short introduction to binary session types, and then show how they can be translated into our language, making use of redirect. Binary session types are equivalent to local types without participant annotations. The annotations are not necessary in the binary case, because there is only one other participant to communicate with: 𝐵 ∈ BType ::= !{ℓ : 𝜏 . 𝐵 } | ?{ℓ : 𝜏 . 𝐵 } | End ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) The operations for binary channels are defined in terms of multiparty operations as follows: fork (𝑒 ) ≜ redirect[1 ↦→ 0](fork(𝑒 )) send (𝑒 , ℓ :𝑒 ) ≜ send[0](𝑒 , ℓ :𝑒 ) 𝐵 𝐵 1 2 1 2 close (𝑒 ) ≜ close(𝑒 ) receive (𝑒 ) ≜ receive[0](𝑒 ) 𝐵 𝐵 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:14 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Γ ⊢ 𝑒 :J𝐵 K −◦ 1 Γ ⊢ 𝑒 :JEndK Γ ⊥ Γ Γ ⊢ 𝑒 :J!{ℓ : 𝜏 . 𝐵 } K Γ ⊢ 𝑒 :𝜏 𝐿 𝐿 1 2 1 1 ℓ ℓ ℓ ∈𝐼 𝐿 2 2 ℓ Γ ⊢ fork (𝑒 ) :J𝐵 K Γ ⊢ close (𝑒 ) :1 Γ ∪ Γ ⊢ send (𝑒 , ℓ :𝑒 ) :J𝐵 K 𝐵 𝐿 𝐵 1 2 𝐵 1 2 ℓ 𝐿 Γ ⊢ 𝑒 :J?{ℓ : 𝜏 . 𝐵 } K ℓ ℓ ℓ ∈𝐼 𝐿 Γ ⊢ receive (𝑒 ) :Σ . 𝜏 × J𝐵 K 𝐵 ℓ ∈𝐼 ℓ ℓ 𝐿 Fig. 5. Derivable typing rules for binary session types. We do a binary spawn using the n-ary fork, then the local type of the endpoint of the spawner gets annotated with 1’s (because it is communicating with endpoint 1) and the local type of the endpoint of the forked-off thread gets annotated with 0’s (because it is communicating with endpoint 0). In order to implement a type-preserving translation, we redirect all annotations to 0. This enables us to canonically translate binary session types 𝐵 to multiparty local types J𝐵 K by using 𝑝 = 0 for every participant annotation: J!{ℓ : 𝜏 . 𝐵 } K ≜ ![0]{ℓ : 𝜏 . J𝐿 K } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ ℓ 𝐿 ℓ ∈𝐼 J?{ℓ : 𝜏 . 𝐵 } K ≜ ?[0]{ℓ : 𝜏 . J𝐿 K } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ ℓ 𝐿 ℓ ∈𝐼 JEndK ≜ End We then prove that the usual typing rules for binary session types are derivable in our system. For fork, this amounts to defining a global type J𝐵 K to govern the binary interaction: J!{ℓ : 𝜏 . 𝐵 } K ≜ [0 → 1]{ℓ : 𝜏 . J𝐵 K } ℓ ℓ ℓ ∈𝐼 𝐺 ℓ ℓ 𝐺 ℓ ∈𝐼 J?{ℓ : 𝜏 . 𝐵 } K ≜ [1 → 0]{ℓ : 𝜏 . J𝐵 K } ℓ ℓ ℓ ∈𝐼 𝐺 ℓ ℓ 𝐺 ℓ ∈𝐼 JEndK ≜ End After redirecting, the projections have the right local types for 𝐵 and the dual 𝐵 (flips all ? with ! and vice versa): −1 Lemma 4.1. J𝐵 K ⇂ 0 = 𝜋 (J𝐵 K ) and J𝐵 K ⇂ 1 = J𝐵 K 𝐺 𝐿 𝐺 𝐿 Using this lemma and translation of types, we can prove that the binary typing rules for fork , send , receive and close are derivable (Figure 5). 𝐵 𝐵 𝐵 𝐵 This section shows that MPGV supports the full power of GV-style binary session types, including treatment of sessions as first-class data and dynamic spawning of sessions. Note that redirecting is crucial: without it we are not able to do a type-preserving translation, because local types ![0] and ?[0] are incompatible with ![1] and ?[1]. 5 THE DEADLOCK AND LEAK FREEDOM THEOREM MPGV guarantees strong properties for well-typed programs, while supporting dynamic spawning, session interleaving, and first-class endpoints. These properties are: Type safety: The only way for a thread to get stuck is by blocking to receive from an empty buffer. Session fidelity: The values sent to and received from buffers match the types in the protocol. Global progress: Configurations of a well-typed initial program are either final or can take a step. Deadlock freedom: No subset of the threads get stuck by waiting for each other. Memory leak freedom: All data always remains reachable. Ideally, we would like to capture these properties in a single theorem that subsumes them all. As a first step, we formulate global progress as follows: Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:15 Theorem 5.1 (Global progress). If ∅ ⊢ 𝑒 :1, and ([𝑒 ], ∅) { (𝑒,®ℎ ), then: cfg ′ ′ ′ ′ (1) there exists (𝑒® ,ℎ ) such that (𝑒,®ℎ ) { (𝑒® ,ℎ ), or cfg (2) 𝑒® = () for all 𝑖 ∈ dom(𝑒®) and ℎ = ∅. This theorem rules out whole-program deadlocks and ensures that all buffers have been correctly deallocated when the program finishes. However, this theorem does not guarantee anything as long as there is still a single thread that can step. Thus it does not guarantee local deadlock freedom, nor memory leak freedom while the program is still running. Moreover, it does not even guarantee type safety: a situation in which a thread is stuck on a type error is not ruled out by this theorem as long as there is another thread that can still step. We therefore state partial deadlock freedom and memory leak freedom theorems, but we strengthen both so that they become equivalent. We use the definitions of partial deadlock and memory leak freedom of Jacobs et al. [2022a] and apply them to MPGV. We need the following notions: :: • The set 𝑣 ∈ V = Thread(𝑖 ) | Session(𝑠 ) ranging over possible threads and sessions. • The function refs (𝑣 ) ⊆ V giving the set of sessions that 𝑣 references. (𝑒,®ℎ ) • The predicate blocked (𝑣 ,𝑣 ) stating that thread 𝑣 = Thread(𝑖 ) is blocked on session (𝑒,®ℎ ) 1 2 1 𝑣 = Session(𝑠 ). • The function active(𝑒,®ℎ ) ⊆ V giving the set of active threads and sessions in the configuration. Using these notions, we strengthen partial deadlock freedom to incorporate aspects of memory leak freedom. Definition 5.2 (Partial deadlock/leak). Given a configuration (𝑒,®ℎ ), a subset 𝑆 ⊆ V of the threads and sessions is in a partial deadlock/leak if the following conditions hold: (1) We have ∅ ⊂ 𝑆 ⊆ active(𝑒,®ℎ ). (2) For all threads Thread(𝑖 ) ∈ 𝑆 , the expression 𝑒 cannot step in the heap ℎ. (3) If Thread(𝑖 ) ∈ 𝑆 and blocked (Thread(𝑖 ), Session(𝑠 )), then Session(𝑠 ) ∈ 𝑆 . (𝑒,®ℎ ) (4) If Session(𝑠 ) ∈ 𝑆 and Session(𝑠 ) ∈ refs (𝑣 ), then 𝑣 ∈ 𝑆 . (𝑒,®ℎ ) Definition 5.3 (Partial deadlock/leak freedom). A configuration (𝑒,®ℎ ) is deadlock/leak free if no 𝑆 ⊆ V is in a partial deadlock/leak in (𝑒,®ℎ ). Conversely, we strengthen memory leak freedom (i.e., full reachability) to incorporate aspects of deadlock freedom. Definition 5.4 (Reachability). We inductively define the threads and sessions reachable in (𝑒,®ℎ ): (1) Thread(𝑖 ) is reachable if either • the expression 𝑒 can step in the heap ℎ, or • there exists an 𝑠 such that Session(𝑠 ) is reachable and blocked (Thread(𝑖 ), Session(𝑠 )). (𝑒,®ℎ ) (2) Session(𝑠 ) is reachable if there exists a reachable 𝑣 such that Session(𝑠 ) ∈ refs (𝑣 ). (𝑒,®ℎ ) Definition 5.5 (Full reachability). A configuration (𝑒,®ℎ ) is fully reachable if all 𝑣 ∈ active(𝑒,®ℎ ) are reachable in (𝑒,®ℎ ). As in Jacobs et al. [2022a]’s language for binary sessions, the strengthened versions of deadlock freedom and full reachability are equivalent, and well-typed MPGV programs satisfy both properties: Theorem 5.6. A configuration (𝑒,®ℎ ) is deadlock/leak free if and only if it is fully reachable. Theorem 5.7. If ∅ ⊢ 𝑒 :1 and ([𝑒 ], ∅) { (𝑒,®ℎ ), then (𝑒,®ℎ ) is fully reachable and deadlock/leak cfg free. The final theorem encompasses type safety, session fidelity, deadlock freedom, and memory leak freedom. Global progress (Theorem 5.1) also follows as a corollary from the final theorem. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:16 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 6 EXTENSION: CONSISTENCY WITHOUT GLOBAL TYPES Inspired by Scalas and Yoshida [2019a,b], we define a notion of consistency that does not rely on global types. This notion of consistency plays an important role in our proof of deadlock freedom (ğ7 ), but is also more flexible. It is more flexible in the sense that consistent(𝐿 , . . ., 𝐿 ) (premise of 0 𝑛 fork in Figure 3) may hold even if no global type exists whose projections are 𝐿 , . . ., 𝐿 . For example, 1 𝑛 there exists no global type for the local types 𝐿 = ![1]N.?[1]N.End and 𝐿 = ![0]N.?[0]N.End 0 1 because they both start with a send. Nevertheless, it would be safe and deadlock free to allow this protocol, given an asynchronous semantics. The more flexible notion of consistency we define in ğ6.1 does allow this protocol. In ğ6.2 we show that the existence of a global type for local types implies our flexible notion of consistency. 6.1 Defining Consistency without Global Types At a high level, we define consistent(𝐿 , . . ., 𝐿 ) as follows: 0 𝑛 łThe local types 𝐿 , . . ., 𝐿 of a session are consistent if no deadlock can occur within 0 𝑛 the session when considering all possible interleavings of participant actions, assuming that each participant 𝑝 follows its respective local type 𝐿 .ž Our goal is to define this notion solely as a property of the local types 𝐿 , . . ., 𝐿 , so that consistency 0 𝑛 of a session’s local types can be proven without considering other sessions. To do so, we define the notion of shadow buffers : fin fin 𝑄 ∈ ShadowBuf ≜ Participant −⇀ (Participant −⇀ List(Label × Type)) Shadow buffers are similar to the physical buffers in the heap, but there are two differences. First, whereas the physical buffers contain pairs ⟨ℓ :𝑣 ⟩ of labels and values, shadow buffers contain pairs ⟨ℓ :𝜏 ⟩ of labels and types. Second, whereas the heap concerns all sessions, shadow buffers only concern a single session. Hence, the heap ranges over endpoints (recall that Endpoint ≜ Session × Participant), but shadow buffers range over mere participants. Shadow buffers allow us to simulate the local execution of a session on the abstract level. If all fin the possible local executions allowed by a set of local types L : Participant −⇀ LType on a set of ˆ ˆ shadow buffers 𝑄 are type safe and deadlock free, we say that 𝑄 is consistent with L, which we denote by consistent(𝑄, L), and define as follows: Definition 6.1. The judgment consistent(𝑄, L) is defined as the most permissive relation satisfying the following properties: (1) Consistency is preserved by sends, i.e., for every participant 𝑝 with L(𝑝 ) = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } , ℓ ℓ ℓ ∈𝐼 then consistent(push(𝑞,𝑝, ⟨ℓ :𝜏 ⟩ ,𝑄 ), L[𝑝 := 𝐿 ]). ℓ ℓ (2) Consistency is preserved by receives, i.e., for every participant 𝑞 with L(𝑞 ) = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } , ℓ ℓ ℓ ∈𝐼 ′ ′ ˆ ˆ ˆ and pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ), then ℓ ∈ 𝐼 , and consistent(𝑄 , L[𝑞 := 𝐿 ]), and 𝜏 = 𝜏 . ℓ ℓ (3) Consistency is preserved by channel closure, i.e., for every participant 𝑝 with L(𝑝 ) = End, then consistent(𝑄 \{𝑝 }, L\{𝑝 }). (4) Either all buffers have been deallocated ( 𝑄 = ∅) or there is a participant 𝑞 such that 𝑞 ’s local type L(𝑞 ) is a send or a close, or L(𝑞 ) is a receive and the corresponding buffer contains a value, ′ ′ ˆ ˆ ˆ i.e., pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ) for some label ℓ, type 𝜏 , and new set of shadow buffers 𝑄 . (5) For each participant there is a corresponding set of buffers and vice versa, i.e., dom(L) = dom(𝑄 ). Note that the cases for the preservation of consistent(𝑄, L) under the sends, receives, and channel ′ ′ ′ ′ ˆ ˆ closure refer to a recursive occurrence consistent(𝑄 , L ) for some 𝑄 and L . Since we consider There exist other extensions of (multiparty) session types that allow for a more flexible notion of consistency. In particular, session-type systems with asynchronous subtyping also support this example [Ghilezan et al. 2021; Mostrous et al. 2009]. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:17 the most permissive relation, these recursive occurrences should be interpreted coinductivelyÐwe use Coq’s CoInductive keyword in the mechanization. The first three properties are used to show that the channel operations are type safe and the resulting state is again consistent. The fourth property is used to show deadlock freedom. The fifth property is required for technical reasons because we support the possibility of some participants deallocating their buffers while other participants are continuing to communicate with each other. With this at hand, we define the new consistency predicate used in the fork typing rule: ® ® ® Definition 6.2. We define consistent(𝐿 ) as consistent(init(length(𝐿 )), 𝐿 ), where init(𝑛 ) creates 𝑛 empty buffers, and the list 𝐿 is converted into a map in the natural way. Note that we need to use the finite map representation because some participants can close their channel before others (see Item 3 in Definition 6.1 ), and then they disappear from L (lists do not allow gaps in the middle, whereas finite maps do). 6.2 Global Types Imply Consistency The goal of this section is to show that if there is a global type for a set of local types, then the local types are consistent in the sense of the preceding section: Theorem 6.3. If there is a global type𝐺 with𝑛 +1 participants such that𝐺 ⇂ 0 = 𝐿 , . . .,𝐺 ⇂ 𝑛 = 𝐿 , 0 𝑛 then consistent(𝐿 , . . ., 𝐿 ). 0 𝑛 This lemma shows that we did not lose anything by using the more flexible notion of consistency without global typesÐthe programs we are able to type check with the more flexible notion of consistency are a superset of the programs we are able to type check using global types. We cannot prove Theorem 6.3 directly using coinduction, because the coinductive conclusion is not general enough. We need a more general property that involves the consistency judgment ˆ ˆ consistent(𝑄, L) for an arbitrary set of shadow buffers 𝑄 . Our generalized property (Lemma 6.4) makes use of the notion runtime global types, inspired by the work of Castro-Perez et al. [2021]. Runtime global types. To model the state of a global type during an interaction in which some messages have already been sent but not yet received, we define runtime global types as: ℓ? :: 𝑅 ∈ RType = [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } | Cont 𝐺 1 2 ℓ ℓ ℓ ∈𝐼 (𝑖𝑑𝑛 ) Runtime global types differ from ordinary global types ( ğ3.2.3 ) in three aspects: (1) Operations in runtime global types have an optional label ℓ on the arrow. If no label is present (i.e., [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } ), then both the send and receive remain to happen. If a label ℓ is 1 2 ℓ ℓ ℓ ∈𝐼 present (i.e., [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } ), then the send portion (with label ℓ) of the operation has 1 2 ℓ ℓ ℓ ∈𝐼 already happened, but the receive is still pending. (2) Runtime global types are defined inductively rather than coinductively, because only finitely many messages have been sent at any given point in time. (3) Instead of having End, they have Cont 𝐺 , indicating that the protocol continues as ordinary global type 𝐺 . Runtime local type projections. The projections 𝑅 ⇂ 𝑝 = 𝐿 of runtime global types onto local types can be found in Figure 6. These rules are inductively defined. Intuitively, when an operation [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 occurs in the runtime global type, then the projection onto 𝑝 ignores ℓ ℓ ℓ ∈𝐼 the operation and continues with 𝑅 because the send by 𝑝 with label ℓ has already happened. However, the projection onto 𝑞 in this case still has to take the receive part of this operation into Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:18 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝑞 ≠ 𝑟 ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 𝑝 ≠ 𝑟 ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 ℓ ℓ ℓ ℓ ℓ? [𝑟 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ℓ [𝑝 → 𝑟 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ℓ 𝑟 ∉ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 𝐼 ≠ ∅ 𝑞 ≠ 𝑟 𝑅 ⇂ 𝑟 = 𝐿 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = 𝐿 Cont 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = 𝐿 ℓ ℓ ′ ′ ˆ ˆ ˆ ˆ ˆ ˆ pop(𝑞,𝑝, 𝑄 ) = ⊥ ∀ℓ. 𝑅 ⇂⇂ 𝑄 pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ) 𝑅 ⇂⇂ 𝑄 𝑄 = ∅ ℓ ℓ ℓ ˆ ˆ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂⇂ 𝑄 Cont 𝐺 ⇂⇂ 𝑄 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂⇂ 𝑄 ℓ ℓ Fig. 6. Projections of runtime global types: (1) local type projections 𝑅 ⇂ 𝑝 = 𝐿 , and (2) shadow buffer projections 𝑅 ⇂⇂ 𝑄 (inductive). account, because the receive has not happened yet. The other cases are similar to the projections for ordinary global types (Figure 3), and ensure that the protocol remains well-formed. Runtime buffer projections. We also define the judgment 𝑅 ⇂⇂ 𝑄 , which says that the messages in the runtime global type 𝑅 correspond to the shadow buffers 𝑄 . Runtime global types imply consistency. Using the notion of runtime global type and runtime projections, we are able to show the following lemma: Lemma 6.4. The judgment consistent(𝑄, L) holds if there exists a runtime global type 𝑅 for which the following four conditions hold: (1) 𝑅 ⇂⇂ 𝑄 (2) ∀𝑝. 𝑅 ⇂ 𝑝 = 𝐿 (𝑝 ) (3) participants(𝑅 ) ⊆ dom(L) ˆ ˆ (4) ∀𝑝. if 𝑄 (𝑝 ) = ⊥ then 𝑝 ∉ dom(L) else dom(L) ⊆ dom(𝑄 (𝑝 )). The lemma is proved using coinduction, and relies on a series of auxiliary lemmas (see the Coq development for details [Jacobs et al. 2022b]). Once we have this lemma, Theorem 6.3 follows by relating projection of runtime global types to projection of ordinary global types. 7 PROOF OF DEADLOCK AND LEAK FREEDOM We give an overview of the proof of our main result, Theorem 5.7. The proof is quite technical, but since all parts have been mechanized in Coq [Jacobs et al. 2022b], one can trust the theorems independent of the pen-and-paper description of the proof. We hope to provide enough insights into the proof to make our results reproducible and extensible. The high level structure of the proof is as follows: • We define an invariant on the runtime configuration, which states (1) that everything in the configuration is well-typed and that the buffer contents are consistent with respect to the local types of each channel endpoint, and (2) that the topology of the configuration is acyclic. • We prove that the invariant is preserved by steps of the operational semantics (łpreservationž). • We prove that configurations that satisfy the invariant cannot be in a deadlock (łprogressž). To deal with linearity and acyclicity we use the connectivity graph framework of Jacobs et al. [2022a], which provides a couple of features to make our proof feasible. First, it provides a generic construction to define the invariantÐit allows us to provide local invariants for threads and channels, which the framework then lifts to an invariant for whole runtime configurations. Second, it makes use of separation logic to hide reasoning about linearity. Third, it provides generic reasoning principles to prove the preservation (of acyclicity and typing) and progress parts of the proof. Fourth, it is implemented as a library in Coq, so it allows us to mechanize our proofs. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:19 fin 𝑃,𝑄 ∈ sProp ≜ (V −⇀ E) → Prop V ::= Thread(𝑖 ) | Session(𝑠 ) (Emp)(Σ) ≜ (Σ = ∅) E ≜ Participant × LType fin (False)(Σ) ≜ False Σ ∈ V −⇀ E (True)(Σ) ≜ True (𝑃 ∨ 𝑄 )(Σ) ≜ 𝑃 (Σ) ∨ 𝑄 (Σ) (⌜𝜙 ⌝)(Σ) ≜ 𝜙 ∧ (Σ = ∅) (𝑃 ∧ 𝑄 )(Σ) ≜ 𝑃 (Σ) ∧ 𝑄 (Σ) ′ ′ (own(Σ ))(Σ) ≜ (Σ = Σ ) (∃𝑥. 𝑃 (𝑥 ))(Σ) ≜ ∃𝑥. 𝑃 (𝑥 )(Σ) (𝑃 )(Σ) ≜ 𝑃 (∅) ∧ Σ = ∅ (∀𝑥. 𝑃 (𝑥 ))(Σ) ≜ ∀𝑥. 𝑃 (𝑥 )(Σ) (𝑃 ∗ 𝑄 )(Σ) ≜ ∃Σ Σ . dom(Σ ) ∩ dom(Σ ) = ∅ ∧ Σ = Σ ⊎ Σ ∧ 𝑃 (Σ ) ∧ 𝑄 (Σ ) 1 2 1 2 1 2 1 2 ′ ′ ′ ′ (𝑃 −∗ 𝑄 )(Σ) ≜ ∀Σ . dom(Σ) ∩ dom(Σ ) = ∅ ∧ 𝑃 (Σ ) ⇒ 𝑄 (Σ ⊎ Σ ) Fig. 7. The definition of the separation logic connectives. At the high-level, the structure of our proof and our use of the connectivity framework is similar to Jacobs et al. [2022a]’s proof for binary session types. To use the framework to obtain the invariant for configurations ( ğ7.3 ), we first define a runtime type system for expressions to express the local invariant for threads (ğ7.1 ), and define a local invariant for the buffers that back a session ( ğ7.2 ). The new element of our proof is handling multiparty instead of binary sessions, for which we make use of our notion of shadow buffers ( ğ6 ). With the invariant for configurations at hand, we prove that this invariant holds for the initial configurations and is preserved by the operational semantics ( ğ7.4 ). The new element is an ex- tension of the connectivity graph framework to handle n-ary graph transformations to support the multiparty case. To complete the proof, we show that the configuration invariant implies Theorem 5.7, our main deadlock freedom theorem (ğ7.5 ). 7.1 Runtime Type System The first step to define the invariant for configurations is to define a runtime typing judgment for expressions. The runtime judgment differs from the static typing judgment ( ğ3.2 ) in the sense that it should account for channel literals #[𝑐, 𝜋 ] that appear after the execution of a fork. Traditionally, this is done by extending the typing judgment Σ; Γ ⊢ 𝑒 : 𝜏 with an additional context Σ that keeps track of the types of the channel literals (often called a heap typing). To avoid having to thread through such this context everywhere, and having to deal with splitting conditions of this context (due to linearity), we make use of separation logic [O’Hearn and Pym 1999; O’Hearn et al. 2001]. This follows the approach in the connectivity graph framework [Jacobs et al. 2022a], which in turn is based on Rouvoet et al. [2020]’s use of separation logic to hide heap typings in intrinsically-typed interpreters for linear languages in Agda. Our runtime judgment Γ ⊨ 𝑒 : 𝜏 is formalized as a separation logic proposition sProp, i.e., a predicate over heap typings Σ. The semantics of the separation logic connectives can be found in Figure 7 and the rules of our runtime type system in Figure 8. Crucially, the use of separating conjunction in the rules of n-ary constructs hides the splitting of the heap typing Σ, and the use of own(𝑠 ↦→ (𝑝, 𝜋 (𝐿 ))) in the rule for endpoint literals #[(𝑠,𝑝 ), 𝜋 ] makes sure the type of each literal matches up with the heap typing Σ. Note that the runtime judgment Γ ⊨ 𝑒 :𝜏 is defined recursively on the structure of 𝑒 . To assert that 𝑃 ∈ sProp is true, means to assert that 𝑃 (∅) holds. The actual type of Σ in Figure 7 also accounts for threads in addition to sessions. This is due to the use of the connectivity graph framework, which we discuss in ğ7.3 . Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:20 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers ⌜Γ unr⌝ ∗ own(𝑠 ↦→ (𝑝, 𝜋 (𝐿 ))) (Γ ∪ {𝑥 ↦→ 𝜏 } ⊨ 𝑒 :𝜏 ) ∗ ⌜Γ unr⌝ ∗ ⌜𝑥 ∉ Γ⌝ 1 2 ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ #[(𝑠,𝑝 ), 𝜋 ] :𝐿 Γ ⊨ 𝜆𝑥. 𝑒 :𝜏 → 𝜏 1 2 ⌜Γ ⊥ · · · ⊥ Γ ⌝ ∗ ⌜consistent(𝐿 , 𝐿 , . . ., 𝐿 )⌝ ∗ [ ] 𝑝 ∈ {1..𝑛 }. Γ ⊨ 𝑒 :𝐿 −◦ 1 1 𝑛 0 1 𝑛 ∗ 𝑝 𝑝 𝑝 -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ∪ · · · ∪ Γ ⊨ fork(𝑒 , . . .,𝑒 ) :𝐿 1 𝑛 1 𝑛 0 Γ ⊨ 𝑒 :End ⌜Γ ⊥ Γ ⌝ ∗ Γ ⊨ 𝑒 :![𝑝 ]{ℓ : 𝜏 . 𝐿 } ∗ Γ ⊨ 𝑒 :𝜏 1 2 1 1 ℓ ℓ ℓ ∈𝐼 2 2 ℓ --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ close(𝑒 ) :1 Γ ∪ Γ ⊨ send[𝑝 ](𝑒 , ℓ :𝑒 ) :𝐿 1 2 1 2 ℓ Γ ⊨ 𝑒 :?[𝑝 ]{ℓ : 𝜏 . 𝐿 } Γ ⊨ 𝑒 :𝜋 (𝐿 ) ℓ ℓ ℓ ∈𝐼 -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ receive[𝑝 ](𝑒 ) :Σ . 𝜏 × 𝐿 Γ ⊨ redirect[𝜋 ](𝑒 ) :𝐿 ℓ ∈𝐼 ℓ ℓ Fig. 8. Selected separation logic runtime typing rules (recursive). local wf(𝑒,®ℎ ) ≜ wf(wf ) (𝑒,®ℎ ) wf(𝑃 ) ≜ ∃𝐺 : Cgraph(V, E). ∀𝑣 ∈ V. 𝑃 (𝑣, in(𝐺,𝑣 ))(out(𝐺,𝑣 )) ⌜Δ = ∅⌝ ∗ (∅ ⊨ 𝑒 :1) if 𝑣 = Thread(𝑖 ),𝑖 < |𝑒®|  𝑖   ⌜Δ = ∅⌝ if 𝑣 = Thread(𝑖 ),𝑖 ≥ |𝑒®| local wf (𝑣, Δ) ≜ fin (𝑒,®ℎ ) ∃L ∈ Participant −⇀ LType. if 𝑣 = Session(𝑠 ) ⌜Δ = toMultiset(L)⌝ ∗ consistent(ℎ| , L) ˆ ˆ ˆ consistent(𝑄, L) ≜ ∃𝑄. ⌜consistent(𝑄, L)⌝ ∗ 𝑄 ∝ 𝑄 ˆ ˆ ˆ ˆ ˆ 𝑄 ∝ 𝑄 ≜ [ ] 𝑄 ;𝑄 ∈ 𝑄 ;𝑄. [ ] 𝑄 ;𝑄 ∈ 𝑄 ;𝑄 . ∗ 𝑝 𝑝 ∗ 𝑝𝑞 𝑝𝑞 𝑝 𝑝 [ ] ⟨ℓ :𝑣 ⟩ ; ⟨ℓ :𝜏 ⟩ ∈ 𝑄 ;𝑄 . ⌜ℓ = ℓ ⌝ ∗ (∅ ⊨ 𝑣 :𝜏 ) ∗ 1 2 𝑝𝑞 𝑝𝑞 1 2 Fig. 9. Configuration invariant. To prove the initialization lemma (Lemma 7.4), we state in separation logic that statically well- typed expressions are well-typed in the runtime type system: Lemma 7.1. ⌜Γ ⊢ 𝑒 :𝜏 ⌝ −∗ Γ ⊨ 𝑒 :𝜏 7.2 The Buffer Invariant We now define an invariant consistent(𝑄, L) to express that the buffers 𝑄 for a given session 𝑠 fin are consistent with respect to a set of local types L : Participant −⇀ LType. The buffer invariant is similar to the consistency judgment consistent(𝑄, L) we defined in ğ6.1 , but it operates on physical buffers 𝑄 (i.e., buffers with values) instead of shadow buffers 𝑄 (i.e., buffers with types): fin fin 𝑄 ∈ Buf ≜ Participant −⇀ (Participant −⇀ List(Label ×Val)) (We use the notation ℎ| to obtain the buffers for a session 𝑠 from the heap ℎ.) Since MPGV allows to send arbitrary data over channels, the values in buffers can themselves contain channel literals. Hence, similar to the runtime typing judgment, the buffer invariant needs to be indexed by a heap typing Σ, which we hide again by considering consistent(𝑄, L) to be a Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:21 separation logic proposition sProp. The definition of consistent(𝑄, L) ∈ sProp can be found in Figure 9. This definition contains two key ingredients. First, it makes use of consistent(𝑄, L) ∈ Prop from ğ6 to specify that local types L are consistent with some (existentially quantified) shadow ˆ ˆ buffers 𝑄 . Second, it makes use of the auxiliary definition 𝑄 ∝ 𝑄 ∈ sProp in Figure 9 to specify that the labels in the physical buffers 𝑄 are equal to those in the shadow buffers 𝑄 , and that the values in the physical buffers 𝑄 have types determined by the corresponding entry in the shadow buffers 𝑄 . (The notation [ ] 𝑥 ;𝑦 ∈ 𝑋 ;𝑌. 𝑃 (𝑥,𝑦 ) in Figure 9 is an n-ary separating conjunction: it states that the collections 𝑋,𝑌 (lists or finite maps) have the same domain, and gives 𝑃 (𝑋 ,𝑌 ) ∗ · · · ∗𝑃 (𝑋 ,𝑌 ), 0 0 𝑛 𝑛 where (𝑋 ,𝑌 ) are corresponding elements in the collections.) 𝑖 𝑖 The invariant consistent(𝑄, L) for physical buffers has preservation and initialization properties paralleling to the rules of the consistency relation consistent(𝑄, L) for shadow buffers ( Defini- tions 6.1 and 6.2). Since consistent(𝑄, L) is a separation logic proposition, these properties are stated using the separation logic connectives (and thus implicitly describe the threading and splitting of the heap typing Σ). Lemma 7.2. The buffer invariant is preserved by a sends, receives, and channel closure: • If L(𝑝 ) = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } , then: ℓ ℓ ℓ ∈𝐼 (∅ ⊨ 𝑣 :𝜏 ) ∗ consistent(𝑄, L) −∗ consistent(push(𝑞,𝑝, ⟨ℓ :𝜏 ⟩ ,𝑄 ), L[𝑝 := 𝐿 ]). ℓ ℓ ℓ ˆ ˆ • If L(𝑞 ) = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } , and pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ), then ℓ ℓ ℓ ∈𝐼 consistent(𝑄, L) −∗ ⌜ℓ ∈ 𝐼 ⌝ ∗ consistent(𝑄 , L[𝑞 := 𝐿 ]) ∗ (∅ ⊨ 𝑣 :𝜏 ). ℓ ℓ • If L(𝑝 ) = End, then consistent(𝑄, L) −∗ consistent(𝑄 \{𝑝 }, L\{𝑝 }). ® ® ® Lemma 7.3. If consistent(𝐿 ), then Emp −∗ consistent(init(length(𝐿 )), 𝐿 ). 7.3 The Configuration Invariant The invariant wf(𝑒,®ℎ ) for configurations (𝑒,®ℎ ) ensures that every thread in 𝑒® is well-typed, the contents of the buffers ℎ| for each session 𝑠 in ℎ are well-typed, the types of the channel literals match up with the types of the channels, and the communication topology is acyclic. To define this invariant, we instantiate the connectivity graph framework of Jacobs et al. [2022a] with the runtime typing judgment from ğ7.1 and the buffer invariant from ğ7.2 . The first ingredient of the connectivity framework is the data type Cgraph(V, E), which represents a directed graph with vertices ranging over the set V and edge labels ranging over the set E. This graph should be acyclic in an undirected sense (i.e., the undirected erasure of the graph forms an undirected unrooted forest). We instantiate V and E in Cgraph(V, E) as follows: V ::= Thread(𝑖 ) | Session(𝑠 ) E ≜ Participant × LType The second ingredient of the connectivity graph framework is a generic invariant wf(𝑃 ), which lifts a local invariant predicate 𝑃 (𝑣, Δ) ∈ sProp to whole runtime configurations. The local predicate 𝑃 links the local configuration state of each vertex 𝑣 (i.e., the expression for a thread and the buffers for a session) to the multiset Δ of labels on the incoming edges of vertex 𝑣 . Our instantiation local 𝑃 (𝑣, Δ) ≜ wf (𝑣, Δ) is given in Figure 9. Intuitively, the local invariant for a thread (case (𝑒,®ℎ ) 𝑣 = Thread(𝑖 )) says that the expression 𝑒 of that thread is well-typed in the runtime type system with respect to the local types on the outgoing edges of the thread’s vertex in the connectivity graph. The local invariant for a session (case 𝑣 = Session(𝑠 )) says that the buffers ℎ| of that session are well-typed with respect to the local types on the incoming edges of the session’s vertex in the connectivity graph, where the endpoints stored in the buffers get their local types from the outgoing edges. The invariant for the whole configuration wf(𝑒,®ℎ ) says that there exists an acyclic graph 𝐺 : Cgraph(V, E) such that the local invariant predicate holds for all 𝑣 ∈ V. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:22 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝑇 𝑇 𝑣 𝑣 𝑣 𝑆 1 𝑖 𝑛 ... ... 𝐿 𝐿 1 𝑛 fork(𝑣 , · · · ,𝑣 ) { 𝑐 1 𝑛 𝑇 𝑇 𝑇 1 · · · · · · 𝑛 𝑣 𝑣 𝑣 1 𝑖 𝑛 ... ... ? ? ![𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ 𝑇 𝑆 ? 𝑇 𝑆 ? send[𝑝 ](𝑐, ℓ :𝑣 ) { 𝑐 ? ? 𝑣 𝑣 ? ? ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } 𝐿 ℓ ℓ ℓ ∈𝐼 ℓ 𝑇 𝑆 ? 𝑇 𝑆 ? receive[𝑝 ](𝑐 ){ ⟨ℓ : (𝑣,𝑐 )⟩ ? ? 𝑣 𝑣 ? ? close(𝑐 ) { () End 𝑇 𝑆 ? 𝑇 𝑆 ? ? ? Fig. 10. Graphical depiction of how multiparty interactions change the logical connectivity. Blue circles are multiparty sessions, brown squares are threads. A blue circle abstracts over the 𝑛 × 𝑛 communication paths among the 𝑛 session participants, where each endpoint has buffers for incoming messages from every other endpoint. An edge from 𝑇 to 𝑆 indicates that thread 𝑇 has an endpoint of session 𝑆 . An edge from a session 𝑆 to a session 𝑆 indicates that an endpoint of 𝑆 is stored in one of the buffers of 𝑆 . The figure provides a 1 2 2 1 local viewpoint, only depicting the notions directly involved in an interaction and omitting other threads and sessions that are connected to the depicted ones as well. While the communication topology is cyclic within a multiparty session (where the global types rule out deadlock), it is acyclic between multiparty sessions, an invariant preserved by multiparty interactions. Acyclicity is crucial for deadlock and memory leak freedom. 7.4 Initialization and Preservation of the Invariant The invariant holds for initial configurations and is preserved by the operational semantics: Lemma 7.4. If ∅ ⊢ 𝑒 :1, then wf([𝑒 ], ∅). ′ ′ ′ ′ Lemma 7.5. If (𝑒,®ℎ ) { (𝑒® ,ℎ ), then wf(𝑒,®ℎ ) implies wf(𝑒® ,ℎ ). cfg The proof of the last lemma involves three aspects. First, because the configuration changes, we need to produce a connectivity graph for the new configuration as the connectivity graph is existentially quantified in the configuration invariant wf(𝑒,®ℎ ). Second, we need to show that the new connectivity graph is acyclic in the appropriate sense. Third, we need to show that all the local local invariant predicates wf (𝑣, Δ) still hold. The interesting cases of this proof are the steps that (𝑒,®ℎ ) involve the channel operations, for which the graph transformations are depicted in Figure 10. Proving these graph transformations by picking a new graph by hand is cumbersome (especially in a mechanized proof). The connectivity graph framework therefore provides abstract separation logic lemmas to prove the transformations without having to mention the graph or having to deal Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:23 with its acyclicity explicitly. We can re-use some of these abstract transformation rules, but for the 𝑛 -ary fork we need a new rule (which we state abstractly for arbitrary vertices V and edge labels E). Lemma 7.6. Let 𝑣 ,𝑣 ∈ V and 𝑤 , . . .,𝑤 ∈ V. To prove wf(𝑃 ) implies wf(𝑃 ), it suffices to prove, 1 2 1 𝑛 for all Δ ∈ Multiset E: (1) 𝑃 (𝑣, Δ) −∗ 𝑃 (𝑣, Δ) for all 𝑣 ∈ V \ {𝑣 ,𝑣 ,𝑤 , . . .,𝑤 } 1 2 1 𝑛 (2) 𝑃 (𝑣, Δ) −∗ ⌜Δ = ∅⌝ for all 𝑣 ∈ {𝑣 ,𝑤 , . . .,𝑤 } 2 1 𝑛 (3) 𝑃 (𝑣 , Δ) −∗ ∃ 𝑙 , . . .,𝑙 . (own(𝑣 ↦→ 𝑙 ) −∗ 𝑃 (𝑣 , Δ)) ∗ 1 0 𝑛 2 0 1 𝑃 (𝑣 , {𝑙 , . . .,𝑙 }) ∗ 2 0 𝑛 ([ ]𝑖 ∈ {1..𝑛 }. own(𝑣 ↦→ 𝑙 ) −∗ 𝑃 (𝑣 , ∅)) ∗ 2 𝑖 𝑖 7.5 Proof of the Reachability Theorem We give an intuitive description of the proof of our main reachability theorem (Theorem 5.7). Waiting induction. At the top level of the proof, we apply the waiting induction principle of the connectivity graph library. Waiting induction relies on acyclicity of the graph and allows one to prove a predicate 𝑃 (𝑣 ) for all vertices 𝑣 ∈ V of a graph 𝐺 : Cgraph(V, E), while assuming ′ ′ ′ the łinduction hypothesisž that 𝑃 (𝑣 ) already holds for all vertices 𝑣 such that 𝑣 is waiting for 𝑣 , where łwaiting forž is a binary relation chosen by us. The predicate 𝑃 (𝑣 ) that we aim to prove for all vertices (i.e., threads and sessions) is that 𝑣 is reachable (see Theorem 5.7). The waiting relation we use is based on the blocked (𝑣,𝑣 ) relation, defined in ğ5 . Waiting induction gives us the (𝑒,®ℎ ) following induction hypotheses when proving that 𝑣 is reachable: For threads: If the thread is blocked on a session, we may assume that the session is reachable. For sessions: The owners of the session that are not blocked on this session are reachable. Reachability of threads. To show that a thread is reachable, we must show that it can take a step, or that it is blocked on an endpoint of a session that is reachable. By typing, either the thread can take a pure step, or is a session operation where all subexpressions are values. A session operation can proceed if the structure of the heap is valid, which we can conclude from the configuration invariant. The only possibility for a blocked operation is if we are trying to receive and the buffer we are trying to receive from is currently empty. Here, the waiting induction hypothesis applies (because blocked holds), using which we can show that the session that we (𝑒,®ℎ ) are blocked on is reachable. Then, by the definition of reachability, the thread is also reachable. Reachability of sessions. To show that a session 𝑠 is reachable we must show that there exists a thread or session 𝑣 that is (1) reachable, (2) holds an endpoint of 𝑠 , and (3) is not blocked on 𝑠 . We use the consistency of the buffers and local types of the session to show that there is an endpoint of 𝑠 whose owner 𝑣 is not blocked on this session (though 𝑣 may be blocked on another session). This allows us to use the induction hypothesis to conclude that 𝑣 is reachable (because blocked (Session(𝑠 ),𝑣 ) does not hold). Then, using the definition of reachability for sessions, (𝑒,®ℎ ) we conclude that 𝑠 is reachable. Main results. Theorem 5.7 is obtained by combining the reasoning above with Lemma 7.4 and Lemma 7.5. Global progress (Theorem 5.1) follows as an easy corollary. For two directions of the equivalence of partial deadlock/leak freedom with full reachability (Theorem 5.6), we show that none of the objects in a deadlock/leak are reachable, and vice versa that the set of non-reachable threads and channels forms a deadlock/leak if this set is nonempty. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:24 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 8 MECHANIZATION All our results have been mechanized in Coq using Iris Proof Mode [Krebbers et al. 2017, 2018] for the separation-logic part. The final results of our mechanization are Theorem 5.1, Theorem 5.6, and Theorem 5.7. We have also mechanized the translation from binary to multiparty in Figure 5 and have proved that it is type preserving. The mechanization is 10.4k lines of Coq code, consisting of 217 definitions, and 638 proved lemmas and theorems. Approximately half of the mechanization consists of results specific to our multiparty calculus, and the other half consists of the framework of Jacobs et al. [2022a], extended with support for n-ary graph transformations (ğ7.4 ). Archive of the mechanization. The Coq mechanization can be found at Jacobs et al. [2022b]. Partial deadlock freedom and the empty type. A surprising technical result of the mecha- nization is that while global progress remains true in the presence of𝑛 -ary sum types, we discovered that partial deadlock freedom is by default false for languages that allow 𝑛 = 0. The reason is that a thread can throw away endpoints by pattern matching on the empty sum type. While this pattern match will never execute because the empty type can only be produced by a looping expression (thus guaranteeing global progress), the thread can still lose an endpoint during a substitution step before the empty pattern match happens. This can create a partial deadlock for the threads holding the other endpoints of the session. To fix this, we amend the typing judgment Γ ⊢ 𝑒 :𝜏 to require the variable context Γ to be empty when pattern matching on an empty sum type. This formally ensures that the thread’s expression keeps track of all endpoints and does not lose any. This does not limit the expressivity of empty types because one can obtain a value of any type from an empty pattern match, including a function that can eat the remaining variables in the context. 9 RELATED WORK To relate MPGV to the existing body of work it is helpful to consider two axes of categorization: mechanization and session type philosophy. The use of a proof assistant to mechanize correctness results has only been taken up recently by the session type community. Typeset pen-and-paper proofs and appeals to results in logic (e.g., cut elimination) still constitute the status quo. We summa- rize mechanizations of session types below, but remark that only two works target mechanization of deadlock freedom up to date: Castro-Perez et al. [2021] for a single multiparty session and Jacobs et al. [2022a] for GV-style binary session types. At first blush, session types can be distinguished into binary and multiparty. Whereas binary session types restrict the concurrent interaction to two participants, multiparty session types allow an arbitrary but statically determined number of participants (łrolesž), by complementing the local perspective of a participant with a global type. A more foundational distinction, especially given the unifying nature of MPGV, is underlying philosophy. Session types [Honda 1993; Honda et al. 1998] have been conceived as a typing discipline for process calculi and as such preserve the fundamental characteristics of concurrent computation. Concurrent computation is inherently non-deterministic and may also give raise to deadlocks. For example, the below session-typed program from [Gay and Vasconcelos 2010] (page 38) is well-typed but deadlocks: ⟨let𝑐 = request𝑎 in let𝑐 = request𝑎 in let (𝑐 ,𝑥 ) = receive𝑐 in send𝑣 𝑐 ⟩ || 1 1 2 2 1 1 2 ⟨let𝑑 = accept𝑎 in let𝑑 = accept𝑎 in let (𝑑 ,𝑦 ) = receive𝑑 in send𝑤 𝑑 ⟩ 1 1 2 2 1 2 1 The program composes two threads (processes) in parallel, amounting to two binary interleaved sessions 𝑎 and 𝑎 . Sessions are initiated by matching a request for a session (request𝑎 ) with 1 2 1 an accept for that session (accept𝑎 ) creating two new endpoints per session (𝑐 and 𝑐 ). The 1 1 2 interleaving of the two sessions causes a deadlock: the receive on 𝑐 blocks the send on 𝑐 , which is 1 2 necessary for the former. The pairing of session requests with matching accepts is non-deterministic. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:25 For example, if we compose the two threads with a third thread that is also accepting a session 𝑎 , then only one of the two accepting threads will be chosen. This initialization pattern carries over to multiparty sessions [Honda et al. 2008, 2016]. In the multiparty case a request is parameterized with the number of participants 𝑛 and accepts with the role names ranging from 1 to 𝑛 − 1. Like binary session types, multiparty session types that assume this initialization pattern can deadlock. In particular, deadlocks can arise if a participant simultaneously engages in several sessions. A strategy adopted by some multiparty session type work (e.g., Castro-Perez et al. [2021]) is to restrict a program to a single global multiparty session, precluding dynamic session spawning and first-class sessions. Alternatively, advanced multiparty session-type systems [Coppo et al. 2013; Bettini et al. 2008; Coppo et al. 2016] employ extrinsic orders/priorities to rule out deadlocks among interleaved multiparty sessions, requiring order annotations in addition to global type declarations. We refer to the line of session type work that adopts the initialization pattern shown above, which separates session creation from thread spawning, as traditional session types. We like to contrast this line of work with the one that adopts an initialization pattern based on cut, inspired by the Curry-Howard correspondence between linear logic and the session-typed 𝜋 -calculus [Caires and Pfenning 2010; Wadler 2012; Lindley and Morris 2015; Kokke et al. 2019], which we refer to as logic-based session types. Logic-based session types come with strong guarantees out of the box. These include, besides session fidelity, deadlock freedom. Given our focus on deadlock freedom, MPGV adopts the initialization pattern of logic-based session types and generalizes GV’s fork construct [Wadler 2012; Lindley and Morris 2015, 2016b, 2017; Fowler et al. 2019, 2021] for binary session types to the 𝑛 -ary setting. The above program would thus not type check in MPGV. A recent extension of GV by Fowler et al. [2021], Hypersequent GV (HGV), adopts hypersequents [Montesi and Peressotti 2018; Kokke et al. 2019], inspired by Avron [1991], to facilitate a tighter correspondence to the session-typed 𝜋 -calculus and simplify GV’s meta theory by accounting for the forest topology of runtime structures. While this account is reminiscent of our notion of logical topology, the specifics of HGV and our MPGV system are quite different. Most notably, HGV employs structural congruences for runtime typing, whereas our dynamics operates on a flat thread pool and heap (allowing an arbitrary thread to step without prior application of structural congruences) and our runtime typing relies on separation logic and connectivity graphs. We next review the individual related work in more detail, referring to our categorization of traditional and logic-based session types as convenient. Given our focus on mechanization, we start with mechanized related work and then conclude with non-mechanized related work. Mechanized. The only existing work on mechanizing deadlock freedom for multiparty session types is Zooid, a DSL by Castro-Perez et al. [2021] embedded in Coq. Although a traditional session type language in spirit, Zooid does neither support session spawning nor delegation, but restricts a program to a single global multiparty session. Zooid programs thus rule out deadlocks caused by multiparty session interleavings by construction. Thanks to a shallow embedding in Coq, Zooid programs can be extracted from Coq to OCaml via Coq’s extraction mechanism. Send and receive operations are handled as monadic operations in which the endpoint is implicit (because there is a unique global session). A shallow embedding of binders works in this context because Zooid variables can only contain purely functional data, which can be represented as Coq data. Our definition of (runtime) global types and projections is inspired by Zooid. MPGV not only differs from Zooid in its support for multiple interacting sessions, first-class endpoints, dynamic spawning, and delegation, but also in statement and precision of the deadlock freedom property. Our mechanization guarantees global progressÐincluding the stronger notions of partial deadlock/leak freedom. Zooid’s main result, on the other hand, is phrased in terms of Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:26 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers traces, asserting that for all traces produced by a well-typed process there exists a matching trace in the larger system. This result relies on properties of global types from the literature and also assumes the ability to choose a favorable schedule. Our mechanization in contrast states deadlock freedom for all executions/schedules and gives a closed end-to-end proof in Coq. Jacobs et al. [2022a] contribute a mechanization of deadlock freedom for a variant of GV, and thus target binary session types. Like our mechanization, theirs accommodates dynamic session spawning and delegation, but restricted to the binary setting. Jacobs et al. [2022a] moreover contribute the notion of a connectivity graph, a parametric proof method for deadlock freedom, relying on acyclicity of the communication topology. We extend this proof method with 𝑛 -ary operations and support of cyclic connectivity within a session governed by consistency. Our generalization to 𝑛 -ary operations also enables our encoding of binary session types in MPGV (ğ4 ). Unlike Jacobs et al.’s variant of GV, our MPGV system moreover supports choice, and thus provides the first mechanization of deadlock and leak freedom for binary session types with choice. Moreover, there exists work on mechanizing the metatheory of binary session types. Thiemann [2019] proves type safety of a linear 𝜆 -calculus with session types inspired by GV. The result does not include deadlock nor memory leak freedom. Hinrichsen et al. [2021] prove type safety for a comprehensive session-typed language with locks, subtyping and polymorphism using Iris in Coq. Their type system is affine, which means that deadlocks are considered safe. Tassarotti et al. [2017] prove termination preservation of a compiler for an affine session-typed language using Iris in Coq. More distantly, there exist various mechanized results involving the 𝜋 -calculus. Goto et al. [2016] prove type safety for a 𝜋 -calculus with a polymorphic session type system in Coq. Their type system allows dropping channels, and hence does not enjoy deadlock nor memory leak freedom. Ciccone and Padovani [2020] mechanize dependent binary session types by embedding them into a 𝜋 -calculus in Agda. They prove subject reduction (i.e., preservation) and that typing is preserved by structural congruence, but not deadlock or memory leak freedom. Similarly, Zalakain and Dardha [2021] mechanize subject reduction of a resource-aware 𝜋 -calculus, focusing on the handling of linear resources through leftover typing. Gay et al. [2020] study various notions of duality in Agda, and show that distribution laws for duality over the recursion operator are unsound. We adopted their approach of using coinductive types for mechanizing general recursive session types. Lastly, mechanizations of choreographic languages [Montesi 2020; Cruz-Filipe et al. 2021a,b] focus on determinism, confluence, and Turing completeness, with deadlock freedom holding by design. Non-mechanized. The work that is most closely related to ours in terms of underlying philoso- phy but non-mechanized is the work by Carbone et al. [2015, 2016, 2017] on coherence proofs. The authors introduce a proof theory grounded in classical linear logic via a Curry-Howard correspon- dence, illuminating the connection between binary and multiparty session types, in a 𝜋 -calculus setting. The correspondence is due the novel notion of coherence, which generalizes duality known from binary session types to compatibility of local types with a global type of a multiparty session. Given a coherence derivation, an𝑛 -ary cut permits composing𝑛 participants concurrently, similar to our 𝑛 -ary fork. Coherence also enables a semantic-preserving translation from multiparty sessions to corresponding binary sessions via an arbiter process [Carbone et al. 2016]. Deadlock freedom follows from cut admissibility and cut elimination, giving a normalization argument. Such an argument is made possible by using cut reductions for the semantics and restricting to a non-Turing complete calculus without loops or recursion. In contrast, we provide a complete mechanization of deadlock freedom of an 𝑛 -ary session-typed functional language, with recursive types, first-class endpoints, and a realistic asynchronous operational semantics based on an unstructured thread pool. Our encoding of binary sessions in MPGV moreover does not require an arbiter process. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:27 Similarly, Caires and Pérez [2016] embed multiparty session types in a binary calculus by a translation from a global type to a medium process. Instead of communicating with each other, the participants communicate with the central medium process. This approach inherits deadlock freedom from the surrounding binary calculus, but requires central coordination and sequentializes the communication. Toninho and Yoshida [2018] show that the interconnection networks of classical linear logic (CLL) are strictly less expressive than those of a multiparty session calculus. Partial multiparty compatibility is used to define a new binary cut rule that can form circular interconnections but preserves the deadlock-freedom of CLL, albeit for a single multiparty session. More distantly related are works that use Kobayashi-style type systems [Kobayashi 1997, 2002, 2006; Giachino et al. 2014; Kobayashi and Laneve 2017] that enrich channel typing with usage information and partial orders to rule out cyclic dependencies among channel actions. In the traditional multiparty setting this is most notably the work by Coppo et al. [2013]; Bettini et al. [2008]; Coppo et al. [2016], which contributes an interaction type system that ensures deadlock freedom not only within but also between several multiparty sessions. This work not only differs from MPGV in that it requires ordering annotations in addition to global type declarations, but also in the statement of the global progress property. To account for processes that lack a communication partner, a possibility in the traditional setting, progress is stated relative to a catalyzing process that, if present, would allow the closed program to step. MPGV sets itself additionally apart in its tight integration with a functional language. Kobayashi-style systems have also been adopted for logic-based binary session types [Dardha and Gay 2018; Kokke and Dardha 2021b,a]. The authors introduce a multicut, which allows for circular topologies within a session. To rule out deadlocks by type checking, session types must be annotated with priorities. Priority polymorphism has been used by Padovani [2014] to support cyclic interleavings of recursive processes. Partial order annotations, called worlds, are also used by Balzer et al. [2019], in a logic-based binary session type calculus that combines linear and shared [Balzer and Pfenning 2017; Balzer et al. 2018] sessions. Shared session types introduce a controlled form of aliasing, an extension we would like to consider in future work. A somewhat orthogonal approach to ensuring progress in the presence of dynamic thread allocation is to make global types more powerful. While traditional multiparty session types involve a fixed number of participants per session, Deniélou and Yoshida [2011]; Demangeon and Honda [2012]; Hu and Yoshida [2017] proposed extensions of single-session systems to make that number dynamic. This line of work does not support sessions as first-class data, and the expressivity is orthogonal to GV and MPGV. Hence, extending MPGV with a dynamic number of participants is an interesting extension for future work. ACKNOWLEDGMENTS We thank the anonymous reviewers for their helpful feedback and especially for their encour- agement to explore a more permissive consistency condition than compliance with a global type, resulting in ğ6 . We are grateful to Jorge Pérez, Bas van den Heuvel, Dan Frumin, and Bernardo Toninho for discussions on this paper and related work. Robbert Krebbers was supported by the Dutch Research Council (NWO), project 016.Veni.192.259. Stephanie Balzer was supported in part by AFOSR under grant FA9550-21-1-0385 (Tristan Nguyen, program manager) and by the National Science Foundation under award number CCF-2211996. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR or NSF. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:28 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers REFERENCES Arnon Avron. 1991. Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence 4 (1991), 225ś248. https://doi.org/10.1007/BF01531058 Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. PACMPL 1, ICFP (2017), 37:1ś37:29. https://doi.org/10.1145/3110281 Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. 2018. A Universal Session Type for Untyped Asynchronous Communication. In CONCUR (LIPIcs, Vol. 118). 30:1ś30:18. https://doi.org/10.4230/LIPIcs.CONCUR.2018.30 Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In ESOP (LNCS, Vol. 11423). 611ś639. https://doi.org/10.1007/978-3-030-17184-1_22 Lorenzo Bettini, Mario Coppo, Loris D’Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2008. Global Progress in Dynamically Interleaved Multiparty Sessions. In CONCUR (LNCS, Vol. 5201). 418ś433. https: //doi.org/10.1007/978-3-540-85361-9_33 Luís Caires and Jorge A. Pérez. 2016. Multiparty Session Types Within a Canonical Binary Theory, and Beyond. In FORTE (LNCS, Vol. 9688). 74ś95. https://doi.org/10.1007/978-3-319-39570-8_6 Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR (LNCS, Vol. 6269). 222ś236. https://doi.org/10.1007/978-3-642-15375-4_16 Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. 2016. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In CONCUR (LIPIcs, Vol. 59). 33:1ś33:15. https://doi.org/10. 4230/LIPIcs.CONCUR.2016.33 Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR (LIPIcs, Vol. 42). 412ś426. https://doi.org/10.4230/LIPIcs.CONCUR.2015.412 Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2017. Multiparty session types as coherence proofs. Acta Informatica 54, 3 (2017), 243ś269. https://doi.org/10.1007/s00236-016-0285-y David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. 2021. Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes. In PLDI. 237ś251. https://doi.org/10. 1145/3453483.3454041 David Castro-Perez, Francisco Ferreira, and Nobuko Yoshida. 2020. EMTST: Engineering the Meta-theory of Session Types. In TACAS (2) (LNCS, Vol. 12079). 278ś285. https://doi.org/10.1007/978-3-030-45237-7_17 Ruofei Chen, Stephanie Balzer, and Bernardo Toninho. 2022. Ferrite: A Judgmental Embedding of Session Types in Rust. In ECOOP (LIPIcs, Vol. 222). 22:1ś22:28. https://doi.org/10.4230/LIPIcs.ECOOP.2022.22 Luca Ciccone and Luca Padovani. 2020. A Dependently Typed Linear 𝜋 -Calculus in Agda. In PPDP. 8:1ś8:14. https: //doi.org/10.1145/3414080.3414109 Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2013. Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions. In COORDINATION. https://doi.org/10.1007/978-3-642- 38493-6_4 Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2016. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 26, 2 (2016), 238ś302. https://doi.org/10.1017/S0960129514000188 Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a Recursive Module?. In PLDI. 50ś63. https://doi.org/10.1145/ 301618.301641 Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. 2021a. Certifying Choreography Compilation. In ICTAC (LNCS, Vol. 12819). 115ś133. https://doi.org/10.1007/978-3-030-85315-0_8 Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. 2021b. Formalising a Turing-Complete Choreographic Language in Coq. In ITP (LIPIcs, Vol. 193). 15:1ś15:18. https://doi.org/10.4230/LIPIcs.ITP.2021.15 Ornela Dardha and Simon J. Gay. 2018. A New Linear Logic for Deadlock-Free Session-Typed Processes. In FOSSACS (LNCS, Vol. 10803). 91ś109. https://doi.org/10.1007/978-3-319-89366-2_5 Romain Demangeon and Kohei Honda. 2012. Nested Protocols in Session Types. In CONCUR (LNCS, Vol. 7454). 272ś286. https://doi.org/10.1007/978-3-642-32940-1_20 Pierre-Malo Deniélou and Nobuko Yoshida. 2011. Dynamic multirole session types. In POPL. 435ś446. https://doi.org/10. 1145/1926385.1926435 Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. 2006. Session Types for Object-Oriented Languages. In ESOP (LNCS, Vol. 4067). 328ś352. https://doi.org/10.1007/11785477_20 Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. 2021. Separating Sessions Smoothly. In CONCUR (LIPIcs, Vol. 203). 36:1ś36:18. https://doi.org/10.4230/LIPIcs.CONCUR.2021.36 Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. 2019. Exceptional Asynchronous Session Types: Session Types Without Tiers. PACMPL 3, POPL (2019), 28:1ś28:29. https://doi.org/10.1145/3290341 Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. 2020. Duality of Session Types: The Final Cut. In PLACES (EPTCS, Vol. 314). 23ś33. https://doi.org/10.4204/EPTCS.314.3 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:29 Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear Type Theory for Asynchronous Session Types. JFP 20, 1 (2010), 19ś50. https://doi.org/10.1017/S0956796809990268 Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. 2021. Precise subtyping for asynchronous multiparty sessions. PACMPL 5, POPL (2021), 1ś28. https://doi.org/10.1145/3434297 Elena Giachino, Naoki Kobayashi, and Cosimo Laneve. 2014. Deadlock Analysis of Unbounded Process Networks. In CONCUR (LNCS, Vol. 8704). 63ś77. https://doi.org/10.1007/978-3-662-44584-6_6 Matthew A. Goto, Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, and James Riely. 2016. An Extensible Approach to Session Polymorphism. MSCS 26, 3 (2016), 465ś509. https://doi.org/10.1017/S0960129514000231 Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. 178ś198. https://doi.org/10.1145/3437992.3439914 Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR (LNCS, Vol. 715). 509ś523. https://doi.org/10.1007/3-540- 57208-2_35 Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP (LNCS, Vol. 1381). 122ś138. https://doi.org/10.1007/BFb0053567 Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In POPL. 273ś284. https://doi.org/10.1145/1328438.1328472 Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM 63, 1 (2016), 9:1ś9:67. https://doi.org/10.1145/2827695 Raymond Hu and Nobuko Yoshida. 2017. Explicit Connection Actions in Multiparty Session Types. In FASE (LNCS, Vol. 10202). 116ś133. https://doi.org/10.1007/978-3-662-54494-5_7 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. https://doi.org/10.1016/j.scico.2018.08.005 Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. 2010. Session Type Inference in Haskell. In PLACES (EPTCS, Vol. 69). 74ś91. https://doi.org/10.4204/EPTCS.69.6 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022a. Connectivity graphs: a method for proving deadlock freedom based on separation logic. PACMPL 6, POPL, 1ś33. https://doi.org/10.1145/3498662 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022b. MPGV Coq development. https://doi.org/10.5281/zenodo. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session Types for Rust. In WGP. 13ś22. https://doi.org/10.1145/2808098.2808100 Alex C. Keizer, Henning Basold, and Jorge A. Pérez. 2021. Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols. In ESOP (LNCS, Vol. 12648). 375ś403. https://doi.org/10.1007/978-3-030-72019-3_14 Naoki Kobayashi. 1997. A Partially Deadlock-Free Typed Process Calculus. In LICS. 128ś139. https://doi.org/10.1109/LICS. 1997.614941 Naoki Kobayashi. 2002. A Type System for Lock-Free Processes. I&C 177, 2 (2002), 122ś159. https://doi.org/10.1006/inco. 2002.3171 Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In CONCUR (LNCS, Vol. 4137). 233ś247. https: //doi.org/10.1007/11817949_16 Naoki Kobayashi and Cosimo Laneve. 2017. Deadlock Analysis of Unbounded Process Networks. Inf. Comput. 252 (2017), 48ś70. https://doi.org/10.1016/j.ic.2016.03.004 Wen Kokke. 2019. Rusty Variation: Deadlock-free Sessions with Failure in Rust. In ICE (EPTCS, Vol. 304). 48ś60. https: //doi.org/10.4204/EPTCS.304.4 Wen Kokke and Ornela Dardha. 2021a. Deadlock-Free Session Types in Linear Haskell. In Haskell Symposium. 1ś13. https://doi.org/10.1145/3471874.3472979 Wen Kokke and Ornela Dardha. 2021b. Prioritise the Best Variation. In FORTE (LNCS, Vol. 12719). 100ś119. https: //doi.org/10.1007/978-3-030-78089-0_6 Wen Kokke, Fabrizio Montesi, and Marco Peressotti. 2019. Better Late Than Never: a Fully-Abstract Semantics for Classical Processes. PACMPL 3, POPL (2019), 24:1ś24:29. https://doi.org/10.1145/3290337 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. https://doi.org/10.1145/3236772 Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. 205ś217. https://doi.org/10.1145/3009837.3009855 Sam Lindley and J. Garrett Morris. 2015. A Semantics for Propositions as Sessions. In ESOP (LNCS, Vol. 9032). 560ś584. https://doi.org/10.1007/978-3-662-46669-8_23 Sam Lindley and J. Garrett Morris. 2016a. Embedding Session Types in Haskell. In Haskell Symposium. 133ś145. https: //doi.org/10.1145/2976002.2976018 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:30 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Sam Lindley and J. Garrett Morris. 2016b. Talking Bananas: Structural Recursion For Session Types. In ICFP. 434ś447. https://doi.org/10.1145/2951913.2951921 Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools. https://homepages.inf.ed.ac.uk/slindley/papers/fst.pdf Fabrizio Montesi. 2020. Introduction to Choreographies. (2020). https://www.fabriziomontesi.com/teaching/ct-2020/files/ chor-notes.pdf Draft. Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. CoRR abs/1803.01049 (2018). arXiv:1803.01049 http://arxiv.org/abs/1803.01049 Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP (LNCS, Vol. 5502). 316ś332. https://doi.org/10.1007/978-3-642-00590-9_23 Peter W. O’Hearn and David J. Pym. 1999. The Logic Of Bunched Implications. Bulletin of Symbolic Logic 5, 2 (1999), 215ś244. https://doi.org/10.2307/421090 Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL (LNCS, Vol. 2142). 1ś19. https://doi.org/10.1007/3-540-44802-0_1 Luca Padovani. 2014. Deadlock and lock freedom in the linear 𝜋 -calculus. In LICS. 72:1ś72:10. https://doi.org/10.1145/ 2603088.2603116 Luca Padovani. 2017. A Simple Library Implementation of Binary Sessions. JFP 27 (2017), e4. https://doi.org/10.1017/ S0956796816000289 Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In FoSSaCS (LNCS, Vol. 9034). 3ś22. https://doi.org/10.1007/978-3-662-46678-0_1 Riccardo Pucella and Jesse A. Tov. 2008. Haskell Session Types with (Almost) No Class. In Haskell Symposium. 25ś36. https://doi.org/10.1145/1411286.1411290 Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In CPP. 284ś298. https://doi.org/10.1145/3372885.3373818 Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In ECOOP (LIPIcs, 56). 21:1ś21:28. https://doi.org/10.4230/LIPIcs.ECOOP.2016.21 Alceste Scalas and Nobuko Yoshida. 2019a. Less is more: multiparty session types revisited. PACMPL 3, POPL (2019), 30:1ś30:29. https://doi.org/10.1145/3290343 Alceste Scalas and Nobuko Yoshida. 2019b. Less is more: multiparty session types revisited (technical report). https: //www.doc.ic.ac.uk/research/technicalreports/2018/DTRS18-6.pdf Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP (LNCS, Vol. 10201). 909ś936. https://doi.org/10.1007/978-3-662-54434-1_34 Peter Thiemann. 2019. Intrinsically-Typed Mechanized Semantics for Session Types. In PPDP. 19:1ś19:15. https://doi.org/10. 1145/3354166.3354184 Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation. Carnegie Mellon University and New University of Lisbon. Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In ESOP (LNCS, Vol. 7792). 350ś369. https://doi.org/10.1007/978-3-642-37036-6_20 Bernardo Toninho and Nobuko Yoshida. 2018. Interconnectability of Session-Based Logical Processes. TOPLAS 40, 4 (2018), 17:1ś17:42. https://doi.org/10.1145/3242173 Philip Wadler. 2012. Propositions as Sessions. In ICFP. 273ś286. https://doi.org/10.1145/2364527.2364568 Uma Zalakain and Ornela Dardha. 2021. 𝜋 with Leftovers: A Mechanisation in Agda. In FORTE (LNCS, Vol. 12719). 157ś174. https://doi.org/10.1007/978-3-030-78089-0_9 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png ACM SIGBED Review Association for Computing Machinery

Multiparty GV: functional multiparty session types with certified deadlock freedom

ACM SIGBED Review , Volume 6 (ICFP): 30 – Aug 29, 2022

Loading next page...
 
/lp/association-for-computing-machinery/multiparty-gv-functional-multiparty-session-types-with-certified-RIOhZPS5JC

References (140)

Publisher
Association for Computing Machinery
Copyright
Copyright © 2022 Owner/Author
eISSN
1551-3688
DOI
10.1145/3547638
Publisher site
See Article on Publisher Site

Abstract

Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom JULES JACOBS, Radboud University Nijmegen, The Netherlands STEPHANIE BALZER, Carnegie Mellon University, USA ROBBERT KREBBERS, Radboud University Nijmegen, The Netherlands Session types have recently been integrated with functional languages, bringing message-passing concurrency to functional programming. Channel endpoints then become first-class and can be stored in data structures, captured in closures, and sent along channels. Representatives of the GV (Wadler’s łGood Variationž) session type family are of particular appeal because they not only assert session fidelity but also deadlock freedom, inspired by a Curry-Howard correspondence to linear logic. A restriction of current versions of GV, however, is the focus on binary sessions, limiting concurrent interactions within a session to two participants. This paper introduces Multiparty GV (MPGV), a functional language with multiparty session types, allowing concurrent interactions among several participants. MPGV upholds the strong guarantees of its ancestor GV, including deadlock freedom, despite session interleaving and delegation. MPGV has a novel redirecting construct for modular programming with first-class endpoints, thanks to which we give a type-preserving translation from binary session types to MPGV to show that MPGV is strictly more general than binary GV. All results in this paper have been mechanized using the Coq proof assistant. CCS Concepts: • Software and its engineering → Concurrent programming languages. Additional Key Words and Phrases: Session types, message-passing concurrency, deadlock freedom ACM Reference Format: Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. Proc. ACM Program. Lang. 6, ICFP, Article 107 (August 2022), 30 pages. https://doi.org/10.1145/3547638 1 INTRODUCTION Session types are a type discipline for message-passing concurrency. Originally developed in the context of process calculi by Honda [1993]; Honda et al. [1998], they were later generalized to object-oriented [Dezani-Ciancaglini et al. 2006] and functional languages [Gay and Vasconcelos 2010] leading to implementations in mainstream languages like Haskell [Pucella and Tov 2008; Imai et al. 2010; Lindley and Morris 2016a], Scala [Scalas and Yoshida 2016], OCaml [Padovani 2017; Imai et al. 2019], and Rust [Jespersen et al. 2015; Kokke 2019; Chen et al. 2022]. A particularly exciting development is the GV (łGood Variationž) session type family, pioneered by Gay and Vasconcelos [2010], later coined GV and refined by Wadler [2012], and further developed by e.g., Lindley and Morris [2015, 2016b, 2017]; Fowler et al. [2019, 2021]; Kokke and Dardha [2021b]; Jacobs et al. [2022a]. The GV family combines session types with functional programming by treating session-typed channels as first-class data, similar to references in ML. Channels can be stored in data structures (like lists), captured by closures, and sent along channels (even when contained in Authors’ addresses: Jules Jacobs, Radboud University Nijmegen, The Netherlands, mail@julesjacobs.com; Stephanie Balzer, Carnegie Mellon University, USA, balzers@cs.cmu.edu; Robbert Krebbers, Radboud University Nijmegen, The Netherlands, mail@robbertkrebbers.nl. This work is licensed under a Creative Commons Attribution 4.0 International License. © 2022 Copyright held by the owner/author(s). 2475-1421/2022/8-ART107 https://doi.org/10.1145/3547638 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:2 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers data structures, thus generalizing delegation). Similarly, the SILL family of session type languages [Toninho et al. 2013; Pfenning and Griffith 2015 ; Toninho 2015] integrates a process language via a contextual monad with an unrestricted functional language. Aside from a tight integration with functional programming, a key strength of GV and SILL representatives is that they do not only guarantee type safety (łwell-typed programs cannot get stuck due to illegal operationsž), but also deadlock freedom or global progress (łwell-typed programs cannot end up waiting for each otherž). This result follows from adopting a session initialization pattern based on cut, inspired by the Curry-Howard correspondence between linear logic and the session-typed 𝜋 -calculus [Caires and Pfenning 2010; Wadler 2012]. Such a pattern combines session creation and thread spawning to avoid deadlocks. The family of session types based on the pioneering work by Honda [1993]; Honda et al. [1998], in contrast, separates session creation from thread (process) spawning and thus does not prevent deadlocks. A cut-based initialization pattern also seamlessly integrates with channels as first-class data. The restriction of interactions to two participants, present in GV, SILL, and session types based on the pioneering work by Honda [1993]; Honda et al. [1998], led to the development of multiparty session types [Honda et al. 2008, 2016]. Multiparty session types allow an arbitrary but statically determined number of participants (łrolesž) to engage in a session. The key ingredient of multiparty session types is a global type that defines a protocol from the perspective of the entire session, from which local types for each participant can be generated. A global type not only increases expressivity but also establishes deadlock freedom for a system consisting of a single session. The development of GV-style session types and multiparty session types has mostly happened independently of each other. There exists no system that combines the flexibility of functional programming with the expressivity of multiparty session types. This paper introduces Multiparty GV (MPGV)Ða linear lambda calculus with first-class multiparty sessions and dynamic thread and channel initialization. Deadlock freedom is guaranteed purely by linear type checking and an 𝑛 -ary łforkž inspired by a cut-based initialization pattern. MPGV complements linear sessions with standard unrestricted functional types and language features, such as general recursive functions and algebraic data types. The integration of multiparty session types into a GV-style functional language brings a number of challenges: Deadlock freedom. Although global types guarantee deadlock freedom for a single multiparty session, global types alone cannot guarantee deadlock freedom for interleaved multiparty sessions. To establish deadlock freedom in the presence of dynamic session spawning and session delegation, where participants can engage in several multiparty sessions simultaneously, Kobayashi-style or ł ders/prioritiesž [ Kobayashi 1997, 2002, 2006] have been used to rule out cyclic dependencies among channel actions. The resulting interaction type systems [Coppo et al. 2013; Bettini et al. 2008; Coppo et al. 2016] are complementary in terms of expressivity compared to GV. They are more powerful in the sense that they allow cyclic communication topologies within and between sessions. However, well-typed programs in GV cannot be translated into these systems because orders/priorities are static and sessions are not first-class data. In this paper we take the GV approach to deadlock freedomÐMPGV features an 𝑛 -ary łforkž that combines the creation of 𝑛 threads and multiparty session for 𝑛 participants. While this makes the MPGV type system and operational semantics simple, proving that it in fact guarantees deadlock freedom is challenging. To handle dynamic thread and channel creation, direct-style deadlock freedom proofs of GV (like those by Lindley and Morris [2015]; Fowler et al. [2021]; Jacobs et al. [2022a]) crucially rely on the communication topology remaining acyclic during program execution. For multiparty session types this is not the caseÐthe communication topology between sessions is acyclic, but the communication topology within a session is not. The key insight of our work is Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:3 to represent the cyclic communication topology within sessions as an acyclic graph at the logical level, without needing central coordination in the operational semantics. Participant redirecting. Binary session types specify the types of data that is being sent and received, while local multiparty session types also specify the participants names to/from whom that data is received. These names make programming with first-class sessions non modular since the exact participants are fixed in type signatures. Suppose that one has library functions 𝑓 and 𝑔 such that 𝑓 returns a session of a certain session type, and 𝑔 expects an argument with that same session type, but with different participant names. We introduce a łredirectingž construct, which allows an endpoint to be passed to functions where different participant names are expected. Using this construct, we give a type-preserving translation from binary session types into MPGV, showing that MPGV restricted to two participants per session is at least as expressive as GV. Mechanization. The complexities of session types, especially in the multiparty setting, and the existence of published broken proofsÐincluding the failure of subject reduction for several multiparty systems [Scalas and Yoshida 2019a]Ðgave the impetus for mechanization. Whereas there exists extensive work on mechanizing the meta-theory of binary session types [Thiemann 2019; Rouvoet et al. 2020; Hinrichsen et al. 2021; Tassarotti et al. 2017; Goto et al. 2016; Ciccone and Padovani 2020; Castro-Perez et al. 2020; Gay et al. 2020], deadlock freedom for binary session types has only recently been mechanized by Jacobs et al. [2022a]. For multiparty session types, the only mechanization is Zooid by Castro-Perez et al. [2021], which mechanizes the trace semantics of a single multiparty session and proves that it conforms to its global type. In the spirit of this line of work, we provide a full mechanization of all our results in the Coq proof assistant. Contributions and outline. Our main contribution is MPGVÐthe first deadlock-free linear lambda calculus with first-class multiparty sessions, dynamic thread and channel initialization, and functional features like general recursive functions and algebraic data types. Concretely: • We explain the key ideas behind MPGV in the context of new and existing examples (ğ2 ). • We formalize the type system and operational semantics of MPGV (ğ3 ). • We give a type-preserving embedding of GV-style binary session types into MPGV, using our new redirecting construct, showing that MPGV goes strictly beyond binary session types (ğ4 ). • We prove a combined partial deadlock and memory-leak freedom theorem for multiparty session types that also subsumes type safety and global progress (ğ5 and ğ7 ). • Inspired by Scalas and Yoshida [2019a], we extend MPGV with a more flexible notion of consis- tency that does not rely on global types (ğ6 ). • We mechanize all our results in the Coq proof assistant (ğ8 ). 2 MPGV BY EXAMPLE We introduce MPGV’s features, based on examples (ğ2.1 ś ğ2.8 ), and provide the main intuitions for how MPGV guarantees deadlock freedom for cyclic intra-session topologies (ğ2.9 ). 2.1 Global and Local Types Similar to original multiparty session types [Honda et al. 2008], sessions in MPGV can be described by a global type. A simple example of a global type is: 𝐺 ≜ [0 → 1]N.[1 → 2]N.[2 → 0]N.End. This global type says that participant 0 first sends a value of natural number type N to participant 1, then 1 sends a N to 2, then 2 sends a N to 0, and finally the protocol ends. The global type 𝐺 induces Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:4 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers local types for each participant 𝑝 via projections 𝐺 ⇂ 𝑝 : 𝐺 ⇂ 0 = ![1]N.?[2]N.End 𝐺 ⇂ 1 = ?[0]N.![2]N.End 𝐺 ⇂ 2 = ?[1]N.![0]N.End The local type ![𝑝 ]𝜏.𝐿 indicates that the next action should be sending a value 𝑣 of type 𝜏 to participant 𝑝 , to then continue with 𝐿 . Dually, ?[𝑝 ]𝜏.𝐿 indicates that the next action should be receiving a value 𝑣 of type 𝜏 from participant 𝑝 , to then continue with 𝐿 . Finally, End states that the protocol has finished and the participant’s endpoint should be closed. 2.2 Combined Session and Channel Initialization With our simple global type 𝐺 at hand, we now give a program that implements this global type: let 𝑐 : ![1]N.?[2]N.End = fork(service , service ) in 0 1 2 let 𝑐 : ?[2]N.End = send[1](𝑐 , 99) in 0 0 let (𝑐 ,𝑛 ) : End × N = receive[2](𝑐 ) in 0 0 close(𝑐 ) The fork operation simultaneously forks off 2 threads and creates 3 channel endpoints for the participants in the session. The fork returns endpoint 𝑐 with type 𝐺 ⇂ 0 = ![1]N.?[2]N.End, and runs functions service and service (shown below) in background threads. The main thread uses 1 2 send[1](𝑐 , 99) to send the message ł 99ž to participant 1 ( i.e., service ). As is common in functional 0 1 session-typed languages, the send and receive operations of MPGV return the endpoint back to us. The returned endpoint will be at a different type, because the step has been taken in the session type. For convenience, the above code let-binds the returned endpoint to the same name. The main thread then uses the operation receive[2](𝑐 ) and blocks to receive a message from endpoint 2 (i.e., service ). After the message has been received, it closes the endpoint using close. Similar to many multiparty session-type systems, MPGV uses numbers for participant names in send and receive to indicate which other participant the communication concerns. Note that also for receive it is necessary to indicate which participant to receive from, because multiple participants could send a message to the same participant simultaneously, and these messages may have different types. The endpoint returned from fork has participant number 0, and endpoints of the forked-off threads have participant numbers 1, 2, etc. The forked-off threads could be implemented as: service : (?[0]N.![2]N.End) → 1 service : (?[1]N.![0]N.End) → 1 1 2 service 𝑐 ≜ let (𝑐 ,𝑛 ) = receive[0](𝑐 ) in service 𝑐 ≜ let (𝑐 ,𝑛 ) = receive[1](𝑐 ) in 1 1 1 1 2 2 2 2 let 𝑐 = send[2](𝑐 ,𝑛 + 3) in let 𝑐 = send[0](𝑐 ,𝑛 + 4) in 1 1 2 2 close(𝑐 ) close(𝑐 )) 1 2 The arguments of fork are closures that take the endpoint (typed with local type𝐺 ⇂ 𝑝 ) as argument and return the unit value when done. The first forked-off thread service tries to receive a message from participant 0 (i.e., the main thread), increments the received number, and passes it on to endpoint 2 (i.e., service ). Similarly, the second forked-off thread service receives a number from 2 2 participant 1 (i.e., service ), increments it, and passes it to participant 0 (i.e., the main thread). Novel elements of MPGV. The 𝑛 -ary fork ensures that the communication topology between sessions remains acyclic. This is in contrast to original multiparty session-type systems [Honda et al. 2008], which use service names to create new sessions between already existing, concurrently running processes, selecting the participating processes non-deterministically in case there are several attempting to participate (see ğ9 for an in-depth discussion). By separating session creation from thread spawning in these original systems, cyclic communication topologies can be created, and hence interleaved sessions can deadlock. Inspired by binary session-typed lambda-calculi like GV [Wadler 2012; Lindley and Morris 2015] and multi-cut with coherence proofs [Carbone et al. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:5 2015, 2016, 2017], MPGV combines session creation with thread spawning, to maintain acyclicity of the communication topology and guarantee deadlock freedom. 2.3 Interleaving and First-Class Endpoints We now illustrate MPGV’s support for session interleaving and delegation. Similar to the original versions of GV by Gay and Vasconcelos [2010]; Wadler [2012], MPGV obtains delegation without the need for special language constructs since endpoints are first class. We modify the example from ğ2.2 , which performs its communication actions on 𝑐 locally, by letting the main thread fork off yet another thread to perform the communication: let 𝑐 : 𝐺 ⇂ 0 = fork(service , service ) in 0 1 2 ′ ′ let 𝑑 : 𝐺 ⇂ 0 = fork(𝑑𝜆 : 𝐺 ⇂ 1. let (𝑑 ,𝑥 ) : (![0]N.End) × (𝐺 ⇂ 0) = receive[0](𝑑 ) in 0 1 1 1 let 𝑥 : ?[2]N.End = send[1](𝑥, 99) in let (𝑥,𝑛 ) : End × N = receive[2](𝑥 ) in let 𝑑 : End = send[0](𝑑 ,𝑛 ) in 1 1 close(𝑥 ); close(𝑑 )) in let 𝑑 : ?[1]N.End = send[1](𝑑 ,𝑐 ) in 0 0 0 let (𝑑 ,𝑛 ) : End × N = receive[1](𝑑 ) in 0 0 close(𝑑 ) To type the second fork, we need to come up with a second global type that governs the communi- cation between the third forked-off thread and the main thread: 𝐺 ≜ [0 → 1](𝐺 ⇂ 0).[1 → 0]N.End where 𝐺 ⇂ 0 = ![1]N.?[2]N.End ′ ′ The projections are 𝐺 ⇂ 0 = ![1](𝐺 ⇂ 0).?[1]N.End and 𝐺 ⇂ 1 = ?[0](𝐺 ⇂ 0).![0]N.End. This global type shows that participant 0 (the main thread) of 𝐺 first delegates an endpoint with local type 𝐺 ⇂ 0 to participant 1 of 𝐺 (the third forked-off thread), which then sends a natural number back. In the code, the main thread sends endpoint 𝑐 , which the third forked-off thread receives as 𝑥 . The third forked-off thread then executes the communication according to local type 𝐺 ⇂ 0, and sends back a natural number to the main thread. Novel elements of MPGV. As demonstrated by the above example, MPGV’s session-typed endpoints are first class and can thus be sent over channels ( i.e., delegated) like any other data. MPGV not only allows sending single endpoints over channels, but also lists of endpoints (ğ2.8 ) or closures, which may capture endpoints. Data types that contain endpoints are treated linearly in order to protect type safety, whereas data types that cannot contain endpoints (e.g., lists of natural numbers) may be freely copied and discarded. MPGV guarantees deadlock freedom in the presence of interleaved sessions solely by linear typing and 𝑛 -ary fork, and without any extrinsic mechanisms like orders/priorities [Bettini et al. 2008; Coppo et al. 2013, 2016]. 2.4 Participant Redirecting In the example from ğ2.2 we have two threads service and service that were doing more or less the 1 2 same thing (adding 3 and 4, respectively). To obtain a language that enables modular programming, we would like to write a single function that generalizes both services that we could use for both threads in the fork operation. Let us try to make an attempt: service : N → (?[0]N.![1]N.End) → 1 service 𝑎 𝑐 ≜ let (𝑐,𝑛 ) = receive[0](𝑐 ) in let 𝑐 = send[1](𝑐,𝑛 + 𝑎 ) in close(𝑐 ) Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:6 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers The function service takes a natural number 𝑎 for the value that should be added. Unfortunately, service 3 and service 4 cannot readily be used because their types do not match up with 𝐺 ⇂ 1 = ?[0]N.![2]N.End and 𝐺 ⇂ 2 = ?[1]N.![0]N.End since the participant numbers are off. MPGV provides a redirect[𝜋 ](𝑐 ) operation that allows us to locally redirect participant numbers, making it possible for a programmer to pass endpoints to destinations where different participant numbers are expected in the type signature. The informal semantics of the redirect operation is that any send[𝑝 ] and receive[𝑝 ] operations on 𝑐 = redirect[𝜋 ](𝑐 ) get redirected to send[𝜋 (𝑝 )] and receive[𝜋 (𝑝 )] on 𝑐 . With MPGV’s redirect operation at hand, we can change the fork in the first line of the example in ğ2.2 into: fork(𝑐𝜆 . service 3 (redirect[0 ↦→ 0, 1 ↦→ 2](𝑐 )),𝑐𝜆 . service 4 (redirect[0 ↦→ 1, 1 ↦→ 0](𝑐 ))) 1 1 2 2 Novel elements of MPGV. Redirecting is a novel concept that has not been explored in multiparty session types to our knowledge. Redirecting is important for modularity because it allows composing a function 𝑓 with a function 𝑔 with compatible range and domain types even when participant numbers are at odds. Redirecting is also crucial for embedding binary sessions in MPGV; without redirecting, that would not be possible (see ğ4 ). 2.5 Choice and Recursive Session Types Similar to traditional (multiparty) session types, MPGV supports choice and recursion. For example: ′′ ′′ 𝐺 ≜ [0 → 1]{𝐴 : N.𝐺 , 𝐵 : string.End} In this global type, participant 0 sends participant 1 a choice label {,𝐴 𝐵 }. If the choice label is 𝐴 , then the payload of the message is of type N, and the protocol recursively loops back to the initial state. If the choice label is 𝐵 , then the payload of the message is of type string, and then the protocol ends. This gives the following local projections: ′′ ′′ ′′ ′′ 𝐺 ⇂ 0 ≜ ![1]{𝐴 : N.(𝐺 ⇂ 0), 𝐵 : string.End} 𝐺 ⇂ 1 ≜ ?[0]{𝐴 : N.(𝐺 ⇂ 1), 𝐵 : string.End} With choice, not all global types one can write down are valid: all the branches of a choice must have equal projections for participants that are neither the sender nor the receiver of the choice. This is to ensure that each participant always has enough information to determine the type of the next message that they should send or expect to receive [Honda et al. 2008, 2016]. MPGV supports recursive functions, which are crucial to provide implementations of recursive session types. 2.6 Two Buyer Protocol The two buyer protocol is a classic example from the literature [Honda et al. 2008] with two buyers (Alice and Bob) and a Seller. The protocol has the following global type in MPGV (we use symbolic participant identifiers for readability; one can take 𝑆 = 0, 𝐴 = 1, 𝐵 = 2): 𝐺 ≜ [𝐴 → 𝑆 ]string.[𝑆 → 𝐴 ]N. [𝑆 → 𝐵 ]N.[𝐴 → 𝐵 ]N. 𝑆𝐴𝐵 [𝐵 → 𝑆 ]{Yes : [𝑆 → 𝐵 ]date. End, No : End} This global protocol has the following projections for Alice, Bob, and Seller: 𝐺 ⇂ 𝐴 = ![𝑆 ]string.?[𝑆 ]N.![𝐵 ]N.End 𝑆𝐴𝐵 𝐺 ⇂ 𝐵 = ?[𝑆 ]N.?[𝐴 ]N.![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End} 𝑆𝐴𝐵 𝐺 ⇂ 𝑆 = ?[𝐴 ]string.![𝐴 ]N.![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End} 𝑆𝐴𝐵 The participants perform the following interactions: (1) Alice tells the Seller which item she wants to buy ([𝐴 → 𝑆 ]string). (2) The Seller tells both Alice and Bob how much the item costs ([𝑆 → 𝐴 ]N. [𝑆 → 𝐵 ]N). Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:7 (3) Alice tells Bob how much money she is willing to contribute to the purchase ([𝐴 → 𝐵 ]N). (4) Bob decides whether they can afford the item, and informs the Seller of his decision ( [𝐵 → 𝑆 ]{Yes : . . ., No : . . .}). (5) If Bob says Yes, the Seller sends Bob the date at which the item will be delivered and then ends the protocol ([𝑆 → 𝐵 ]date.End). (6) If Bob says No, the protocol ends immediately (End). A possible implementation of the Seller is as follows: seller : 𝐺 ⇂ 𝑆 → 1 𝑆𝐴𝐵 seller 𝑐 ≜ let (𝑐 ,𝑖𝑡𝑒𝑚 ) : (![𝐴 ]N.![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) × string = receive[𝐴 ](𝑐 ) in 𝑆 𝑆 let 𝑐 : ![𝐵 ]N.?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) = send[𝐴 ](𝑐 , cost(𝑖𝑡𝑒𝑚 )) in 𝑆 𝑆 let 𝑐 : ?[𝐵 ]{Yes : ![𝐵 ]date.End, No : End}) = send[𝐵 ](𝑐 , cost(𝑖𝑡𝑒𝑚 )) in 𝑆 𝑆 match receive [𝐵 ](𝑐 ) with { ⟨Yes :𝑐 : ![𝐵 ]date.End⟩ ↦→ let 𝑐 : End = send[𝐵 ](𝑐 , date(𝑖𝑡𝑒𝑚 )) in close(𝑐 ) 𝑆 𝑆 𝑆 𝑆 ⟨No :𝑐 : End⟩ ↦→ close(𝑐 ) 𝑆 𝑆 In the case ⟨Yes :𝑐 ⟩, we have 𝑐 : ![𝐵 ]date.End, whereas in case ⟨No :𝑐 ⟩ we have 𝑐 : End, so the 𝑆 𝑆 𝑆 𝑆 type of the endpoint depends on which choice was made by Bob. Assuming that we also have functions alice : 𝐺 ⇂ 𝐴 → 1 and bob : 𝐺 ⇂ 𝐵 → 1 for Alice and Bob, we can run the two 𝑆𝐴𝐵 𝑆𝐴𝐵 buyer protocol with program seller (fork(alice, bob)). 2.7 Three Buyer Protocol and Session Delegation The two buyer example has been extended with delegation by Honda et al. [2008]. To help Alice and Bob, there is a fourth person, Carol. If Bob and Alice cannot afford the item together, then instead of replying No to the Seller, Bob will send the remainder of his session to Carol (i.e., delegation). Carol will then respond Yes to the Seller, if the three of them together have enough money. This is modeled by a separate session between Bob and Carol with global type: 𝐺 ≜ [𝐵 → 𝐶 ](N × ![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}).End 𝐶𝐵 Because Bob needs access to Carol, his function is parameterized by that endpoint 𝑐 as well as his own endpoint 𝑐 in the two buyer protocol between him, Alice, and the Seller: bob : 𝐺 ⇂ 𝐵 → 𝐺 ⇂ 𝐵 → 1 del 𝐶𝐵 𝑆𝐴𝐵 bob 𝑐 𝑐 ≜ let (𝑐 ,𝑐𝑜𝑠𝑡 ) : (?[𝐴 ]N.![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}) × N = receive[𝑆 ](𝑐 ) in del 𝐶 𝐵 𝐵 𝐵 let (𝑐 ,𝑐𝑜𝑛𝑡𝑟𝑖𝑏 ) : (![𝑆 ]{Yes : ?[𝑆 ]date.End, No : End}) × N = receive[𝐴 ](𝑐 ) in 𝐵 𝐴 𝐵 if 𝑐𝑜𝑠𝑡 − 𝑐𝑜𝑛𝑡𝑟𝑖𝑏 < 𝑚𝑎𝑥 then let 𝑐 : ?[𝑆 ]date.End = send[𝑆 ](𝑐 , ⟨𝑌𝑒𝑠 ⟩) in 𝐵 𝐵 let (𝑐 ,𝑑𝑎𝑡𝑒 ) : End × date = receive[𝑆 ](𝑐 ) in 𝐵 𝐵 close(𝑐 ) else let 𝑐 : End = send[𝐶 ](𝑐 , (𝑐𝑜𝑠𝑡 − 𝑐𝑜𝑛𝑡𝑟𝑖𝑏 − 𝑚𝑎𝑥 ,𝑐 )) in 𝐶 𝐶 𝐴 𝐵 𝐵 close(𝑐 ) In the else branch, Bob sends his endpoint 𝑐 over his connection to Carol, 𝑐 . We can run the three 𝐵 𝐶 buyer protocol with the following program, assuming that we have carol : 𝐺 ⇂ 𝐶 → 1: 𝐶𝐵 let 𝑐 : 𝐺 ⇂ 𝐵 = fork(carol) in 𝐶 𝐶𝐵 seller (fork(alice, bob 𝑐 )) del 𝐶 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:8 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝐴 𝐴 𝐴 { { { 𝐶 𝐶 𝐶 𝐶 𝑆 𝐵 𝑆 𝐵 𝑆 𝑆 𝐴 𝐴 𝐴 { { { 𝑆 𝐶 𝑆 𝐶 𝑆 𝐶 𝑆 𝐶 1 1 1 1 𝑆 𝑆 𝑆 𝐵 2 𝑆 𝐵 2 𝑆 𝑆 Fig. 1. Steps in three buyer protocol. Top: physical communication paths; bottom: logical connectivity. Depending on thread scheduling, operations can be executed in a different order. One possible execution is graphically depicted in the top row of Figure 1. In the left picture, we have the session between 𝐴 , 𝐵 , and 𝑆 , and the session between 𝐵 and 𝐶 . In our operational semantics, the participants are connected directly, and each participant has their own set of buffers in the heap, separate from the others. At some point Bob decides to send his session to Carol (second picture), so the connections of 𝐵 get moved to 𝐶 . Bob then ends his session with Carol (third picture). Alice ends her participation in the session (fourth picture). This deletes her buffers from the heap, even though the Seller and Carol may still be actively communicating. The global type ensures that whenever Alice is allowed to close her session, the other participants are guaranteed not to perform further communication with her. 2.8 Endpoints in Data Structures Because of the functional nature of MPGV, we can freely intermix sessions and data structures. We give an example of a department store, to which we can send several buyers in a list. The department store will then let the buyers interact by applying the 𝑠𝑒𝑙𝑙𝑒𝑟 function for us. To illustrate recursive protocols, the department store loops around and accepts new buyers: departmentstore : (𝜇𝑥. ?[𝐶 ]List(𝐺 ⇂ 𝑆 ).𝑥 ) → 1 𝑆𝐴𝐵 departmentstore 𝑐 ≜ let (𝑐 ,𝑒𝑑𝑛𝑝𝑜𝑖𝑛𝑡𝑠 ) = receive[𝐶 ](𝑐 ) in 𝐷 𝐷 𝐷 map seller 𝑒𝑑𝑛𝑝𝑜𝑖𝑛𝑡𝑠 ; departmentstore 𝑐 Given a function buyers : string → 𝐺 ⇂ 𝑆 that starts up the two or three buyers trying to buy 𝑆𝐴𝐵 an item of the given name and returns the seller’s endpoint to interact with them, we can start a department store and send buyers to it as follows: let store = fork(departmentstore) in let 𝑐 = buyers ł ℎ𝑎𝑡 ” in let 𝑐 = buyers ł 𝑐𝑜𝑤 ” in let store = send[𝐷 ](store, [𝑐 ;𝑐 ]) in 1 2 let 𝑐 = buyers ł 𝑔𝑒𝑔 ” in let 𝑐 = buyers ł 𝑏𝑜𝑤 ” in let store = send[𝐷 ](store, [𝑐 ;𝑐 ]) in . . . 3 4 Novel elements of MPGV. MPGV allows multiparty endpoints to be stored in data structures, and captured in closures, which can then be sent as messages. This is in contrast to earlier multiparty systems, where endpoints can either not be manipulated at all [Castro-Perez et al. 2021], or where Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:9 there is a separate syntactic category for endpoints, which cannot be mixed with data [Honda et al. 2008; Coppo et al. 2016; Bettini et al. 2008; Coppo et al. 2013]. 2.9 Deadlock Freedom of MPGV MPGV’s deadlock freedom proof is based on two key ideas: (1) local progress within a session is guaranteed by the global type, and (2) global progress between sessions is guaranteed by our 𝑛 -ary fork and linear typing, asserting that the communication topology between sessions remains acyclic (despite first-class endpoints). To reason about deadlock freedom we abstract a logical connectivity topology from the physical communication topology and prove that the logical connectivity topology remains acyclic. The logical topology of the three buyer protocol is depicted in the bottom row of Figure 1. It introduces a blue circle for each multiparty session, abstracting over the cyclic topology within a session and exposing the acyclicity of the logical topology. Figure 1 shows that the logical connectivity topology remains acyclic throughout the execution. This holds for any well-typed MPGV programÐ Figure 10 in ğ 7 shows how the logical topology is transformed and remains acyclic for each of the session operations. Novel elements of MPGV. Similar to binary variants of GV, MPGV ensures global progress and deadlock freedom for an entire program, solely by linear typing. In contrast, earlier multiparty systems either guarantee deadlock freedom only for a single session [Castro-Perez et al. 2021; Honda et al. 2008], or for multiple sessions if types are augmented with extrinsic orders/priorities [Coppo et al. 2016; Bettini et al. 2008; Coppo et al. 2013]. Moreover, our global progress and deadlock freedom theorems are mechanized in Coq (ğ5 ). 3 THE SEMANTICS OF MPGV 3.1 Syntax and Operational Semantics Each configuration in our small-step operational semantics consists of a thread pool and heap, which stores a vector of buffers for each endpoint: fin fin 𝜌 ∈ Cfg ≜ List Expr × Heap ℎ ∈ Heap ≜ Endpoint −⇀ (Participant −⇀ List (Label ×Val)) :: An endpoint 𝑐 ∈ Endpoint = (𝑠,𝑝 ) consists of a number 𝑠 ∈ Session identifying the session, and a number 𝑝 ∈ Participant identifying the participant number of the endpoint in the session. The operational semantics has three reduction relations. Firstly, 𝑒 { 𝑒 for pure reductions pure ′ ′ of expressions. Secondly, (𝑒,ℎ ) { (𝑒 ,ℎ ,𝑒®) for reductions of channel operations involving the head heap ℎ, with the option to spawn a list of new threads 𝑒® (a non-empty list for fork, and an empty ′ ′ list for the other operations). Thirdly, (𝑒,®ℎ ) { (𝑒® ,ℎ ) between configurations, which performs cfg { on some thread in the thread pool, and also handles evaluation contexts. The formal syntax head and operational semantics of MPGV can be found in Figure 2. We give an informal description of the semantics of the message-passing operations fork, send, receive, close, and redirect next. Fork. The fork operation fork(𝑣 , . . .,,𝑣 ) spawns 𝑛 threads and creates a new session between 1 𝑛 the 𝑛 + 1 endpoints. The session 𝑠 has (𝑛 + 1) × (𝑛 + 1) buffers in the heap ℎ for the 𝑛 + 1 endpoints, such that the buffer stored at ℎ(𝑠,𝑞 )(𝑝 ) queues messages sent from 𝑝 to 𝑞 . Session endpoints 𝑐 are represented as triples 𝑐 = #[(𝑠,𝑝 ), 𝜋 ] of a session address 𝑠 ∈ Session, endpoint number fin 𝑝 ∈ Participant, and translation vector 𝜋 : Participant −⇀ Participant, which is used for redirecting and initialized by fork to be the identity mapping. Each of the values 𝑣 passed as arguments to fork must be a closure that accepts an endpoint as its argument, so that the threads run function calls 𝑣 #[(𝑠,𝑖 ), id] for 𝑖 = 1..𝑛 . The fork returns endpoint #[(𝑠, 0), id]. A usage pattern is: let 𝑐 = fork((𝑐𝜆 . 𝑒 ), . . ., (𝑐𝜆 . 𝑒 )) in 𝑒 0 1 1 𝑛 𝑛 0 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:10 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Expressions, values, and evaluation contexts :: 𝑒 ∈ Expr = 𝑥 | () | 𝑛 | (𝑒,𝑒 ) | ⟨ℓ :𝑒 ⟩ | 𝜆𝑥. 𝑒 | rec 𝑓 𝑥. 𝑒 | 𝑒 𝑒 | fork(𝑒, . . .,𝑒 ) | send[𝑝 ](𝑒, ℓ :𝑒 ) | receive[𝑝 ](𝑒 ) | close(𝑒 ) | redirect[𝜋 ](𝑒 ) | let 𝑥 = 𝑒 in 𝑒 | let (𝑥 ,𝑥 ) = 𝑒 in 𝑒 | match 𝑒 with {⟨ℓ :𝑥 ⟩ ↦→ 𝑒 ; . . .} 1 2 ℓ ∈𝐼 𝑣 ∈Val ::= () | 𝑛 | (𝑣,𝑣 ) | ⟨ℓ :𝑣 ⟩ | 𝜆𝑥. 𝑒 | rec 𝑓 𝑥. 𝑒 | #[𝑐, 𝜋 ] 𝐾 ∈ Ctx ::= □ | (𝐾,𝑒 ) | (𝑣,𝐾 ) | 𝐾 𝑒 | 𝑣 𝐾 | let 𝑥 = 𝐾 in 𝑒 | · · · Data structures 𝑠 ∈ Session ≜ N 𝑐 ∈ Endpoint ≜ Session × Participant fin 𝑝,𝑞 ∈ Participant ≜ N 𝜋 ∈ Translation ≜ Participant −⇀ Participant fin fin ℓ ∈ Label ≜ N ℎ ∈ Heap ≜ Endpoint −⇀ (Participant −⇀ List (Label ×Val)) 𝜌 ∈ Cfg ≜ List Expr × Heap Small-step operational semantics (𝑒 ,ℎ) { (𝑒 ,ℎ,𝜖 ) (if 𝑒 { 𝑒 ) 1 head 2 1 pure 2 (fork(𝑣 , . . .,𝑣 ),ℎ) { (#[(𝑠, 0), id],ℎ ⊎ {(𝑠, 0) ↦→ 𝜖,®. . ., (𝑠,𝑛 ) ↦→ 𝜖®}, 1 𝑛 head [𝑣 #[(𝑠, 1), id], . . .,𝑣 #[(𝑠,𝑛 ), id]]) 1 𝑛 (send[𝑞 ](#[(𝑠,𝑝 ), 𝜋 ], ℓ :𝑣 ),ℎ) { (#[(𝑠,𝑝 ), 𝜋 ], push((𝑠, 𝜋 (𝑞 )),𝑝, ⟨ℓ :𝑣 ⟩ ,ℎ),𝜖 ) head (receive[𝑝 ](#[(𝑠,𝑞 ), 𝜋 ]),ℎ) { (⟨ℓ : (𝑣, #[(𝑠,𝑞 ), 𝜋 ])⟩ ,ℎ ,𝜖 ) head ⟨ ⟩ (if pop((𝑠,𝑞 ), 𝜋 (𝑝 ),ℎ) = ( ℓ :𝑣 ,ℎ )) (close(#[(𝑠,𝑝 ), 𝜋 ]),ℎ) { ((),ℎ\{(𝑠,𝑝 )},𝜖 ) head (redirect[𝜋 ](#[(𝑠,𝑝 ), 𝜋 ]),ℎ) { (#[(𝑠,𝑝 ), 𝜋 ◦ 𝜋 ],ℎ,𝜖 ) 1 2 head 2 1 ′ ′ ′ ′ (𝑒 ® ++ [𝐾 [ 𝑒 ]] ++ 𝑒 ® ,ℎ) { (𝑒 ® ++ [𝐾 [ 𝑒 ]] ++ 𝑒 ® ++ 𝑒,®ℎ ) (if (𝑒,ℎ ) { (𝑒 ,ℎ ,𝑒®)) 𝑎 𝑏 cfg 𝑎 𝑏 head Fig. 2. Syntax and operational semantics of MPGV (selected rules). Send. The send operation send[𝑞 ](𝑐, ℓ : 𝑣 ) sends the message ⟨ℓ :𝑣 ⟩ to 𝑞 via the endpoint 𝑐 = #[(𝑠,𝑝 ), 𝜋 ] by adding the message to the end of buffer (using the operation push((𝑠, 𝜋 (𝑞 )),𝑝, ⟨ℓ :𝑣 ⟩ ,ℎ) in Figure 2). The message is tagged with a label ℓ, which can influence the future actions allowed to be performed by the participant. We revisit this in detail when we introduce the typing rules. Our send operation is asynchronous. One can encode synchronous communication by inserting after each message 𝐴 → 𝐵 a dummy message 𝐵 → 𝐴 with type unit to enforce synchronization. Receive. The receive operation receive[𝑝 ](𝑐 ) receives a message from 𝑝 via endpoint 𝑐 = #[(𝑠,𝑞 ), 𝜋 ]. The receive operation takes the first message out of buffer (using the operation pop((𝑠,𝑞 ), 𝜋 (𝑝 ),ℎ) = (⟨ℓ :𝑣 ⟩ ,ℎ ) in Figure 2). If the buffer is empty, the operation blocks until a message becomes available. Close. The close operation close(𝑐 ) deletes all the buffers from which the endpoint 𝑐 = #[(𝑠,𝑞 ), 𝜋 ] receives messages, that is, it simply deletes entry ℎ((𝑠,𝑞 )) of the heap. fin Redirect. The redirecting operation 𝑐 = redirect[𝜋 ](𝑐 ) where 𝜋 ∈ Participant −⇀ Participant redirects messages so that send and receive operations to 𝑝 on 𝑐 are redirected to 𝜋 (𝑝 ) on 𝑐 . Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:11 Γ ⊥ Γ Γ ⊢ 𝑒 :𝜏 ⇒ = 𝜏 Γ ⊢ 𝑒 :𝜏 (⇒ =) ∈ {→,−◦} 1 2 1 1 1 2 2 2 1 Γ unr 𝑥 ∉ Γ {𝑥 ↦→ 𝜏 } ∪ Γ ⊢ 𝑥 :𝜏 Γ ∪ Γ ⊢ 𝑒 𝑒 :𝜏 1 2 1 2 2 Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 𝑥 ∉ Γ Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 Γ unr 𝑥 ∉ Γ 1 2 1 2 Γ ⊢ 𝜆𝑥. 𝑒 :𝜏 −◦ 𝜏 Γ ⊢ 𝜆𝑥. 𝑒 :𝜏 → 𝜏 1 2 1 2 Γ ∪ {𝑓 ↦→ (𝜏 → 𝜏 ),𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 Γ unr 𝑓 ,𝑥 ∉ Γ Γ ⊢ 𝑒 :𝜏 1 2 1 2 ℓ Γ ⊢ rec 𝑓 𝑥. 𝑒 :𝜏 → 𝜏 Γ ⊢ ⟨ℓ :𝑒 ⟩ :Σ . 𝜏 1 2 ℓ ∈𝐼 ℓ Γ ⊥ Γ Γ ⊢ 𝑒 :Σ . 𝜏 ∀ℓ ∈ 𝐼. Γ ∪ {𝑥 ↦→ 𝜏 } ⊢ 𝑒 :𝜏 𝑥 ∉ Γ (𝐼 = ∅ =⇒ Γ = ∅) 1 2 1 ℓ ∈𝐼 ℓ 2 ℓ ℓ ℓ ℓ 2 2 Γ ∪ Γ ⊢ match 𝑒 with {⟨ℓ :𝑥 ⟩ ↦→ 𝑒 ; . . .} :𝜏 1 2 ℓ ℓ ℓ ∈𝐼 Γ ⊥ · · · ⊥ Γ consistent(𝐿 , 𝐿 , . . ., 𝐿 ) ∀𝑝 ∈ {1..𝑛 }. Γ ⊢ 𝑒 :𝐿 −◦ 1 Γ ⊢ 𝑒 :End 1 𝑛 0 1 𝑛 𝑝 𝑝 𝑝 Γ ∪ · · · ∪ Γ ⊢ fork(𝑒 , . . .,𝑒 ) :𝐿 Γ ⊢ close(𝑒 ) :1 1 𝑛 1 𝑛 0 Γ ⊥ Γ Γ ⊢ 𝑒 :![𝑝 ]{ℓ : 𝜏 . 𝐿 } Γ ⊢ 𝑒 :𝜏 Γ ⊢ 𝑒 :?[𝑝 ]{ℓ : 𝜏 . 𝐿 } 1 2 1 1 ℓ ℓ ℓ ∈𝐼 2 2 ℓ ℓ ℓ ℓ ∈𝐼 Γ ∪ Γ ⊢ send[𝑝 ](𝑒 , ℓ :𝑒 ) :𝐿 Γ ⊢ receive[𝑝 ](𝑒 ) :Σ . 𝜏 × 𝐿 1 2 1 2 ℓ ℓ ∈𝐼 ℓ ℓ Γ ⊢ 𝑒 :𝜋 (𝐿 ) Γ ⊢ redirect[𝜋 ](𝑒 ) :𝐿 Fig. 3. Selected MPGV typing rules. Operationally, this composes the translation vector of 𝑐 with 𝜋 : redirect[𝜋 ](#[(𝑠,𝑝 ), 𝜋 ]) = #[(𝑠,𝑝 ), 𝜋 ◦ 𝜋 ] 1 2 2 1 For details, see Figure 2. This operation is required to make multiparty sessions formally subsume binary sessions (ğ4 ), but is independently useful for modular programming with first-class endpoints (ğ2.4 ), because it allows the programmer to pass endpoints to destinations where different endpoint numbers are expected in the type signature. 3.2 Static Type System The functional layer of MPGV features base types, products, closures, sums, and equi-recursive types [Crary et al. 1999]. The message-passing layer of MPGV features multiparty sessions with n-ary choice. Formally the types of MPGV are given by: :: 𝜏 ∈ Type = 1 | N | 𝜏 × 𝜏 | 𝜏 −◦ 𝜏 | 𝜏 → 𝜏 | Σ . 𝜏 | 𝐿 ℓ ∈𝐼 ℓ (𝑐𝑜𝑖𝑑𝑛 ) :: 𝐿 ∈ LType = ![𝑝 ]{ℓ : 𝜏 . 𝐿 } | ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } | End ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) The functional types 𝜏 and local session types 𝐿 are mutually defined: functional types occur as messages in local types, and local types are functional types. To support equi-recursive types, we define Type and LType coinductively, allowing types to refer to themselves [Crary et al. 1999; Gay et al. 2020; Jacobs et al. 2022a; Castro-Perez et al. 2021; Keizer et al. 2021]. Mutually recursive functional types and local types can be constructed using corecursion in the meta logic (i.e., Coq), so Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:12 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers there is no explicit recursion operator. We use = to denote coinductive equivalence (i.e., bisimulation). The typing rules for MPGV’s judgment Γ ⊢ 𝑒 :𝜏 are displayed in Figure 3. 3.2.1 Unrestricted Types. We have linear function types 𝜏 −◦ 𝜏 , which must be used exactly once, 1 2 and whose lambda expressions can capture linear data. We also have unrestricted functions 𝜏 → 𝜏 , 1 2 which can be used any number of times (incl. zero times), but whose lambda expressions cannot capture linear data. We define the subset UType ⊆ Type of unrestricted types as: 𝜏 ˜ ∈ UType ::= 1 | N | 𝜏 ˜ × 𝜏 ˜ | 𝜏 → 𝜏 | Σ . 𝜏 ˜ ℓ ∈𝐼 ℓ (𝑐𝑜𝑖𝑑𝑛 ) Note that 𝜏 → 𝜏 is always unrestricted, even if 𝜏 and 𝜏 are restricted, because closures of 1 2 1 2 unrestricted function type cannot contain endpoints. To support linear and unrestricted types in the typing judgment, context disjointness Γ ⊥ Γ is 1 2 defined such that if Γ and Γ both contain variable 𝑥 , the two contexts must assign equal types 1 2 to 𝑥 (i.e., Γ (𝑥 ) = Γ (𝑥 )), and the type they assign to 𝑥 must be an unrestricted type. This ensures 1 2 that the union operation Γ ∪ Γ on contexts is well-defined whenever it is used in the typing rules 1 2 (for instance, if Γ = {𝑥 : N;𝑦 : N} and Γ = {𝑦 : N}, then Γ ∪ Γ = {𝑥 : N;𝑦 : N}). A context is 1 2 1 2 unrestricted if all its types are unrestricted. 3.2.2 Local Types. Local types describe the protocol that an endpoint 𝑐 must follow: • If 𝑐 : ![𝑝 ]{ℓ : 𝜏 . 𝐿 } then the next action on 𝑐 has to be send[𝑝 ](𝑐, ℓ :𝑣 ), and 𝑣 : 𝜏 and the ℓ ℓ ℓ ∈𝐼 ℓ continuation type 𝐿 of 𝑐 is determined by the sent label ℓ ∈ 𝐼 . • If 𝑐 : ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } then the next action on 𝑐 has to be receive[𝑝 ](𝑐 ), and the received label ℓ ℓ ℓ ∈𝐼 ℓ ∈ 𝐼 determines the type 𝜏 of the value received and the next type 𝐿 of 𝑐 . ℓ ℓ • If 𝑐 : End then the next action on 𝑐 must be close(𝑐 ). Due to linear typing of endpoints, we must use each endpoint variable exactly once. Like in other session typed languages, this is necessary for type safety. For the typing rule of redirect (if 𝑒 : 𝜋 (𝐿 ), then redirect[𝜋 ](𝑒 ) : 𝐿 ), we define the action of a renaming 𝜋 (not necessarily injective) on local types: 𝜋 (![𝑝 ]{ℓ : 𝜏 . 𝐿 } ) ≜ ![𝜋 (𝑝 )]{ℓ : 𝜏 . 𝜋 (𝐿 )} ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝜋 (?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ) ≜ ?[𝜋 (𝑝 )]{ℓ : 𝜏 . 𝜋 (𝐿 )} ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝜋 (End) ≜ End 3.2.3 Global Types and Projections. The typing rule for fork (Figure 3) requires a session’s local types 𝐿 , . . ., 𝐿 to be consistent. Consistency means, for instance, that if participant 𝑝 sends a value 0 𝑛 of type 𝜏 to participant 𝑞 , then 𝑞 is expecting to receive a value of type 𝜏 from 𝑝 at that point in the protocol. Traditionally, consistency is defined by the existence of a global type that governs the communication between all participants in a session. Global types are of the form: 𝐺 ∈ GType ::= [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝐺 } | End 1 2 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) A global type [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝐺 } expresses that the first action in the protocol is for participant 1 2 ℓ ℓ ℓ ∈𝐼 𝑝 to send a message to 𝑝 , such that if the label in the message is chosen to be ℓ, then the payload 1 2 of the message has to have type 𝜏 , and then the global protocol continues as 𝐺 . Note that łglobalž ℓ ℓ in our use of łglobal typež means global with respect to a session, not the whole programÐeach different session started by a fork can have its own global type. Local types can be extracted from global types by a projection judgment 𝐺 ⇂ 𝑝 = 𝐿 , indicating that participant 𝑝 ’s local type is 𝐿 if the global type is 𝐺 . The judgment is coinductively defined in Figure 4. The first two rules state how the sender and receiver of a message in the global type are Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:13 𝑟 ≠ 𝑞 ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 𝑟 ≠ 𝑝 ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ ℓ ℓ ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· [𝑟 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } [𝑝 → 𝑟 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 𝑟 ∉ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝐺 ⇂ 𝑟 = 𝐿 𝑟 guards 𝐺 𝐼 ≠ ∅ 𝑟 ∉ participants(𝐺 ) ℓ ℓ ·· ····················································································· ·· ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· · ·· [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ⇂ 𝑟 = 𝐿 𝐺 ⇂ 𝑟 = End ℓ ℓ ℓ ∈𝐼 𝑟 ∈ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝑟 guards 𝐺 𝑟 guards [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } 𝑟 guards [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝐺 } ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 Fig. 4. Coinductive projection rules (dotted line) and inductive guardedness rules (solid line). projected. The third rule states how other participants not involved in the message are projected. For participants not involved in the message, we require that participant to guard the rest of the global type, which means that the participant occurs in the global type at finite depth along every branch. The fourth rule states that if a participant does not occur in the global type, then it projects to End. Our projection rules are similar to those of Zooid [Castro-Perez et al. 2021]. Traditionally, consistency consistent(𝐿 , . . ., 𝐿 ) is expressed in terms of a global type 𝐺 such 0 𝑛 that 𝐺 ⇂ 0 = 𝐿 , . . .,𝐺 ⇂ 𝑛 = 𝐿 , and 𝐺 ⇂ 𝑚 = End for 𝑚 > 𝑛 . In ğ6 we develop, inspired by Scalas 0 𝑛 and Yoshida [2019a], a more permissive notion of consistency that is independent of a global type, permitting deadlock-free scenarios for which no appropriate global type can be found. ğ6.2 then shows that the traditional notion of consistency based on global types implies our new notion. 4 TRANSLATION FROM BINARY TO MULTIPARTY We show that a GV-style binary session-typed language falls out as a special mode of use of our multiparty language MPGV by giving a type-preserving translation of binary channel operations into MPGV. We consider this an important benchmark, because whereas traditional multiparty systems do support such a translationÐthe output of the translation does not necessarily fall into the fragment of the language where the type system ensures deadlock freedom if whole programs instead of single sessions are considered. There are two main obstacles in existing systems: (1) after translation, participant numbers do not match up, and (2) in systems such as Coppo et al. [2013]; Bettini et al. [2008]; Coppo et al. [2016], deadlock-freedom mechanisms such as orders/priorities prevent programs from being translated because these orders are absent in the source program, so after translation one must come up with an order on sessions. The latter is not always possible if sessions are used in a different orders in different branches of a conditional. Finally, translation of an expressive language such as GV requires the target language to support storing endpoints in data structures, as GV supports this. MPGV overcomes all these obstacles. We start by giving a short introduction to binary session types, and then show how they can be translated into our language, making use of redirect. Binary session types are equivalent to local types without participant annotations. The annotations are not necessary in the binary case, because there is only one other participant to communicate with: 𝐵 ∈ BType ::= !{ℓ : 𝜏 . 𝐵 } | ?{ℓ : 𝜏 . 𝐵 } | End ℓ ℓ ℓ ∈𝐼 ℓ ℓ ℓ ∈𝐼 (𝑐𝑜𝑖𝑑𝑛 ) The operations for binary channels are defined in terms of multiparty operations as follows: fork (𝑒 ) ≜ redirect[1 ↦→ 0](fork(𝑒 )) send (𝑒 , ℓ :𝑒 ) ≜ send[0](𝑒 , ℓ :𝑒 ) 𝐵 𝐵 1 2 1 2 close (𝑒 ) ≜ close(𝑒 ) receive (𝑒 ) ≜ receive[0](𝑒 ) 𝐵 𝐵 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:14 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Γ ⊢ 𝑒 :J𝐵 K −◦ 1 Γ ⊢ 𝑒 :JEndK Γ ⊥ Γ Γ ⊢ 𝑒 :J!{ℓ : 𝜏 . 𝐵 } K Γ ⊢ 𝑒 :𝜏 𝐿 𝐿 1 2 1 1 ℓ ℓ ℓ ∈𝐼 𝐿 2 2 ℓ Γ ⊢ fork (𝑒 ) :J𝐵 K Γ ⊢ close (𝑒 ) :1 Γ ∪ Γ ⊢ send (𝑒 , ℓ :𝑒 ) :J𝐵 K 𝐵 𝐿 𝐵 1 2 𝐵 1 2 ℓ 𝐿 Γ ⊢ 𝑒 :J?{ℓ : 𝜏 . 𝐵 } K ℓ ℓ ℓ ∈𝐼 𝐿 Γ ⊢ receive (𝑒 ) :Σ . 𝜏 × J𝐵 K 𝐵 ℓ ∈𝐼 ℓ ℓ 𝐿 Fig. 5. Derivable typing rules for binary session types. We do a binary spawn using the n-ary fork, then the local type of the endpoint of the spawner gets annotated with 1’s (because it is communicating with endpoint 1) and the local type of the endpoint of the forked-off thread gets annotated with 0’s (because it is communicating with endpoint 0). In order to implement a type-preserving translation, we redirect all annotations to 0. This enables us to canonically translate binary session types 𝐵 to multiparty local types J𝐵 K by using 𝑝 = 0 for every participant annotation: J!{ℓ : 𝜏 . 𝐵 } K ≜ ![0]{ℓ : 𝜏 . J𝐿 K } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ ℓ 𝐿 ℓ ∈𝐼 J?{ℓ : 𝜏 . 𝐵 } K ≜ ?[0]{ℓ : 𝜏 . J𝐿 K } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ ℓ 𝐿 ℓ ∈𝐼 JEndK ≜ End We then prove that the usual typing rules for binary session types are derivable in our system. For fork, this amounts to defining a global type J𝐵 K to govern the binary interaction: J!{ℓ : 𝜏 . 𝐵 } K ≜ [0 → 1]{ℓ : 𝜏 . J𝐵 K } ℓ ℓ ℓ ∈𝐼 𝐺 ℓ ℓ 𝐺 ℓ ∈𝐼 J?{ℓ : 𝜏 . 𝐵 } K ≜ [1 → 0]{ℓ : 𝜏 . J𝐵 K } ℓ ℓ ℓ ∈𝐼 𝐺 ℓ ℓ 𝐺 ℓ ∈𝐼 JEndK ≜ End After redirecting, the projections have the right local types for 𝐵 and the dual 𝐵 (flips all ? with ! and vice versa): −1 Lemma 4.1. J𝐵 K ⇂ 0 = 𝜋 (J𝐵 K ) and J𝐵 K ⇂ 1 = J𝐵 K 𝐺 𝐿 𝐺 𝐿 Using this lemma and translation of types, we can prove that the binary typing rules for fork , send , receive and close are derivable (Figure 5). 𝐵 𝐵 𝐵 𝐵 This section shows that MPGV supports the full power of GV-style binary session types, including treatment of sessions as first-class data and dynamic spawning of sessions. Note that redirecting is crucial: without it we are not able to do a type-preserving translation, because local types ![0] and ?[0] are incompatible with ![1] and ?[1]. 5 THE DEADLOCK AND LEAK FREEDOM THEOREM MPGV guarantees strong properties for well-typed programs, while supporting dynamic spawning, session interleaving, and first-class endpoints. These properties are: Type safety: The only way for a thread to get stuck is by blocking to receive from an empty buffer. Session fidelity: The values sent to and received from buffers match the types in the protocol. Global progress: Configurations of a well-typed initial program are either final or can take a step. Deadlock freedom: No subset of the threads get stuck by waiting for each other. Memory leak freedom: All data always remains reachable. Ideally, we would like to capture these properties in a single theorem that subsumes them all. As a first step, we formulate global progress as follows: Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:15 Theorem 5.1 (Global progress). If ∅ ⊢ 𝑒 :1, and ([𝑒 ], ∅) { (𝑒,®ℎ ), then: cfg ′ ′ ′ ′ (1) there exists (𝑒® ,ℎ ) such that (𝑒,®ℎ ) { (𝑒® ,ℎ ), or cfg (2) 𝑒® = () for all 𝑖 ∈ dom(𝑒®) and ℎ = ∅. This theorem rules out whole-program deadlocks and ensures that all buffers have been correctly deallocated when the program finishes. However, this theorem does not guarantee anything as long as there is still a single thread that can step. Thus it does not guarantee local deadlock freedom, nor memory leak freedom while the program is still running. Moreover, it does not even guarantee type safety: a situation in which a thread is stuck on a type error is not ruled out by this theorem as long as there is another thread that can still step. We therefore state partial deadlock freedom and memory leak freedom theorems, but we strengthen both so that they become equivalent. We use the definitions of partial deadlock and memory leak freedom of Jacobs et al. [2022a] and apply them to MPGV. We need the following notions: :: • The set 𝑣 ∈ V = Thread(𝑖 ) | Session(𝑠 ) ranging over possible threads and sessions. • The function refs (𝑣 ) ⊆ V giving the set of sessions that 𝑣 references. (𝑒,®ℎ ) • The predicate blocked (𝑣 ,𝑣 ) stating that thread 𝑣 = Thread(𝑖 ) is blocked on session (𝑒,®ℎ ) 1 2 1 𝑣 = Session(𝑠 ). • The function active(𝑒,®ℎ ) ⊆ V giving the set of active threads and sessions in the configuration. Using these notions, we strengthen partial deadlock freedom to incorporate aspects of memory leak freedom. Definition 5.2 (Partial deadlock/leak). Given a configuration (𝑒,®ℎ ), a subset 𝑆 ⊆ V of the threads and sessions is in a partial deadlock/leak if the following conditions hold: (1) We have ∅ ⊂ 𝑆 ⊆ active(𝑒,®ℎ ). (2) For all threads Thread(𝑖 ) ∈ 𝑆 , the expression 𝑒 cannot step in the heap ℎ. (3) If Thread(𝑖 ) ∈ 𝑆 and blocked (Thread(𝑖 ), Session(𝑠 )), then Session(𝑠 ) ∈ 𝑆 . (𝑒,®ℎ ) (4) If Session(𝑠 ) ∈ 𝑆 and Session(𝑠 ) ∈ refs (𝑣 ), then 𝑣 ∈ 𝑆 . (𝑒,®ℎ ) Definition 5.3 (Partial deadlock/leak freedom). A configuration (𝑒,®ℎ ) is deadlock/leak free if no 𝑆 ⊆ V is in a partial deadlock/leak in (𝑒,®ℎ ). Conversely, we strengthen memory leak freedom (i.e., full reachability) to incorporate aspects of deadlock freedom. Definition 5.4 (Reachability). We inductively define the threads and sessions reachable in (𝑒,®ℎ ): (1) Thread(𝑖 ) is reachable if either • the expression 𝑒 can step in the heap ℎ, or • there exists an 𝑠 such that Session(𝑠 ) is reachable and blocked (Thread(𝑖 ), Session(𝑠 )). (𝑒,®ℎ ) (2) Session(𝑠 ) is reachable if there exists a reachable 𝑣 such that Session(𝑠 ) ∈ refs (𝑣 ). (𝑒,®ℎ ) Definition 5.5 (Full reachability). A configuration (𝑒,®ℎ ) is fully reachable if all 𝑣 ∈ active(𝑒,®ℎ ) are reachable in (𝑒,®ℎ ). As in Jacobs et al. [2022a]’s language for binary sessions, the strengthened versions of deadlock freedom and full reachability are equivalent, and well-typed MPGV programs satisfy both properties: Theorem 5.6. A configuration (𝑒,®ℎ ) is deadlock/leak free if and only if it is fully reachable. Theorem 5.7. If ∅ ⊢ 𝑒 :1 and ([𝑒 ], ∅) { (𝑒,®ℎ ), then (𝑒,®ℎ ) is fully reachable and deadlock/leak cfg free. The final theorem encompasses type safety, session fidelity, deadlock freedom, and memory leak freedom. Global progress (Theorem 5.1) also follows as a corollary from the final theorem. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:16 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 6 EXTENSION: CONSISTENCY WITHOUT GLOBAL TYPES Inspired by Scalas and Yoshida [2019a,b], we define a notion of consistency that does not rely on global types. This notion of consistency plays an important role in our proof of deadlock freedom (ğ7 ), but is also more flexible. It is more flexible in the sense that consistent(𝐿 , . . ., 𝐿 ) (premise of 0 𝑛 fork in Figure 3) may hold even if no global type exists whose projections are 𝐿 , . . ., 𝐿 . For example, 1 𝑛 there exists no global type for the local types 𝐿 = ![1]N.?[1]N.End and 𝐿 = ![0]N.?[0]N.End 0 1 because they both start with a send. Nevertheless, it would be safe and deadlock free to allow this protocol, given an asynchronous semantics. The more flexible notion of consistency we define in ğ6.1 does allow this protocol. In ğ6.2 we show that the existence of a global type for local types implies our flexible notion of consistency. 6.1 Defining Consistency without Global Types At a high level, we define consistent(𝐿 , . . ., 𝐿 ) as follows: 0 𝑛 łThe local types 𝐿 , . . ., 𝐿 of a session are consistent if no deadlock can occur within 0 𝑛 the session when considering all possible interleavings of participant actions, assuming that each participant 𝑝 follows its respective local type 𝐿 .ž Our goal is to define this notion solely as a property of the local types 𝐿 , . . ., 𝐿 , so that consistency 0 𝑛 of a session’s local types can be proven without considering other sessions. To do so, we define the notion of shadow buffers : fin fin 𝑄 ∈ ShadowBuf ≜ Participant −⇀ (Participant −⇀ List(Label × Type)) Shadow buffers are similar to the physical buffers in the heap, but there are two differences. First, whereas the physical buffers contain pairs ⟨ℓ :𝑣 ⟩ of labels and values, shadow buffers contain pairs ⟨ℓ :𝜏 ⟩ of labels and types. Second, whereas the heap concerns all sessions, shadow buffers only concern a single session. Hence, the heap ranges over endpoints (recall that Endpoint ≜ Session × Participant), but shadow buffers range over mere participants. Shadow buffers allow us to simulate the local execution of a session on the abstract level. If all fin the possible local executions allowed by a set of local types L : Participant −⇀ LType on a set of ˆ ˆ shadow buffers 𝑄 are type safe and deadlock free, we say that 𝑄 is consistent with L, which we denote by consistent(𝑄, L), and define as follows: Definition 6.1. The judgment consistent(𝑄, L) is defined as the most permissive relation satisfying the following properties: (1) Consistency is preserved by sends, i.e., for every participant 𝑝 with L(𝑝 ) = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } , ℓ ℓ ℓ ∈𝐼 then consistent(push(𝑞,𝑝, ⟨ℓ :𝜏 ⟩ ,𝑄 ), L[𝑝 := 𝐿 ]). ℓ ℓ (2) Consistency is preserved by receives, i.e., for every participant 𝑞 with L(𝑞 ) = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } , ℓ ℓ ℓ ∈𝐼 ′ ′ ˆ ˆ ˆ and pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ), then ℓ ∈ 𝐼 , and consistent(𝑄 , L[𝑞 := 𝐿 ]), and 𝜏 = 𝜏 . ℓ ℓ (3) Consistency is preserved by channel closure, i.e., for every participant 𝑝 with L(𝑝 ) = End, then consistent(𝑄 \{𝑝 }, L\{𝑝 }). (4) Either all buffers have been deallocated ( 𝑄 = ∅) or there is a participant 𝑞 such that 𝑞 ’s local type L(𝑞 ) is a send or a close, or L(𝑞 ) is a receive and the corresponding buffer contains a value, ′ ′ ˆ ˆ ˆ i.e., pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ) for some label ℓ, type 𝜏 , and new set of shadow buffers 𝑄 . (5) For each participant there is a corresponding set of buffers and vice versa, i.e., dom(L) = dom(𝑄 ). Note that the cases for the preservation of consistent(𝑄, L) under the sends, receives, and channel ′ ′ ′ ′ ˆ ˆ closure refer to a recursive occurrence consistent(𝑄 , L ) for some 𝑄 and L . Since we consider There exist other extensions of (multiparty) session types that allow for a more flexible notion of consistency. In particular, session-type systems with asynchronous subtyping also support this example [Ghilezan et al. 2021; Mostrous et al. 2009]. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:17 the most permissive relation, these recursive occurrences should be interpreted coinductivelyÐwe use Coq’s CoInductive keyword in the mechanization. The first three properties are used to show that the channel operations are type safe and the resulting state is again consistent. The fourth property is used to show deadlock freedom. The fifth property is required for technical reasons because we support the possibility of some participants deallocating their buffers while other participants are continuing to communicate with each other. With this at hand, we define the new consistency predicate used in the fork typing rule: ® ® ® Definition 6.2. We define consistent(𝐿 ) as consistent(init(length(𝐿 )), 𝐿 ), where init(𝑛 ) creates 𝑛 empty buffers, and the list 𝐿 is converted into a map in the natural way. Note that we need to use the finite map representation because some participants can close their channel before others (see Item 3 in Definition 6.1 ), and then they disappear from L (lists do not allow gaps in the middle, whereas finite maps do). 6.2 Global Types Imply Consistency The goal of this section is to show that if there is a global type for a set of local types, then the local types are consistent in the sense of the preceding section: Theorem 6.3. If there is a global type𝐺 with𝑛 +1 participants such that𝐺 ⇂ 0 = 𝐿 , . . .,𝐺 ⇂ 𝑛 = 𝐿 , 0 𝑛 then consistent(𝐿 , . . ., 𝐿 ). 0 𝑛 This lemma shows that we did not lose anything by using the more flexible notion of consistency without global typesÐthe programs we are able to type check with the more flexible notion of consistency are a superset of the programs we are able to type check using global types. We cannot prove Theorem 6.3 directly using coinduction, because the coinductive conclusion is not general enough. We need a more general property that involves the consistency judgment ˆ ˆ consistent(𝑄, L) for an arbitrary set of shadow buffers 𝑄 . Our generalized property (Lemma 6.4) makes use of the notion runtime global types, inspired by the work of Castro-Perez et al. [2021]. Runtime global types. To model the state of a global type during an interaction in which some messages have already been sent but not yet received, we define runtime global types as: ℓ? :: 𝑅 ∈ RType = [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } | Cont 𝐺 1 2 ℓ ℓ ℓ ∈𝐼 (𝑖𝑑𝑛 ) Runtime global types differ from ordinary global types ( ğ3.2.3 ) in three aspects: (1) Operations in runtime global types have an optional label ℓ on the arrow. If no label is present (i.e., [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } ), then both the send and receive remain to happen. If a label ℓ is 1 2 ℓ ℓ ℓ ∈𝐼 present (i.e., [𝑝 → 𝑝 ]{ℓ : 𝜏 . 𝑅 } ), then the send portion (with label ℓ) of the operation has 1 2 ℓ ℓ ℓ ∈𝐼 already happened, but the receive is still pending. (2) Runtime global types are defined inductively rather than coinductively, because only finitely many messages have been sent at any given point in time. (3) Instead of having End, they have Cont 𝐺 , indicating that the protocol continues as ordinary global type 𝐺 . Runtime local type projections. The projections 𝑅 ⇂ 𝑝 = 𝐿 of runtime global types onto local types can be found in Figure 6. These rules are inductively defined. Intuitively, when an operation [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 occurs in the runtime global type, then the projection onto 𝑝 ignores ℓ ℓ ℓ ∈𝐼 the operation and continues with 𝑅 because the send by 𝑝 with label ℓ has already happened. However, the projection onto 𝑞 in this case still has to take the receive part of this operation into Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:18 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝑞 ≠ 𝑟 ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 𝑝 ≠ 𝑟 ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 ℓ ℓ ℓ ℓ ℓ? [𝑟 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ℓ [𝑝 → 𝑟 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ℓ 𝑟 ∉ {𝑝,𝑞 } ∀ℓ ∈ 𝐼. 𝑅 ⇂ 𝑟 = 𝐿 𝐼 ≠ ∅ 𝑞 ≠ 𝑟 𝑅 ⇂ 𝑟 = 𝐿 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = 𝐿 Cont 𝐺 ⇂ 𝑟 = 𝐿 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂ 𝑟 = 𝐿 ℓ ℓ ′ ′ ˆ ˆ ˆ ˆ ˆ ˆ pop(𝑞,𝑝, 𝑄 ) = ⊥ ∀ℓ. 𝑅 ⇂⇂ 𝑄 pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ) 𝑅 ⇂⇂ 𝑄 𝑄 = ∅ ℓ ℓ ℓ ˆ ˆ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂⇂ 𝑄 Cont 𝐺 ⇂⇂ 𝑄 ℓ ℓ [𝑝 → 𝑞 ]{ℓ : 𝜏 . 𝑅 } ⇂⇂ 𝑄 ℓ ℓ Fig. 6. Projections of runtime global types: (1) local type projections 𝑅 ⇂ 𝑝 = 𝐿 , and (2) shadow buffer projections 𝑅 ⇂⇂ 𝑄 (inductive). account, because the receive has not happened yet. The other cases are similar to the projections for ordinary global types (Figure 3), and ensure that the protocol remains well-formed. Runtime buffer projections. We also define the judgment 𝑅 ⇂⇂ 𝑄 , which says that the messages in the runtime global type 𝑅 correspond to the shadow buffers 𝑄 . Runtime global types imply consistency. Using the notion of runtime global type and runtime projections, we are able to show the following lemma: Lemma 6.4. The judgment consistent(𝑄, L) holds if there exists a runtime global type 𝑅 for which the following four conditions hold: (1) 𝑅 ⇂⇂ 𝑄 (2) ∀𝑝. 𝑅 ⇂ 𝑝 = 𝐿 (𝑝 ) (3) participants(𝑅 ) ⊆ dom(L) ˆ ˆ (4) ∀𝑝. if 𝑄 (𝑝 ) = ⊥ then 𝑝 ∉ dom(L) else dom(L) ⊆ dom(𝑄 (𝑝 )). The lemma is proved using coinduction, and relies on a series of auxiliary lemmas (see the Coq development for details [Jacobs et al. 2022b]). Once we have this lemma, Theorem 6.3 follows by relating projection of runtime global types to projection of ordinary global types. 7 PROOF OF DEADLOCK AND LEAK FREEDOM We give an overview of the proof of our main result, Theorem 5.7. The proof is quite technical, but since all parts have been mechanized in Coq [Jacobs et al. 2022b], one can trust the theorems independent of the pen-and-paper description of the proof. We hope to provide enough insights into the proof to make our results reproducible and extensible. The high level structure of the proof is as follows: • We define an invariant on the runtime configuration, which states (1) that everything in the configuration is well-typed and that the buffer contents are consistent with respect to the local types of each channel endpoint, and (2) that the topology of the configuration is acyclic. • We prove that the invariant is preserved by steps of the operational semantics (łpreservationž). • We prove that configurations that satisfy the invariant cannot be in a deadlock (łprogressž). To deal with linearity and acyclicity we use the connectivity graph framework of Jacobs et al. [2022a], which provides a couple of features to make our proof feasible. First, it provides a generic construction to define the invariantÐit allows us to provide local invariants for threads and channels, which the framework then lifts to an invariant for whole runtime configurations. Second, it makes use of separation logic to hide reasoning about linearity. Third, it provides generic reasoning principles to prove the preservation (of acyclicity and typing) and progress parts of the proof. Fourth, it is implemented as a library in Coq, so it allows us to mechanize our proofs. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:19 fin 𝑃,𝑄 ∈ sProp ≜ (V −⇀ E) → Prop V ::= Thread(𝑖 ) | Session(𝑠 ) (Emp)(Σ) ≜ (Σ = ∅) E ≜ Participant × LType fin (False)(Σ) ≜ False Σ ∈ V −⇀ E (True)(Σ) ≜ True (𝑃 ∨ 𝑄 )(Σ) ≜ 𝑃 (Σ) ∨ 𝑄 (Σ) (⌜𝜙 ⌝)(Σ) ≜ 𝜙 ∧ (Σ = ∅) (𝑃 ∧ 𝑄 )(Σ) ≜ 𝑃 (Σ) ∧ 𝑄 (Σ) ′ ′ (own(Σ ))(Σ) ≜ (Σ = Σ ) (∃𝑥. 𝑃 (𝑥 ))(Σ) ≜ ∃𝑥. 𝑃 (𝑥 )(Σ) (𝑃 )(Σ) ≜ 𝑃 (∅) ∧ Σ = ∅ (∀𝑥. 𝑃 (𝑥 ))(Σ) ≜ ∀𝑥. 𝑃 (𝑥 )(Σ) (𝑃 ∗ 𝑄 )(Σ) ≜ ∃Σ Σ . dom(Σ ) ∩ dom(Σ ) = ∅ ∧ Σ = Σ ⊎ Σ ∧ 𝑃 (Σ ) ∧ 𝑄 (Σ ) 1 2 1 2 1 2 1 2 ′ ′ ′ ′ (𝑃 −∗ 𝑄 )(Σ) ≜ ∀Σ . dom(Σ) ∩ dom(Σ ) = ∅ ∧ 𝑃 (Σ ) ⇒ 𝑄 (Σ ⊎ Σ ) Fig. 7. The definition of the separation logic connectives. At the high-level, the structure of our proof and our use of the connectivity framework is similar to Jacobs et al. [2022a]’s proof for binary session types. To use the framework to obtain the invariant for configurations ( ğ7.3 ), we first define a runtime type system for expressions to express the local invariant for threads (ğ7.1 ), and define a local invariant for the buffers that back a session ( ğ7.2 ). The new element of our proof is handling multiparty instead of binary sessions, for which we make use of our notion of shadow buffers ( ğ6 ). With the invariant for configurations at hand, we prove that this invariant holds for the initial configurations and is preserved by the operational semantics ( ğ7.4 ). The new element is an ex- tension of the connectivity graph framework to handle n-ary graph transformations to support the multiparty case. To complete the proof, we show that the configuration invariant implies Theorem 5.7, our main deadlock freedom theorem (ğ7.5 ). 7.1 Runtime Type System The first step to define the invariant for configurations is to define a runtime typing judgment for expressions. The runtime judgment differs from the static typing judgment ( ğ3.2 ) in the sense that it should account for channel literals #[𝑐, 𝜋 ] that appear after the execution of a fork. Traditionally, this is done by extending the typing judgment Σ; Γ ⊢ 𝑒 : 𝜏 with an additional context Σ that keeps track of the types of the channel literals (often called a heap typing). To avoid having to thread through such this context everywhere, and having to deal with splitting conditions of this context (due to linearity), we make use of separation logic [O’Hearn and Pym 1999; O’Hearn et al. 2001]. This follows the approach in the connectivity graph framework [Jacobs et al. 2022a], which in turn is based on Rouvoet et al. [2020]’s use of separation logic to hide heap typings in intrinsically-typed interpreters for linear languages in Agda. Our runtime judgment Γ ⊨ 𝑒 : 𝜏 is formalized as a separation logic proposition sProp, i.e., a predicate over heap typings Σ. The semantics of the separation logic connectives can be found in Figure 7 and the rules of our runtime type system in Figure 8. Crucially, the use of separating conjunction in the rules of n-ary constructs hides the splitting of the heap typing Σ, and the use of own(𝑠 ↦→ (𝑝, 𝜋 (𝐿 ))) in the rule for endpoint literals #[(𝑠,𝑝 ), 𝜋 ] makes sure the type of each literal matches up with the heap typing Σ. Note that the runtime judgment Γ ⊨ 𝑒 :𝜏 is defined recursively on the structure of 𝑒 . To assert that 𝑃 ∈ sProp is true, means to assert that 𝑃 (∅) holds. The actual type of Σ in Figure 7 also accounts for threads in addition to sessions. This is due to the use of the connectivity graph framework, which we discuss in ğ7.3 . Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:20 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers ⌜Γ unr⌝ ∗ own(𝑠 ↦→ (𝑝, 𝜋 (𝐿 ))) (Γ ∪ {𝑥 ↦→ 𝜏 } ⊨ 𝑒 :𝜏 ) ∗ ⌜Γ unr⌝ ∗ ⌜𝑥 ∉ Γ⌝ 1 2 ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ #[(𝑠,𝑝 ), 𝜋 ] :𝐿 Γ ⊨ 𝜆𝑥. 𝑒 :𝜏 → 𝜏 1 2 ⌜Γ ⊥ · · · ⊥ Γ ⌝ ∗ ⌜consistent(𝐿 , 𝐿 , . . ., 𝐿 )⌝ ∗ [ ] 𝑝 ∈ {1..𝑛 }. Γ ⊨ 𝑒 :𝐿 −◦ 1 1 𝑛 0 1 𝑛 ∗ 𝑝 𝑝 𝑝 -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ∪ · · · ∪ Γ ⊨ fork(𝑒 , . . .,𝑒 ) :𝐿 1 𝑛 1 𝑛 0 Γ ⊨ 𝑒 :End ⌜Γ ⊥ Γ ⌝ ∗ Γ ⊨ 𝑒 :![𝑝 ]{ℓ : 𝜏 . 𝐿 } ∗ Γ ⊨ 𝑒 :𝜏 1 2 1 1 ℓ ℓ ℓ ∈𝐼 2 2 ℓ --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ close(𝑒 ) :1 Γ ∪ Γ ⊨ send[𝑝 ](𝑒 , ℓ :𝑒 ) :𝐿 1 2 1 2 ℓ Γ ⊨ 𝑒 :?[𝑝 ]{ℓ : 𝜏 . 𝐿 } Γ ⊨ 𝑒 :𝜋 (𝐿 ) ℓ ℓ ℓ ∈𝐼 -----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------∗ Γ ⊨ receive[𝑝 ](𝑒 ) :Σ . 𝜏 × 𝐿 Γ ⊨ redirect[𝜋 ](𝑒 ) :𝐿 ℓ ∈𝐼 ℓ ℓ Fig. 8. Selected separation logic runtime typing rules (recursive). local wf(𝑒,®ℎ ) ≜ wf(wf ) (𝑒,®ℎ ) wf(𝑃 ) ≜ ∃𝐺 : Cgraph(V, E). ∀𝑣 ∈ V. 𝑃 (𝑣, in(𝐺,𝑣 ))(out(𝐺,𝑣 )) ⌜Δ = ∅⌝ ∗ (∅ ⊨ 𝑒 :1) if 𝑣 = Thread(𝑖 ),𝑖 < |𝑒®|  𝑖   ⌜Δ = ∅⌝ if 𝑣 = Thread(𝑖 ),𝑖 ≥ |𝑒®| local wf (𝑣, Δ) ≜ fin (𝑒,®ℎ ) ∃L ∈ Participant −⇀ LType. if 𝑣 = Session(𝑠 ) ⌜Δ = toMultiset(L)⌝ ∗ consistent(ℎ| , L) ˆ ˆ ˆ consistent(𝑄, L) ≜ ∃𝑄. ⌜consistent(𝑄, L)⌝ ∗ 𝑄 ∝ 𝑄 ˆ ˆ ˆ ˆ ˆ 𝑄 ∝ 𝑄 ≜ [ ] 𝑄 ;𝑄 ∈ 𝑄 ;𝑄. [ ] 𝑄 ;𝑄 ∈ 𝑄 ;𝑄 . ∗ 𝑝 𝑝 ∗ 𝑝𝑞 𝑝𝑞 𝑝 𝑝 [ ] ⟨ℓ :𝑣 ⟩ ; ⟨ℓ :𝜏 ⟩ ∈ 𝑄 ;𝑄 . ⌜ℓ = ℓ ⌝ ∗ (∅ ⊨ 𝑣 :𝜏 ) ∗ 1 2 𝑝𝑞 𝑝𝑞 1 2 Fig. 9. Configuration invariant. To prove the initialization lemma (Lemma 7.4), we state in separation logic that statically well- typed expressions are well-typed in the runtime type system: Lemma 7.1. ⌜Γ ⊢ 𝑒 :𝜏 ⌝ −∗ Γ ⊨ 𝑒 :𝜏 7.2 The Buffer Invariant We now define an invariant consistent(𝑄, L) to express that the buffers 𝑄 for a given session 𝑠 fin are consistent with respect to a set of local types L : Participant −⇀ LType. The buffer invariant is similar to the consistency judgment consistent(𝑄, L) we defined in ğ6.1 , but it operates on physical buffers 𝑄 (i.e., buffers with values) instead of shadow buffers 𝑄 (i.e., buffers with types): fin fin 𝑄 ∈ Buf ≜ Participant −⇀ (Participant −⇀ List(Label ×Val)) (We use the notation ℎ| to obtain the buffers for a session 𝑠 from the heap ℎ.) Since MPGV allows to send arbitrary data over channels, the values in buffers can themselves contain channel literals. Hence, similar to the runtime typing judgment, the buffer invariant needs to be indexed by a heap typing Σ, which we hide again by considering consistent(𝑄, L) to be a Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:21 separation logic proposition sProp. The definition of consistent(𝑄, L) ∈ sProp can be found in Figure 9. This definition contains two key ingredients. First, it makes use of consistent(𝑄, L) ∈ Prop from ğ6 to specify that local types L are consistent with some (existentially quantified) shadow ˆ ˆ buffers 𝑄 . Second, it makes use of the auxiliary definition 𝑄 ∝ 𝑄 ∈ sProp in Figure 9 to specify that the labels in the physical buffers 𝑄 are equal to those in the shadow buffers 𝑄 , and that the values in the physical buffers 𝑄 have types determined by the corresponding entry in the shadow buffers 𝑄 . (The notation [ ] 𝑥 ;𝑦 ∈ 𝑋 ;𝑌. 𝑃 (𝑥,𝑦 ) in Figure 9 is an n-ary separating conjunction: it states that the collections 𝑋,𝑌 (lists or finite maps) have the same domain, and gives 𝑃 (𝑋 ,𝑌 ) ∗ · · · ∗𝑃 (𝑋 ,𝑌 ), 0 0 𝑛 𝑛 where (𝑋 ,𝑌 ) are corresponding elements in the collections.) 𝑖 𝑖 The invariant consistent(𝑄, L) for physical buffers has preservation and initialization properties paralleling to the rules of the consistency relation consistent(𝑄, L) for shadow buffers ( Defini- tions 6.1 and 6.2). Since consistent(𝑄, L) is a separation logic proposition, these properties are stated using the separation logic connectives (and thus implicitly describe the threading and splitting of the heap typing Σ). Lemma 7.2. The buffer invariant is preserved by a sends, receives, and channel closure: • If L(𝑝 ) = ![𝑞 ]{ℓ : 𝜏 . 𝐿 } , then: ℓ ℓ ℓ ∈𝐼 (∅ ⊨ 𝑣 :𝜏 ) ∗ consistent(𝑄, L) −∗ consistent(push(𝑞,𝑝, ⟨ℓ :𝜏 ⟩ ,𝑄 ), L[𝑝 := 𝐿 ]). ℓ ℓ ℓ ˆ ˆ • If L(𝑞 ) = ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } , and pop(𝑞,𝑝, 𝑄 ) = (⟨ℓ :𝜏 ⟩ ,𝑄 ), then ℓ ℓ ℓ ∈𝐼 consistent(𝑄, L) −∗ ⌜ℓ ∈ 𝐼 ⌝ ∗ consistent(𝑄 , L[𝑞 := 𝐿 ]) ∗ (∅ ⊨ 𝑣 :𝜏 ). ℓ ℓ • If L(𝑝 ) = End, then consistent(𝑄, L) −∗ consistent(𝑄 \{𝑝 }, L\{𝑝 }). ® ® ® Lemma 7.3. If consistent(𝐿 ), then Emp −∗ consistent(init(length(𝐿 )), 𝐿 ). 7.3 The Configuration Invariant The invariant wf(𝑒,®ℎ ) for configurations (𝑒,®ℎ ) ensures that every thread in 𝑒® is well-typed, the contents of the buffers ℎ| for each session 𝑠 in ℎ are well-typed, the types of the channel literals match up with the types of the channels, and the communication topology is acyclic. To define this invariant, we instantiate the connectivity graph framework of Jacobs et al. [2022a] with the runtime typing judgment from ğ7.1 and the buffer invariant from ğ7.2 . The first ingredient of the connectivity framework is the data type Cgraph(V, E), which represents a directed graph with vertices ranging over the set V and edge labels ranging over the set E. This graph should be acyclic in an undirected sense (i.e., the undirected erasure of the graph forms an undirected unrooted forest). We instantiate V and E in Cgraph(V, E) as follows: V ::= Thread(𝑖 ) | Session(𝑠 ) E ≜ Participant × LType The second ingredient of the connectivity graph framework is a generic invariant wf(𝑃 ), which lifts a local invariant predicate 𝑃 (𝑣, Δ) ∈ sProp to whole runtime configurations. The local predicate 𝑃 links the local configuration state of each vertex 𝑣 (i.e., the expression for a thread and the buffers for a session) to the multiset Δ of labels on the incoming edges of vertex 𝑣 . Our instantiation local 𝑃 (𝑣, Δ) ≜ wf (𝑣, Δ) is given in Figure 9. Intuitively, the local invariant for a thread (case (𝑒,®ℎ ) 𝑣 = Thread(𝑖 )) says that the expression 𝑒 of that thread is well-typed in the runtime type system with respect to the local types on the outgoing edges of the thread’s vertex in the connectivity graph. The local invariant for a session (case 𝑣 = Session(𝑠 )) says that the buffers ℎ| of that session are well-typed with respect to the local types on the incoming edges of the session’s vertex in the connectivity graph, where the endpoints stored in the buffers get their local types from the outgoing edges. The invariant for the whole configuration wf(𝑒,®ℎ ) says that there exists an acyclic graph 𝐺 : Cgraph(V, E) such that the local invariant predicate holds for all 𝑣 ∈ V. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:22 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 𝑇 𝑇 𝑣 𝑣 𝑣 𝑆 1 𝑖 𝑛 ... ... 𝐿 𝐿 1 𝑛 fork(𝑣 , · · · ,𝑣 ) { 𝑐 1 𝑛 𝑇 𝑇 𝑇 1 · · · · · · 𝑛 𝑣 𝑣 𝑣 1 𝑖 𝑛 ... ... ? ? ![𝑝 ]{ℓ : 𝜏 . 𝐿 } ℓ ℓ ℓ ∈𝐼 𝐿 ℓ 𝑇 𝑆 ? 𝑇 𝑆 ? send[𝑝 ](𝑐, ℓ :𝑣 ) { 𝑐 ? ? 𝑣 𝑣 ? ? ?[𝑝 ]{ℓ : 𝜏 . 𝐿 } 𝐿 ℓ ℓ ℓ ∈𝐼 ℓ 𝑇 𝑆 ? 𝑇 𝑆 ? receive[𝑝 ](𝑐 ){ ⟨ℓ : (𝑣,𝑐 )⟩ ? ? 𝑣 𝑣 ? ? close(𝑐 ) { () End 𝑇 𝑆 ? 𝑇 𝑆 ? ? ? Fig. 10. Graphical depiction of how multiparty interactions change the logical connectivity. Blue circles are multiparty sessions, brown squares are threads. A blue circle abstracts over the 𝑛 × 𝑛 communication paths among the 𝑛 session participants, where each endpoint has buffers for incoming messages from every other endpoint. An edge from 𝑇 to 𝑆 indicates that thread 𝑇 has an endpoint of session 𝑆 . An edge from a session 𝑆 to a session 𝑆 indicates that an endpoint of 𝑆 is stored in one of the buffers of 𝑆 . The figure provides a 1 2 2 1 local viewpoint, only depicting the notions directly involved in an interaction and omitting other threads and sessions that are connected to the depicted ones as well. While the communication topology is cyclic within a multiparty session (where the global types rule out deadlock), it is acyclic between multiparty sessions, an invariant preserved by multiparty interactions. Acyclicity is crucial for deadlock and memory leak freedom. 7.4 Initialization and Preservation of the Invariant The invariant holds for initial configurations and is preserved by the operational semantics: Lemma 7.4. If ∅ ⊢ 𝑒 :1, then wf([𝑒 ], ∅). ′ ′ ′ ′ Lemma 7.5. If (𝑒,®ℎ ) { (𝑒® ,ℎ ), then wf(𝑒,®ℎ ) implies wf(𝑒® ,ℎ ). cfg The proof of the last lemma involves three aspects. First, because the configuration changes, we need to produce a connectivity graph for the new configuration as the connectivity graph is existentially quantified in the configuration invariant wf(𝑒,®ℎ ). Second, we need to show that the new connectivity graph is acyclic in the appropriate sense. Third, we need to show that all the local local invariant predicates wf (𝑣, Δ) still hold. The interesting cases of this proof are the steps that (𝑒,®ℎ ) involve the channel operations, for which the graph transformations are depicted in Figure 10. Proving these graph transformations by picking a new graph by hand is cumbersome (especially in a mechanized proof). The connectivity graph framework therefore provides abstract separation logic lemmas to prove the transformations without having to mention the graph or having to deal Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:23 with its acyclicity explicitly. We can re-use some of these abstract transformation rules, but for the 𝑛 -ary fork we need a new rule (which we state abstractly for arbitrary vertices V and edge labels E). Lemma 7.6. Let 𝑣 ,𝑣 ∈ V and 𝑤 , . . .,𝑤 ∈ V. To prove wf(𝑃 ) implies wf(𝑃 ), it suffices to prove, 1 2 1 𝑛 for all Δ ∈ Multiset E: (1) 𝑃 (𝑣, Δ) −∗ 𝑃 (𝑣, Δ) for all 𝑣 ∈ V \ {𝑣 ,𝑣 ,𝑤 , . . .,𝑤 } 1 2 1 𝑛 (2) 𝑃 (𝑣, Δ) −∗ ⌜Δ = ∅⌝ for all 𝑣 ∈ {𝑣 ,𝑤 , . . .,𝑤 } 2 1 𝑛 (3) 𝑃 (𝑣 , Δ) −∗ ∃ 𝑙 , . . .,𝑙 . (own(𝑣 ↦→ 𝑙 ) −∗ 𝑃 (𝑣 , Δ)) ∗ 1 0 𝑛 2 0 1 𝑃 (𝑣 , {𝑙 , . . .,𝑙 }) ∗ 2 0 𝑛 ([ ]𝑖 ∈ {1..𝑛 }. own(𝑣 ↦→ 𝑙 ) −∗ 𝑃 (𝑣 , ∅)) ∗ 2 𝑖 𝑖 7.5 Proof of the Reachability Theorem We give an intuitive description of the proof of our main reachability theorem (Theorem 5.7). Waiting induction. At the top level of the proof, we apply the waiting induction principle of the connectivity graph library. Waiting induction relies on acyclicity of the graph and allows one to prove a predicate 𝑃 (𝑣 ) for all vertices 𝑣 ∈ V of a graph 𝐺 : Cgraph(V, E), while assuming ′ ′ ′ the łinduction hypothesisž that 𝑃 (𝑣 ) already holds for all vertices 𝑣 such that 𝑣 is waiting for 𝑣 , where łwaiting forž is a binary relation chosen by us. The predicate 𝑃 (𝑣 ) that we aim to prove for all vertices (i.e., threads and sessions) is that 𝑣 is reachable (see Theorem 5.7). The waiting relation we use is based on the blocked (𝑣,𝑣 ) relation, defined in ğ5 . Waiting induction gives us the (𝑒,®ℎ ) following induction hypotheses when proving that 𝑣 is reachable: For threads: If the thread is blocked on a session, we may assume that the session is reachable. For sessions: The owners of the session that are not blocked on this session are reachable. Reachability of threads. To show that a thread is reachable, we must show that it can take a step, or that it is blocked on an endpoint of a session that is reachable. By typing, either the thread can take a pure step, or is a session operation where all subexpressions are values. A session operation can proceed if the structure of the heap is valid, which we can conclude from the configuration invariant. The only possibility for a blocked operation is if we are trying to receive and the buffer we are trying to receive from is currently empty. Here, the waiting induction hypothesis applies (because blocked holds), using which we can show that the session that we (𝑒,®ℎ ) are blocked on is reachable. Then, by the definition of reachability, the thread is also reachable. Reachability of sessions. To show that a session 𝑠 is reachable we must show that there exists a thread or session 𝑣 that is (1) reachable, (2) holds an endpoint of 𝑠 , and (3) is not blocked on 𝑠 . We use the consistency of the buffers and local types of the session to show that there is an endpoint of 𝑠 whose owner 𝑣 is not blocked on this session (though 𝑣 may be blocked on another session). This allows us to use the induction hypothesis to conclude that 𝑣 is reachable (because blocked (Session(𝑠 ),𝑣 ) does not hold). Then, using the definition of reachability for sessions, (𝑒,®ℎ ) we conclude that 𝑠 is reachable. Main results. Theorem 5.7 is obtained by combining the reasoning above with Lemma 7.4 and Lemma 7.5. Global progress (Theorem 5.1) follows as an easy corollary. For two directions of the equivalence of partial deadlock/leak freedom with full reachability (Theorem 5.6), we show that none of the objects in a deadlock/leak are reachable, and vice versa that the set of non-reachable threads and channels forms a deadlock/leak if this set is nonempty. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:24 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers 8 MECHANIZATION All our results have been mechanized in Coq using Iris Proof Mode [Krebbers et al. 2017, 2018] for the separation-logic part. The final results of our mechanization are Theorem 5.1, Theorem 5.6, and Theorem 5.7. We have also mechanized the translation from binary to multiparty in Figure 5 and have proved that it is type preserving. The mechanization is 10.4k lines of Coq code, consisting of 217 definitions, and 638 proved lemmas and theorems. Approximately half of the mechanization consists of results specific to our multiparty calculus, and the other half consists of the framework of Jacobs et al. [2022a], extended with support for n-ary graph transformations (ğ7.4 ). Archive of the mechanization. The Coq mechanization can be found at Jacobs et al. [2022b]. Partial deadlock freedom and the empty type. A surprising technical result of the mecha- nization is that while global progress remains true in the presence of𝑛 -ary sum types, we discovered that partial deadlock freedom is by default false for languages that allow 𝑛 = 0. The reason is that a thread can throw away endpoints by pattern matching on the empty sum type. While this pattern match will never execute because the empty type can only be produced by a looping expression (thus guaranteeing global progress), the thread can still lose an endpoint during a substitution step before the empty pattern match happens. This can create a partial deadlock for the threads holding the other endpoints of the session. To fix this, we amend the typing judgment Γ ⊢ 𝑒 :𝜏 to require the variable context Γ to be empty when pattern matching on an empty sum type. This formally ensures that the thread’s expression keeps track of all endpoints and does not lose any. This does not limit the expressivity of empty types because one can obtain a value of any type from an empty pattern match, including a function that can eat the remaining variables in the context. 9 RELATED WORK To relate MPGV to the existing body of work it is helpful to consider two axes of categorization: mechanization and session type philosophy. The use of a proof assistant to mechanize correctness results has only been taken up recently by the session type community. Typeset pen-and-paper proofs and appeals to results in logic (e.g., cut elimination) still constitute the status quo. We summa- rize mechanizations of session types below, but remark that only two works target mechanization of deadlock freedom up to date: Castro-Perez et al. [2021] for a single multiparty session and Jacobs et al. [2022a] for GV-style binary session types. At first blush, session types can be distinguished into binary and multiparty. Whereas binary session types restrict the concurrent interaction to two participants, multiparty session types allow an arbitrary but statically determined number of participants (łrolesž), by complementing the local perspective of a participant with a global type. A more foundational distinction, especially given the unifying nature of MPGV, is underlying philosophy. Session types [Honda 1993; Honda et al. 1998] have been conceived as a typing discipline for process calculi and as such preserve the fundamental characteristics of concurrent computation. Concurrent computation is inherently non-deterministic and may also give raise to deadlocks. For example, the below session-typed program from [Gay and Vasconcelos 2010] (page 38) is well-typed but deadlocks: ⟨let𝑐 = request𝑎 in let𝑐 = request𝑎 in let (𝑐 ,𝑥 ) = receive𝑐 in send𝑣 𝑐 ⟩ || 1 1 2 2 1 1 2 ⟨let𝑑 = accept𝑎 in let𝑑 = accept𝑎 in let (𝑑 ,𝑦 ) = receive𝑑 in send𝑤 𝑑 ⟩ 1 1 2 2 1 2 1 The program composes two threads (processes) in parallel, amounting to two binary interleaved sessions 𝑎 and 𝑎 . Sessions are initiated by matching a request for a session (request𝑎 ) with 1 2 1 an accept for that session (accept𝑎 ) creating two new endpoints per session (𝑐 and 𝑐 ). The 1 1 2 interleaving of the two sessions causes a deadlock: the receive on 𝑐 blocks the send on 𝑐 , which is 1 2 necessary for the former. The pairing of session requests with matching accepts is non-deterministic. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:25 For example, if we compose the two threads with a third thread that is also accepting a session 𝑎 , then only one of the two accepting threads will be chosen. This initialization pattern carries over to multiparty sessions [Honda et al. 2008, 2016]. In the multiparty case a request is parameterized with the number of participants 𝑛 and accepts with the role names ranging from 1 to 𝑛 − 1. Like binary session types, multiparty session types that assume this initialization pattern can deadlock. In particular, deadlocks can arise if a participant simultaneously engages in several sessions. A strategy adopted by some multiparty session type work (e.g., Castro-Perez et al. [2021]) is to restrict a program to a single global multiparty session, precluding dynamic session spawning and first-class sessions. Alternatively, advanced multiparty session-type systems [Coppo et al. 2013; Bettini et al. 2008; Coppo et al. 2016] employ extrinsic orders/priorities to rule out deadlocks among interleaved multiparty sessions, requiring order annotations in addition to global type declarations. We refer to the line of session type work that adopts the initialization pattern shown above, which separates session creation from thread spawning, as traditional session types. We like to contrast this line of work with the one that adopts an initialization pattern based on cut, inspired by the Curry-Howard correspondence between linear logic and the session-typed 𝜋 -calculus [Caires and Pfenning 2010; Wadler 2012; Lindley and Morris 2015; Kokke et al. 2019], which we refer to as logic-based session types. Logic-based session types come with strong guarantees out of the box. These include, besides session fidelity, deadlock freedom. Given our focus on deadlock freedom, MPGV adopts the initialization pattern of logic-based session types and generalizes GV’s fork construct [Wadler 2012; Lindley and Morris 2015, 2016b, 2017; Fowler et al. 2019, 2021] for binary session types to the 𝑛 -ary setting. The above program would thus not type check in MPGV. A recent extension of GV by Fowler et al. [2021], Hypersequent GV (HGV), adopts hypersequents [Montesi and Peressotti 2018; Kokke et al. 2019], inspired by Avron [1991], to facilitate a tighter correspondence to the session-typed 𝜋 -calculus and simplify GV’s meta theory by accounting for the forest topology of runtime structures. While this account is reminiscent of our notion of logical topology, the specifics of HGV and our MPGV system are quite different. Most notably, HGV employs structural congruences for runtime typing, whereas our dynamics operates on a flat thread pool and heap (allowing an arbitrary thread to step without prior application of structural congruences) and our runtime typing relies on separation logic and connectivity graphs. We next review the individual related work in more detail, referring to our categorization of traditional and logic-based session types as convenient. Given our focus on mechanization, we start with mechanized related work and then conclude with non-mechanized related work. Mechanized. The only existing work on mechanizing deadlock freedom for multiparty session types is Zooid, a DSL by Castro-Perez et al. [2021] embedded in Coq. Although a traditional session type language in spirit, Zooid does neither support session spawning nor delegation, but restricts a program to a single global multiparty session. Zooid programs thus rule out deadlocks caused by multiparty session interleavings by construction. Thanks to a shallow embedding in Coq, Zooid programs can be extracted from Coq to OCaml via Coq’s extraction mechanism. Send and receive operations are handled as monadic operations in which the endpoint is implicit (because there is a unique global session). A shallow embedding of binders works in this context because Zooid variables can only contain purely functional data, which can be represented as Coq data. Our definition of (runtime) global types and projections is inspired by Zooid. MPGV not only differs from Zooid in its support for multiple interacting sessions, first-class endpoints, dynamic spawning, and delegation, but also in statement and precision of the deadlock freedom property. Our mechanization guarantees global progressÐincluding the stronger notions of partial deadlock/leak freedom. Zooid’s main result, on the other hand, is phrased in terms of Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:26 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers traces, asserting that for all traces produced by a well-typed process there exists a matching trace in the larger system. This result relies on properties of global types from the literature and also assumes the ability to choose a favorable schedule. Our mechanization in contrast states deadlock freedom for all executions/schedules and gives a closed end-to-end proof in Coq. Jacobs et al. [2022a] contribute a mechanization of deadlock freedom for a variant of GV, and thus target binary session types. Like our mechanization, theirs accommodates dynamic session spawning and delegation, but restricted to the binary setting. Jacobs et al. [2022a] moreover contribute the notion of a connectivity graph, a parametric proof method for deadlock freedom, relying on acyclicity of the communication topology. We extend this proof method with 𝑛 -ary operations and support of cyclic connectivity within a session governed by consistency. Our generalization to 𝑛 -ary operations also enables our encoding of binary session types in MPGV (ğ4 ). Unlike Jacobs et al.’s variant of GV, our MPGV system moreover supports choice, and thus provides the first mechanization of deadlock and leak freedom for binary session types with choice. Moreover, there exists work on mechanizing the metatheory of binary session types. Thiemann [2019] proves type safety of a linear 𝜆 -calculus with session types inspired by GV. The result does not include deadlock nor memory leak freedom. Hinrichsen et al. [2021] prove type safety for a comprehensive session-typed language with locks, subtyping and polymorphism using Iris in Coq. Their type system is affine, which means that deadlocks are considered safe. Tassarotti et al. [2017] prove termination preservation of a compiler for an affine session-typed language using Iris in Coq. More distantly, there exist various mechanized results involving the 𝜋 -calculus. Goto et al. [2016] prove type safety for a 𝜋 -calculus with a polymorphic session type system in Coq. Their type system allows dropping channels, and hence does not enjoy deadlock nor memory leak freedom. Ciccone and Padovani [2020] mechanize dependent binary session types by embedding them into a 𝜋 -calculus in Agda. They prove subject reduction (i.e., preservation) and that typing is preserved by structural congruence, but not deadlock or memory leak freedom. Similarly, Zalakain and Dardha [2021] mechanize subject reduction of a resource-aware 𝜋 -calculus, focusing on the handling of linear resources through leftover typing. Gay et al. [2020] study various notions of duality in Agda, and show that distribution laws for duality over the recursion operator are unsound. We adopted their approach of using coinductive types for mechanizing general recursive session types. Lastly, mechanizations of choreographic languages [Montesi 2020; Cruz-Filipe et al. 2021a,b] focus on determinism, confluence, and Turing completeness, with deadlock freedom holding by design. Non-mechanized. The work that is most closely related to ours in terms of underlying philoso- phy but non-mechanized is the work by Carbone et al. [2015, 2016, 2017] on coherence proofs. The authors introduce a proof theory grounded in classical linear logic via a Curry-Howard correspon- dence, illuminating the connection between binary and multiparty session types, in a 𝜋 -calculus setting. The correspondence is due the novel notion of coherence, which generalizes duality known from binary session types to compatibility of local types with a global type of a multiparty session. Given a coherence derivation, an𝑛 -ary cut permits composing𝑛 participants concurrently, similar to our 𝑛 -ary fork. Coherence also enables a semantic-preserving translation from multiparty sessions to corresponding binary sessions via an arbiter process [Carbone et al. 2016]. Deadlock freedom follows from cut admissibility and cut elimination, giving a normalization argument. Such an argument is made possible by using cut reductions for the semantics and restricting to a non-Turing complete calculus without loops or recursion. In contrast, we provide a complete mechanization of deadlock freedom of an 𝑛 -ary session-typed functional language, with recursive types, first-class endpoints, and a realistic asynchronous operational semantics based on an unstructured thread pool. Our encoding of binary sessions in MPGV moreover does not require an arbiter process. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:27 Similarly, Caires and Pérez [2016] embed multiparty session types in a binary calculus by a translation from a global type to a medium process. Instead of communicating with each other, the participants communicate with the central medium process. This approach inherits deadlock freedom from the surrounding binary calculus, but requires central coordination and sequentializes the communication. Toninho and Yoshida [2018] show that the interconnection networks of classical linear logic (CLL) are strictly less expressive than those of a multiparty session calculus. Partial multiparty compatibility is used to define a new binary cut rule that can form circular interconnections but preserves the deadlock-freedom of CLL, albeit for a single multiparty session. More distantly related are works that use Kobayashi-style type systems [Kobayashi 1997, 2002, 2006; Giachino et al. 2014; Kobayashi and Laneve 2017] that enrich channel typing with usage information and partial orders to rule out cyclic dependencies among channel actions. In the traditional multiparty setting this is most notably the work by Coppo et al. [2013]; Bettini et al. [2008]; Coppo et al. [2016], which contributes an interaction type system that ensures deadlock freedom not only within but also between several multiparty sessions. This work not only differs from MPGV in that it requires ordering annotations in addition to global type declarations, but also in the statement of the global progress property. To account for processes that lack a communication partner, a possibility in the traditional setting, progress is stated relative to a catalyzing process that, if present, would allow the closed program to step. MPGV sets itself additionally apart in its tight integration with a functional language. Kobayashi-style systems have also been adopted for logic-based binary session types [Dardha and Gay 2018; Kokke and Dardha 2021b,a]. The authors introduce a multicut, which allows for circular topologies within a session. To rule out deadlocks by type checking, session types must be annotated with priorities. Priority polymorphism has been used by Padovani [2014] to support cyclic interleavings of recursive processes. Partial order annotations, called worlds, are also used by Balzer et al. [2019], in a logic-based binary session type calculus that combines linear and shared [Balzer and Pfenning 2017; Balzer et al. 2018] sessions. Shared session types introduce a controlled form of aliasing, an extension we would like to consider in future work. A somewhat orthogonal approach to ensuring progress in the presence of dynamic thread allocation is to make global types more powerful. While traditional multiparty session types involve a fixed number of participants per session, Deniélou and Yoshida [2011]; Demangeon and Honda [2012]; Hu and Yoshida [2017] proposed extensions of single-session systems to make that number dynamic. This line of work does not support sessions as first-class data, and the expressivity is orthogonal to GV and MPGV. Hence, extending MPGV with a dynamic number of participants is an interesting extension for future work. ACKNOWLEDGMENTS We thank the anonymous reviewers for their helpful feedback and especially for their encour- agement to explore a more permissive consistency condition than compliance with a global type, resulting in ğ6 . We are grateful to Jorge Pérez, Bas van den Heuvel, Dan Frumin, and Bernardo Toninho for discussions on this paper and related work. Robbert Krebbers was supported by the Dutch Research Council (NWO), project 016.Veni.192.259. Stephanie Balzer was supported in part by AFOSR under grant FA9550-21-1-0385 (Tristan Nguyen, program manager) and by the National Science Foundation under award number CCF-2211996. Any opinions, findings and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the AFOSR or NSF. Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:28 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers REFERENCES Arnon Avron. 1991. Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence 4 (1991), 225ś248. https://doi.org/10.1007/BF01531058 Stephanie Balzer and Frank Pfenning. 2017. Manifest Sharing with Session Types. PACMPL 1, ICFP (2017), 37:1ś37:29. https://doi.org/10.1145/3110281 Stephanie Balzer, Frank Pfenning, and Bernardo Toninho. 2018. A Universal Session Type for Untyped Asynchronous Communication. In CONCUR (LIPIcs, Vol. 118). 30:1ś30:18. https://doi.org/10.4230/LIPIcs.CONCUR.2018.30 Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. 2019. Manifest Deadlock-Freedom for Shared Session Types. In ESOP (LNCS, Vol. 11423). 611ś639. https://doi.org/10.1007/978-3-030-17184-1_22 Lorenzo Bettini, Mario Coppo, Loris D’Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. 2008. Global Progress in Dynamically Interleaved Multiparty Sessions. In CONCUR (LNCS, Vol. 5201). 418ś433. https: //doi.org/10.1007/978-3-540-85361-9_33 Luís Caires and Jorge A. Pérez. 2016. Multiparty Session Types Within a Canonical Binary Theory, and Beyond. In FORTE (LNCS, Vol. 9688). 74ś95. https://doi.org/10.1007/978-3-319-39570-8_6 Luís Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions. In CONCUR (LNCS, Vol. 6269). 222ś236. https://doi.org/10.1007/978-3-642-15375-4_16 Marco Carbone, Sam Lindley, Fabrizio Montesi, Carsten Schürmann, and Philip Wadler. 2016. Coherence Generalises Duality: A Logical Explanation of Multiparty Session Types. In CONCUR (LIPIcs, Vol. 59). 33:1ś33:15. https://doi.org/10. 4230/LIPIcs.CONCUR.2016.33 Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2015. Multiparty Session Types as Coherence Proofs. In CONCUR (LIPIcs, Vol. 42). 412ś426. https://doi.org/10.4230/LIPIcs.CONCUR.2015.412 Marco Carbone, Fabrizio Montesi, Carsten Schürmann, and Nobuko Yoshida. 2017. Multiparty session types as coherence proofs. Acta Informatica 54, 3 (2017), 243ś269. https://doi.org/10.1007/s00236-016-0285-y David Castro-Perez, Francisco Ferreira, Lorenzo Gheri, and Nobuko Yoshida. 2021. Zooid: A DSL for Certified Multiparty Computation: From Mechanised Metatheory to Certified Multiparty Processes. In PLDI. 237ś251. https://doi.org/10. 1145/3453483.3454041 David Castro-Perez, Francisco Ferreira, and Nobuko Yoshida. 2020. EMTST: Engineering the Meta-theory of Session Types. In TACAS (2) (LNCS, Vol. 12079). 278ś285. https://doi.org/10.1007/978-3-030-45237-7_17 Ruofei Chen, Stephanie Balzer, and Bernardo Toninho. 2022. Ferrite: A Judgmental Embedding of Session Types in Rust. In ECOOP (LIPIcs, Vol. 222). 22:1ś22:28. https://doi.org/10.4230/LIPIcs.ECOOP.2022.22 Luca Ciccone and Luca Padovani. 2020. A Dependently Typed Linear 𝜋 -Calculus in Agda. In PPDP. 8:1ś8:14. https: //doi.org/10.1145/3414080.3414109 Mario Coppo, Mariangiola Dezani-Ciancaglini, Luca Padovani, and Nobuko Yoshida. 2013. Inference of Global Progress Properties for Dynamically Interleaved Multiparty Sessions. In COORDINATION. https://doi.org/10.1007/978-3-642- 38493-6_4 Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. 2016. Global Progress for Dynamically Interleaved Multiparty Sessions. MSCS 26, 2 (2016), 238ś302. https://doi.org/10.1017/S0960129514000188 Karl Crary, Robert Harper, and Sidd Puri. 1999. What is a Recursive Module?. In PLDI. 50ś63. https://doi.org/10.1145/ 301618.301641 Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. 2021a. Certifying Choreography Compilation. In ICTAC (LNCS, Vol. 12819). 115ś133. https://doi.org/10.1007/978-3-030-85315-0_8 Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. 2021b. Formalising a Turing-Complete Choreographic Language in Coq. In ITP (LIPIcs, Vol. 193). 15:1ś15:18. https://doi.org/10.4230/LIPIcs.ITP.2021.15 Ornela Dardha and Simon J. Gay. 2018. A New Linear Logic for Deadlock-Free Session-Typed Processes. In FOSSACS (LNCS, Vol. 10803). 91ś109. https://doi.org/10.1007/978-3-319-89366-2_5 Romain Demangeon and Kohei Honda. 2012. Nested Protocols in Session Types. In CONCUR (LNCS, Vol. 7454). 272ś286. https://doi.org/10.1007/978-3-642-32940-1_20 Pierre-Malo Deniélou and Nobuko Yoshida. 2011. Dynamic multirole session types. In POPL. 435ś446. https://doi.org/10. 1145/1926385.1926435 Mariangiola Dezani-Ciancaglini, Dimitris Mostrous, Nobuko Yoshida, and Sophia Drossopoulou. 2006. Session Types for Object-Oriented Languages. In ESOP (LNCS, Vol. 4067). 328ś352. https://doi.org/10.1007/11785477_20 Simon Fowler, Wen Kokke, Ornela Dardha, Sam Lindley, and J. Garrett Morris. 2021. Separating Sessions Smoothly. In CONCUR (LIPIcs, Vol. 203). 36:1ś36:18. https://doi.org/10.4230/LIPIcs.CONCUR.2021.36 Simon Fowler, Sam Lindley, J. Garrett Morris, and Sára Decova. 2019. Exceptional Asynchronous Session Types: Session Types Without Tiers. PACMPL 3, POPL (2019), 28:1ś28:29. https://doi.org/10.1145/3290341 Simon J. Gay, Peter Thiemann, and Vasco T. Vasconcelos. 2020. Duality of Session Types: The Final Cut. In PLACES (EPTCS, Vol. 314). 23ś33. https://doi.org/10.4204/EPTCS.314.3 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom 107:29 Simon J. Gay and Vasco Thudichum Vasconcelos. 2010. Linear Type Theory for Asynchronous Session Types. JFP 20, 1 (2010), 19ś50. https://doi.org/10.1017/S0956796809990268 Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. 2021. Precise subtyping for asynchronous multiparty sessions. PACMPL 5, POPL (2021), 1ś28. https://doi.org/10.1145/3434297 Elena Giachino, Naoki Kobayashi, and Cosimo Laneve. 2014. Deadlock Analysis of Unbounded Process Networks. In CONCUR (LNCS, Vol. 8704). 63ś77. https://doi.org/10.1007/978-3-662-44584-6_6 Matthew A. Goto, Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, and James Riely. 2016. An Extensible Approach to Session Polymorphism. MSCS 26, 3 (2016), 465ś509. https://doi.org/10.1017/S0960129514000231 Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, and Jesper Bengtson. 2021. Machine-checked semantic session typing. In CPP. 178ś198. https://doi.org/10.1145/3437992.3439914 Kohei Honda. 1993. Types for Dyadic Interaction. In CONCUR (LNCS, Vol. 715). 509ś523. https://doi.org/10.1007/3-540- 57208-2_35 Kohei Honda, Vasco Thudichum Vasconcelos, and Makoto Kubo. 1998. Language Primitives and Type Discipline for Structured Communication-Based Programming. In ESOP (LNCS, Vol. 1381). 122ś138. https://doi.org/10.1007/BFb0053567 Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2008. Multiparty Asynchronous Session Types. In POPL. 273ś284. https://doi.org/10.1145/1328438.1328472 Kohei Honda, Nobuko Yoshida, and Marco Carbone. 2016. Multiparty Asynchronous Session Types. J. ACM 63, 1 (2016), 9:1ś9:67. https://doi.org/10.1145/2827695 Raymond Hu and Nobuko Yoshida. 2017. Explicit Connection Actions in Multiparty Session Types. In FASE (LNCS, Vol. 10202). 116ś133. https://doi.org/10.1007/978-3-662-54494-5_7 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. https://doi.org/10.1016/j.scico.2018.08.005 Keigo Imai, Shoji Yuen, and Kiyoshi Agusa. 2010. Session Type Inference in Haskell. In PLACES (EPTCS, Vol. 69). 74ś91. https://doi.org/10.4204/EPTCS.69.6 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022a. Connectivity graphs: a method for proving deadlock freedom based on separation logic. PACMPL 6, POPL, 1ś33. https://doi.org/10.1145/3498662 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers. 2022b. MPGV Coq development. https://doi.org/10.5281/zenodo. Thomas Bracht Laumann Jespersen, Philip Munksgaard, and Ken Friis Larsen. 2015. Session Types for Rust. In WGP. 13ś22. https://doi.org/10.1145/2808098.2808100 Alex C. Keizer, Henning Basold, and Jorge A. Pérez. 2021. Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols. In ESOP (LNCS, Vol. 12648). 375ś403. https://doi.org/10.1007/978-3-030-72019-3_14 Naoki Kobayashi. 1997. A Partially Deadlock-Free Typed Process Calculus. In LICS. 128ś139. https://doi.org/10.1109/LICS. 1997.614941 Naoki Kobayashi. 2002. A Type System for Lock-Free Processes. I&C 177, 2 (2002), 122ś159. https://doi.org/10.1006/inco. 2002.3171 Naoki Kobayashi. 2006. A New Type System for Deadlock-Free Processes. In CONCUR (LNCS, Vol. 4137). 233ś247. https: //doi.org/10.1007/11817949_16 Naoki Kobayashi and Cosimo Laneve. 2017. Deadlock Analysis of Unbounded Process Networks. Inf. Comput. 252 (2017), 48ś70. https://doi.org/10.1016/j.ic.2016.03.004 Wen Kokke. 2019. Rusty Variation: Deadlock-free Sessions with Failure in Rust. In ICE (EPTCS, Vol. 304). 48ś60. https: //doi.org/10.4204/EPTCS.304.4 Wen Kokke and Ornela Dardha. 2021a. Deadlock-Free Session Types in Linear Haskell. In Haskell Symposium. 1ś13. https://doi.org/10.1145/3471874.3472979 Wen Kokke and Ornela Dardha. 2021b. Prioritise the Best Variation. In FORTE (LNCS, Vol. 12719). 100ś119. https: //doi.org/10.1007/978-3-030-78089-0_6 Wen Kokke, Fabrizio Montesi, and Marco Peressotti. 2019. Better Late Than Never: a Fully-Abstract Semantics for Classical Processes. PACMPL 3, POPL (2019), 24:1ś24:29. https://doi.org/10.1145/3290337 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. https://doi.org/10.1145/3236772 Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017. Interactive Proofs in Higher-Order Concurrent Separation Logic. In POPL. 205ś217. https://doi.org/10.1145/3009837.3009855 Sam Lindley and J. Garrett Morris. 2015. A Semantics for Propositions as Sessions. In ESOP (LNCS, Vol. 9032). 560ś584. https://doi.org/10.1007/978-3-662-46669-8_23 Sam Lindley and J. Garrett Morris. 2016a. Embedding Session Types in Haskell. In Haskell Symposium. 133ś145. https: //doi.org/10.1145/2976002.2976018 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022. 107:30 Jules Jacobs, Stephanie Balzer, and Robbert Krebbers Sam Lindley and J. Garrett Morris. 2016b. Talking Bananas: Structural Recursion For Session Types. In ICFP. 434ś447. https://doi.org/10.1145/2951913.2951921 Sam Lindley and J. Garrett Morris. 2017. Lightweight Functional Session Types. In Behavioural Types: from Theory to Tools. https://homepages.inf.ed.ac.uk/slindley/papers/fst.pdf Fabrizio Montesi. 2020. Introduction to Choreographies. (2020). https://www.fabriziomontesi.com/teaching/ct-2020/files/ chor-notes.pdf Draft. Fabrizio Montesi and Marco Peressotti. 2018. Classical Transitions. CoRR abs/1803.01049 (2018). arXiv:1803.01049 http://arxiv.org/abs/1803.01049 Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. 2009. Global Principal Typing in Partially Commutative Asynchronous Sessions. In ESOP (LNCS, Vol. 5502). 316ś332. https://doi.org/10.1007/978-3-642-00590-9_23 Peter W. O’Hearn and David J. Pym. 1999. The Logic Of Bunched Implications. Bulletin of Symbolic Logic 5, 2 (1999), 215ś244. https://doi.org/10.2307/421090 Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In CSL (LNCS, Vol. 2142). 1ś19. https://doi.org/10.1007/3-540-44802-0_1 Luca Padovani. 2014. Deadlock and lock freedom in the linear 𝜋 -calculus. In LICS. 72:1ś72:10. https://doi.org/10.1145/ 2603088.2603116 Luca Padovani. 2017. A Simple Library Implementation of Binary Sessions. JFP 27 (2017), e4. https://doi.org/10.1017/ S0956796816000289 Frank Pfenning and Dennis Griffith. 2015. Polarized Substructural Session Types. In FoSSaCS (LNCS, Vol. 9034). 3ś22. https://doi.org/10.1007/978-3-662-46678-0_1 Riccardo Pucella and Jesse A. Tov. 2008. Haskell Session Types with (Almost) No Class. In Haskell Symposium. 25ś36. https://doi.org/10.1145/1411286.1411290 Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser. 2020. Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In CPP. 284ś298. https://doi.org/10.1145/3372885.3373818 Alceste Scalas and Nobuko Yoshida. 2016. Lightweight Session Programming in Scala. In ECOOP (LIPIcs, 56). 21:1ś21:28. https://doi.org/10.4230/LIPIcs.ECOOP.2016.21 Alceste Scalas and Nobuko Yoshida. 2019a. Less is more: multiparty session types revisited. PACMPL 3, POPL (2019), 30:1ś30:29. https://doi.org/10.1145/3290343 Alceste Scalas and Nobuko Yoshida. 2019b. Less is more: multiparty session types revisited (technical report). https: //www.doc.ic.ac.uk/research/technicalreports/2018/DTRS18-6.pdf Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A Higher-Order Logic for Concurrent Termination-Preserving Refinement. In ESOP (LNCS, Vol. 10201). 909ś936. https://doi.org/10.1007/978-3-662-54434-1_34 Peter Thiemann. 2019. Intrinsically-Typed Mechanized Semantics for Session Types. In PPDP. 19:1ś19:15. https://doi.org/10. 1145/3354166.3354184 Bernardo Toninho. 2015. A Logical Foundation for Session-Based Concurrent Computation. Ph. D. Dissertation. Carnegie Mellon University and New University of Lisbon. Bernardo Toninho, Luís Caires, and Frank Pfenning. 2013. Higher-Order Processes, Functions, and Sessions: A Monadic Integration. In ESOP (LNCS, Vol. 7792). 350ś369. https://doi.org/10.1007/978-3-642-37036-6_20 Bernardo Toninho and Nobuko Yoshida. 2018. Interconnectability of Session-Based Logical Processes. TOPLAS 40, 4 (2018), 17:1ś17:42. https://doi.org/10.1145/3242173 Philip Wadler. 2012. Propositions as Sessions. In ICFP. 273ś286. https://doi.org/10.1145/2364527.2364568 Uma Zalakain and Ornela Dardha. 2021. 𝜋 with Leftovers: A Mechanisation in Agda. In FORTE (LNCS, Vol. 12719). 157ś174. https://doi.org/10.1007/978-3-030-78089-0_9 Proc. ACM Program. Lang., Vol. 6, No. ICFP, Article 107. Publication date: August 2022.

Journal

ACM SIGBED ReviewAssociation for Computing Machinery

Published: Aug 29, 2022

Keywords: Session types

There are no references for this article.