Keywords

1 Introduction

Modern society is increasingly dependent on large-scale software systems that are distributed, collaborative, and communication-centred. One of the techniques developed to handle the additional complexity caused by distributed actors are multiparty session types (MPST) [19]. MPST allow to specify the desired behaviour of communication protocols as by-design correct types that are used to verify the communication structure of software products. The properties guaranteed by well-typed processes cover communication safety (all processes conform to globally agreed communication protocols) and liveness properties such as deadlock-freedom. Their main advantage is that their verification method is extremely efficient—in comparison to e. g. standard model checking.

MPST were developed to govern communication and concurrency in distributed systems. However, as it is typical for type systems, standard MPST variants (without dependable types) do not support the analysis of properties that require the consideration of concrete runs or concrete values of variables.

The hardest part about the verification of distributed systems is the state space explosion that results from concurrent communication attempts, i. e., the exponential blow-up that results from computing all possible combinations of potential communication partners. The problem of concurrency mainly lies in the communication structure, which is already completely captured by MPST. We show that the knowledge of a program/system to be well-typed, allows us to sequentialise it following the structure of its global type and thereby to remove all communication. Accordingly, we show how we can benefit from the effort we spend on an MPST analysis of a system also for the verification of its properties that go beyond its communication structure.

We use the global type of a well-typed system to guide its sequentialisation. We refer to the result as sequential global process (SGP), although it might still contain parallel compositions, albeit only on completely independent parts. Since the structure of communication was already verified by the well-typedness proof, we can reduce communication to value updates. More precisely, we map well-typed systems that interact concurrently, to SGP-systems without any interaction mechanisms or name binders. Such SGP-systems consist of a vector of variables with values and a SGP-process that simulates the data flow of the original system. Therefore, we translate the reception of data in communication into updates of the vector in the SGP-system. By removing the communication we remove also the problem of state space explosion. Our translation is valid if the considered process is well-typed w. r. t. a (set of) global type(s). Thereby, we sequentialise communications that may happen concurrently in the original system but are sequential in global types. Note that such communications are always causally independent of each other, thus ordering them does not significantly influence the behaviour of the system, e. g. it does not influence what values are computed. Apart from such sequentialisations the original system and its abstraction into a SGP-system behave similarly.

Contributions. We provide an algorithm to remove communication from well-typed systems and thereby sequentialise them, while preserving the evolution of data of the original system. Deriving this algorithm was technically challenging but the result is a simple rewriting function and easy to automate.

Then we prove that, provided that the original system was well-typed, the algorithm produces a SGP-system that is closely related to the original system: the original system and its abstraction are related by a variant of operational correspondence [14] and are coupled similar [23]. With that, the derived SGP-system is a good abstraction of the original system that can be used instead of the original to verify properties on concrete data. Since the mapping into SGP-systems is usually linear and because SGP-systems do not contain any form of interaction or binders, properties can be checked more efficiently.

Finally, we provide a mapping—that is again a simple rewriting algorithm—from SGP-processes into Promela, the input language of the model checker Spin [16, 17]. With that, the properties that are not already guaranteed by the MPST analysis but require the consideration of concrete runs or concrete data can be checked. Since the main challenge here is the sequentialisation of concurrent systems into interaction-free abstractions, the translation of SGP-systems into Promela is simple and can be used as a role model to obtain similar mappings for other model checkers.

Related Work. Intuitively, the technique that we present in this paper is a special case of partial order reduction (compare e. g. to [24]) as they can be found in model checkers. This technique tries to reduce the state space that has to be inspected in verification, by identifying different sequences of transitions that lead to similar states. Here, instead of searching for such similar states, we follow the structure of the global type, where well-typedness ensures that the generated abstraction captures the complete state space of the original system modulo coupled similarity.

The approach of [1] is very similar to this paper. Just as our algorithm, they rewrite a program (written in Haskell) by replacing communication with value updates, to obtain a sequential abstraction of the program on that verification—e. g. of termination based on values that are computed at runtime—can be done efficiently. The main difference is that [1] requires that the considered programs satisfy symmetric non-determinism whereas we require that programs are well-typed using MPST. Assuming asynchronous communication, symmetric non-determinism means that every receive in a given program location can receive only messages from either a single process or a set of symmetric processes, i. e., processes running the same code, at the same program location. MPST are more flexible, i. e., are not limited to systems that satisfy symmetric non-determinism. Hence, the method presented here can be applied to a larger class of programs.

Interestingly, we find a similar idea also in papers about the verification of distributed algorithms via invariants that use so-called standard forms (compare e. g. to [9, 29]), where the global view gets constructed by gathering and combining all local processes. In case of [29] standard forms have their own TLA-like semantics that is 1-to-1 correspondent to the calculus semantics for proving properties on data. The main difference to these approaches is that we completely remove communication and present an algorithm to automatically derive this global view from a given well-typed system and its global type.

In [6] global types are translated into processes to mediate between multiparty and binary session types. These mediator processes capture the behaviour of global types—w. r. t. the communication structure and not values—to provide a disciplined communication exchange that allows to translate MPST into binary sessions. In contrast to this approach, we map processes onto processes and use global types to guide this mapping, where the communication structure is removed and our focus is on the evolution of data.

Choreographies [22] are global descriptions of distributed systems from which the distributed system is generated by endpoint projection. In contrast, we start with the distributed system and its global type. Note that global types describe solely the communication structure, i. e., interactions, of the system and do not contain any other implementation details of single peers. With that, MPST have an advantage in comparison to choreographies in industrial settings, where different parts are developed independently. Moreover, we also consider the case of interleaved MPST sessions. Our challenge is to derive a global description on how the data evolves in the system. This is related to the extraction of choreographies from distributed systems as discussed in [7, 10]. However, without the global type as guide, the described algorithms to extract choreographies are exponential, whereas our algorithm is usually linear.

In [5] MPST are extended by assertions that allow to verify properties on data values provided that these properties are satisfied in all runs. In contrast, our approach allows to efficiently compute the exact values that are computed in concrete runs. Moreover, the language of assertions is limited to the language defined in [5] and an extension might require to redo some proofs, whereas here only the translation into Promela, i. e., the use of a concrete model checker, forces us to limit the languages of expressions and properties. The algorithm to sequentialise systems into SGP-systems does not rely on such limitations. A prominent example of a property that cannot be analysed statically is termination of a loop after computing some value. To prove such properties, a type system can use dependent types such as e. g. in [28]. In contrast to such extensions of MPST with dependable types, we do not add any complexity to the type system (or provide any new variant of MPST). Instead we provide a simple rewriting algorithm that transforms a well-typed system (after the type check) into an abstraction on that remaining properties on data can be verified with existing specialised tools.

Overview. In Sect. 2 we introduce multiparty session types very briefly. Section 3 describes how well-typed systems are sequentialised. Section 3.1 introduces a calculus for sequential global processes, Sect. 3.2 describes an algorithm to map into SGP-systems for the case of synchronous MPST and single sessions, and Sect. 3.3 discusses asynchronous variants of MPST and extends the algorithm to cover interleaved sessions. Section 4 shows operational correspondence and relates the original system and its abstraction by coupled similarity. Then, Sect. 5 illustrates how the sequentialisation can be used to verify properties of the original system. It discusses the limits of this method, i. e., what kind of properties cannot be analysed this way and presents a mapping from SGP-processes into Promela. We conclude in Sect. 6. Missing proofs and additional material can be found in [26].

2 Multiparty Session Types in a Nutshell

Our aim is to use the structure of a global type to remove communication—and with that the related concurrency—from the problem of verifying properties on the evolution of values. We conjecture that this procedure can be used for all kind of MPST variants but explain the method on a simple variant of synchronous MPST w. r. t. a single session. Later we extend our algorithm to asynchronous MPST with interleaved sessions. To explain the basic idea, we use a variant of multiparty synchronous session types as introduced in [2] with some alternations similar to variants as e. g. in [4, 11, 30].

MPST were developed to govern communication and concurrency in distributed systems. Therefore, systems are checked against a global type. Global types specify the desired communication structure from a global point of view. The specified communication structure of a global type describes a session and the participants of such a session are called roles. Here, they are given by

The first construct specifies a communication from Role  to that offers different branches for the receiver with respect to a label that is transmitted by the sender, where are the sorts (i. e., base types) of the transmitted values. If is a singleton, we abbreviate communication with . The other constructs introduce parallel composition, recursion, and successful termination.

The systems, that we want to analyse, are modelled in a session calculus. As usual, we use an extension of the \( \pi \)-calculus [21] given by

The first two constructs are used to initiate a session. The next two constructs model the sender and the receiver of a communication within a session, where the are (input bounded) variables that are instantiated as result of a communication by the received values. The remaining constructs introduce conditionals, parallel composition, termination, restriction, and recursion. Since we want to use the model checker Spin later, we restrict expressions (the values that are transmitted in communication) and conditions (used to guide conditionals) to functions that are known by Promela, the input language of Spin.

We use structural congruence () to abstract from syntactically different but semantically similar processes, where is the least congruence that satisfies alpha-conversion () and the rules:

The reduction semantics of the session calculus is given by the rules:

The Rule Link initialises a session on the roles , where requested the session on channel and each participates in the session as . Communication within a session is described by Rule Com, where in the case of matching roles and labels the continuations of sender and receiver are unguarded and the variables are replaced by the values in the receiver. The Rules If-T and If-F reduce conditionals as expected. The remaining rules allow for steps in various contexts and are standard.

Let return the roles used in a global type or a process. A process has an actor on if has an unguarded subterm of the form with or (for session invitations) or an unguarded subterm of the form or (for communication). Let be set of actors in . If unambiguous, i. e., if there is only one session, we omit the session channel and abbreviate actors by their role.

The processes are checked against their specification in type judgements , where \( \varGamma , \varDelta \) are type environments that are built from the type information in the global type. A system that passes such a type check is denoted as well-typed. The design of MPST guarantees strong properties for the communication structure of well-typed systems.

Theorem 1

Assume , i. e.,  is well-typed.

  • Subject Reduction: If then there is \( \varDelta ' \) such that .

  • Linearity: has no two unguarded senders/receivers for the same actor.

  • Progress: If then either or .

To prove these properties, we have to reason about the typing rules that define under which circumstances a type judgement is valid. Due to space limitations, the typing rules as well as some other important aspects of MPST (e. g. projection and local types) and the proofs are postponed to [26]. Note that we do not introduce a new variant of MPST. Instead we rely on a standard MPST variant of that we introduced global types and the session calculus, because they are necessary to understand the remainder of this paper.

3 Sequentialising Well-Typed Systems

MPST are designed to analyse the communication structure of a system. Well-typed systems are guaranteed to satisfy properties like communication safety or progress. What remains, are safety and liveness properties that involve data.

We use the global type of a well-typed term to guide the sequentialisation of the implementation. The result is a kind of process that we call sequential global process (SGP), although it might still contain parallel compositions but only on completely independent parts. This abstraction of the implementation allows us to analyse properties on the values of data in the implementation without the problem of state space explosion that is caused by the concurrency of communication in the original system.

3.1 A Calculus for Sequential Global Processes

SGP-processes are simple processes consisting of assignments of values to variables, conditionals, parallelism, termination, and recursion.

Definition 1

(SGP-Processes). SGP-processes are given by

where are expressions to calculate a value, are boolean conditions, and process variables.

SGP-processes introduce a new operator to assign values to variables in a vector. An assignment describes a SGP-process that updates the variables \( \tilde{v} \) by the values and then continues as , where is short hand for . If \( \tilde{v} \) (and accordingly also ) is the empty sequence, then we abbreviate this empty assignment by . Note that SGP-processes inherit the parallel operator not from processes but from global types. Thus, the parallel composition describes that and are independent, i. e., all variables that appear on both sides are used as read-only on both sides. The remaining operators for conditionals, successful termination, and recursion are inherited from processes. Note that SGP-processes do neither contain any interaction mechanisms nor name binders. But we still have branching via conditionals and recursion.

The SGP-processes are combined with a vector \( \mathcal {V} \) of variables, that represents the current values of the local variables of all processes of the original distributed system. They consist of the input bounded variables of the implementation. A SGP-system then consists of a knowledge vector \( \mathcal {V} \) and a SGP-process S.

Fig. 1.
figure 1

Reduction Semantics of SGP-Systems.

Full size image

Structural congruence on SGP-processes \( \equiv _{\textsf {S}}\) is the restriction of on SGP-processes. Let \( \equiv _{\mathcal {S}}\) be the least congruence that satisfies the rules and . We write for the result of replacing, for all \( v_i \in \tilde{v} \), the current value of the variable \( v_i \) in the vector \( \mathcal {V} \) by the value that results from the evaluation of the expressions . The semantics of SGP-systems is given in Fig. 1. We naturally extend substitution to SGP-systems, i. e.,  . Let be the result of replacing all variables v in conditions and expressions in that are not sequentially hidden after an assignment of v by the current value of v in \( \mathcal {V} \), e. g. :

3.2 Mapping Well-Typed Systems onto SGP-Systems

We use the global type of a well-typed process to sequentialise into a SGP-process. Because of the parallel operator, SGP-processes are not completely sequential. However, since we remove communication and with it all forms of interaction from SGP-processes, parallel composition in SGP-processes is between independent parts only. More precisely, SGP-systems cover read and write operations on their vector of variables that simulate the evolution of knowledge in the original distributed system.

The main idea of the algorithm is simple. We fuse matching senders and receivers, i. e., the receiver that receives a message with the sender that transmitted this message, into a single SGP value assignment. The value assignment captures what the processes gain as new information from a communication. The problem is that finding the matching communication partners in the general \(\pi \)-calculusis NP-hard. In the \(\pi \)-calculusit is possible to have several matching receivers for a single sender or vice versa. Performing a communication step can unguard further senders and receivers. So different choices of matching pairs of communication partners and different orders in that communications are performed influence the further behaviour. To reduce the complexity of this problem, we use the type information that allows us to completely avoid the search for matching communication partners.

Firstly, well-typedness guarantees that there are no races at runtime, i. e., in no state there is more than one matching receiver for a sender and vice versa. This ensures, that for each well-typed system there is indeed a single SGP-abstraction that captures its overall behaviour, whereas without well-typedness (i. e., in the presence of races) several SGP-abstractions might be necessary to describe the behaviour of a single system. Secondly, well-typedness also ensures that there are no orphan communication partners, i. e., each sender will eventually meet a matching receiver and vice versa. Finally, the global type of a well-typed system tells us when and where communication takes place. Or, more precisely, the global type tells us one possible order of the communications and well-typedness ensures that all other possible orderings of communications of the system are similar (see Sect. 4). Accordingly, we do not search for matching communication partners but follow the structure of the global type. If the global type specifies that next there is a communication then we know that in the mentioned actors the respective send and receive action is indeed unguarded or guarded only by conditionals, that can be resolved without interactions.

Similarly, it is difficult in general \(\pi \)-calculussystems to identify at which point we have to introduce a global loop to translate the recursive behaviour of the single actors into a recursion of the global abstraction. Again we follow the structure of the global type and simply introduce a global loop if the global type loops, while ignoring the structure of recursion in the actors and only unfolding local recursion if necessary.

When we remove communication prefixes in order to obtain a SGP-process, we lose their respective scopes. To avoid ambiguities in SGP-systems and to clarify the owner of variables, we indicate input bounded variables, i. e., the variables a SGP-process may write on, by its corresponding actor. The variables indicated by an actor are the local knowledge of this actor. SGP-processes that are derived from well-typed processes will not have write access on variables of other actors but may read them to perform value updates.

The following mapping relies on the fact that the parallel composition is well-typed w. r. t. the global type . We prove in Theorem 2 below, that this mapping indeed produces a SGP-process in this case.

Definition 2

The partial mapping is defined inductively as:

figure bm

Note that the different cases of this definition are ordered. Thus, a conditional is not resolved (Case 10) unless none of the other cases can be applied. The first two cases provide the base cases for global types that are terminated (Case 1) or reduced to a type variable (Case 2). In these two cases the considered processes are ignored. The next three cases do not alter the type but prepare processes by removing restriction on session channels (Case 3)—which is safe because we will also remove all communication prefixes—splitting parallel compositions (Case 4), and unfolding recursion (Case 5). Because we require that process variables are guarded by a communication prefix, we cannot unfold the same recursion twice without applying another case in between.

The next three cases map processes that are well-typed w. r. t. a global type on communication (Case 6), parallel composition (Case 7), and recursion (Case 8), i. e., here we follow the structure of the global type to map the process. Case 6 unifies the sender and the receiver of a communication specified in the global type and maps it on corresponding value assignments. These assignments simulate the reception of the values on the variables of the receiver , where is the result of indicating the variables with the actor of the receiving end. The substitution of into ensures that names of different parallel branches are not confused.

This substitution does not remove all remaining name clashes but only the harmful clashes between parallel composed components of the considered system. Sequential composed input binders on the same variable and of the same actor are translated to the same name. If we apply this algorithm on processes that are not well-typed, we may still have parallel occurrences of syntactically the same name in parallel composed input binders. But well-typedness ensures that all such occurrences are linked to different actors and are thus distinguished. With that, we unify variables—that might have been denoted the same on purpose—and reduce the vector of variables in the SGP-system. Also, input bounded variables of different iterations of recursion are unified.

Case 7 maps a parallel composition of global types on a parallel composition of SGP-processes. Note that in both cases, parallel composition is between independent objects that have no means of interaction. To split the parallel components of the system accordingly, we rely on their roles. Well-typedness of the system ensures that it can be split as required.

Case 8 introduces recursion if the global type tells us to do so. This case does not alter the considered system or enforces any requirements on the structure of the system. Well-typedness ensures that the structure of the system w. r. t. recursion matches the recursion of the global type, but not necessarily that the system and the global type use recursion at the same time. For example is well-typed w. r. t.  , although the global type partially unfolds the recursion in comparison to the recursion of the process. Therefore, we rely on well-typedness and use only the global type to determine the correct place of recursion, where Case 5 allows to unfold recursion in processes. To ensure that the process variables of nested recursions are not confused, the Cases 2 and 8 use the type variable of the global type as index to distinguish process variables.

Case 9 unifies session invitations and the corresponding acceptances and maps them on an empty value assignment \( \tau \). The session invitation mechanism is already validated in the well-typedness proof and does not influence the data of the processes in the system. Thus, it is safe to ignore this step in SGP-processes.

Case 10 maps a conditional of one of the parallel components of the system to a conditional in the SGP-process. Global types do not consider conditionals of processes, but well-typedness ensures that both cases of the conditional have to follow the same global type. Because of that, both cases of the SGP-conditional inherit the same global type. To avoid unnecessary branching, we delay the mapping of conditionals until this is necessary e. g. to unguard a sender or receiver of a communication that is specified in the global type.

The mapping in Definition 2 is not deterministic, because it does not enforce an order in that several unguarded conditionals are mapped in Case 10 and this leads to different possible SGP-processes. Similarly, it is not specified in which order several restrictions in Case 3, several parallel compositions in Case 4, or several recursive processes in Case 5 are handled, though different orders in these cases will not lead to different SGP-processes. The other cases are guided by the global type or the fact that there is only one session. To obtain a deterministic version—and simplify the proofs—and to minimize the size of the computed SGP-process, we assume that Definition 2 gives precedence to parallel branches that implement (1) senders and (2) receivers that are unguarded in the global type and (3) smaller roles. However, different orders in that conditionals are handled lead to weakly bisimilar SGP-processes, because only unguarded conditionals are mapped, the translated subprocesses of the conditional are guarded by the resulting SGP-conditional, and an unguarded conditional will reduce to the same case in a single \( \tau \)-step regardless of when we perform this step.

3.3 Asynchrony and Interleaved Sessions

The mapping in Definition 2 is designed for a synchronous variant of multiparty session types and only single sessions, because the syntax and semantics is simpler in these cases. However, the mapping in Definition 2 is exactly the same for the case of multiparty asynchronous session types as introduced in [19, 20].

Note that the semantics of the session calculus defined in [19, 20] use messages queues to reflect the asynchronous nature of communication. Sending and receiving are decoupled into two separate steps to transmit and then read from message queues. Nonetheless, when we remove communication in the mapping , we unify sending and receiving into value assignments as described in the Case 6 of Definition 2. This is because, SGP-processes are designed to track the evolution of data values of processes and therefore only the reception of values is relevant. Intuitively, value assignments of SGP-processes reflect the case that a participant of a session has learned new information by the reception of values and this information flow is covered by value assignments. To determine the correct point in the behaviour of the system in that a particular participant gains new information through the reception of values, we rely on the fact that for this communication to happen both communication partners, the sender and the receiver have to be unguarded. Well-typedness and the structure of the global type, guide us in the case of concurrently enabled communication prefixes.

The definition of well-typed processes for several interleaved sessions is more difficult. As described in [3], we have to ensure that actions of different sessions do not cause deadlocks by cyclic dependencies. Processes with only acyclic dependencies between interactions of different sessions are denoted as globally progressing. However, adapting to allow for several interleaved sessions in processes that are globally progressing is straightforward. First we remove name clashes between session channels using alpha conversion. Then we adapt the mapping of Definition 2 into , where the latter expects a set and a set of pairs of global types and session channels as input such that the parallel composition is well-typed w. r. t.  and does not contain name clashes between session channels.

Definition 3

  is defined inductively as:

figure cg

To deal with multiple sessiones (and their global types), we split Case 1 into a case to introduce the SGP-process \(\mathbf {0}\) as soon as the set of considered global types is empty (Case 1a) and a case to remove terminated global types end from the set (Case 1b). In a similar way, we split Case 7 into a case to introduce a parallel composition of SGP-processes if the considered sets of processes can be partitioned into two sets that implement the actors of different sessions (Case 7a) and a case to split parallel global types (Case 7b), i. e., to replace by if there is a such that . The adaptation of the Cases 3, 4, 5, 6, 9, and 10 to multiple global types is straightforward. The Cases 2 and 8 for recursion, are replaced by variants that require all types of the considered set of global types to be reduced to a type variable or a recursive global type, respectively. With that we follow [3], that similarly requires that interleaved sessions can be joined in recursion. The remaining cases are straightforwardly adapted to sets of types.

Note that an implementation of this algorithm should exploit the acyclic dependency relation that is build according to [3] between interactions of different sessions. This relation tells us for the Cases 6 and 9, whether the required communication partners for a session are already unguarded or guarded by another session. In the latter case this communication will introduce a dependency from another session to this session and the respective case cannot be applied. Similarly, this relation tells us for Case 7a that it is possible to introduce a SGP parallel composition if and only if we can split the set of sessions into two disjoint sets such that there are no dependencies between the sessions in different sets.

We overload the definition of for interleaved sessions. Let be well-typed w. r. t.  and . Then the corresponding SGP-system is , where \( \mathcal {V} \) is the vector of names in .

Note that the results of Sect. 4 are proved in [26] for both variants: and . As we claim, we can extend this algorithm to all variants of MPST that satisfy linearity, i. e., all MPST variants we are aware of. This also includes variants with session delegation. Delegation can be handled similarly to session invitations using a substitution for the delegated session name.

4 Relating the Implementation and Its Sequentialisation

We show that for all processes that are well-typed w. r. t. the global types , the mapping is defined and returns a SGP-process. Therefore, we show that all cases of Definition 3 except for Case 8 preserve well-typedness in their recursive calls. By an induction over and the structure of the respective types, we show then that—after some preparation steps in the Cases 3, 4, 5, and 10 that do not alter the type—well-typedness ensures that the structure of the system is as required by the respective case to reduce the types. The case of a single session—if is well-typed w. r. t.  then is a SGP-process—is a special case of the following theorem.

Theorem 2

If the process is well-typed w. r. t.  then is defined and returns a SGP-process.

Given a well-typed process, the computation of the mapping and the size of the constructed SGP-process are usually linear in the size of combined with the sum of the sizes of its types. As discussed in [26], an exponential blow-up cannot be completely avoided but results only from not optimal conditionals, i. e., conditionals that are not only used to branch between alternative labels of an immediately following sender, or from actors that are not influenced by the choice of a branch of a communication in that the sender is preceded by such a conditional. By design, the algorithm in Definition 2 will even in these bad cases minimize the size of the generated SGP-process by delaying the mapping of conditionals as long as possible. In general the computation of the SGP-system is efficient, i. e., usually fast, and the construction does not suffer from the problem of state space explosion, i. e., the generated SGP-system is usually not considerably larger than the original system. Since the construction sequentialises the original system and thereby removes all forms of interaction and restriction, the verification of the SGP-abstraction is much easier than the verification of the original system.

It remains to show, that the SGP-abstraction of a well-typed system that is generated by and the original system are semantically similar enough, such that the analysis of the SGP-abstraction allows to verify properties of the original system. Intuitively, a well-typed system and its sequentionalisation into a SGP-system have the same steps, but SGP-systems may force an order on steps that are unordered in the original system. This happens for global types such as that combine causally unrelated communications sequentially.

Example 1

Consider the global type that consists of two causally independent communications. The system

is a well-typed implementation of this global type. The algorithm of Definition 2 maps this process to the SGP-system , where . The process has, modulo structural congruence, two maximal runs

figure dl

where . But the abstraction simulates only the sequence of steps at the top

in that first process receives the value 5—and the SGP-process accordingly updates the variable of —and then receives the value 4.

Except for such sequentialisations from the global type, the original system and its SGP-system are similar. In particular, this means that each step of the SGP-system can be simulated by the original system. Thus, SGP-systems do not introduce new behaviour.

Theorem 3 (Soundness)

If is well-typed w. r. t. \( \mathcal {G} \) then for all such that there exist some such that , is well-typed w. r. t. \( \mathcal {G}' \), and .

Although the SGP-system can perform intuitively the same steps as the original system, the order that is forced on some steps by the above discussed sequentialisations prevents us from obtaining the same result in the other direction. However, only the order of steps can differ. Because of that, whenever the original system does a step there is a sequence of steps bringing the original system towards a state that can be reached by the SGP-system. To prove this result, we rely on the observation that the behaviour of a SGP-process follows the global type it was constructed from and well-typedness forces processes to similarly follow the specification in their types. Since renamings of input binders change the vector of variables of a SGP-system, we assume that no alpha conversion is used to rename input binders in the following.

Theorem 4 (Completeness)

Let . If the system is well-typed w. r. t. \( \mathcal {G} \) then for all there exist such that , is well-typed w. r. t. \( \mathcal {G}'' \), and .

Interestingly, the combination of Theorem 3 and Theorem 4 is similar to (weak) operational correspondence as it is introduced in [14] as criterion for the quality of encodings. Using the results from [25], then the sequentialisation of a system is correspondence similar to the original system, where correspondence simulation \( \precsim \) was introduced in [25].

Corollary 1

If is well-typed w. r. t.  then .

Correspondence similarity is strictly weaker than bisimilarity, but it implies coupled similarity. Coupled similarity was introduced in [23] as a weaker variant of bisimilarity that allows to relate the distributed implementation to a global specification. Similarly, we relate the sequentialisation to the distributed implementation in . As explained in [23], bisimilarity is in general too strict to relate a distributed implementation with a global specification. So, following the hierarchy in [12, 13], coupled similarity (or the only slightly stronger correspondence simulation) is intuitively the strictest simulation relation that we could expect here.

5 Using SGP-Abstractions for Verification

To verify properties that are based on data values, we can use standard verification techniques such as model checking on the generated SGP-systems. The correspondence simulation between the SGP-system and the original system ensures that properties that are valid for the SGP-system are also valid for , if these properties are preserved modulo \( \precsim \). For the presented approach, this is the case for all properties on the values of data variables—that reflect the reception of values in the original system—that do not require to compare different such variables that are updated concurrently in the original system as explained in Example 1.

Accordingly, we cannot use this method to verify properties on the relation between variables that are updated concurrently in the original system. This is because, we use the structure of the global type to sequentialise. If—as in the case of in Example 1—the global type combines independent communications sequentially, then the mapping forces an order on the corresponding value updates following the global types \( \mathcal {G} \) and not the process .

However, this problem occurs only w. r. t. communications that are causally unrelated, i. e., such properties are in general problematic in distributed systems. Since these values are altered independently in the original system, properties that relate their values will often not hold in all runs. The easiest way to avoid such false positives, is to compute the causal relation of the communications in \( \mathcal {G} \). Remember that global types do not contain binders. Thus, computing the causality relation for a single session can be done in a similar way as in the \(\pi \)-calculus (compare e. g. to [27]), but does not have to bother about binders and scope extrusion. To obtain a causality relation for the case of globally interleaved sessions, we combine the relation that captures dependencies between the interactions of different sessions of [3] with the causality within a session. A property of the SGP-system then holds for the original system if it is invariant under different linearisations of this causal order.

To illustrate the verification of system properties, we use the model checker Spin [16, 17] and translate SGP-systems into Promela, the input language of Spin. Therefore, we provide an algorithm to translate a SGP-process into Promela code. This algorithm serves as a role model to obtain similar mappings for other model checkers. We choose SPIN to illustrate how our algorithm for well-typed systems compares to the standard partial order reduction techniques that are implemented in SPIN and that work without the type information. Other implementations might prefer a model checker that is specialised on the analyses of data instead of concurrency issues such as nuXmv [8].

First we generate a preamble for the Promela program, i. e., declare variables and set their initial values. The variables are obtained from the vector of variables \( \mathcal {V} \) in a SGP-system . Sometimes the initial values are directly specified by the implementation or are given as parameters of the implementation. Otherwise, the developer has to pick suitable initial values respecting their respective sorts.

The translation into Promela consists of two layers. The outer layer creates the proctype that is required by Promela and passes the term onto the inner layer . The inner layer is simple: Variable assignments are translated to variable assignments encapsulated in an atomic block if multiple assignments are done simultaneously. Recursion is implemented by introducing a label and jumping to that label when the recursion variable is called.

Definition 4

(Translation of SGP-Processes into Promela )

where for each a separate proctype is introduced with .

Note that, if \(\tilde{v}\) and \(\tilde{e}\) are singletons in , the atomic block is omitted.

In [26] we present a toy example to illustrate our approach. It implements a simple auctioneer system consisting of an auctioneer and two bidders. After translating this example into a SGP-system and then into Promela, some properties given as LTL-formulae are verified in SPIN.

Moreover, to visualise the state-space explosion problem, we implemented the key-exchange part of the Needham-Schroeder protocol. We derived the sequentialised (s) version out of the distributed (d) version using our algorithm. The following table shows time and memory needed to check our Promela implementation of the Needham-Schroeder protocol. Spin crashed before it could compute the distributed versions for more than 6 participants.

participants

2(d)

2(s)

4(d)

4(s)

6(d)

6(s)

8(d)

8(s)

10(d)

10(s)

seconds

0.01

0

0.19

0

51.7

0.05

–

1.27

–

36.2

MB

128

128

137

129

1836

138

–

360

–

5809

6 Conclusions

We introduce a mapping from well-typed systems—that are distributed concurrent systems that interact by communication—into SGP-systems—that simulate the information flow of the original system from a global point of view and that do not have interactions. The algorithm to compute these SGP-systems is usually linear in the size of the original system. Without interactions and only finite vectors of variables, the verification of properties is significantly more efficient for SGP-systems than for the original system. The presented mapping ensures that properties that hold for the SGP-system are also valid for the original system modulo coupled similarity. Finally, we present a second mapping from SGP-systems into Promela; the input language of the Spin model checker.

To formalise the relation between the original system and its sequentialisation into a SGP-system, we relate them by correspondence simulation. Correspondence simulation was described in [25] to describe the relation that the criterion operational correspondence forces on processes and their encodings. As discussed in [14, 15], operational correspondence is essential to reason about the quality of encodings between process calculi. In this sense, the presented mapping is a good encoding. Moreover, correspondence similarity implies coupled similarity. As discussed in [23], coupled similarity is a good way to relate central specifications—or in our case global sequentialisations—to their distributed implementations. Since bisimilarity is in general too strict to relate the original system and its sequentialisation, coupled similarity (or the only slightly stronger correspondence simulation) is intuitively the strictest simulation relation that we could expect here.

Multiparty session types are already a very efficient verification tool for all properties about the communication structure of systems. The presented sequentialisation allows us to benefit from their efficiency also in the verification of properties that are usually not in the range of type systems, because they require the consideration of concrete runs of the system or the values of variables.

Due to the interleaving of independent actions, the state space of a concurrent system is in the worst case exponentially larger than of its sequentialisation. As an example, we implemented the Needham-Schroeder public key protocol with 10 pairs of processes that interact with the same server (see [26]). Spin generated for the original system more than 35 million states (matching more than 154 million states while using more than 7,5GB memory) before crashing after 969 seconds. For the sequentialisation Spin computed the complete model in only 62 seconds generating 75 million states.

The Scribble project [18, 31] provides a tool set that allows to specify and check multiparty session types. They also provide a tool to check a given implementation against a given type. The presented algorithms could support such tool sets by increasing the kinds of properties that can be analysed within such a tool set, while the efficiency of such tools is not negatively influenced. In fact, the derivation of SGP-abstractions can be directly integrated into the type check such that SGP-abstracts are produced as a by-product of type checking.