Access the full text.
Sign up today, get an introductory month for just $19.
References for this paper are not available at this time. We will be adding them shortly, thank you for your patience.
Logical Methods in Computer Science Volume 17, Issue 1, 2021, pp. 20:1–20:35 Submitted Dec. 16, 2019 https://lmcs.episciences.org/ Published Mar. 04, 2021 A SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING AND ITS IMPLEMENTATION a b c d MARIO BRAVETTI , MARCO CARBONE , JULIEN LANGE , NOBUKO YOSHIDA , AND GIANLUIGI ZAVATTARO University of Bologna / INRIA FoCUS Team e-mail address : fmario.bravetti,gianluigi.zavattarog@unibo.it IT University of Copenhagen e-mail address : carbonem@itu.dk Royal Holloway, University of London e-mail address : julien.lange@rhul.ac.uk Imperial College London e-mail address : n.yoshida@imperial.ac.uk Abstract. Session types, types for structuring communication between endpoints in concurrent systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of systems, where a program has not precisely the expected behavior but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed dierently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive de nition of asynchronous subtyping; this tree could be in nite, and the algorithm checks for the presence of nite witnesses of in nite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm. 1. Introduction Session types are behavioural types that specify the structure of communication between the endpoints of a system or the processes of a concurrent program. In recent years, session types have been integrated into several mainstream programming languages (see, e.g., [HY16, Pad17, SY16, LM16, OY16, ABB 16, NHYA18]) where they specify the pattern of interactions that each endpoint must follow, i.e., a communication protocol. The notion of Key words and phrases: Session types, and Concurrency, and Subtyping, and Algorithm. © M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro LOGICAL METHODS CC l IN COMPUTER SCIENCE DOI:10.23638/LMCS-17(1:20)2021 Creative Commons 20:2 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 q1 q1 !pr !nd q1 q2 q3 ?ko !nd !pr ?ok !ko ?nd ?pr !ok ?ok ?ko q q 2 2 M M = M M C S S Figure 1: Hospital Service example. M is the (re ned) session type of the client, M is a supertype of the client M , and M is the session type of the server. 1 !pr ?ok !nd q q 2 3 ?ko Figure 2: Re ned Hospital Service client. M is an asynchronous subtype of M , i.e., a R C re ned session type of the Hospital Service client. duality is at the core of theories based on session types, where it guarantees that each send (resp. receive) action is matched by a corresponding receive (resp. send) action, and thus rules out deadlocks [dBBLZ18] and orphan messages. A two-party communication protocol speci ed as a pair of session types is \correct" (deadlock free, etc) when these types are dual of each other. Unfortunately, in practice, duality is a too strict prerequisite, since it does not provide programmers with the exibility necessary to build practical implementations of a given protocol. A natural solution for relaxing this rigid constraint is to adopt a notion of (session) subtyping which lets programmers implement re nements of the speci cation (given as a session type). In particular, an endpoint implemented as program P with type M can always be safely replaced by another program P with type M whenever M is a 2 1 1 1 subtype of M (written M 4 M in this paper). 2 1 2 The two main known notions of subtyping for session types dier in the type of communication they support: either synchronous (rendez-vous) or asynchronous (over unbounded FIFO channels). Synchronous session subtyping checks, by means of a so-called subtyping simulation game, that the subtype implements fewer internal choices (sends), and more external choices (receives), than its supertype. Hence checking whether two types are related can be done eciently (quadratic time wrt. the size of the types [LY16]). Synchronous session subtyping is of limited interest in modern programming languages such as Go and Rust, which provide asynchronous communication over channels. Indeed, in an asynchronous setting, the programmer needs to be able to make the best of the exibility given by non- blocking send actions. This is precisely what the asynchronous session subtyping oers: it widens the synchronous subtyping relation by allowing the subtype to anticipate send (output) actions, when this does not aect its communication partner, i.e., it will notably execute all required receive (input) actions later. We illustrate the salient points of the asynchronous session subtyping with Figures 1 and 2, which depict the hypothetical session types of the client and server endpoints of a Hospital Service, represented as communicating machines | an equivalent formalism [BZ83, DY12], see Figure 3. Let us consider Figure 1 rst. Machine M (right) is a server which can deal S Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:3 with two types of requests: it can receive either a message nd (next patient data) or a message pr (patient report). After receiving a message of either type, the server replies with ok or ko, indicating whether the evaluation of received data was successful or not, then it returns to its starting state. Machine M (middle) represents the type of the client. It is the dual of the server M (written M ), as required in standard two-party session types S S without subtyping. A programmer may want to implement a slightly improved program which behaves as Machine M (left). This version starts by sending nd , then keeps sending patient reports (pr ) until the previously sent data are deemed satisfactory (it receives ok ). In fact, machine M is a synchronous subtype of machine M , because of the covariance of outputs, i.e., M is a subtype of M , hence it can send fewer messages. Note that M can receive the same messages as M . Machine M in Figure 2 is another re nement of Machine C R M , but M is not a synchronous subtype of M . Instead, M is an asynchronous subtype C R C R of M . Indeed, M is able to receive the same set of messages as M , each of the sent C R C messages are also allowed by M , and the system consisting of the parallel composition of machines M and M communicating via unbounded FIFO channels is free from deadlocks R S and orphan messages. We will use this example (M 4 M ) in the rest of the paper to R C illustrate our theory. Figure 3 gives the session types corresponding to the machines in Figures 1 and 2, where & indicates an external choice and indicates an internal choice. Recently, we have proven that checking whether two types are in the asynchronous subtyping relation is, unfortunately, undecidable [BZ20, BCZ18, LY17, BCZ17]. In order to mitigate this negative result, some theoretical algorithms have been proposed for restricted subclasses of session types. These restrictions can be divided into two main categories: syntactical restrictions, i.e., allowing only one type of non-unary branching (internal or external choice), or adding bounds on the number of pending messages in FIFO communica- tion channels. Both types of restrictions are problematic in practice. Syntactic restrictions disallow protocols featuring both types of internal/external choices, e.g., the machines M and M in Figure 1 contain (non-unary) external and internal choices. On the other hand, applying a bound to the subtyping relation is generally dicult because (i) it is generally undecidable whether such a bound exists, (ii) the channel bounds used in the implementation (if any) might not be known at compile time, and (iii) very simple systems, such as the one consisting of the parallel composition of machines M and M discussed above, require R S unbounded communication channels. The main contribution of this paper is to give a sound algorithm for checking asynchro- nous session subtyping that does not impose syntactical restrictions nor bounds as done in previous works. Overview of our approach. Our approach will allow to algorithmically check the sub- typing between session types like M and M . In a nutshell, our algorithm proceeds as R C follows. We play the classical subtyping simulation game with the subtype and supertype candidates. The game terminates when we encounter a failure, meaning that the two types are not in the subtyping relation, or when we detect a repetitive behaviour in the game. In the latter case, we check whether this repetitive behaviour (which can always be found) satis es sucient conditions that guarantee that the subtyping simulation game will never encounter failures. If the conditions are satis ed the algorithm concludes that the two types are in the subtyping relation, otherwise no nal verdict is returned. More precisely, session subtyping is de ned following a coinductive approach (De - nition 2.6) that formalises a check on the types that can be intuitively seen as a game. At each step of the game, the candidate subtype proposes a challenge (either an input 20:4 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 or an output action to be executed) and the candidate supertype is expected to reply by performing a corresponding action. The game ends in two possible ways: either both types terminate by reaching their end state (success) or the candidate supertype is unable to reply to the challenge (failure). In case of failure, the two types are not in the subtyping relation, otherwise they are. This game is the so-called subtyping simulation game, and we formally represent it as a simulation tree (De nition 3.2). Hence two types are in the subtying relation if and only if their simulation tree does not reach a failure (Theorem 3.4). Recall that asynchronous session subtyping allows the subtype to anticipate output actions wrt. the supertype. Hence, during the subtyping simulation game, a supertype can reply to an output challenge by considering outputs that are not immediately available, but are guarded by inputs. These inputs cannot be forgotten during the game, because they could be necessary to reply to subsequent input challenges. Thus, they are recorded in so-called input trees (De nition 2.2). Due to outputs inside loops, we can accumulate an unbounded amount of inputs, thus generating input trees of unbounded depth. For this reason, it is generally not possible to algorithmically compute the entire simulation tree. To overcome this problem, we propose a termination condition that intuitively says that the computation of the simulation tree can be stopped when we reach a point in the game that precisely corresponds to a previous point, or diers simply because \more" inputs have been accumulated (Theorem 3.8). Using this termination condition, we compute a nite pre x of the simulation tree. Given this nite tree, our algorithm proceeds as follows: (i) it extracts special subtrees, called candidate subtrees, from the tree (De nition 3.6), and then (ii) checks whether all these subtrees satisfy certain properties guaranteeing that, even if we have stopped the game, it would certainly continue without reaching a failure. This is guaranteed if we have stopped the computation of the simulation tree by reaching an already considered point, because subsequent continuations of the game will continue repeating the exact same steps. In contrast, if we have stopped with \more" inputs, we must have the guarantee that all possible continuations of the simulation game cannot be negatively aected by these additional input accumulations. We formalise a sucient condition on candidate subtrees (that are named witness trees when they satisfy such a condition, see De nition 3.16) that provides such a guarantee. Concretely we use input tree equations (a sort of context-free tree grammar, see De ni- tion 3.11) to nitely represent both the possible inputs of the candidate subtype and the inputs that can be accumulated by the candidate supertype. We then de ne a compatibility relation on input tree equations, see De nition 3.12. In a witness tree we impose that the input tree equations of the inputs accumulated by the candidate supertype are compatible with those of the candidate subtype. This implies that the candidate supertype will be always ready to reply to all possible input challenges of the candidate subtype, simply by considering already accumulated inputs (see our main Theorem 3.19). If all the candidate subtrees satisfy our sucient conditions we can conclude that the two initial session types are in the subtyping relation, otherwise the algorithm replies with \I don't know" meaning that it is not possible to conclude with a nal verdict. 1.1. Structure of the paper. The remainder of the paper is structured as follows. § 2 reports some preliminary de nitions, namely the formalisation of session types as communi- cating machines and the de nition of asynchronous session subtyping. Our approach for a sound algorithmic characterisation of asynchronous session subtyping is presented in § 3. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:5 n o M = x: nd : y: & ok : x; ko : fpr : yg n o M = x: nd : & ok : x; ko : fpr : xg M = x: nd : &f ok : x; ko : x g; pr : &f ok : x; ko : x g M = x: & nd : fok : x; ko : xg; pr : fok : x; ko : xg Figure 3: Session types corresponding to the machines in Figures 1 and 2. We also discuss in § 4 a full implementation of our algorithm; this has been used to test our approach on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm. Finally, the paper includes a discussion about related work in § 5 and some concluding remarks in § 6. This article is a full version of [BCL 19a], with improved presentation, re ned de nitions, detailed proofs and additional examples. Moreover, this version presents an empirical evaluation of our algorithm: we tested the implementation of our algorithm on automatically generated session types, see § 4. We have also given an expanded discussion of related work and possible extensions that can be addressed in the future, see § 5 and § 6. 2. Communicating Machines and Asynchronous Subtyping In this section, we recall the de nition of two-party communicating machines, that commu- nicate over unbounded FIFO channels (§ 2.1), and de ne asynchronous subtyping for session types [CDSY17, CDCY14], which we adapt to communicating machines, following [BCZ18] (§ 2.2). 2.1. Communicating Machines. Let A be a ( nite) alphabet, ranged over by a, b, etc. We let !, ! , etc. range over words in A . The set of send (resp. receive) actions is Act = f!gA, (resp. Act = f?g A). The set of actions is Act = Act [ Act , ranged over by `, where a ? ! ? send action !a puts message a on an (unbounded) buer, while a receive action ?a represents def def the consumption of a from a buer. We de ne dir (!a ) = ! and dir (?a ) = ? and let and ' range over Act . We write for the concatenation operator on words and we write for the empty word (overloaded for A and A ). In this work, we only consider communicating machines which correspond to (two-party) session types. Hence, we focus on deterministic (communicating) nite-state machines, without mixed states (i.e., states that can re both send and receive actions) as in [DY12, DY13]. De nition 2.1 (Communicating Machine). A communicating machine M is a tuple (Q; q ; ) where Q is the ( nite) set of states, q 2 Q is the initial state, and 2 Q Act Q is a 0 00 0 transition relation. We further require that 8q; q ; q 2 Q: 8`; ` 2 Act : 0 0 00 0 (1) (q; `; q ); (q; ` ; q ) 2 implies dir (`) = dir (` ), and 0 00 0 00 (2) (q; `; q ); (q; `; q ) 2 implies q = q . 0 0 We write q ! q for (q; `; q ) 2 , omit unnecessary labels, and write ! for the re exive transitive closure of ! . 20:6 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 Condition (1) requires all states to be directed, while Condition (2) enforces determinism, i.e., all actions outgoing from a given state are pairwise distinct. Given M = (Q; q ; ), we say that q 2 Q is nal, written q 9, i 8q 2 Q: 8` 2 0 0 Act: (q; `; q ) 2= . A state q 2 Q is sending (resp. receiving ) i q is not nal and 8q 2 0 0 Q: 8` 2 Act: (q; `; q ) 2 : dir (`) = ! (resp. dir (`) = ?). We use (q; `) to stand for q such that (q; `; q ) 2 . ` ` 1 ` k i We write q ! q i there are q ; : : : ; q 2 Q such that q ! q for 1 i k. 0 k 1 k1 i1 i Given a list of messages ! = a a (k 0), we write ?! for the list ?a ?a and !! for 1 k 1 k !a !a . Given 2 Act we de ne snd( ) and rcv( ): 8 8 0 0 0 0 > > a snd( ) if =!a a rcv( ) if =?a < < 0 0 0 0 snd( ) = snd( ) if =?a rcv( ) = rcv( ) if =!a > > : : if = if = That is snd( ) (resp. rcv( )) extracts the messages in send (resp. receive) actions from a sequence . 2.2. Asynchronous Session Subtyping. 2.2.1. Input trees and contexts. We de ne some structures and functions which we use to formalise the subtyping relation. In particular, we use syntactic constructs used to record the input actions that have been anticipated by a candidate supertype, e.g., machine M in De nition 2.6, as well as the local states it may reach. First, input trees (De nition 2.2) record input actions in a standard tree structure. De nition 2.2 (Input Tree). An input tree is a term of the grammar: T ::= q j ha : T i i i i2I In the sequel, we use T to denote the input trees over states q 2 Q. An input context is an input tree with \holes" in the place of sub-terms. De nition 2.3 (Input Context). An input context is a term of A ::= [ ] j ha : A i , j i i i2I where all indices j, denoted by I (A), are distinct and are associated to holes. For input trees and contexts of the form ha : T i and ha : A i , we assume that i i i2I i i i2I I 6= ;, 8i 6= j 2 I: a 6= a , and that the order of the sub-terms is irrelevant. When convenient, i j we use set-builder notation to construct input trees or contexts, e.g., ha : T j i 2 Ii. i i i2I(A) Given an input context A and an input context A for each i in I (A), we writeA[A ] i i for the input context obtained by replacing each hole [ ] in A by the input context A . We i i i2I(A) write A[T ] for the input tree where holes are replaced by input trees. i Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:7 2.2.2. Auxiliary functions. In the rest of the paper we use the following auxiliary functions on communicating machines. Given a machine M = (Q; q ; ) and a state q 2 Q, we de ne: ?! ?! 0 + 0 0 0 cycle(?; q) () 9! 2 A ; ! 2 A ; q 2 Q: q ! q ! q (with ? 2 f!; ?g), ?a !a 0 0 0 0 in(q) = fa j 9q :q ! q g and out(q) = fa j 9q :q ! q g, let the partial function inTree() be de ned as: ? if cycle(?; q) inTree(q) = q if in(q) = ? ha : inTree((q; ?a ))i if in(q) = fa j i 2 Ig =6 ? i i i2I i Predicate cycle(?; q) says that, from q, we can reach a cycle with only sends (resp. receives), depending on whether ? =! or ? =?. The function in(q) (resp. out(q)) returns the messages that can be received (resp. sent) from q. When de ned, inTree(q) returns the tree containing all sequences of messages which can be received from q until a nal or sending state is reached. Intuitively, inTree(q) is unde ned when cycle(?; q) as it would return an in nite tree. Example 2.4. Given M (Figure 1), we have the following: in(q ) = ; in(q ) = fok; kog 1 2 out(q ) = fnd; prg out(q ) = ; 1 2 inTree(q ) = q inTree(q ) = hok : q ; ko : q i 1 1 2 1 1 Example 2.5. Consider the following machine M : !b !c ?d p p p p 0 1 2 3 !a From state p we can reach state p with an output. The latter can loop into itself. Hence, 0 1 we have both cycle(!; p ) and cycle(!; p ). 0 1 2.2.3. Asynchronous subtyping. We present our de nition of asynchronous subtyping (follow- ing the orphan-message-free version from [CDCY14]). Our de nition is a simple adaptation of [BCZ18, De nition 2.4] (given on syntactical session types) to the setting of communicating machines. De nition 2.6 (Asynchronous Subtyping). Let M = (Q ; q ; ) for i 2 f1; 2g. R is an i i 0 i asynchronous subtyping relation on Q T such that (p; T ) 2 R implies: 1 Q (1) if p 9 then T = q such that q 9; (2) if p is a receiving state then (a) if T = q then q is a receiving state and ?a ?a 0 0 0 0 0 0 8q 2 Q s:t: q ! q : 9p 2 Q s:t: p ! p ^ (p ; q ) 2 R; 2 1 ?a 0 0 0 (b) if T = ha : T i then 8i 2 I: 9p 2 Q s:t: p ! p ^ (p ; T ) 2 R; i i i2I 1 i (3) if p is a sending state then In de nitions for syntactical session types, e.g., [MY15], input contexts are used to accumulate inputs that precede anticipated outputs; here, having no speci c syntax for inputs, we use input trees instead. 20:8 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 (a) if T = q and q is a sending state, then !a !a 0 0 0 0 0 0 8p 2 Q s:t: p ! p : 9q 2 Q s:t: q ! q ^ (p ; q ) 2 R; 1 2 i2I h2H (b) otherwise, if T = A[q ] then :cycle(!; p) and 8i2I:inTree(q ) =A [q ] and i i i i;h !a 0 0 8p 2Q s:t: p ! p : !a 0 0 0 0 h2H i2I 8i2I:8h2H : 9q 2Q s:t: q ! q ^ (p ;A[A [q ] ] ) 2 R. i 2 i i;h i;h i;h i;h M is an asynchronous subtype of M , written M 4 M , if there is an asynchronous subtyping 1 2 1 2 relation R such that (q ; q ) 2 R. 0 0 1 2 The relation M 4 M checks that M is a subtype of M by executing M and simulating 1 2 1 2 1 its execution with M . M may re send actions earlier than M , in which case M is allowed 2 1 2 2 to re these actions even if it needs to re some receive actions rst. These receive actions are accumulated in an input context and are expected to be subsequently matched by M . Due to the presence of such an input context, the states reached by M during the computation are represented as input trees. The de nition rst dierentiates the type of state p: Final: Case (1) says that if M is in a nal state, then M is in a nal state with an empty 1 2 input context. Receiving: Case (2) says that if M is in a receiving state, then either (2a) the input context is empty (T = q) and M must be able to receive all messages that M can 1 2 receive; or, (2b) M must be able to consume all the messages at the root of the input tree. Sending: Case (3) applies when M is in a sending state, there are two sub-cases. Case (3a) says that if the input context is empty (T = q) and q is also a sending state, then M must be able to send all messages that M can send. If this sub-case above 2 1 does not apply (i.e., the input context is not empty or q is not a sending state), then the one below must hold. Case (3b) enforces correct output anticipation, i.e., M must be able to send every a h2H that M can send after some receive actions recorded in each A [q ] . Note that 1 i i;h whichever receiving path M chooses, it must be able to send all possible output actions !a of M , i.e., !a should be available at the end of each receiving path. Moreover, given that there are accumulated inputs, we require that cycle(!; p) does not hold, guaranteeing that subtyping preserves orphan-message freedom, i.e., such accumulated receive actions will be eventually executed. Observe that Case (2) enforces a form of contra-variance for receive actions, while Case (3) enforces a form of covariance for send actions. Example 2.7. Consider M and M from Figures 1 and 2, we have M 4 M (see § 3). A C R R C fragment of the relation R from De nition 2.6 is given in Figure 4. Considering the identi er (bottom left) of each node in Figure 4, we have: Case (1) of De nition 2.6 does not apply to any con guration in this example (there is no nal node in these machines). Case (2a) applies to node n , i.e., q 4 q (note that q are receiving states in both 1 2 2 2 machines). Case (2b) applies to nodes n , n , and n ; where q of machine M is a receiving state 5 9 13 2 R and the input context is not empty. Case (3a) applies to nodes n , n , and n , where the input context is empty and both 0 2 3 states are sending states. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:9 Case (3b) applies to nodes n , n , n , n , n , n , n , n , n , and n . Observe that 4 6 7 8 10 11 12 14 15 16 this case does not require the input context to be non-empty (e.g., n ), and that the condition :cycle(!; p) holds for all states p in M since there is no send-only cycle in this machine. Example 2.8. For the two machines below, we have M 64 M and M 64 M : 1 2 2 1 !b ?c ?c !b p p p q q q 1 2 3 1 2 3 M : M : 1 2 !a !a For the M 64 M case consider the initial con guration (p ; q ). Since p is a sending 1 2 1 1 1 state, but q is a receiving state, Case (3b) appears to be the only applicable case of De nition 2.6. However, we have cycle(!; p ) hence (p ; q ) 2= R, for every asynchronous 1 1 1 subtyping relation R. For the M 64 M case, consider the initial con guration (q ; p ). Since q is a receiving 2 1 1 1 1 state, only Case 2 would be applicable. However, the input context is empty and p is a sending state, therefore neither Case (2a) nor Case (2b) apply hence (q ; p ) 2= R, for every 1 1 asynchronous subtyping relation R. 3. A Sound Algorithm for Asynchronous Subtyping Our subtyping algorithm takes two machines M and M then produces three possible 1 2 outputs: true, false, or unknown, which respectively indicate that M 4 M , M 46 M , or 1 2 1 2 that the algorithm was unable to prove either of these two results. The algorithm consists of three stages. (1) It builds the simulation tree of M and M (see De nition 3.2) that 1 2 represents sequences of checks between M and M , corresponding to the checks in the 1 2 de nition of asynchronous subtyping. Simulation trees may be in nite, but the construction terminates whenever: either it reaches a node that cannot be expanded, it visits a node whose label has been seen along the path from the root, or it expands a node whose ancestors validate a termination condition that we formalise in Theorem 3.8. The resulting tree satis es one of the following conditions: (i) it contains a leaf that could not be expanded because the node represents an unsuccessful check between M and M (in which case the 1 2 algorithm returns false ), (ii) all leaves are successful nal con gurations, see Condition (1) of De nition 2.6, in which case the algorithm replies true, or (iii) for each leaf n it is possible to identify a corresponding ancestor anc(n). In this last case the tree and the identi ed ancestors are passed onto the next stage. (2) The algorithm divides the nite tree into several subtrees rooted at those ancestors that do not have other ancestors above them (see the strategy that we outline on page 16). (3) The nal stage analyses whether each subtree is of one of the two following kinds. (i) All the leaves in the subtree have the same label as their ancestors: in this case all checks required to verify subtyping have been performed. (ii) The subtree is a witness subtree (see De nition 3.16), meaning that all the checks that may be considered in any extension of the nite subtree are guaranteed to be successful as well. If all the identi ed subtrees are of one of these two kinds, the algorithm replies true. Otherwise, it replies unknown. 20:10 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 3.1. Generating Asynchronous Simulation Trees. We rst de ne labelled trees, of which our simulation trees are instances; then, we give the operational rules for generating a simulation tree from a pair of communicating machines. De nition 3.1 (Labelled Tree). A labelled tree is a tree (N; n ; ,! ;L; ; ), consisting of nodes N , root n 2 N , edges ,! N N , and node labelling function L : N 7! . 0 0 Hereafter, we write n ,! n when (n; ; n ) 2,! and write n ,! n when there 1 k+1 0 0 are n ; : : : ; n , such that n ,! n for all 1 i k. We write n ,! n when n ,! n for 1 i i+1 k+1 some and the label is not relevant. As usual, we write ,! for the re exive and transitive closure of ,! , and ,! for its transitive closure. Moreover, we reason up-to tree isomorphism, i.e., two labelled trees are equivalent if there exists a bijective node renaming that preserves both node labelling and labelled transitions. We can then de ne simulation trees, labelled trees representing all possible con gurations reachable by the simulation checked by asynchronous session subtyping. De nition 3.2 (Simulation Tree). Let M = (P; p ; ) and M = (Q; q ; ) be two 1 0 1 2 0 2 communicating machines. The simulation tree of M and M , written simtree(M ; M ), is a 1 2 1 2 labelled tree (N; n ; ,! ;L; Act; P T ). The labels (p; T ) 2 (P T ) are denoted also with 0 Q Q p4 T . In order to de ne ,! and L, we rst consider an Act -labelled relation on (P T ), 0 0 with elements denoted with p4 T ,! p 4 T , de ned as the minimal relation satisfying the following rules: ?a ?a !a !a 0 0 0 0 p ! p q ! q in(p) in(q) p ! p q ! q out(p) out(q) (In) (Out) ?a !a 0 0 0 0 p4 q ,! p 4 q p4 q ,! p 4 q ?a p ! p k 2 I in(p) fa j i 2 Ig (InCtx) ?a p4ha : T i ,! p 4 T i i i2I k !a p ! p :cycle(!; p) !a h2H 0 8j 2 J: inTree(q ) =A [q ] ^8h 2 H :(out(p) out(q )^ q ! q ) j j j;h j j;h j;h j;h (OutAcc) !a j2J 0 0 h2H j2J p4A[q ] ,! p 4A[A [q ] ] j j j;h We now de ne ,! and L as the transition relation and the labelling function s.t. L(n ) = p 4 q and, for each n 2 N with L(n) = p4 T , the following holds: 0 0 ` ` 0 0 0 0 0 0 0 if p4 T ,! p 4 T then there exists a unique n s.t. n ,! n with L(n ) = p 4 T ; ` ` 0 0 0 0 0 0 if n ,! n with L(n ) = p 4 T then p4 T ,! p 4 T . Notice that such a tree exists (it can be constructed inductively starting from the root n ) and it is unique (up-to tree isomorphism). Given machines M and M , De nition 3.2 generates a tree whose nodes are labelled by 1 2 i2I terms of the form p4A[q ] where p represents the state of M , A represents the receive i 1 actions accumulated by M , and each q represents the state of machine M after each path 2 i 2 th of accumulated receive actions from the root of A to the i hole. Note that we overload the 0 + 0 0 A tree is a connected directed graph without cycles: 8n 2 N: n ,! n^8n; n 2 N: n ,! n : n 6= n . 0 Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:11 q 4 q 1 1 0 !pr ko ok ko ok !nd q q q 2 2 q q ?ko ?ok 2 2 q 4 q q 4 q q 4 q 3 1 2 2 1 1 n ?ok n n n 3 1 2 !nd !pr !nd ?ko ko ok q 4 q 24 q 4 q ko ok 1 2 3 2 ?ko n n 4 7 ko ok q q q q 24 34 2 2 ko ok ko ok n q q 2 2 q q q q 2 2 2 2 ?ok !pr q 4 q 1 2 ko ok ko ok !nd ko ok ko ok q q 24 14 ko ok ko ok ko ok ko ok ko ok ko ok q q q q 2 2 2 2 q q q q q q q q 2 2 2 2 2 2 2 2 ?ko ko ok ko ok ko ok !pr ko ok ko ok q q q 14 34 14 ko ok ko ok ko ok ko ok ?ok ko ok ko ok ko ok ko ok q q q q q q q q 2 2 2 2 2 2 2 2 q q q q q q q q 2 2 2 2 2 2 2 2 n15 n14 n16 Figure 4: Part of the simulation tree (solid edges only) and candidate tree for M 4 M R C (Figure 1 and 2). The root is circled in thicker line. The node identities are shown at the bottom left of each label. symbol 4 used for asynchronous subtyping (De nition 2.6), however the actual meaning is always made clear by the context. We comment each rule in detail below. Rules (In) and (Out) enforce contra-variance of inputs and covariance of outputs, respec- tively, when no accumulated receive actions are recorded, i.e., A is a single hole. Rule (In) corresponds to Case (2a) of De nition 2.6, while rule (Out) corresponds to Case (3a). Rule (InCtx) is applicable when the input tree A is non-empty and the state p (of M ) is able to perform a receive action corresponding to any message located at the root of the input tree (contra-variance of receive actions). This rule corresponds to Case (2b) of De nition 2.6. Rule (OutAcc) allows M to execute some receive actions before matching a send action executed by M . This rule corresponds to Case (3b) of De nition 2.6. Intuitively, each send action outgoing from state p must also be eventually executable from each of the states q j2J (in M ) which occur in the input tree A[q ] . The possible combinations of receive actions 2 j executable from each q before executing !a is recorded in A , using inTree(q ). We assume j j j that the premises of this rule only hold when all invocations of inTree() are de ned. Each tree of accumulated receive actions is appended to its respective branch of the input context !a 0 h2H j2J 0 A, using the notation A[A [q ] ] . The premise out(p) out(q ) ^ q ! q j;h j;h j;h j;h guarantees that each q can perform the send actions available from p (covariance of j;h send actions). The additional premise :cycle(!; p) corresponds to that of Case (3b) of De nition 2.6. Example 3.3. Figure 4 gives a graphical view of the initial part of the simulation tree simtree(M ; M ). Consider the solid edges only for now, they correspond to the ,! -relation. R C Observe that all branches of the simulation tree are in nite; some traverse nodes with 20:12 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 in nitely many dierent labels, due to the unbounded growth of the input trees (e.g., the one repeatedly performing transitions !nd?ko!pr ); while others traverse nodes with nitely many distinct labels (e.g., the one performing rst transitions !nd?ko!pr and then repeatedly performing !nd?ok ). We adapt the terminology of [JM99] and say that a node n of simtree(M ; M ) is a 1 2 leaf if it has no successors. A leaf n is successful i L(n) = p4 q, with p and q nal; all other leaves are unsuccessful. A branch (a full path through the tree) is successful i it is in nite or nishes with a successful leaf; otherwise it is unsuccessful. Using this terminology, we relate asynchronous subtyping (De nition 2.6) with simulation trees (De nition 3.2) in Theorem 3.4. Theorem 3.4. Let M = (P; p ; ) and M = (Q; q ; ) be two communicating machines. 1 0 1 2 0 2 All branches in simtree(M ; M ) are successful if and only if M 4 M . 1 2 1 2 Proof. We start from the if part. Consider two communicating machines M = (P; p ; ) 1 0 1 and M = (Q; q ; ) such that M 4 M . By de nition of M 4 M , we have that there 2 0 2 1 2 1 2 exists an asynchronous subtyping R such that (p ; q ) 2 R. Consider now simtree(M ; M ) = 0 0 1 2 (N; n ; ,! ;L; Act; P T ), having a root labelled with p 4 q . We have that also other 0 Q 0 0 nodes n 2 N are such that L(n) = p4 T implies (p; T ) 2 R. This is easily proved by induction on the length of the sequence of transitions n ,! n, observing that the rules for the construction of the simulation tree check on p and T the same properties checked by the de nition of asynchronous session subtyping, and generate new transitions to nodes 0 0 0 0 labelled with p 4 T corresponding to the pairs (p ; T ) that are required to be in R. This guarantees that, for every n in the simulation tree, either L(n) = p4 q with p 9 and q 9 (i.e., p and q are nal) implying that the branch to n is successful, or there exists n such that n ,! n . This guarantees that in simtree(M ; M ) there exists no unsuccessful branch. 1 2 We now move to the only if part. Consider two communicating machines M = (P; p ; ) 1 0 1 and M = (Q; q ; ) and their simulation tree simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ). 2 0 2 1 2 0 Q Consider now the relation R P T such that (p; T ) 2 R if and only if there exists n 2 N s.t. L(n) = p4 T . With similar arguments as in the above case, we prove that R is an asynchronous subtyping relation. Hence, given that L(n ) = p 4 q , we have (p ; q ) 2 R, 0 0 0 0 0 hence also M 4 M . 1 2 3.2. A Simulation Tree-Based Algorithm. A consequence of the undecidability of asynchronous session subtyping [LY17, BCZ18, BCZ17] is that checking whether all branches in simtree(M ; M ) are successful is undecidable. The problem follows from the presence of 1 2 in nite branches that cannot be algorithmically identi ed. Our approach is to characterise nite subtrees (called witness subtrees ) such that all the branches that traverse these nite subtrees are guaranteed to be in nite. The presentation of our algorithm is in three parts. In Part (1), we give the de nition of the kind of nite subtree (of a simulation tree) we are interested in (called candidate subtrees). In Part (2), we give an algorithm to extract candidate subtrees from a simulation tree simtree(M ; M ). In Part (3) we show how to check whether a candidate subtree (which 1 2 is nite) is a witness of in nite branches (hence successful) in the simulation tree. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:13 3.2.1. Part 1. Characterising nite and candidate sub-trees. We de ne the candidate subtrees of a simulation tree, which are nite subtrees accompanied by an ancestor function mapping each boundary node n to a node located on the path from the root of the tree to n. De nition 3.5 (Finite Subtree). A nite subtree (r; B) of a labelled tree S = (N; n ; ,! ; L; ; ), with r being the subtree root and B N the nite set of its leaves (boundary nodes), is the subgraph of S such that: (1) 8n2B: r ,! n; 0 + 0 (2) 8n2B: 6 9n 2B: n ,! n ; and 0 0 0 (3) 8n 2 N: r ,! n =) 9n 2 B: n ,! n _ n ,! n. 0 0 We use nodes(S; r; B) = fn 2 N j 9n 2 B: r ,! n ,! n g to denote the ( nite) set of nodes of the nite subtree (r; B). Notice that r 2 nodes(S; r; B) and B nodes(S; r; B). Condition (1) requires that each boundary node can be reached from the root of the subtree. Condition (2) guarantees that the boundary nodes are not connected, i.e., they are on dierent paths from the root. Condition (3) enforces that each branch of the tree passing through the root r contains a boundary node. De nition 3.6 (Candidate Subtree). Let M = (P; p ; ) and M = (Q; q ; ) be two 1 0 1 2 0 2 communicating machines with simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ). 1 2 0 A candidate subtree of simtree(M ; M ) is a nite subtree (r; B) paired with a function 1 2 anc : B 7! nodes(simtree(M ; M ); r; B)nB such that, for all n 2 B, we have: anc(n) ,! n 1 2 and there are p;A;A ; I; J;fq j j 2 Jg and fq j i 2 Ig such that j i i2I 0 j2J L(n) = p4A[q ] ^ L(anc(n)) = p4A [q ] ^ fq j i 2 Ig fq j j 2 Jg i j i j A candidate subtree is a nite subtree accompanied by a total function on its boundary nodes. The purpose of function anc is to map each boundary node n to a \similar" ancestor 0 0 n such that: n is a node (dierent from n) on the path from the root r to n (recall that we have r 2= B) such that the labels of n and n share the same state p of M , and the states of M (that populate the holes in the leaves of the input context of the boundary node) are a subset of those considered for the ancestor. Given a candidate subtree, we write img (anc) 0 0 for the set fn j 9n 2 B: anc(n ) = ng, i.e., img (anc) is the set of ancestors in the candidate subtree. Example 3.7. Figure 4 depicts a nite subtree of simtree(M ; M ). We can distinguish R C several distinct candidate subtrees in Figure 4. For instance one subtree is rooted at n , and its boundary nodes are fn ; n ; n ; n ; n g; another subtree is rooted at n and its 2 6 11 14 16 8 boundary nodes are fn ; n ; n g (boundary nodes are highlighted with a double border). 11 14 16 In each subtree, the anc function is represented by the dashed edges from its boundary nodes to their respective ancestors. 3.2.2. Part 2. Identifying candidate subtrees. We now describe how to generate a nite subtree of the simulation tree, from which we extract candidate subtrees. Since simulation trees are potentially in nite, we need to identify termination conditions (i.e., conditions on nodes that become the boundary of the generated nite subtree). 20:14 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 We rst need to de ne the auxiliary function extract(A; !), which checks the presence of a sequence of messages ! in an input context A, and extracts the residual input context. >A if ! = 0 0 extract(A; !) = extract(A ; ! ) if ! = a ! ;A = ha : A i ; and i 2 J i i j j j2J ? otherwise Our termination condition is formalised in Theorem 3.8 below. This result follows from an argument based on the niteness of the states of M and of the sets of states from M 1 2 (which populate the holes of the input contexts in the labels of the nodes in the simulation tree). We write minHeight(A) for the smallest height (A), with i 2 I (A), where height (A) i i th is the length of the path from the root of the input context A to the i hole. Theorem 3.8. Let M = (P; p ; ) and M = (Q; q ; ) be two communicating machines 1 0 1 2 0 2 with simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ). 1 2 0 Q For each in nite path n ,! n ,! n ,! n ,! there exist i < j < k, with 0 1 2 l h2H 0 h2H 00 h2H i j k L(n ) = p4A [q ] L(n ) = p4A [q ] L(n ) = p4A [q ] i i h j j k k h h 0 00 such that fq j h 2 H g fq j h 2 H g and fq j h 2 H g fq j h 2 H g; j h i k h i h h and, for n ,! n : i j (i) rcv( ) = ! ! with ! s.t. 9t; z: extract(A ; ! ) = [ ] ^ extract(A ; ! ) = [ ] , or 1 2 1 i 1 t k 1 z (ii) minHeight(extract(A ; rcv( ))) minHeight(extract(A ; rcv( ))). i k Proof. Let M = (P; p ; ) and M = (Q; q ; ) be two communicating machines with 1 0 1 2 0 2 simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ), and let n ,! n ,! n ,! n ,! be an 1 2 0 Q 0 1 2 l in nite path in the simulation tree. For each n , let S be the pair (p ; R ), with p 2 P and i i i i i j2J R Q, such that L(n ) = p 4A [q ] and R = fq j j 2 J g. Notice that there are at i i i i j i j i jQj most jPj 2 distinct pairs (p ; R ), in which p is an element taken from the nite set P , i i i and R is a subset of the nite set Q. This guarantees the existence of in nite pairs of nodes 0 0 0 (n ; n ); (n ; n ); : : : ; (n ; n ); : : : taken from the above in nite path, such that, for all j: i i i 1 i 2 i i 1 2 j S = S and j i i < i < i and j j+1 0 jQj i i jPj 2 . The above follows from the possibility to repeatedly select, by following from left to right the in nite sequence n ,! n ,! n ,! n ,! , the rst occurring pair (n ; n ), with k < l, 0 1 2 l k l jQj such that S = S . Being the rst pair of this type that occurs, we have that lk jPj 2 . k l For the above in nite list of pairs (n ; n 0 ); (n ; n 0 ); : : : ; (n ; n 0 ); : : : let be such i i i j 1 i 2 i j i 1 2 j that n ,! n . All these in nitely many sequences of actions have bounded length i j jQj (smaller than jPj 2 ), hence in nitely many of them will coincide (this is because there are only boundedly many distinct actions that are admitted). Let be such a sequence of actions that is considered for in nitely many paths n ,! n 0 . Moreover, being the possible j i distinct (p ; Q ) nite, there exists one pair (p; Q) such that in nitely many of these paths i i n ,! n 0 will be such that S = S 0 = (p; Q). i i i i j j j j Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:15 Summarising, we have proved the existence of (n ; n 0 ); (n ; n 0 ); : : : ; (n ; n 0 ); : : : , v v v 1 v 2 v j v 1 2 j with v < v < v for all j, for which there exist (p; Q) and such that, for all j, n ,! n 0 j j+1 v v j j and S = S 0 = (p; Q). j v We now consider ! = rcv(). We have that the input actions in !, executed in each h2H path n ,! n 0 , will be matched by the input context A of L(n ) = p4A [q ] . There v v j v j j j j are two possibilities: (1) either ! is included in a path root-hole of A (hence extract(A ; !) is de ned), j j (2) or there exists a path root-hole which corresponds to a pre x of ! (in this case we have that ! = ! ! with extract(A ; ! ) = [ ] ). 1 2 j 1 t At least one of the two cases occurs in nitely often, i.e., there exist in nitely many indices j, such that for all paths n ,! n 0 item 1 holds, or there exist in nitely many indices j, v v such that for all paths n ,! n 0 item 2 holds. In the rst case, we have that there exist at v v least two indices j and j such that minHeight(extract(A ; !)) minHeight(extract(A ; !)) 1 2 j j 1 2 (in fact, minHeight() returns a non negative value, hence such values cannot in nitely decrease). In the second case, we have that there exist at least two indices j and j such 1 2 that extract(A ; ! ) = [ ] and extract(A ; ! ) = [ ] for the same ! pre x of ! (in fact, j 1 t j 1 t 1 1 j 2 j 1 2 ! has only nitely many pre xes). We can conclude that the thesis holds by considering i = v , j = v and k = v . j j 1 j 2 Intuitively, the theorem above says that for each in nite branch in the simulation tree, we can nd special nodes n , n and n such that the set of states in A (resp. A ) is i j k j k included in that of A and the receive actions in the path from n to n are such that: either i i j (i) only a precise pre x of such actions will be taken from the receive actions accumulated in n and n or (ii) all of them will be taken from the receive actions in which case n must k k have accumulated more receive actions than n . Case (i) deals with in nite branches with only nite labels (hence nite accumulation) while case (ii) considers those cases in which there is unbounded accumulation along the in nite branch. As an example of this latter case, consider the simulation tree depicted in Figure 4. Let n = n , n = n and n = n . These nodes are along the same path, moreover we i 8 j 12 k 16 h2H 0 h2H 00 h2H i j k have L(n ) = q 4A [q ] , L(n ) = q 4A [q ] , L(n ) = q 4A [q ] with fq j i 1 i h j 1 j k 1 k h h h 0 00 h 2 H g = fq j h 2 H g = fq j h 2 H g = fq g and 0 = minHeight(extract(A ; ?ko)) i j k 2 i h h minHeight(extract(A ; ?ko)) = 2. Notice that the path in the simulation tree from n to n k 8 16 can be in nitely repeated with the eect of increasing the height of the input context. Based on Theorem 3.8, the following algorithm generates a nite subtree of simtree(M ; M ): 1 2 Starting from the root, compute the branches of simtree(M ; M ) stopping 1 2 when one of the following types of node is encountered: a leaf, a node n with a label already seen along the path from the root to n, or a node n (with the corresponding node n ) as those described by the above Theorem 3.8. Example 3.9. Consider the nite subtree in Figure 4. It is precisely the nite subtree identi ed as described above: we stop generating the simulation tree at nodes n , n , n , 2 6 11 and n (because their labels have been already seen at the corresponding ancestors n , 14 0 n , n , and n ) and n (because of the ancestors n and n such that n , n and n 4 8 12 16 8 12 8 12 16 correspond to the nodes n , n and n of Theorem 3.8). i j k The order nodes are generated is not important (our implementation uses a DFS approach, cf. §4). 20:16 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 When the computed nite subtree contains an unsuccessful leaf, we can immediately conclude that the considered communicating machines are not related. Otherwise, we extract smaller nite subtrees (from the subtree) that are potential candidates to be subsequently checked. We de ne the anc function as follows: for boundary nodes n with an ancestor 0 0 0 n such that L(n) = L(n ) we de ne anc(n) = n ; for boundary nodes n with the corresponding node n as those described by Theorem 3.8, we de ne anc(n ) = n . The extraction of the nite subtrees is done by characterising k i their roots (and taking as boundary their reachable boundary nodes): let 0 0 0 P = fn 2 img (anc) j 9n : anc(n ) = n^L(n) 6= L(n )g, the set of such roots 0 0 + is R = fn 2 P j69n 2 P: n ,! ng. Intuitively, to extract subtrees, we restrict our attention to the set P of ancestors with a label dierent from their corresponding boundary node (corresponding to branches that can generate unbounded accumulation). We then consider the forest of subtrees rooted in nodes in P without an ancestor in P . Notice that for successful leaves we do not de ne anc; hence, only extracted subtrees without successful nodes have a completely de ned anc function. These are candidate subtrees that will be checked as described in the next step. Example 3.10. Consider the nite subtree in Figure 4. Following the strategy above we ex- tract from it the candidate subtree rooted at n (white nodes), with boundary fn ; n ; n g. 8 11 14 16 Note that each ancestor node above n has a label identical to its boundary node. 3.2.3. Part 3. Checking whether the candidate subtrees are witnesses of in nite branches. The nal step of our algorithm consists in verifying a property on the identi ed candidate subtrees which guarantees that all branches traversing the root of the candidate subtree are in nite, hence successful. A candidate subtree satis es this property when it is also a witness subtree, which is the key notion (De nition 3.16) presented in this third part. In order for a subtree to be a witness, we require that any behaviour in the simulation tree going beyond the subtree is the in nite repetition of the behaviour already observed in the considered nite subtree. This in nite repetition is only possible if whatever receive actions are accumulated in the input context A (using Rule (OutAcc)) are eventually executed by the candidate subtype M in Rule (InCtx). The compatibility check between the receive actions that can be accumulated and the receive actions that are eventually executed is done by rst synthesising a nite representation of the possible (repeated) accumulation of the candidate supertype M and the possible (repeated) receive actions of the candidate subtype M . We then check whether these representations of the input actions are compatible, wrt. the v-relation, see De nition 3.12. We de ne these representations of the input behaviours as a system of (possibly) mutually recursive equations, which we call a system of input tree equations. Intuitively, a system of input tree equations represents a family of trees, that we use to represent the input behaviour of types. We need to consider families of trees because types include also output actions that, in case we are concerned with input actions only, can be seen as internal silent actions, representing nondeterministic choices among alternative future inputs (i.e. alternative subtrees). De nition 3.11 (Input Tree Equations). Given a set of variables V , ranged over by X , an input tree expression is a term of the grammar E ::= X j ha : E i j hE i i i i2I i i2I Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:17 The free variables of an input tree expression E are the variables which occur in E. Let T be the set of input tree expressions whose free variables are in V . A system of input tree equations is a tuple G = (V; X ; E) consisting of a set of variables V , an initial variable X 2 V , and with E consisting of exactly one input tree expression def X = E for each X 2 V , with E 2 T . Given an input tree expression of the form ha : E i or hE i , we assume that I 6= ;, i i i2I i i2I 8i 6= j 2 I: a 6= a , and that the order of the sub-terms is irrelevant. Whenever convenient, i j we use set-builder notation to construct an input tree expression, e.g., hE j i 2 Ii. In an input tree equation, the construct ha : E i represents the capability of accumulating (or i i i2I actually executing) the receive actions on each message a then behaving as in E . The i i construct hE i represents a silent choice between the dierent capabilities E . i i2I i We now de ne the notion of compatibility between two systems of input tree equations. Intuitively, two systems of input tree equations are compatible when all the trees of the former have less alternatives than the trees of the latter. More precisely, at each input choice, the alternative branchings of the former are included in those of the latter. De nition 3.12 (Input Tree Compatibility). Given two systems of input tree equations 0 0 0 0 0 G = (V; X ; E) and G = (V ; X ; E ), such that V \V = ;, we say that G is compatible with 0 0 0 G , written G v G , if there exists a compatibility relation R T T . That is a relation R s.t. (X ; X ) 2 R and: def 0 0 (1) if (X; E) 2 R then (E ; E) 2 R with X = E ; def 0 0 (2) if (E; X ) 2 R then (E; E ) 2 R with X = E ; (3) if (hE i ; E) 2 R then 8i 2 I: (E ; E) 2 R; i i2I i (4) if (E;hE i ) 2 R then 8i 2 I: (E; E ) 2 R; i i2I i 0 0 (5) if (ha : E i ;ha : E i ) 2 R then I J and 8i 2 I: (E ; E ) 2 R. i i i2I j j2J i j i 0 0 We extend the use of v, de ned on input tree equations, to terms E 2 T and E 2 T ; 0 0 namely, we write E v E if there exists a compatibility relation R s.t. (E; E ) 2 R. Notice that compatibility is formally de ned following a coinductive approach that 0 0 performs the following checks on G and G , starting from the initial pair (X ; X ). The rst two items of De nition 3.12 let variables be replaced by their respective de nitions. The next two items explore all the successors of silent choices. The last item guarantees that all the receive actions of the l.h.s. can be actually matched by receive actions in the r.h.s. The check of compatibility will be used in De nition 3.16, in order to control that the candidate supertype always has input branchings included in those of the candidate subtype. More precisely, we will check that the system of input tree equations, that represents the possible inputs of the supertype, is compatible with that of the candidate subtype. Example 3.13. Consider the two systems of input tree equations in Figure 5. We have G v G . We enumerate a few pairs which must be in the embedding relation: Initial variables: (X ; Y ) 0 n Unfold X (Case (1) of Def. 3.12) (hok : X ; ko : X i; Y ) 0 q ;n q ;n n 2 8 2 8 8 Unfold Y (Case (2) of Def. 3.12) (hok : X ; ko : X i;hY i) n q ;n q ;n n 8 2 8 2 8 9 Silent-choice (Case (4) of Def. 3.12) (hok : X ; ko : X i; Y ) q ;n q ;n n 2 8 2 8 9 Unfold Y (Case (2) of Def. 3.12) (hok : X ; ko : X i;hok : Y ; ko : Y i) n q ;n q ;n n n 9 2 8 2 8 8 10 Choice (Case (2) of Def. 3.12) (X ; Y ) and (X ; Y ) q ;n n q ;n n 2 8 8 2 8 10 20:18 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 def X = hok : X ; ko : X i 0 q ;n q ;n 2 8 2 8 def def X = hok : X ; ko : X i Y = hY i q ;n q ;n q ;n n n 2 8 2 9 2 9 8 9 def def X = hX ; X i Y = hok : Y ; ko : Y i q ;n q ;n q ;n n n n 2 9 2 8 2 10 9 8 10 def def X = hok : X ; ko : X i Y = hY i q ;n q ;n q ;n n n 2 10 2 12 2 12 10 12 def def X = hok : X ; ko : X i Y = hok : Y ; ko : Y i q ;n q ;n q ;n n n n 2 12 2 13 2 13 13 12 15 def def X = hX ; X i Y = hY i q ;n q ;n q ;n n n 2 13 2 12 2 15 15 8 def X = hok : X ; ko : X i q ;n q ;n q ;n 2 15 2 8 2 8 X X q ;n q ;n 2 13 2 15 Y Y n n 15 8 ?ko ?ok ?ok ?ko ?ko ?ko ?ok X q ;n 0 2 8 ?ok Y Y q ;n n n 2 12 13 9 ?ko ?ok ?ok ?ko ?ko ?ok X X q ;n q ;n 2 10 2 9 Y Y n n 12 10 G G Figure 5: Input tree equations for M 4 M (Figures 1 and 2) and their graphical represen- R C tations. The starting variables are X and Y . Silent choices are diamond-shaped 0 n nodes, other nodes are rectangles. Before giving the de nition of a witness subtree, we introduce a few auxiliary functions on which it relies. Given a machine M = (Q; q ; ), a state q 2 Q, and a word ! 2 A , we de ne accTree(q; !) as follows: >q if ! = !a 0 0 i2I 0 i2I 0 accTree(q; !) = A[accTree(q ; ! )] if ! = a ! ;A[q ] =inTree(q);8i2I: q ! q i i i i ? otherwise Function accTree(q; !) is a key ingredient of the witness subtree de nition as it allows for the construction of the accumulation of receive actions (represented as an input tree) that is generated from a state q mimicking the sequence of send actions sending the messages in !. We illustrate the usage of accTree(q; !) in Example 3.14 below. We use the auxiliary function minAcc(k; Q ; ) below to ensure that the eect of per- forming the transitions from an ancestor to a boundary node is that of increasing (possibly non-strictly) the accumulated receive actions. Here, k represents a known lower bound for the length of the sequences of receive actions accumulated in an input context A, i.e., a lower bound for minHeight(A). Assuming that the holes in A contain the states populating the set of states Q , the function returns a lower bound for the length of the sequences of accumulated receive actions after the transitions in have been executed. Formally, given a natural number k (k 0), a sequence of action 2 Act , and a set of states fq j j 2 Jg Q, we de ne this function as follows: j Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:19 minAcc(k;fq j j 2 Jg; ) = k if = > 0 >minAcc(k 1;fq j j 2 Jg; ) if = ?a ^ k > 0 if = !a ^ minAcc(k+min minHeight(A );fq jj 2 J; i 2 I g; ) j2J j i;j j i2I > j 8j2J: accTree(q ; a)=A [q ] j j i;j otherwise Example 3.14. Consider the transitions from node n to n in Figure 4. There are two 7 9 send actions !pr and !nd that cannot be directly red from state q which is a receiving state; the eect is to accumulate receive actions. Such an accumulation is computed by accTree(q ; pr nd ) = hko : hko : q ; ok : q i; ok : hko : q ; ok : q ii. For this sequence of 2 2 2 2 2 transitions, the eect on the (minimal) length of the accumulated receive actions can be computed by minAcc(0;fq g; !pr!nd ) = 2; meaning that before executing the sequence of transitions !pr!nd state q has not accumulated receive actions in front, while at the end an input context with minimal depth 2 is generated as accumulation. We now prove a couple of properties of minAcc(n; Q ; ). Proposition 3.15. If minAcc(k; Q ; ) is de ned, then the following statements hold: 0 0 0 0 0 (1) for each k k we have that k minAcc(k; Q ; ) = k minAcc(k ; Q ; ); 0 00 0 0 00 0 0 00 00 (2) if = then minAcc(k; Q ; ) = minAcc(minAcc(k; Q ; ); Q ; ) with 00 0 00 h2H Q = fq j h 2 H s.t. accTree(q; snd( )) = A [q ] g; h h q2Q 00 00 0 00 00 (3) if minAcc(k; Q ; ) is de ned for a set of states Q s.t. Q Q then minAcc(k; Q ; ) minAcc(k; Q ; ). 0 0 0 0 A direct consequence of (1) is that: minAcc(k ; Q ; ) minAcc(k; Q ; ) = k k 0. Proof. Item 1 is proved by induction on the length of . If the length of is 0 then 0 0 0 0 = and k minAcc(k; Q ; ) = k minAcc(k ; Q ; ) = 0. In the inductive case we 0 0 0 have two distinct cases: if =?a we have k > 0 and k minAcc(k; Q ; ?a ) = 0 0 0 0 0 0 0 0 0 0 0 kminAcc(k1; Q ; ) and k > 0 and k minAcc(k ; Q ; ?a ) = k minAcc(k 1; Q ; ), 0 0 0 0 0 0 and by inductive hypothesis k 1 minAcc(k 1; Q ; ) = k 1 minAcc(k 1; Q ; ) 0 0 0 0 0 0 0 hence also k minAcc(k 1; Q ; ) = k minAcc(k 1; Q ; ); if =!a we have 0 0 00 0 0 0 0 0 k minAcc(k; Q ; !a ) = k minAcc(k + w; Q ; ) and k minAcc(k ; Q ; !a ) = 0 0 00 0 00 k minAcc(k + w; Q ; ) for a set of states Q and a value w, and by inductive hypothesis 00 0 0 0 00 0 k + w minAcc(k + w; Q ; ) = k + w minAcc(k + w; Q ; ) hence also k minAcc(k + 00 0 0 0 00 0 w; Q ; ) = k minAcc(k + w; Q ; ). Item 2 is proved by induction on the length of . In the base case, the thesis di- 0 00 rectly follows from minAcc(k; Q ; ) = k and accTree(q; ) = q (hence we have Q = 0 0 000 Q ). In the inductive case we have two distinct cases: If =?a we have (k > 0 0 000 00 0 000 00 00 because minAcc(k; Q ; ?a ) is de ned) minAcc(minAcc(k; Q ; ?a ); Q ; ) = 0 000 00 00 minAcc(minAcc(k 1; Q ; ); Q ; ), but the latter, by applying the inductive hypothesis, 0 000 00 0 000 00 0 000 coincides with minAcc(k 1; Q ; ) = minAcc(k; Q ; ?a ). If =!a we 0 000 00 00 000 000 00 00 have minAcc(minAcc(k; Q ; !a ); Q ; ) = minAcc(minAcc(k + w; Q ; ); Q ; ), for 000 0 the set of states Q obtained by allowing the states in Q to anticipate !a and a value w that depends on Q and a (see de nition of the minAcc function); the latter, by applying the 000 000 00 00 inductive hypothesis, coincides with minAcc(k + w; Q ; ) (because Q is obtained 20:20 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 000 000 000 from Q by allowing the states in Q to anticipate the send actions in ), which is equal 0 000 00 000 0 to minAcc(k; Q ; !a ) as Q and w depend on Q and a as described above. Item 3 is proved by induction on the length of . The base case is trivial because 00 0 minAcc(k; Q ; ) = minAcc(k; Q ; ) = k. In the inductive case we have two distinct cases: If 0 00 0 00 0 =?a we have minAcc(k; Q ; ?a ) = minAcc(k 1; Q ; ) with the latter, by inductive 0 0 0 0 hypothesis, that is smaller than or equal to minAcc(k 1; Q ; ) = minAcc(k; Q ; ?a ). If 0 00 0 000 0 000 =!a we have minAcc(k; Q ; !a ) = minAcc(k+w; Q ; ) for a set of states Q obtained from Q by allowing its states to anticipate !a and w the corresponding minimal height. Now, if we allow the states in the smaller (or equal) set Q to anticipate !a, we obtain a smaller (or 0000 0 equal) set Q and a value w that cannot be smaller than w, hence we can apply the inductive 0000 0 hypothesis to obtain the greater or equal value minAcc(k + w; Q ; ), which is smaller or 0 0000 0 0 0 equal, for item 1 of this Proposition, than minAcc(k +w ; Q ; ) = minAcc(k; Q ; !a ). We nally give the de nition of witness subtree. De nition 3.16 (Witness Subtree). Let M = (P; p ; ) and M = (Q; q ; ) be two 1 0 1 2 0 2 communicating machines with simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ). A candidate 1 2 0 Q subtree of simtree(M ; M ) with root r, boundary B, and ancestor function anc, is a witness 1 2 if the following holds: (1) For all n 2 B, given such that anc(n) ,! n, we have jrcv( )j > 0. 0 0 i2I (2) For all n 2 img (anc) and n 2 img (anc)[ B such that n ,! n , L(n) = p4A[q ] , and 0 0 0 j2J L(n ) = p 4A [q ] , we have that : 00 h2H (a) 8i 2 I : fq j h 2 H s.t. accTree(q ; snd( )) = A [q ] g fq j j 2 Jg; h i h j (b) if n 2 B then minAcc(minHeight(A);fq j i 2 Ig; ) minHeight(A). (3) G v G where (a) G = (fX g[fX j q 2 Q; n 2 nodes(S; r; B)nBg; X ; E) with E de ned as follows: 0 q;n 0 def (i) X = TfX =q j q 2 Qg, with L(r) = p4 T 0 q;r def (ii) X = q;n ?a ?a hX 0 j 9a:n ,! n i if 9a:n ,! q;tr(n ) !a !a i2I 0 i2I 0 hA[X 0 0 ] j 9a:n ,! n ^ inTree(q) =A[q ] ^8i2I:q ! q i otherwise i i q ;tr(n ) i 0 0 0 (b) G = (fY j n 2 nodes(S; r; B)nBg; Y ; E ) with E de ned as follows: n r !a !a 0 0 0 hY 0 j n ,! n i if 9n :n ,! n def tr(n ) Y = ?a ?a : 0 0 0 ha : Y 0 j n ,! n i if 9n :n ,! n tr(n ) where tr(n) = n, if n 62 B; tr(n) = anc(n), otherwise. Condition (1) requires the existence of a receive transition between an ancestor and a boundary node. This implies that if the behaviour beyond the witness subtree is the repetition of behaviour already observed in the subtree, then there cannot be send-only cycles. Condition (2a) requires that the transitions from ancestors to boundary nodes (or to other ancestors) are such that they include those behaviours that can be computed by the accTree function. We assume that this condition does not hold if accTree(q ; snd( )) = ? for any i 2 I ; hence the states q of M in an ancestor are able to mimic all the send actions i 2 performed by M along the sequences of transitions in the witness subtree starting from the considered ancestor. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:21 Condition (2b) ensures that by repeating transitions from ancestors to boundary nodes, the accumulation of receive actions is, overall, non-decreasing. In other words, the rate at which accumulation is taking place is higher than the rate at which the context is reduced by Rule (InCtx). Condition (3) checks that the receive actions that can be accumulated by M (represented by G) and those that are expected to be actually executed by M (represented by G ) are compatible. In G, there is an equation for the root node and for each pair consisting of a local state in M and a node n in the witness subtree. The equation for the root node is given in (3(a)i), where we simply transform an input context into an input tree expression. The other equations are given in (3(a)ii), where we use the partial function inTree(q). Each equation represents what can be accumulated by starting from node n (focusing on local state q). In G , there is an equation for each node n in the witness subtree, as de ned in (3b) There are two types of equations depending on the type of transitions outgoing from node n. A send transition leads to silent choices, while receive transitions generate corresponding receive choices. Example 3.17. We have that the candidate subtree rooted at n in Figure 4 satis es De nition 4. (1) Each path from an ancestor to a boundary node includes at least one receive action. (2a) For each sequence of transitions from an ancestor to a boundary node (or another ancestor) the behaviour of the states of M , as computed by the accTree function, has already been observed. (2b) For each sequence of transitions from an ancestor to a boundary node, the rate at which receive actions are accumulated is higher than or equal to the rate at which they are removed from the accumulation. (3) The systems of input tree equations G (3a) and G (3b) are given in Figure 5, and are compatible, see Example 3.13. We now describe how G and G (Figure 5) are constructed from the witness tree rooted at n in Figure 4. For G we have the following equations: def X = hok : X ; ko : X i since the root of the witness tree is n and its label is 0 q ;n q ;n 8 2 8 2 8 q 4hok : q ; ko : q i. In Figure 5, we depict this equation as a pair of transitions from 1 2 2 the node labelled by X to the node labelled by X 0 q ;n 2 8 def X = hok : X ; ko : X i since n has a unique outgoing send transition to n , q ;n q ;n q ;n 8 9 2 8 2 9 2 9 !nd i.e., n in Case (3(a)ii) of De nition 3.16, and inTree(q ) = hok : q ; ko : q i with q ! q 2 1 1 1 2 !pr and q ! q in M 1 2 C def X = hX ; X i since n has two receive transitions: one to n (a boundary q ;n q ;n q ;n 9 11 2 9 2 8 2 10 node whose ancestor is n , i.e., tr(n ) = n ) and one to n (which is not boundary node, 8 11 8 10 i.e., tr(n ) = n ) 10 10 def X = hok : X ; ko : X i since n has a unique outgoing send transition to q ;n q ;n q ;n 10 2 10 2 12 2 12 n , and inTree(q ) = hok : q ; ko : q i 12 2 1 1 def X = hok : X ; ko : X i since n has a unique outgoing send transition to q ;n q ;n q ;n 12 2 12 2 13 2 13 n , and inTree(q ) = hok : q ; ko : q i 13 2 1 1 def X = hX ; X i since n has two receive transitions: one to n (a boundary q ;n q ;n q ;n 9 14 2 13 2 12 2 15 node whose ancestor is n ) and one to n (which is not boundary node) 12 15 def X = hok : X ; ko : X i since inTree(q ) = hok : q ; ko : q i and n has q ;n q ;n q ;n 2 1 1 15 2 15 2 8 2 8 a unique outgoing send transition to n , which is a boundary node (n 2 B) whose 16 16 ancestor is n . We omit the other equations, e.g., X as they are not reachable from X . q ;n 0 1 8 20:22 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 For G we have the following equations: def Y = hY i since n has a unique send transition to n , i.e., n in Case (3b) of De ni- n n 8 9 8 9 tion 3.16, and n is not a boundary node def Y = hok : Y ; ko : Y i since n has two receive transitions: one to n which is not a n n n 9 10 9 8 10 boundary node, and one to n which is a boundary node whose ancestor is n 11 8 def Y = hY i since n has a unique send transition to n which is not a boundary node n n 10 12 10 12 def Y = hY i since n has a unique send transition to n which is not a boundary node n n 12 13 12 13 def Y = hok : Y ; ko : Y i since n has two receive transitions: one to n which is not n n n 13 15 13 12 15 a boundary node, and one to n which is a boundary node whose ancestor is n 14 12 def Y = hY i since n has a unique send transition to n , and n is a boundary node n n 15 16 16 15 8 whose ancestor is n . We now prove the main property of the minAcc(k; Q ; ) function, i.e., given information k and Q extracted from an ancestor n in a witness subtree, such a function correctly computes a lower bound of the length of the input accumulation in a node n reachable from n by executing the sequence of actions . Proposition 3.18. Consider a witness subtree with ancestor function anc; given two nodes 0 0 i2I 0 of the tree, n 2 img (anc) and n s.t. n ,! n , with L(n) = p4A[q ] and L(n ) = 0 0 j2J 0 p 4A [q ] , we have that minAcc(minHeight(A);fq j i 2 Ig; ) minHeight(A ). j i Proof. We prove a more general result proceeding by induction on the length of , i.e., that minAcc(minHeight(A);fq j i 2 Ig; ) minHeight(A ) and fq j j 2 Jg fq j h 2 i j h i2I 000 h2H H s.t. accTree(q ; snd( )) = A [q ] g. The base case is trivial because, by de nition, minAcc(minHeight(A);fq j i 2 Ig; ) = 0 0 minHeight(A) and having n = n then minHeight(A) = minHeight(A ). Moreover, fq j i2I 000 h2H 0 h 2 H s.t. accTree(q ; ) = A [q ] g = fq j i 2 Ig and having n = n then fq j i 2 Ig = i h i i fq j j 2 Jg. 0 0 In the inductive case we have either = ?a or = !a. In both cases we observe that, by de nition of witness subtree, minAcc(minHeight(A);fq j i 2 Ig; ) is de ned as it is de ned for a longer sequence of transitions from n to a boundary node (traversing n ). 0 00 We rst consider = ?a. Let n be the node reached after the sequence of tran- 0 00 00 00 w2W sitions , and let L(n ) = p 4A [q ] . By inductive hypothesis we have that 0 00 00 minAcc(minHeight(A);fq j i 2 Ig; ) minHeight(A ) and, letting Q = fq j i h i2I 0 000 h2H 00 h 2 H s.t. accTree(q ; snd( )) = A [q ] g, we also have fq j w 2 Wg Q . By i w Proposition 3.15, item 2, we have that the following holds: minAcc(minHeight(A);fq j 0 0 00 i 2 Ig; ?a) = minAcc(minAcc(minHeight(A);fq j i 2 Ig; ); Q ; ?a). By de nition 0 00 of minAcc, we also have that minAcc(minAcc(minHeight(A);fq j i 2 Ig; ); Q ; ?a) = minAcc(minHeight(A);fq j i 2 Ig; ) 1. As a direct consequence of the inductive hypoth- 0 00 esis we have minAcc(minHeight(A);fq j i 2 Ig; ) 1 minHeight(A ) 1, but we have 00 0 that minHeight(A ) 1 minHeight(A ), because the eect of an input transition on the input context is simply that of consuming one initial input branching. We conclude this case by observing that fq j j 2 Jg fq j w 2 Wg because, as observed above, the eect of an j w input transition on the input context is simply that of consuming one initial input branching, without changing the states populating the leaves of the input tree. On the other hand, the set of states obtained from the states q by anticipating the outputs in ?a coincides with i Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:23 00 0 0 the above set Q because only send actions are considered, and snd( ) = snd( ?a). By inductive hypothesis, we have fq j w 2 Wg Q . 0 00 We now consider = !a. Let n be the node reached after the sequence of transitions 0 00 00 00 w2W , and let L(n ) = p 4A [q ] . By inductive hypothesis we have that 0 00 minAcc(minHeight(A);fq j i 2 Ig; ) minHeight(A ) and, letting 00 0 000 h2H Q = fq j h 2 H s.t. accTree(q ; ) = A [q ] g h i h i2I we also have fq j w 2 Wg Q . By Proposition 3.15, item 2, minAcc(minHeight(A);fq j i 2 Ig; !a) 0 00 = minAcc(minAcc(minHeight(A);fq j i 2 Ig; ); Q ; !a) moreover, by de nition of minAcc, we have 0 00 minAcc(minAcc(minHeight(A);fq j i 2 Ig; ); Q ; !a) = minAcc(minHeight(A);fq j i 2 Ig; ) + z with z the minimal depth of the holes in the input tree that are accumulated by the !a 00 00 0 states in Q when they anticipate !a. Having n ,! n , we have that the minimal depth 0 0 00 00 of the input tree in n , i.e. minHeight(A ), will increase that of n , i.e. minHeight(A ), depending on new accumulation generated by the anticipation of !a, hence the increase, 0 00 i.e. minHeight(A ) minHeight(A ), will be greater than or equal to the minimal depth of the holes in the input tree that are accumulated by the states in fq j w 2 Wg when they anticipate !a. Being fq j w 2 Wg Q , we have that such an increase will be also greater 0 00 than or equal to z, i.e. minHeight(A ) minHeight(A ) z. As a direct consequence of the inductive hypothesis we have 0 00 0 minAcc(minHeight(A);fq j i 2 Ig; ) + z minHeight(A ) + z minHeight(A ) 000 0 000 h2H We now consider Q = fq j h 2 H s.t. accTree(q ; !a) = A [q ] g; we have h h i2I 000 00 that the states in Q are generated by the states in Q when they anticipate the output !a. The same holds also for fq j j 2 Jg, i.e., the states q are generated by the states in j j fq j w 2 Wg when they anticipate the output !a. Having fq j w 2 Wg Q , we also w w have fq j j 2 Jg Q . We conclude by proving our main result; given a simulation tree with a witness subtree with root r, all the branches in the simulation tree traversing r are in nite (hence successful). Theorem 3.19. Let M = (P; p ; ) and M = (Q; q ; ) be two communicating machines 1 0 1 2 0 2 with simtree(M ; M ) = (N; n ; ,! ;L; Act; P T ). If simtree(M ; M ) has a witness subtree 1 2 0 1 2 0 0 with root r then for every node n 2 N such that r ,! n there exists n such that n ,! n . Proof. Let B be the leaves of the witness subtree rooted in r (i.e. the witness subtree is nodes(S; r; B)). If there exists l 2 B such that n ,! l the thesis trivially holds. For all other nodes n such that r ,! n, there exists l 2 B such that l ,! n. i2I We now prove by induction on the length of l ,! n, with L(n) = p4A[q ] , that 0 0 0 0 j2J there exist m; m 2 nodes(S; r; B)n B, s.t. m 2 img (anc), m ,! m , L(m) = p 4A [q ] , 0 00 k2K L(m ) = p4A [q ] such that: 000 h2H fq j i 2 Ig fq j h 2 H s.t. accTree(q ; snd( )) = A [q ] g; i h j h j2J 20:24 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 i2I A[X 0 ] v Y 0 ; q ;m m minHeight(A) minAcc(minHeight(A );fq j j 2 Jg; ). The base case is when n 2 B. In this case, let m; m = anc(n). The rst item follows from the de nition of candidate subtree according to which fq j i 2 Ig fq j j 2 Jg. i j The second item follows from the following reasoning: we consider X v Y and apply 0 r on such pair the following transformations of the l.h.s. X and r.h.s. Y . We consider the 0 r sequence of transitions from r to n and proceed as follows. For each receive transition ?a o ,! o we modify the r.h.s. by considering Y 0 and the l.h.s. by consuming the initial tr(o ) message a and by replacing each variable X (for any q) with the variable X 0 that, q;o q;tr(o ) ?a inside their corresponding de nitions, is present because of the transition o ,! o . For !a each send transition o ,! o we modify the r.h.s. by considering Y and the l.h.s. by tr(o ) replacing each variable with the term that, inside their corresponding de nitions, is present !a 0 0 i2I because of the transition o ,! o . Since tr(n) = m , we obtain A[X 0 ] v Y 0 . Notice q ;m m that the relation v actually holds because in the modi cation of the initial terms X and Y s.t. X v Y we follow the simulation game formalized in the De nition 3.12 of input r 0 r ?a tree compatibility: in the case of input transitions o ,! o we consume an initial a in both !a terms and resolve some silent choice in the l.h.s; in the case of output transitions o ,! o we resolve the initial silent choice in the r.h.s. while in the l.h.s. we replace variables with their de nition and resolve the initial silent choice in such de nitions. The third item coincides with proving that minHeight(A) minHeight(A ) because, 0 0 having m = m , the sequence is empty in the expression minAcc(minHeight(A );fq j j 2 Jg; ). By de nition of witness subtree, we have that minAcc(minHeight(A );fq j j 2 0 0 0 Jg; ) minHeight(A ) for every sequence of transitions from m to a boundary node, hence also to n. By Proposition 3.18, if we consider the sequence of transitions from 0 0 anc(n) to n, we have that minHeight(A) minAcc(minHeight(A );fq j j 2 Jg; ), from which we conclude minHeight(A) minHeight(A ). We now move to the inductive case. Suppose, by inductive hypothesis, that the above + 0 three properties hold for n s.t. l ,! n, and consider n ,! n . We separate the analysis in two !a parts, the case in which an output action n ,! n is executed, and the opposite case in which ?a n ,! n . We have to show that in both cases there exist two nodes m ; m 2 nodes(S; r; B)nB 1 2 0 0 such that the three properties, de ned for n; m; m , hold also for n ; m ; m , respectively. 1 2 !a !a !a 0 0 0 00 We now consider n ,! n . In this case we have that p ! p , hence also m ,! m . 00 00 We rst consider the case in which m 62 B: in this case we take m = m and m = m . 1 2 The rst item holds because; by inductive hypothesis we have fq j i 2 Ig fq j i h j2J 000 h2H h 2 H s.t. accTree(q ; snd( )) = A [q ] g; by De nition 3.16 of witness subtree, item j h 2a, we have that all the above states q can anticipate the output action !a because 0 0 accTree(q ; snd( )) is de ned for a sequence of actions , from m to a boundary node, that contains snd( )!a as a pre x; and the states in fq j i 2 Ig are modi ed by the transition !a in the same way as the same states that are present also in the superset 000 h2H fq j h 2 H s.t. accTree(q ; snd( )) = A [q ] g change considering the longer h j h j2J sequence snd( )!a instead of snd( ) only. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:25 i2I The second item holds because; by inductive hypothesis we have A[X 0 ] v Y 0 ; the q ;m m 0 i2I accumulated input tree in n is obtained by replacing each of the variables in A[X 0 ] q ;m !a 0 00 with the term that, inside their corresponding de nitions, is present because m ,! m and because, as observed above, each state q can anticipate the output action !a; the l.h.s. term obtained in this way (by simply replacing variables with their de nition and resolving initial silent choices) continue to be in v relation with Y 0 hence also with Y 00 which is present in m m !a 0 00 the de nition of Y because m ,! m . The third item holds because; if we take k = minAcc(minHeight(A );fq j j 2 Jg; ), by inductive hypothesis we have minHeight(A) k; by Proposition 3.15, item 2, we have that minAcc(minHeight(A );fq j j 2 Jg; !a) = minAcc(k; Q; !a) with Q = fq j h 2 j h j2J 000 h2H H s.t. accTree(q ; snd( )) = A [q ] g where J is the set of indices of the holes in the input context in the label of node m; by inductive hypothesis ( rst item) we have that fq j i 2 Ig Q where I is the set of indices of the holes in the input context in the label of node n; by de nition of the minAcc function the increment minAcc(k; Q; !a) k cannot be strictly greater than the increment of minHeight when the transition !a is executed from n to n , because minAcc(k; Q; !a) considers the minimal accumulation generated by the states Q when anticipating !a and, having fq j i 2 Ig Q, such a minimal accumulation cannot be greater than the accumulation generated by the states q present in the leaves of the input tree of n. From the inductive hypothesis minHeight(A) k we, thus, have that minHeight in n is greater or equal to minAcc(k; Q; !a). We now consider the case in which m 2 B. We have two distinct cases: (1) anc(m ) ,! m In this case we take m = m = anc(m ). The rst item holds because of the same 1 2 arguments considered in the corresponding case for m 62 B plus the observation that 000 h2H fq j h 2 H s.t. accTree(q ; snd( )!a) = A [q ] g is a subset of the states h j h j2J in the holes of the input context in m (de nition of witness subtree), which is a subset of the states in the holes of the input context in anc(m ) (de nition of can- didate subtree). The second item holds for the same argument considered in the case m 62 B (simply replacing Y 00 with Y 00 ). The third item holds for the m anc(m ) following reasons. By applying the same arguments considered in the corresponding 00 0 case for m 62 B we obtain that the new minHeight in n is greater or equal than minAcc(minHeight(A );fq j j 2 Jg; !a), where J is the set of indices of the holes in the input context in the label of node m; hence proving the third item reduces to prove 0 0 that minAcc(minHeight(A );fq j j 2 Jg; !a) minAcc(minHeight(A ); Q ; ), with j 1 w w2W 0 L(m ) = p 4A [q ] , Q = fq j w 2 Wg and corresponding to the sequence of 1 1 1 w w w 00 00 0 00 transitions from m = anc(m ) to m that traverses m, hence = !a (for some 00 0 ). This is because minAcc(minHeight(A ); Q ; ) minHeight(A ) by de nition of 1 w 1 witness subtree. By Proposition 3.15, item 2, we have minAcc(minHeight(A ); Q ; 1 w 00 00 00 !a) = minAcc(minAcc(minHeight(A ); Q ; ); Q ; !a) with Q = fq j h 2 1 w h q2Q 00 h2H H s.t. accTree(q; snd( )) = A [q ] g; given that the states fq j j 2 Jg are generated 1 h j starting from the states in Q by anticipation of the send actions in the sequence 00 00 we have that fq j j 2 Jg Q ; by Proposition 3.15, item 3, we have that 00 00 minAcc(minAcc(minHeight(A ); Q ; ); Q ; !a) 1 w minAcc(minAcc(minHeight(A ); Q ; );fq j j 2 Jg; !a); by Proposition 3.18 we have 1 w j 20:26 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 00 0 that minAcc(minHeight(A ); Q ; ) minHeight(A ) and as a consequence of Propo- 1 w 00 00 sition 3.15, item 1, we have that minAcc(minAcc(minHeight(A ); Q ; ); Q ; !a) 1 w 0 00 minAcc(minHeight(A ); Q ; !a); nally by Proposition 3.15, item 3, we have 0 00 0 minAcc(minHeight(A ); Q ; !a) minAcc(minHeight(A );fq j j 2 Jg; !a). + 00 (2) m ,! anc(m ) In this case we take m = m and m = anc(m ). The rst item holds because of the same 1 2 arguments considered in the corresponding case for m 62 B plus the observation (as done 000 h2H in the previous case) that fq j h 2 H s.t. accTree(q ; snd( )!a) = A [q ] g is a h j h j2J subset of the states in the holes of the input context in m (de nition of witness subtree); which is a subset of the states in the holes of the input context in anc(m ) (de nition of candidate subtree); which is subset of fq j h 2 H s.t. accTree(q ; snd( )) = h j j2J 000 h2H 00 00 A [q ] g with s.t. m = m ,! anc(m ) = m . Notice that the latter subset h 1 2 inclusion holds because the states in the holes of the input context in anc(m ) = m are generated starting from the states in Q by anticipation of the send actions in the sequence 00 00 . The second item holds for the same arguments considered in the case m 62 B (simply replacing Y with Y 00 ). We proceed by contraposition to show that the third item m anc(m ) 0 0 j2J 00 also holds. Given L(m) = p 4A [q ] and m ,! anc(m ), we assume by contrapo- 0 0 sition that minHeight applied to n is strictly smaller than minAcc(minHeight(A );fq j 00 0 00 j 2 Jg; ). In the following we let x = minAcc(minHeight(A );fq j j 2 Jg; ). By application of the same arguments as above (case m 62 B, third item), we have that 0 0 minHeight applied to n should be greater than or equal to minAcc(minHeight(A );fq j j 2 Jg; !a), hence also x > minAcc(minHeight(A );fq j j 2 Jg; !a). But being m 00 00 above anc(m ), we have that is a pre x of ; then, by Proposition 3.15, item 2, we have 0 00 000 00 000 minAcc(minHeight(A );fq j j 2 Jg; !a) = minAcc(x; Q ; !a) with = and 00 000 00 h2H Q = fq j h 2 H s.t. accTree(q; snd( )) = A [q ] g where Q = fq j j 2 Jg. h h j j q2Q 00 000 So far, we have proved that x minAcc(x; Q ; !a) > 0. We now observe that, by Proposition 3.18, x is smaller than or equal to minHeight applied to anc(m ), i.e. 00 w2W 0 0 assuming L(anc(m )) = p 4A [q ] and x = minHeight(A ), we have x x ; w 2 w 2 0 0 00 000 by Proposition 3.15, item 2, we have that also x minAcc(x ; Q ; !a) > 0, hence 0 0 00 000 x > minAcc(x ; Q ; !a). By de nition of witness subtree, given that m 2 img (anc) 00 00 and m ,! anc(m ), Q is a (non-strict) subset of the states fq j w 2 Wg, hence 0 00 000 0 by Proposition 3.15, item 3, we obtain minAcc(x ; Q ; !a) minAcc(x ;fq j w 2 Wg; !a). By combination of the last two inequations we obtain minHeight(A ) > minAcc(minHeight(A );fq j w 2 Wg; !a) that contradicts the de nition of witness 2 w subtree (item 2b). ?a ?a 0 0 We now consider n ,! n . In this case we have that p ! p . We have that A cannot be a single hole, otherwise minHeight(A) = 0, that implies minAcc(minHeight(A );fq j j 2 Jg; ) = 0, that implies that there exists a sequence of transitions , extending and 0 0 leading to a boundary node, such that minAcc(minHeight(A );fq j j 2 Jg; ) is unde ned, i2I contrary to what de nition of witness subtree says. Hence A[X 0 ] contains initially an q ;m ?a 0 00 a, that must be mimicked in the simulation game by Y 0 . This implies that also m ,! m . 00 00 We rst consider the case in which m 62 B: in this case we take m = m and m = m . 1 2 The rst item trivially holds because the set on the left cannot grow while the set on the right remains unchanged. The second item trivially holds because by inductive hypothesis Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:27 i2I we have A[X 0 ] v Y 0 ; we modify the l.h.s. by consuming the initial inputs, taking q ;m m the continuation of a, and replacing the remaining variables X 0 with X 00 ; as r.h.s. we q ;m q ;m i i take Y 00 . The relation v continue to hold as we follow on step a of the simulation game formalized in the De nition 3.12 of input tree compatibility, and we resolve some input choices in the l.h.s. The last item holds because the r.h.s. of the inequality reduce by one, while the l.h.s. cannot reduce by more than one. We now consider the case in which m 2 B. 00 + 00 There are two distinct cases: anc(m ) ,! m or m ,! anc(m ). These two cases are treated !a !a 0 0 00 00 as already done above for the case n ,! n , subcase in which m ,! m and m 2 B. i2I We can nally prove the thesis considering L(n) = p4A[q ] . If p is sending, then m can perform all send actions that p can do. Given any of such send actions !a, by de nition of witness subtree we have that accTree(q ; snd( )) is de ned for a sequence of actions , from m to a boundary node, that contains !a as a pre x; hence we 000 h2H have that all the states fq j h 2 H s.t. accTree(q ; snd( )) = A [q ] g can anticipate h j h j2J 000 h2H !a. Given that fq j i 2 Ig fq j h 2 H s.t. accTree(q ; snd( )) = A [q ] g we i j h h j2J also have that all the states q can anticipate !a. The possibility to perform the transition !a n ,! n also requires that p has no in nite loop of send actions, i.e., :cycle(!; p). Assume by contraposition that p has such an in nite loop of send actions. This means that there exists an in nite sequence of output transitions in the witness subtree that starts from the 0 0 00 k2K node m (which is such that L(m ) = p4A [q ] ) reaches a boundary node, and then continues from the ancestor of such boundary node to another boundary node, and so on. Eventually, an ancestor of a reached boundary node will be in between the last traversed ancestor and such boundary node (otherwise, we in nitely move strictly upward in the nite witness subtree, going from boundary nodes to ancestors that are always strictly above the last traversed ancestor). This contradicts the de nition of witness subtree stating that in all paths from an ancestor anc(o), to a corresponding boundary node o, there is at least one receiving transition. If p is receiving, then A cannot be a single hole (see the reasoning above for the case ?a 0 i2I n ,! n ). Let A = ha : A i . Having A[X 0 ] v Y 0 , we have that (by de nition of i i i2I q ;m m ?a i ?a 0 0 Y and v), for every i 2 I , there exists a transition m ,! m hence also p ! p . So we ?a can conclude that we have also n ,! n , for every i 2 I . Hence, we can conclude that if the candidate subtrees of simtree(M ; M ) identi ed 1 2 following the strategy explained in Part (2) are also witness subtrees, then we have M 4 M . 1 2 Remark 3.20. When our algorithm nds a successful leaf, a previously seen label, or a witness subtree in each branch then the machines are in the subtyping relation. If an unsuccessful leaf is found (while generating the initial nite subtree as described in Part (2)), then the machines are not in the subtyping relation. In all other cases, the algorithm is unable to give a decisive verdict (i.e., the result is unknown ). There are two possible causes for an unknown result: either (i) it is impossible to extract a forest of candidate subtrees (i.e., there are successful leaves below some ancestor) or (ii) at least one candidate subtree is not a witness (see Example 3.21). Example 3.21. Consider the machines M and M below: 1 2 20:28 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 ?a ?b q 4 q 1 1 !x !x q 4 q q 4 q q 4 q q 4 q 3 1 2 2 5 3 5 3 n4 n1 n2 n3 !x a b !x ?b !x a b q q 44 14 q 4 q q 4 q 5 3 5 3 a b q 3 n n 7 8 q q 1 3 q q 1 3 ?a a b !x a b q q 34 24 a b q q q 1 3 q q 1 3 !x a b a b a b q !x ?b !x a b q q 3 q 44 14 q 4 q q 4 q 5 3 5 3 a b q n13 n14 a b q a b q q q 1 3 q q 1 3 ?a a b a b a b q !x a b q q q 34 24 a b q a b q a b q q q 1 3 q q 1 3 n16 !x a b a b q a b q a b q a b q q q 1 3 Figure 6: Simulation tree of Example 3.21. ?a ?a ?b q q q 2 1 5 ?b !x M : M : q q q 1 2 2 1 3 !x !x !x !x !x q q 3 4 The simulation tree simtree(M ; M ), whose initial part is given in Figure 6, contains in nitely 1 2 many nodes with labels of the form: q 4ha : ha : ha : hi; b : q i; b : q i; b : q i (e.g., n 1 3 3 3 6 and n in Figure 6). Each of these nodes has two successors, one where ?a is red (the machines stay in their larger loops), and one where ?b is red (the machines move to their self loops). The machines can always enter this send-only cycle, e.g., between n and n or 2 3 between n and n . Because of these send only paths between ancestors (e.g., n ) and 13 14 2 leaves (e.g., n ), Condition (1) of De nition 3.16 never applies on the in nite branches of 3 Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:29 simtree(M ; M ), hence no witness subtrees can be found. Note however that our approach 1 2 successfully identi es a candidate subtree, i.e., the white nodes in Figure 6. 4. Implementation and evaluation To evaluate the applicability and cost of our algorithm, we have produced a faithful imple- mentation of it, which is freely available on GitHub [BCL 19b]. Implementation. The tool is implemented in Haskell and it mostly follows the structure of § 3. (1) It takes two machines M and M as input for which it builds a simulation tree 1 2 following De nition 3.2 in a depth- rst search manner, while recording the nodes visited in dierent branches to avoid re-computing several times the same subtrees. The function terminates whenever it expands a node whose label has been seen along the path from the root; or whenever it expands a node which has two ancestors that validate the termination condition from Theorem 3.8. The resulting tree is then passed onto the next function. (2) The next function divides the nite tree into several ( nite) subtrees following the strategy outlined on page 16. (3) A third function analyses each subtree to verify that they validate conditions (1)-(2b) of De nition 3.16. (4) Finally, for those subtrees that validate the property checked in (3), the tool builds their systems of input tree equations and checks whether they validate the compatibility condition from De nition 3.12. In function (1), if the tool nds a node for which none of the rules of De nition 3.2 apply, then it says that the two types are not related. If each subtree identi ed in (2) corresponds to branches that loop or that lead to a witness tree, then the tool says that the input types are in the subtyping relation. In all other cases, the result is still unknown, hence the tool checks for M 4 M (relying on a previous result showing that M 4 M () M 4 M [LY17,BCZ17]). 2 1 1 2 2 1 Once this pass terminates, the tool returns true or false, accordingly, otherwise the result is unknown. For debugging and illustration purposes, the tool can optionally generate graphical representations of the simulation and candidate trees, as well as the systems of input tree equations. Evaluation. We have run our tool on 174 tests which were either taken from the literature on asynchronous subtyping [LY17, CDSY17], or handcrafted to test the limits of our approach. All of these tests terminate under a second. Out of these tests, 92 are negative (the types are not in the subtyping relation) and our tool gives the expected result (\false") for all of them. The other 82 tests are positive (the types are in the subtyping relation) and our tool gives the expected result (\true") for all but 8 tests, for which it returns \unknown". All of these 8 examples feature complex accumulation patterns, that our theory cannot recognise. Example 3.21 gives a pair of machines for which our tool returns \unknown" for both M 4 M and M 4 M . 1 2 2 1 To assess the cost of our approach in terms of computation time and memory consump- tion, we have automatically generated a series of pairs of communicating machines that are successfully identi ed by our algorithm to be in the asynchronous subtyping relation. Our 20:30 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 benchmarks consists in applying our algorithm to check that M 4 M holds, with M and 1 2 1 M as speci ed below, where n; m 2 N are the parameters of our experiments. 2 >0 f!a ; : : : ; !a g !a !a 0 n 0 n M : M : 1 2 f?b ; : : : ; ?b g 0 m f?b ; : : : ; ?b g 0 m Machine M sends a sequence of n message a , after which it expects to receive a message 1 i from the alphabet fb ; : : : ; b g, then returns to its initial state. Machine M can choose to 0 m 2 send any message in fa ; : : : ; a g, then waits for a message in fb ; : : : ; b g before returning 0 n 0 m to its initial state. Observe that for any n and m we have that M 4 M holds. The shape 1 2 of these machines allows us to assess how our approach fares in two interesting cases: when the sequence of message accumulation grows (i.e., n grows) and when the number of possible branches grows (i.e., m grows). Accordingly, we ran two series of benchmarks. The plots in Figure 7 gives the time taken for our tool to terminate and the maximum amount of memory used during its execution (left and right y axis, respectively) with respect to the parameter n (left-hand side plot) or m (right-hand side plot). The top plots use linear scales for both axes, while the bottom plots show the same data but using a logarithm scale for the y axis. Observe that the left-hand side plot depicts a much steeper curve for computational time than the one of the right. Indeed, the depth of the nite subtree that needs to be computed and analysed increases with n (the depth of the nite subtree is 2n + 5 when m = 1). Accordingly, the depth of the input contexts that need to be recorded increases similarly (2n + 1). Each input context node has two children in this case, i.e., hb : h: : :i; b : h: : :ii. 0 1 In contrast, when m increases the depth of the simulation tree is bounded at 11. Consequently, the sizes of the nite subtrees are stable (depth of 7 when n = 1) but the number of (identical) candidate subtrees that need to be analysed increases, i.e., the tool produces m+1 trees when n=1. In this case the maximum depth of input contexts is also stable (the maximum depth is 3) but their widths increase with m, i.e., we have input context of the form: hb : h: : :i; : : : ; b : h: : :ii. These observations suggest that our algorithm is 0 m better suited to deal with session types that feature few anticipation steps (smaller n), but performs relatively well with types that contain many branches (larger m). The left-hand side plots show that the memory consumption follows a similar exponential growth to the computational time, unsurprisingly. For instance, our tool needs 2GB to check a pair machines where n = 10 and m = 1, and 8 GB when n = 11 and m = 1. The right-hand side plots show a much smaller memory footprint when m increases, this is explained by the fact that the depth of the simulation tree is bounded, only the input context of its nodes are growing in width. The memory in this case is more reasonable, e.g., our tool needs less than 11MB to check a pair of machines where n = 1 and m = 19. We suspect the several jumps in the memory usage curve are due to the GHC runtime requesting new arenas of memory from the operating system. All the benchmarks in this paper were run on an 8-core Intel i7-7700 machine with 16GB RAM running a 64-bit Linux. The time was measured by taking the dierence between the system clock before and after our tool was invoked. The memory usage refers to the maximum resident set size as reported by the /usr/bin/time -v command. Each test was ran 5 times, the plots report the average time (resp. memory) measurements. All our test data and infrastructure are available on our GitHub repository [BCL 19b]. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:31 x 8000000 F(x) ≈ 0.29508 * 1.4588 F(x) ≈ 0.00004 * 4.3344 Exec tion time Exec tion time Memory sage Memory sage 0 0 Parameter n Parameter m F(x) ≈ 0.00004 * 4.3344 F(x) ≈ 0.29508 * 1.4588 Exec tion time 2 Exec tion time Memory sage Memory sage 9 × 10 0 10 1 − 8 × 10 2 − 1 − 3 − 7 × 10 4 − 4 10 10 2 − Parameter m Parameter n Figure 7: Benchmarks: m=1 and increasing n (left) and n=1 and increasing m (right). Top and bottom plot show the same data, but the top plots use linear scales for all axes, the bottom plots use logarithmic scales for the vertical axes. 5. Related Work Gay and Hole [GH99, GH05] were the rst to introduce subtyping for session types. Their de nition, called synchronous subtyping, focuses on the possibility for a subtype to have dierent sets of labels in selections and branchings. In that paper, input selection is covariant (the subtype can have less inputs) while output branching is contravariant (the subtype can have more outputs). In our formulation of subtyping we have the opposite (branchings are covariant and selections are contravariant) because we follow a process-oriented interpretation of session types, while Gay and Hole [GH99, GH05] followed a channel-oriented interpretation. Later, Mostrous et al. [MYH09] extended such notion to asynchronous subtyping, by allowing for delayed inputs. Chen et al. [CDCY14, CDSY17] subsequently provided an alternative de nition which prohibits orphan messages and which is the de nition we adopted in this work. Recently, asynchronous subtyping was shown to be undecidable by reducing it to an equivalent problem for Turing machines [LY17] and queue machines [BCZ17]. Our previous work [LY17, BCZ17, BCZ18] investigated dierent restrictions to achieve decidability: in all of our previous approaches, these restrictions are either (i) setting bounds on the number of pending messages in the FIFO channels, or (ii) restricting the syntax of communicating machines and session types. Lange and Yoshida [LY17, § 4] identi ed two 0.0 2.5 5.0 7.5 8 10.0 12.5 15.0 17.5 0.0 2.5 5.0 7.5 10.0 12.5 15.0 17.5 Time (seconds) Time (seconds) Memory (kbytes) Memory (kbytes) Time (seconds) Time (seconds) Memory (kbytes) Memory (kbytes) 20:32 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 subclasses of (two-party) communicating machines for which the asynchronous subtyping relation is decidable via syntactical restrictions: alternating machines and non-branching machines. Alternating machines were introduced by Gouda et al. [GMY84] and require that each sending transition is followed by a receiving transition. A consequence of this restriction is that each FIFO queue may contain at most one pending message, i.e., it enforces a form of 1-bounded asynchrony. Non-branching machines enforce a syntactical restriction such that each state has at most one outgoing transition, i.e., given M = (Q; q ; ), 8q 2 Q : j(q)j 1. Bravetti et al. [BCZ17, BCZ18] investigate other decidable fragments of asynchronous subtyping. In contrast with the present work and those by Lange and Yoshida, they take a direct syntactical approach, i.e., they work directly on the syntax of (binary) session types rather than communicating machines. Chronologically, their rst article [BCZ17] proves the undecidability of asynchronous session subtyping in a restricted setting in which subtypes are non-branching (see de nition above) in all output selections and supertypes are non-branching in all their input branchings. Then, a decidability result is proved for a fragment in which they additionally impose that the subtype is also non-branching in input branchings (or that the supertype is also non-branching in output selections). Later, in [BCZ18], the same authors consider more fragments, namely k-bounded asynchronous subtyping (bound on the size of input-anticipations), and two syntactical restrictions that imposes non-branching only on outputs (resp. inputs). More formally, following the automata notation, they restrict to machines M s.t. M = (Q; q ; ), 0 0 8q 2 Q : j(q)j 1 with Q coinciding with the set of sending (resp. receiving) states of Q. All such fragments are shown to be decidable. In [BLZ21], Bravetti et al. propose a fair variant of asynchronous session subtyping. This fair subtyping handles candidate subtypes that may simultaneously send each other a nite but unspeci ed amount of messages before removing them from their respective buers. Such types are not supported by the relation studied here, notably due the niteness of input contexts A and the :cycle(!; p) condition in De nition 2.6 (3b). This fair subtyping is shown to be undecidable, but a sound algorithm and its implementation are given in [BLZ21]. The relationship between communicating machines and binary asynchronous session types has been studied in [BZ21], where a correspondence result between asynchronous session subtyping and asynchronous machine re nement is established. On the other hand, the relationship between communicating machines and multiparty asynchronous session types has been studied in [DY12,DY13]. Communicating machines are Turing-powerful, hence their properties are generally undecidable [BZ83]. Many variations have been introduced in order to recover decidability, e.g., using (existential or universal) bounds [GKM07], restricting to dierent types of topologies [LMP08, PP92], or using bag or lossy channels instead of FIFO queues [CHS14, CFI96, AJ93, ABJ98]. In this context, existentially bounded communicating machines [GKM07] are one of the most interesting sub-classes because they include in nite state systems. However, deciding whether communicating machines are existentially bounded is generally undecidable. Lange and Yoshida [LY19] proposed a (decidable) property that soundly characterises existential boundedness on communicating machines corresponding to session types. This property, called k-multiparty compatibility (k-mc), also guarantees that the machines validate the safety property of session types [DY13, LTY15], i.e., all messages that are sent are eventually received and no machine can get permanently stuck waiting for a message. This notion of safety is closely related to asynchronous session subtyping for two-party communicating machines, i.e., we have that M 4 M implies that the system 1 2 M j M is safe [LY17, CDSY17]. Because the present work is restricted to two-party 1 2 Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:33 systems, our algorithm cannot be used to verify the safety of multiparty protocols, e.g., the protocol modelling the double-buering algorithm [MYH09] is 2-multiparty compatible but cannot be veri ed with our subtyping algorithm because it involves three parties. This algorithm is used in multicore systems [SK08] and can be type-checked up-to asynchronous subtyping [MYH09]. An extension of our work to support multiparty protocols is being considered, see § 6. We note that because the k-mc property of [LY19] is based on a bounded analysis, it cannot guarantee the safety of systems that exhibit an intrinsically unbounded behaviour, like machines M and M in Figures 1 and 2. R S 6. Conclusions and Future Work We have proposed a sound algorithm for checking asynchronous session subtyping, showing that it is still possible to decide whether two types are related for many nontrivial examples. Our algorithm is based on a (potentially in nite) tree representation of the coinductive de nition of asynchronous subtyping; it checks for the presence of nite witnesses of in nite successful subtrees. We have provided an implementation and applied it to examples that cannot be recognised by previous approaches. Although the (worst-case) complexity of our algorithm is rather high (the termination condition expects to encounter a set of states already encountered, of which there may be exponentially many), our implementation shows that it actually terminates under a second for machines of size comparable to typical communication protocols used in real programs, e.g., Go programs feature between three and four communication primitives per channel and whose branching construct feature two branches, on average [DL19]. As future work, we plan to enrich our algorithm to recognise subtypes featuring more complex accumulation patterns, e.g., Example 3.21. Moreover, due to the tight correspon- dence with safety of communicating machines [LY17], we plan to investigate the possibility of using our approach to characterise a novel decidable subclass of communicating machines. It is an interesting open question to extend our algorithm to multiparty communications, as multiparty session types allow more permutations of actions inside a single CFSM and can type more practical use cases which involve several participants. Recently precise multiparty asynchronous subtyping (in the sense of [CDCY14, CDSY17, GJP 19]) for the asynchronous multiparty session -calculus [HYC08, HYC16] was proposed in [GPP 21]. In another direction of future work we will consider an algorithm for checking subtyping which is sound, but not complete with respect to [GPP 21]. Finally, a signi cant further extension could be to also encompass pre-emption mechanisms, see e.g. [BZ09, Bra21], which are often used in communication protocols. Acknowledgement The work is partially funded by H2020-MSCA-RISE Project 778233 (BEHAPI); and EP- SRC EP/K034413/1, EP/K011715/1, EP/L00058X/1, EP/N027833/1, EP/N028201/1, EP/T014709/1, EP/V000462/1, EP/T006544/1 and NCSC VeTSS. 20:34 M. Bravetti, M. Carbone, J. Lange, N. Yoshida, and G. Zavattaro Vol. 17:1 References [ABB 16] Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deni elou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95{230, 2016. [ABJ98] Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the- y analysis of systems with unbounded, lossy FIFO channels. In CAV 1998, pages 305{318, 1998. [AJ93] Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In (LICS 1993), pages 160{170, 1993. [BCL 19a] Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping. In CONCUR, volume 140 of LIPIcs, pages 38:1{38:16. Schloss Dagstuhl - Leibniz-Zentrum fur Informatik, 2019. [BCL 19b] Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, and Gianluigi Zavattaro. A sound algorithm for asynchronous session subtyping. https://github.com/julien-lange/ asynchronous-subtyping, 2019. [BCZ17] Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. Undecidability of asynchronous session subtyping. Inf. Comput., 256:300{320, 2017. [BCZ18] Mario Bravetti, Marco Carbone, and Gianluigi Zavattaro. On the boundary between decidability and undecidability of asynchronous session subtyping. Theor. Comput. Sci., 722:19{51, 2018. [BLZ21] Mario Bravetti, Julien Lange, and Gianluigi Zavattaro. Fair re nement for asynchronous session types. In FoSSaCS, Lecture Notes in Computer Science, 2021. To appear. Available at https: //arxiv.org/abs/2101.08181. [Bra21] Mario Bravetti. Axiomatizing maximal progress and discrete time. Log. Methods Comput. Sci., 17(1), 2021. [BZ83] Daniel Brand and Pitro Za ropulo. On communicating nite-state machines. J. ACM, 30(2):323{ 342, 1983. [BZ09] Mario Bravetti and Gianluigi Zavattaro. On the expressive power of process interruption and compensation. Math. Struct. Comput. Sci., 19(3):565{599, 2009. [BZ20] Mario Bravetti and Gianluigi Zavattaro. Process calculi as a tool for studying coordination, contracts and session types. J. Log. Algebraic Methods Program., 112:100527, 2020. [BZ21] Mario Bravetti and Gianluigi Zavattaro. Asynchronous session subtyping as communicat- ing automata re nement. Software and Systems Modeling, 2021. https://doi.org/10.1007/ s10270-020-00838-x. [CDCY14] Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. On the preciseness of subtyping in session types. In PPDP 2014, pages 146{135. ACM Press, 2014. [CDSY17] Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini, Alceste Scalas, and Nobuko Yoshida. On the preciseness of subtyping in session types. Logical Methods in Computer Science, 13(2), 2017. [CFI96] G erard C ec e, Alain Finkel, and S. Purushothaman Iyer. Unreliable channels are easier to verify than perfect channels. Inf. Comput., 124(1):20{31, 1996. [CHS14] Lorenzo Clemente, Fr ed eric Herbreteau, and Gr egoire Sutre. Decidable topologies for communi- cating automata with FIFO and bag channels. In CONCUR 2014, pages 281{296, 2014. [dBBLZ18] Frank S. de Boer, Mario Bravetti, Matias David Lee, and Gianluigi Zavattaro. A petri net based modeling of active objects and futures. Fundam. Informaticae, 159(3):197{256, 2018. [DL19] N. Dilley and J. Lange. An empirical study of messaging passing concurrency in Go projects. In 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER), pages 377{387, Feb 2019. [DY12] Pierre-Malo Deni elou and Nobuko Yoshida. Multiparty session types meet communicating automata. In ESOP 2012, pages 194{213, 2012. [DY13] Pierre-Malo Deni elou and Nobuko Yoshida. Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In ICALP 2013, pages 174{186, 2013. [GH99] Simon J. Gay and Malcolm Hole. Types and subtypes for client-server interactions. In ESOP 1999, pages 74{90, 1999. [GH05] Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Inf., 42(2-3):191{225, 2005. Vol. 17:1 SOUND ALGORITHM FOR ASYNCHRONOUS SESSION SUBTYPING 20:35 [GJP 19] Silvia Ghilezan, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas, and Nobuko Yoshida. Precise subtyping for synchronous multiparty sessions. JLAMP, 104:127{173, 2019. [GKM07] Blaise Genest, Dietrich Kuske, and Anca Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147{167, 2007. [GMY84] Mohamed G. Gouda, Eric G. Manning, and Yao-Tin Yu. On the progress of communications between two nite state machines. Information and Control, 63(3):200{216, 1984. [GPP 21] Silvia Ghilezan, Jovanka Pantovic, Ivan Prokic, Alceste Scalas, and Nobuko Yoshida. Precise Subtyping for Asynchronous Multiparty Sessions. 5:16:1{16:28, 2021. A full version is available from https://arxiv.org/abs/2010.13925. [HY16] Raymond Hu and Nobuko Yoshida. Hybrid session veri cation through endpoint API generation. In FASE 2016, pages 401{418, 2016. [HYC08] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In POPL'08, pages 273{284. ACM, 2008. [HYC16] Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. J. ACM, 63(1):9:1{9:67, 2016. [JM99] Petr Jancar and Faron Moller. Techniques for decidability and undecidability of bisimilarity. In CONCUR 1999, pages 30{45, 1999. [LM16] Sam Lindley and J. Garrett Morris. Embedding session types in Haskell. In Haskell 2016, pages 133{145, 2016. [LMP08] Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Context-bounded analysis of concurrent queue systems. In TACAS 2008, pages 299{314, 2008. [LTY15] Julien Lange, Emilio Tuosto, and Nobuko Yoshida. From communicating machines to graphical choreographies. In POPL 2015, pages 221{232, 2015. [LY16] Julien Lange and Nobuko Yoshida. Characteristic formulae for session types. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 833{850. Springer, 2016. [LY17] Julien Lange and Nobuko Yoshida. On the undecidability of asynchronous session subtyping. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 441{457, 2017. [LY19] Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating session automata. In Computer Aided Veri cation - 31st International Conference, volume 11561 of Lecture Notes in Computer Science, pages 97{117. Springer, 2019. [MY15] Dimitris Mostrous and Nobuko Yoshida. Session typing and asynchronous subtyping for the higher-order -calculus. Inf. Comput., 241:227{263, 2015. [MYH09] Dimitris Mostrous, Nobuko Yoshida, and Kohei Honda. Global principal typing in partially commutative asynchronous sessions. In ESOP 2009, pages 316{332, 2009. [NHYA18] Rumyana Neykova, Raymond Hu, Nobuko Yoshida, and Fahd Abdeljallal. A Session Type Provider: Compile-time API Generation for Distributed Protocols with Interaction Re nements in F]. In CC 2018. ACM, 2018. [OY16] Dominic A. Orchard and Nobuko Yoshida. Eects as sessions, sessions as eects. In POPL 2016, pages 568{581, 2016. [Pad17] Luca Padovani. A simple library implementation of binary sessions. J. Funct. Program., 27:e4, [PP92] Wuxu Peng and S. Purushothaman. Analysis of a class of communicating nite state machines. Acta Inf., 29(6/7):499{522, 1992. [SK08] Jose Sancho and Darren Kerbyson. Analysis of double buering on two dierent multicore architectures: Quad-core opteron and the cell-be. pages 1{12, 04 2008. [SY16] Alceste Scalas and Nobuko Yoshida. Lightweight session programming in scala. In ECOOP 2016, pages 21:1{21:28, 2016. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany
Computing Research Repository – arXiv (Cornell University)
Published: Jun 30, 2019
You can share this free article with as many people as you like with the url below! We hope you enjoy this feature!
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get an introductory month for just $19.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.