Guido Salvaneschi

Joscha Drechsler

Mira Mezini

Towards Distributed Reactive Programming

Keywords: Functional-reactive Programming, Scala, Event-driven Programming

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Reactive applications respond to user input, packets from the network, new values form sensors and other external or internal events. Traditionally, reactive applications are implemented by using the Observer design pattern. The disadvantages of this style, however, have been studied for a long time now [START_REF] Cooper | Embedding dynamic dataflow in a call-by-value language[END_REF][START_REF] Meyerovich | Flapjax: a programming language for ajax applications[END_REF][START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF]. The major points of criticism include verbosity, lack of static reasoning, and inversion of the logic flow of the application.

A first solution proposed by researchers is to provide language-level support for the Observer pattern. For example, in C# classes can expose events to clients beside fields and methods. Other languages that provide advanced event systems include Ptolemy [START_REF] Rajan | Ptolemy: A language with quantified, typed events[END_REF] -which supports event quantification -and EScala [START_REF] Gasiunas | EScala: modular event-driven object interactions in Scala[END_REF] -which supports event combination and implicit events.

A different approach is adopted by reactive languages that directly represent timechanging values and remove inversion of control. Among the others, we mention Fr-Time [START_REF] Cooper | Embedding dynamic dataflow in a call-by-value language[END_REF] (Scheme), FlapJax [START_REF] Meyerovich | Flapjax: a programming language for ajax applications[END_REF] (Javascript), AmbientTalk/R [START_REF] Lombide Carreton | Loosely-coupled distributed reactive programming in mobile ad hoc networks[END_REF] (Smalltalk) and Scala.React [START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF] (Scala). This idea originates from functional reactive programming, which explored the semantics of time-changing values in the setting of (strict) functional languages. Another source of inspiration for reactive languages can be found in illustrious ancestors like the Esterel [START_REF] Berry | The Esterel synchronous programming language: design, semantics, implementation[END_REF] and Signal [START_REF] Gautier | SIGNAL: A declarative language for synchronous programming of real-time systems[END_REF] dataflow languages that focus on realtime constraints. Reactive languages are a promising solution and active research is ongoing in this field.

Reactive languages require careful design to avoid inconsistencies -referred to as glitches [START_REF] Meyerovich | Flapjax: a programming language for ajax applications[END_REF] -that can arise in the update process of time-changing values. All reactive languages proposed so far do not provide these guarantees in the distributed setting. However, applications rarely span over a single host. Rather, most applications are distributed -the client-server architecture being the simplest case.

In summary, distributed reactive programming is an open challenge. Existing reactive languages take into account distribution in the sense that they are capable of transmitting events or propagating function calls among remote hosts that independently run a reactive system. In this way, however, consistency properties, locally enforced by a reactive programming system, are not guaranteed over reactive data flows that cross hosts [START_REF] Bainomugisha | A survey on reactive programming[END_REF]. We show that this limitation can lead to serious errors in the behavior of applications. Despite reactive programming having huge potential as a means to coordinate complex computing systems in a simple way, it struggles to succeed in this context. We argue that the aforementioned limitation is one reason for this.

The contributions of this paper are the following:

-We analyze the drawbacks of the existing approaches and motivate the need for reactive languages that uphold their guarantees in distributed applications. -We propose a research roadmap for distributed reactive programming, including a first solution that demonstrates the feasibility of this goal and can be used for further design refinement and optimization.

Our vision is that distributed reactive programming can be a new way of structuring distributed systems. It centers around the concept of Remote Reactives, remote entities characterized by time-changing values, which clients can compose to model reactive computations and effects that span across multiple hosts.

Motivation

In this section, we introduce the basic concepts of reactive programming, show its advantages over traditional techniques, and describe the challenges of achieving the same result in a distributed setting.

Reactive Programming in a Nutshell Reactive languages provide dedicated abstractions to model time-changing values. Time-changing values are usually referred to as behaviors [START_REF] Cooper | Embedding dynamic dataflow in a call-by-value language[END_REF] or signals [START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF]. For example, in Figure 1 we show a code snippet in Scala.React [START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF] that highlights the mouse cursor when it hits the borders of a window. In Scala.React, signals are time-changing values that are updated automatically; vars are time-changing values that are directly modified. In the example, the position signal models the time-changing value of the mouse position (Line 1). In Line 2, the showCursorChoice var is declared, which is changed by the user settings (not shown) to enable or disable the highlighting feature. In the rest of the paper, we generically refer to vars and signals as reactives. Developers can build expressions upon reactives. In Line 3 we create the isMouseOnBorders signal. It depends on the position signal and evaluates to true if the current position overlaps the window border. The key point is that reactive values that depend on other reactive values are automatically updated when any of their dependencies change. For example, when the position of the mouse changes, any expression associated with the position signal is reevaluated. In our example, the value of isMouseOnBorders is recalculated. This in turn causes the expression defined at Line 4, which combines both the isMouseOnBorders signal and the showCursorChoice var, to be reevaluated. Finally, every time this value changes, it is used to update the highlighting state through the observe statement in Line 5.

A detailed comparison of reactive programming with the Observer pattern is out of the scope of this paper. The advantages of this style over the Observer pattern have been extensively discussed in literature. The interested readers can refer for example to [START_REF] Cooper | Embedding dynamic dataflow in a call-by-value language[END_REF][START_REF] Meyerovich | Flapjax: a programming language for ajax applications[END_REF][START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF]. The main points are summarized hereafter. Callbacks typically have no return type and change the state of the application via side effects. Instead, reactives enforce a more functional style and return a value. As a result, types can guide developers and prevent errors. More importantly, differently from callbacks, reactives are composable, enhancing maintainability and software reuse. Finally, callbacks invert the logic of the application. Instead, reactives express dependencies in a direct way, improving readability and reducing the boilerplate code for callback registration.

Challenges of the Distributed Setting As we have shown, reactive programming is an appealing solution to implement reactive applications. As such, it is desirable to move the advantages of reactive programming to a distributed setting, in the same way as, historically, functions were generalized to remote procedure calls and local events inspired publish-subscribe distributed middleware.

To discuss the challenges of this scenario, we present SimpleEmail, a minimal email application. In SimpleEmail, the server keeps the list of the emails received for an account. The client can request the emails that were received within the last n days and contain a given word and display them on the screen. The client highlights the desired word in the text of each email. Since an email text can span over multiple screen pages, it can be the case that there is no highlighted word on the current page, even if the server returned that email. To make this case less confusing for the user, the client displays a warning message. A proof-of-concept implementation is presented in Figure 2. We assume that reactive values can be shared with other hosts by publishing them on a registry, similarly to Java RMI remote objects. These objects are referred to as Remote Reactives (RRs). Clients can obtain a reference to RRs from the registry. For simplicity, we do not distinguish between remote vars and remote signals and we assume that a RR can be changed only by the client that publishes it.

The client (Figure 2a) publishes a RR that holds the word to look for (Line 2a) and another one with the number of days n (Line 4a). These reactives are automatically updated when the user inserts a new word or a new number in the GUI. The server (Fig- ure 2b) retrieves the word and the days (Lines 5b and 7b) and uses these values to filter the stored emails (Lines 9b-14b). It publishes the RR that holds the result (Line 16b), which is in turn looked up by the client (Line 7a) and displayed in the GUI (Line 9a). The client additionally combines the filtered list of emails with the searched word to determine whether the word is visible on the first page (signal hInFirstPage, Line 12a). This value is then used to decide, whether or not to display the alert (Line 16a) informing the user that the search term is only visible on a different page.

Figure 3 models the dependencies among the reactive values in the SimpleEmail application (the c -respectively s -subscript refers to the client -respectively server -copy of a RR). Suppose, the user now inputs a different word. In the program, this would update the days c reactive. This change would be propagated to the server's instance days s of the reactive, where it causes the reevaluation of the filteredEmails s reactive. The new list of emails is then filtered with the current word s search term and the result is propagated back to the client to updates the display. Now suppose that, instead of days c , word c is updated. This change is likely to propagate to hInFirstPage c first, because the propagation of the value to word s requires network communication. As a result, hInFirstPage c is evaluated with the new word, but the old list of emails. This can result in the word not being found on the current page and, in consequence, the warning message being displayed. Only later, when the change propagated through word s , filteredEmails s and back to filteredEmails c , hInFirstPage c reevaluates to false and the warning is switched back off.

In summary, spurious executions can be generated, depending on the evaluation order of the values in the graph. In our example, this issue only led to the erroneous display of a warning message. However, it is easy to see that in a real system that involves physical actuators, temporary spurious values can have more serious consequences. For example, in a train control system, a rail crossing could be temporarily opened, letting cars cross the railway while a train is approaching.

Temporary inconsistencies due to the propagation order are a known problem in reactive languages, commonly referred to as glitches [START_REF] Cooper | Embedding dynamic dataflow in a call-by-value language[END_REF]. Current reactive languages achieve glitch freedom by keeping the dependency graph of the reactive values topologically sorted; reevaluations are triggered in the correct order, avoiding spurious values. More details on this technique can be found in [START_REF] Meyerovich | Flapjax: a programming language for ajax applications[END_REF][START_REF] Maier | Deprecating the Observer Pattern with Scala[END_REF]. Current reactive languages, however, enforce glitch freedom only locally, but give no guarantees when the communication spans over several hosts as in the presented example. The fundamental point is, that true distributed reactive programming cannot be achieved by naively connecting the dots among single (individually glitch-free) reactive applications. On the contrary, dedicated logic must ensure glitch freedom as a global property of the entire system. Re-using topological sorting in the distributed setting would however force a singlethreaded, centralized execution of updates across the entire application -an approach that we consider unacceptable. Next to finding and implementing a suitable remoting mechanism for reactives, developing an acceptable solution for ensuring glitch freedom in a distributed reactive application is the main challenge in supporting distributed reactive programming.

A Research Roadmap

In this section, we design an initial solution for distributed reactive programming, describe our plans to improve upon it, and present possible application domains.

Distributed Reactive Programming We formulate our solution as a distributed transaction [START_REF] Weikum | Transactional information systems: theory, algorithms, and the practice of concurrency control and recovery[END_REF], for which well-known algorithms are available (e.g. distributed 2PL). Since persistency is not necessarily required, an implementation can leverage distributed software transactional memories [START_REF] Shavit | Software transactional memory[END_REF], which have been proved to efficiently scale up to large-scale clusters [START_REF] Bocchino | Software transactional memory for large scale clusters[END_REF]. A promising alternative for the implementation of our system is the automatic code generation from a specification. The advantage of such an approach is that an efficient and correct-by-construction distributed implementation is automatically derived from a formal model [START_REF] Georgiou | Automated implementation of complex distributed algorithms specified in the ioa language[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. A more detailed comparison with automatic generation of distributed applications can be found in Section 4.

The following operations are a sufficient, minimal set of primitive operations to drive a distributed reactive system and must be executed transactionally. Without loss of generality, we only consider the case in which all the nodes in the distributed graph are remote. Possible optimizations can take advantage of the fact that local reactives are not visible by other participants. A participant updates a RR value. The participant starts a distributed transaction. The change is propagated across the distributed graph, each participant updating the RRs inside the same transaction. In case of a conflict between two transactions executing at the same time, one transaction rolls back, restoring the previous values of all affected reactives, and retries its execution. For this reason, the system requires separation of purely functional update propagation among reactives and side effects in the same style as Scala.React. The execution of the code preforming side-effects is deferred to after the transaction has successfully committed, thereby ensuring glitch freedom even in case a transaction has to be rolled back. Topological sorting of the dependency graph could still be used inside the update transaction to prevent multiple recalculations of the same functional parts. Doing so would, however, imply forcing all hosts' local update threads that are involved in the transaction to emulate a single-threaded execution. Ignoring the topological order would exploit parallel processing capabilities of multiple hosts and could even be used locally on multicore systems, but at the cost of multiple reevaluations. An ideal solution would be designing a new algorithm, which incorporates both concurrent updates of independent reactives (those that are incomparable in the topological order) and prevention of multiple recalculations of affected reactives. It is our goal to provide this hybrid solution.

The case of a participant establishing a new dependency, either independently or as the result of a reevaluation, can be considered a subcase of updating a reactive. Instead of updating the reactive's value, the participant updates the set of dependencies of the reactive. It is even possible, to update both at once. This must be done transactionally as well, to avoid interference with other changes. In addition, all graph modifications must be checked to prevent the introduction of dependency cycles. A participant reads a RR value. Reading must also be transactional, to avoid inconsistent state between subsequent reads of different reactive values -some of which could have been updated by a change propagation in the meantime. This can easily be achieved by executing all the reads inside a transaction.

The solution sketched above allows a certain degree of parallelism between transactions that do not interfere. In this sense, it is already an improvement over transferring the algorithms available in literature to a distributed setting by adopting a naive, centralized execution, regardless of how much independencies in the topological ordering are exploited. Our research plan is to use this solution as the first step to improve upon. For example, as sketched above, it requires finding a performant way to check the dependency graph for cycles. Based on the assumption that dependency changes are less frequent than value updates, using a centralized master that keeps a representation of the entire dependency graph would be a simple way to enable performant execution of this validation while still providing an improvement over executing all updates from a centralized coordinator. Still, this would imply a single point of failure and prevent concurrent changes to the dependency graph. Our plan includes exploring better design options that allow more decentralized approaches. Also, we expect to identify various trade-offs between provided guarantees and processing speed, some of which are described in the following paragraphs.

As long term goals, we envisage three application scenarios: Web applications, enterprise systems, and computing systems in an open environment. The remainder of this section elaborates our visions for each of these.

Web Applications

The solution presented so far provides a general model that is valid on distributed systems with an arbitrary number of hosts. This model directly applies when several browsers share resources among each other through a server 1 . However, we expect that in typical web applications only a client and a server share the RRs. While the aforementioned model proves the feasibility of our research vision, we expect that in a client-server model it can be significantly simplified, reducing the number of messages sent over network and gaining in performance. For example, Javascript applications enforce a single thread model, which solves the problem of synchronizing between concurrent changes for free.

Enterprise Distributed Systems We envisage a scenario in which distributed reactive programming can be used to implement large-scale enterprise systems. In those environments, the consistency constraints required by distributed reactive programming should be provided by a dedicated middleware in the same way e.g. the JMS middleware provides guaranteed delivery and once-and-only-once semantics.

This research direction must take into account that enterprise software often does not run in isolation, but operates inside containers, like Tomcat or JBoss. For example, containers can provide persistence for Enterprise Java Beans (EJB). In a similar way, RRs can be modeled by EJBs, whose consistency is supported by the container Highly Dynamic and Unreliable Environments Distributed systems pose a number of challenges that include slowdown of network communication, node failures, communication errors and network partitioning. Those issues have been studied for a long time by the distributed systems community. An open challenge is to define proper behavior of a reactive system in such conditions. Proper language abstractions should support dealing with those cases with clear semantics. For example, in case of network partitioning, the system should be able to restructure the distributed graph with only the available hosts, but this clearly has an impact on the semantics of the application.

Another aspect we plan to explore is to relax the constraints as a possible reaction to network performance degradation. Reactive programming has been successfully used in the field of ambient-oriented programming [START_REF] Lombide Carreton | Loosely-coupled distributed reactive programming in mobile ad hoc networks[END_REF], where systems are dynamic and unreliable and links can become slow. We envisage a scenario in which glitch-freedom guarantees can occasionally be switched off, in case maintaining them becomes too onerous. Similarly to before, proper abstractions should be introduced to deal with this case.

Evaluation A primary contribution of our research is to provide a new conceptual tool to support the design and the implementation of distributed software. The achievement of such a goal is hard to measure numerically, so we mostly expect feedback from the scientific community. More concretely, we plan to empirically evaluate our findings along two dimensions: On the one hand, we want to evaluate the impact of our solution on the design of a distributed system. Since these phenomena have already been observed in the local setting, we expect that static metrics can significantly improve, including reduced lines of code, reduction of the number of callbacks, and increased code reuse. On the other hand, we plan to evaluate the performances of our solution. Our goal here is not to make it competitive with models that require less stringent consistency guarantees, like publish-subscribe systems or complex event processing engines, but to provide a solution with significant design advantages at a minimum performance penalty.

Related Work

Due to space limitations, related work cannot be discussed extensively. Several languages implement concepts from reactive programming in various flavors. The interested reader can refer to [START_REF] Bainomugisha | A survey on reactive programming[END_REF] for an overview. None of them provides glitch-freedom in the distributed setting. Among the existing reactive languages, AmbientTalk/R [START_REF] Lombide Carreton | Loosely-coupled distributed reactive programming in mobile ad hoc networks[END_REF] is the closest to our approach, and, to the best of our knowledge, it is the only one that has been specifically designed to support distribution in a form similar to remote reactives. In the remainder of this section, we point to the main research areas related to reactive programming and summarize their relation with the subjects discussed in this paper.

Dataflow languages, like Esterel [START_REF] Berry | The Esterel synchronous programming language: design, semantics, implementation[END_REF] and Signal [START_REF] Gautier | SIGNAL: A declarative language for synchronous programming of real-time systems[END_REF] focus on provable time and memory bounds. Differently form reactive languages and functional reactive programming, reactive abstractions are typically second-order, to support compilation to efficient finite state machines.

Self-adjusting computation [START_REF] Acar | Imperative self-adjusting computation[END_REF] automatically derives an incremental version of an algorithm. It mostly focuses on efficiency and algorithmic complexity of the incremental solution, while reactive programming focuses on language abstractions for timechanging values.

The Implementation of distributed algorithms has been explored in form of code generation from formal specifications of I/O automatons [START_REF] Georgiou | Automated implementation of complex distributed algorithms specified in the ioa language[END_REF]. A similar approach [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] generates the distributed programs from a description based on BIP (Behavior, Interaction and Priority) models [START_REF] Basu | Modeling heterogeneous real-time components in bip[END_REF]. We believe that the core of a middleware for distributed reactive programming can be conveniently specified in such a model and automatically generated. Consistency properties like glitch freedom would be provided through the synchronized state transitions offered by petri nets. However, we expect that the application code that builds on top of such a middleware (i.e. on remote reactives) is still written in a "traditional" language. As such, we believe it to be beneficial to allow programmers the implementation of all parts of their application seamlessly in their regular language in the style of reactive programming. Publish-subscribe systems [START_REF] Eugster | The many faces of publish/subscribe[END_REF] leverage inversion of control to loosely couple interacting systems. Differently from publish-subscribe systems, we want to enforce a more tight coupling in the change propagation, to transfer the advantages of the local reactive semantics into the distributed setting.

Complex event processing (CEP) [START_REF] Margara | Processing flows of information: from data stream to complex event processing[END_REF] is about performing queries over streams of data. Similarly to reactive languages, changes in the data result in an update to dependent values -in CEP, query results. Differently from reactive programming, CEP expresses dependencies via SQL-like queries that are usually expressed as strings and not integrated into the language.

Figure 1 .

 1 Figure 1. An example of reactive programming.

2 Database.emails 3 4 7 lookupRR{"days"} 8 9Figure 2 .

 23782 Figure 2. The SimpleEmail application. Client-side (a) and server-side (b).

Figure 3 .

 3 Figure 3. Dependency graph among reactive values in the SimpleEmail application. Dashed arrows indicate over-network dependencies, square nodes indicate observers with side effects.

For example, the AtomizeJS distributed software transactional memory supports this functionality, http://atomizejs.github.com/.

5 Acknowledgments This work has been supported by the German Federal Ministry of Education and Research (Bundesministerium für Bildung und Forschung, BMBF) under grant No. 16BY1206E and by the European Research Council, grant No. 321217.


Hugo Torres

Vasco Thudichum Vasconcelos

Typing Progress in Communication-Centred Systems

We present a type system for the analysis of progress in session-based communication centred systems. Our development is carried out in a minimal setting considering classic (binary) sessions, but building on and generalising previous work on progress analysis in the context of conversation types. Our contributions aim at underpinning forthcoming works on progress for session-typed systems, so as to support richer verification procedures based on a more foundational approach. Although this work does not target expressiveness, our approach already addresses challenging scenarios which are unaccounted for elsewhere in the literature, in particular systems that interleave communications on received session channels.

Introduction

In today's ever-growing cloud infrastructure of computation, communication is more and more of crucial importance. Communication is still of crucial importance even when considering multi-core machines, where processes may interact via shared memory, since such machines will inevitably have to communicate among them. It is then of vital importance to introduce mechanisms that support the development of correct communicating programs, given their wide dissemination, ranging from critical services, such as medical or financial, to those helping people connect with family and friends. Focusing on communication, there are at least two fundamental correctness properties one may be interested in: that interacting parties follow a given communication protocol (fidelity) and that the interaction does not reach a deadlock (progress).

Verification procedures, such as type systems, that statically ensure communicating programs enjoy the properties above can prove to be cost-effective, as they save on software maintenance by preventing bugs from the start, and can help to expedite the software development process. Several type systems have been proposed that single out programs with correct communication behaviour, out of which we distinguish session types, introduced by Honda et al. [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF]. Session types focus on ensuring fidelity in systems where (single-threaded) protocols are carried out between two parties, such as, e.g., a client and a server. Session types are by now widely adopted as the basis of pragmatic typing disciplines, targeting operating system design [START_REF] Fähndrich | Language support for fast and reliable message-based communication in singularity OS[END_REF], middleware communication protocols [START_REF] Vallecillo | Typing the behavior of software components using session types[END_REF] and distributed object-oriented programming [START_REF] Gay | Modular session types for distributed object-oriented programming[END_REF], just to mention a few. Session types have also been generalised so as to consider multiparty interactions [START_REF] Caires | Conversation types[END_REF][START_REF] Honda | Multiparty asynchronous session types[END_REF].

Building on session types, a number of works were proposed that ensure progress (e.g., [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Caires | Conversation types[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF]). This has proven to be a challenging task, in particular regarding the expressiveness of the approaches, even when considering sophisticated typing mechanisms. In this paper we present a typing discipline that distils the basic ingredients necessary to prove progress, building on (classic) session types. This work is not to be viewed as an exercise on expressiveness, capturing every conceivable communication pattern: it fails to do so, even if we are able to address challenging system configurations. Instead, our (far more ambitious) goal is to introduce a foundational approach that will hopefully underpin the development of forthcoming works on progress for communication centred-programming based on session types.

At the basis of our development is the idea that a communication-centred program that enjoys progress is embodied with a natural ordering of communications (or events). Building on this idea, and trying to use as few ingredients as possible, we unify the notions of event and session type so as to characterise the sessions and the ordering of events in a combined and novel way. To achieve this we add to each communication in a session type an annotation that allows to identify the (abstract) communication event that is associated to the (concrete) communication action described by the session type. Then, together with a separate notion of overall ordering of events we are able to distinguish systems that enjoy fidelity and progress.

Remarkably we are able to address challenging configurations (unaccounted for elsewhere in the literature) where processes interleave communications in received session channels, for instance to communicate on other sessions or to initiate new ones. As an example, think of a (service) broker that must interleave communications with a client and a server (not to mention other local or remote resources), using (two binary) session channels that where shared (communicated) among the three parties. Our approach generalises previous work on progress in the context of conversation types [START_REF] Caires | Conversation types[END_REF], a session-based type system that addresses multiparty interaction. Also, differently from other session-types based approaches, our type system works directly on the (standard) π-calculus [START_REF] Milner | A calculus of mobile processes, part I and II[END_REF], exploiting notions from [START_REF] Caires | Conversation types[END_REF] and from a previous work on session types [START_REF] Vasconcelos | Fundamentals of session types[END_REF].

Motivating examples. We illustrate our development by visiting a couple of simple examples. Consider the system shown in Fig. 1 that specifies a basic interaction. The Client process creates a new name chat and sends it on channel service which is read by Server. The synchronisation on service allows the client and the server to share a private channel (chat) where the session will take place. After synchronizing on service, the client proceeds by receiving from channel chat a text message, after which, it sends another text message again on channel chat. The Server process is (continuously ) waiting to receive in service a channel, which instantiates message parameter y. Upon reception, it will then send a text message on that channel, after which, to avoid waiting for the reply, it delegates the rest of the session interaction on y by sending y on channel handle. The Slave process is defined so as to (also continuously) receive a channel name from handle, and then receiving a text message in that channel. The System is defined as the parallel composition of the three processes. Notice we described the system using type information (e.g., "text message"), taking fidelity for granted. Also, in the examples we use basic types (such as string) although our technical development focuses exclusively on channel types.

It is straightforward to see that the system enjoys progress, as the interaction supported by chat does not deadlock. However, we may already use this simple example to convey some intuition on our typing approach. Consider for instance process Slave that receives a channel name from handle and then communicates in the received channel. We may characterise this usage of channel handle with type ? ( ? String ), where ? specifies reception, which may be read as "receives a channel used to receive a string", just like in a regular session type.

We distinguish (session) interactions carried out exactly once (linear, no races) and service definitions that support several interactions (shared or unrestricted) by annotating the type of handle accordingly, i.e., un ? ( lin ? String ), which adds to the description that handle can be used zero or more times while the received channel must be used exactly once (linearly).

Up to now we are using standard session type notions to characterise the usage of a channel (see [START_REF] Vasconcelos | Fundamentals of session types[END_REF]). Building on the standards, we add information that allows to characterise (in an abstract way) the moment in time when the communication is to take place: the event. We say that the communication in handle corresponds to some event in time e 1 , while the reception of the string corresponds to event e 2 , and obtain the type e 1 un ? (e 2 lin ? String ). Notice that e 2 necessarily takes place after e 1 (hence, e 1 and e 2 are different events), to represent which we use e 1 ≺ e 2 (read "e 1 happens before e 2 ").

We are then able to characterise processes with both information on the channel usage and on the expected overall ordering of events, in particular Slave is charaterized by the typing assumption handle : e 1 un ? (e 2 lin ? String ) and ordering of events e 1 ≺ e 2 . Notice that we do not refer to z in the type since z is a name bound to the reception (handle?z). However, and crucially to our approach, we do mention the event where z is involved (e 2 ), and register it both in the message type e 2 lin ? String and in the event ordering e 1 ≺ e 2 . This will allow to crosscheck whether the name sent in handle has a corresponding type so as to keep a sound (overall) ordering. Following the same lines we may characterise process Server by the following typing assumptions. handle is to be used unrestrictedly (un). Furthermore, both processes agree on the moment in time when the communication in handle will take place (e 1 ). Lastly, both processes also agree on the message type e 2 lin ? String , hence Server also knows that the channel sent in handle is involved in e 2 .

We also have that service is used as an unrestricted input, associated to event e 3 , with message type e 4 lin ! String .e 2 lin ? String . The message type captures that the name received from service will be used to output a string (event e 4 ) and after (denoted as . like in session types) used to receive a string (event e 2 ). The last part is realized via the delegation of the session channel in handle, where the delegated usage is given by the message type associated to handle.

The ordering of events that Server expects is e 3 ≺ e 4 ≺ e 1 ≺ e 2 , since the process first receives from service (e 3 ), then in the session channel (e 4 ) and then outputs in handle (e 1 ), delegating the reception usage of the session channel (e 2 ) which necessarily takes places after the channel is sent (hence e 1 ≺ e 2 ). Notice that Server interleaves communications in the received channel y and in handle, addressed by our characterisation based on the fact that the ordering of events (intertwined with channel types) mentions the events associated to communicated names.

As for the characterisation of Client we have that it uses service with the dual usage with respect to Server (Server inputs ? while Client outputs !) and expects ordering e 3 ≺ e 4 ≺ e 2 since it first outputs in service (e 3 ), then sequentially inputs (e 4 ) and outputs (e 2 ) in the session channel. Notice that although the session channel (chat) is private to the Client, the expected ordering mentions events where the private name is involved.

Using the usage and ordering information that characterise Server and Slave we may characterise the system Server | Slave. Channel usage is sound since the two usages of shared name handle are dual as mentioned before. The ordering of events is sound since gathering e 1 ≺ e 2 and e 3 ≺ e 4 ≺ e 1 ≺ e 2 does not introduce cycles in the overall order. Likewise for System since adding the characterisation of the Client we have consistent usages (dual in service) and a sound total ordering (obtained by gathering e 3 ≺ e 4 ≺ e 1 ≺ e 2 and e 3 ≺ e 4 ≺ e 2 ). We are then able to show that System enjoys (not only fidelity but also) progress.

We now consider a slight variation of the previous scenario, illustrated in Fig. 2. The Client and Slave processes are exactly the same with respect to Fig. 1. Between them we find a Proxy and a Master, where the Proxy is used as an intermediary between Client and Master. The Proxy process starts a session with the client (via service) and then starts another session with Master (via masterservice), where the latter is used just to delegate the session channel

P, Q ::= 0 (Inaction) | x!y.P (Output) | P | Q (Parallel) | x?y.P (Input) | (νx)P (Restriction)
| x?y.P (Replicated Input) Fig. 3. Syntax of processes associated to the interaction with the client (notice that the client and the proxy only interact in the service synchronisation). The Master starts a session (via masterservice) and receives in it the session channel used to interact with the client. After that the Master process starts interacting with the Client via the received channel (from then on just like the Server in the previous example).

We may also single out the System shown in Fig. 2 using our type system to show it enjoys progress. Notice the Master process interleaves communications in two received names, one in a session "initiation" and the other in a inner session delegation, which presents no further challenge to our type system since both cases are handled uniformly. Such configuration is unaccounted for in the reference works on progress for sessions [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF].

In the rest of the paper we present our technical development, starting by the definition of the process model, followed by the presentation of the type system and associated results. To finish we discuss related and future work.

Process Model

In this section we present the syntax and semantics of the language of processes, a fragment of the π-calculus [START_REF] Milner | A calculus of mobile processes, part I and II[END_REF][START_REF] Sangiorgi | The π-Calculus: A Theory of Mobile Processes[END_REF]. The syntax of processes is given in Fig. 3, considering an infinite set of names Λ (x, y, . . . ∈ Λ). The (so-called) static fragment of the process model is given by the inaction 0 that represents a process with no behaviour, the parallel composition of processes P | Q that represents a process where P and Q are simultaneously (concurrently) active, or the name restriction (νx)P that represents a process that has a "private" name x (x is bound in (νx)P ). The dynamic (active) fragment of the language is given by the communication prefixes: x!y.P represents a process that outputs name y in channel x and then continues as specified by P ; x?y.P represents a process that receives a name from channel x and then proceeds as P (y is bound in x?y.P );

x?y.P represents a replicated input, i.e., a process able to continuously receive a name from channel x and proceed as P .

In order to keep the setting as simple as possible, we decided not to allow specifying alternative behaviour via summation, +. We believe however that our development can be extended to consider summation along non-surprising lines.

The semantics of the language is defined via structural congruence and reduction relations, to define which we introduce some (standard) notions. We denote by fn(P ) the set of free names that occur in P . Also, we denote by P ≡ α Q that P and Q are equal up to a renaming of bound names. By P {x ← y} we present the process obtained by replacing all free occurrences of x in P by y.

P | 0 ≡ P P1 | P2 ≡ P2 | P1 (P1 | P2) | P3 ≡ P1 | (P2 | P3) P ≡α Q =⇒ P ≡ Q (νx)0 ≡ 0 (νx)(νy)P ≡ (νy)(νx)P P1 | (νx)P2 ≡ (νx)(P1 | P2) (x ∈ fn(P )) Fig. 4. Structural congruence x?y.P | x!z.Q → P {y ← z} | Q (R-Com) P → Q (νx)P → (νx)Q (R-New) x?y.P | x!z.Q → x?y.P | P {y ← z} | Q (R-Rep) P → P P | Q → P | Q (R-Par) P ≡ P P → Q Q ≡ Q P → Q (R-Cong) Fig. 5. Reduction relation
Structural congruence is defined as the least congruence over processes that satisfies the rules in Fig. 4. Structural congruence allows to specify equivalent classes of processes and supports the definition of the reduction relation focusing on the interactions of the (basic) representatives of the equivalent classes.

The reduction relation over processes is given by the rules in Fig. 5, capturing how processes "evolve" via communication. Rule (R-Com) captures the interaction between an output and an input, where the output emits a name that is received in the input (notice the communicated name z replaces the bound input parameter in the continuation P ). Rule (R-Rep) follows the same lines with respect to the communication behaviour, the difference is that in the resulting state the input is again ready to further synchronise. Aiming at a simple subject congruence result, we do not consider the (original to the pi calculus) structural congruence rule that introduces parallel copies of the replicated process, defining instead unbounded behaviour via rule (R-Rep). The remaining rules close the relation under language contexts -(R-New) for name restriction and (R-Par) for parallel composition -and under structural equivalence classes.

Type System

In this section we present our type system, starting by introducing strict partial orders, a crucial notion that allows us to single out well-formed communication dependency structures of processes. We then present our type language which unifies the notions of events and of session types descriptions, and our type system where processes are characterised via their usage of channels (as usual) and of their ordering of events. Finally, we present our results, namely typing preservation under reduction (Theorem 1) and progress (Theorem 2).

The idea of ordering events to guarantee progress is not new (cf., [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF][START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Lynch | Fast allocation of nearby resources in a distributed system[END_REF]) and seems in fact an excellent mechanism to single out sound communica- tion dependency structures. In our approach, we introduce event orderings and session types in a combined and uniform way, aiming at minimising the number of ingredients required to prove progress of communicating processes. We thus find the strict partial orders defined next at the root of our development.

Strict partial orders.

A strict (or irreflexive) partial order ≺ over a set E is a binary relation that is asymmetric (hence irreflexive) and transitive. We call E the set of events, and we let e, e 1 , e 2 , . . . range over E. Furthermore we distinguish two events, and call them end and , that form the "leaves" of the communication dependency tree (since strict partial orders do not admit reflexive pairs, we require two elements to form the "leaf" pair of the relation).

We make use of the following notions on partial orders. The support of a partial order ≺ is the set of elements of E that occur in ≺, defined as follows.

supp(≺)

{e | ∃e 1 .(e 1 , e) ∈≺ ∨ (e, e 1 ) ∈≺}

The support is used in our typing rules so as to allow us to pick "fresh" events, i.e., events that are not referred to by the relation. The relation obtained by adding the least event e to ≺ is denoted by e + ≺. Notice that if e is not in the support of ≺ and ≺ is a strict partial order, then so is e + ≺. The strict partial order ≺ relation obtained by the union of two strict partial orders ≺ 1 and ≺ 2 is denoted by

≺ 1 • ∪ ≺ 2 .
Notice that • ∪ is a partial operation (undefined when the plain union of the relations introduces cycles). We use • ∪ to gather the communication dependency structures of, e.g., two parallel processes.

Types. Having defined the notion of strict partial orders of events we proceed to the presentation of the type language whose syntax is given in Fig. 6. Our types extend session types [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF] with event annotations, and also exploit notions introduced in previous work on session types [START_REF] Vasconcelos | Fundamentals of session types[END_REF] and conversation types [START_REF] Caires | Conversation types[END_REF].

We use polarities, p, to capture communication capabilities: ! captures the output capability, ? captures the input capability and τ captures a synchronisation pair (cf., [START_REF] Caires | Conversation types[END_REF]). Types are divided in two main classes, shared and linear. The former captures the exponential usage of channels, i.e., channels where (communication) races are admissible (intuitively, think of services that may be simultaneously provided and requested by several sites). The latter captures linear usage of channels, where no races are allowed (in the service analogy, the singlethreaded protocol between server and client in a service instance). A shared type e un p T specifies a polarity p that captures a communication capability, an event e so as to create the association between the communication action and the abstract notion of event, and an argument type T that prescribes the delegated behaviour of the communicated channel. The description of a linear type e lin p T.L follows the same lines, except for the continuation L which specifies the behaviour that takes place after the action captured by e lin p T . Linear types are terminated in end, meaning no further interaction is allowed on the channel.

Notice that our types build on the notion of abstract events, differently from other related approaches (cf., [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Caires | Conversation types[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF]) that resort to channel names (and communication labels) to order communication actions. Notice also our types structurally resemble "classic" session types, differing in the introduction of the event identifier, crucial to our approach, the polarity annotation that allows us to avoid polarised channels, and the linear/unrestricted annotation that allows us to avoid separate typing contexts for shared and linear channels and separate typing rules for linear/unrestricted argument type of communications.

We next define some auxiliary notions over types used in our typing rules. The set of elements of E that occur in a type T is denoted by events(T ). Notice that events in messages (argument types) are not included.

events(T )

   e ∪ events(L) if T = e lin p T 1 .L {end} if T = end {e} if T = e un p T 1
The binary relation over E present in a type T is denoted by T ↓. If each linear prefix in T has a distinct event e then it is immediate that T ↓ is a strict partial order. We use T ↓ to single out the order of events prescribed by a type, which essentially is a (single) chain of events in the case that T is a linear type.

T ↓    e + (L ↓) if T = e lin p T 1 .L {(end, )} if T = end {(e, )} if T = e un p T 1
We introduce a predicate that is true for types that do not specify pending communication actions.

matched (T )    matched (L) if T = e lin τ T 1 .L true if T = end or T = e un ? T 1 false otherwise
Matched linear communication actions are captured by τ annotated types. As for shared communication actions, we focus only on unmatched output actions and thus only shared inputs are matched. We will clarify this notion in the definition of splitting (Fig. 8) and in the characterisation of active processes in the context of our main result (Theorem 2), for now it suffices to say that matched shared communications are ?-annotated.

Typing contexts. The syntax of typing contexts is given in Fig. 6. We assume by convention that, in a typing context Γ, x : T , name x does not occur in Γ . Also, we use Γ end to abbreviate a typing context •, x 1 : end, . . . , x k : end for some k ≥ 0 and x 1 , . . . , x k . We introduce some auxiliary predicates over typing contexts to single out typing contexts that refer only to unrestricted and matched communications.

We denote by Γ un contexts that include only shared communications, defined as Γ un ::= • | Γ un , x: end | Γ un , x: e un ! T . Such contexts are used to qualify the exponential resources that a replicated input may use. Since more than one copy of the continuation of a replicated input may be simultaneously active, there must be no linear behaviour present (to avoid communication races). We also exclude shared inputs in Γ un so as to avoid nested replicated inputs. Intuitively, if we admit nested service definitions then, to guarantee progress, we would also require that every service is called at least once (in such way activating all nested service definitions) or characterise progress of open systems by inserting them in the "right" context (cf., [START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF]). We focus on closed systems where all communications are matched, i.e., typed in matched contexts. We lift the matched predicate over types to typing contexts in the expected way: we write matched (•,

x 1 : T 1 , . . . , x k : T k ) if matched (T i ) for all i such that 1 ≤ i ≤ k.
Splitting and conformance. We now introduce two notions crucial to our development, namely splitting (inspired by [START_REF] Baltazar | A type system for flexible role assignment in multiparty communicating systems[END_REF]) that explains how behaviour can be decomposed and safely distributed to distinct parts of a process (e.g., to the branches of a parallel composition), and conformance that captures the desired relation between typing contexts and strict partial orders.

We say a typing context Γ conforms to a strict partial order ≺, denoted by conforms(Γ, ≺), if all event orderings prescribed by the types in Γ are contained in ≺, thus ensuring that the events associated with the communication actions described by the types are part of the overall ordering.

conforms(Γ, ≺)

   true if Γ = • conforms(Γ 1 , ≺) if Γ = Γ 1 ,

x: T and T ↓⊆≺ false otherwise

Splitting is defined for both types and typing contexts, defined via three operations over linear types, shared types and typing contexts. We write T = T 1 • T 2 to mean that type T is split in types T 1 and T 2 , and likewise for Γ = Γ 1 • Γ 2 . Linear type splitting, shared type splitting and context splitting are given by the rules in Figs. 789. Linear type splitting supports the decomposition of a synchronised, τ , session type (including continuation) in the respective dual capabilities !, ?, via rule (L-Dual-1) and its symmetric (L-Dual-2). Notice L = L 1 • L 2 is defined only when matched (L). Essentially, linear type splitting allows to decompose a matched session type in its two dual counterparts (see, e.g., [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]).

Shared type splitting decomposes shared communication capabilities in two distinct ways, depending on whether the polarity of the type to be split is ? or !. A shared input is split in a shared input and either in an output or another input, via rules (S-In-1) and its symmetric (S-In-2). Intuitively, an input that is decomposed in two inputs allows to type processes that separately offer the

• = • • • (C-Empty) Γ = Γ1 • Γ2 Γ, x : T = Γ1, x: T • Γ2 (C-Left) Γ = Γ1 • Γ2 Γ, x : T = Γ1 • Γ2, x: T (C-Right) Γ = Γ1 • Γ2 T = T1 • T2 Γ, x : T = Γ1, x: T1 • Γ2, x: T2 (C-Split)
Fig. 9. Context splitting input capability (e.g., a service that is provided by two distinct sites), and an input that is decomposed in an output and an input allows to type processes that offer the dual communication capabilities (e.g., a service provider and a service client). A shared output is split in two shared outputs -rule (S-Out) -which, intuitively, allows to type processes that offer the output capability separately (e.g., like two service clients). Input capabilities may be further split so as to "absorb" several output capabilities and be distributed in several input capabilities, and output capabilities may also be further split to be distributed in several output capabilities. Notice type splitting (both linear and shared) preserves the argument types so as to guarantee the dual communication actions agree on the type of the communication.

Context splitting allows to split a context in two distinct ways: context entries either go into the left or the right outgoing contexts -rules (C-Left) and its symmetric (C-Right) -or they go in both contexts -rule (C-Split). The latter form lifts the (type) behaviour distribution to the context level, while the former allows to delegate the entire behaviour to a part of the process, leaving no behaviour to the other part. To lighten notation we use

Γ 1 • Γ 2 to represent Γ such that Γ = Γ 1 • Γ 2 (if such Γ exists). Notice that, given Γ 1 and Γ 2 , there is at most one Γ such that Γ = Γ 1 • Γ 2 .
Typing system. We may now present our type system which characterises processes in terms of their usage of channels and of their overall ordering of events, as captured by judgement Γ ; ≺ P where Γ describes channel usage and ≺ gives the ordering of events. We say process P is well-typed if Γ ; ≺ P is the conclusion of a derivation using the rules in Fig. 10. We comment on the rules in Fig. 10. Rule (T-Inact) types the inactive process with a context that associates end to (any set) of channel names and with the "leaf" ordering (the relation with just one pair (end, )). Rule (T-Par) types parallel composition by typing each branch with a slice of the context, obtained via splitting, and with a sub-ordering (such that the union of the sub-orderings is a strict partial order). So, the two branches of the parallel composition may freely refer different channels but they must agree in a sound overall ordering. Rule (T-New) types name restriction by typing the restricted name with a matched type (no unmatched communications). Notice the ordering expected for the interactions in the restricted name is kept in the conclusion, so as to characterise the abstract communication dependencies of the process, which includes (an abstraction of) the communication dependencies of bound names.

Γ end ; {(end, )} 0 (T-Inact) Γ1; ≺1 P Γ2; ≺2 Q Γ1 • Γ2, ≺1 • ∪ ≺2 P | Q (T-
Communication prefixes are typed in separate rules depending on the type of the subject of the communication -notice however that mixing linear and shared types in the same typing context avoids introducing rules that depend on the type of the object of the communication. Rule (T-LIn) types the input on a channel x with linear usage by typing the continuation process considering the continuation session type L for x, the argument type T for the input variable y and ordering ≺. We single out a fresh event e with respect to the continuation (e ∈ supp(≺)) that is used to specify the type of the input, together with the respective ? polarity, argument type T and continuation L. We build a new order from ≺ by setting e as the least element (given by e+≺) since any communication in the continuation depends on the input (hence is greater than e). Notice that the communications in the continuation include the ones that involve the received name, characterised by T and ordered by ≺. Notice also that ≺ is recorded in the conclusion, so as to (also) capture the communication dependencies involving the received name. This is crucial to our approach so as to address processes that interleave communications in received names.

Rule (T-LOut) types the output in a channel x with linear usage by typing the continuation process with the continuation session type L and ordering ≺. The conclusion records the type of the output using a fresh event e with respect to the continuation (ordered by ≺) and also with respect to the type delegated in the communication T (e ∈ supp(≺) ∪ events(T )). The (linear) session type in the conclusion is thus specified using e, the argument type T , the respective ! polarity and continuation L. Event e is also recorded in the ordering of the output as the minimum event e + (≺ • ∪ T ↓), since any communication in the continuation, along with any delegated communication capabilities, depends on the output (hence, are greater than e). We use T ↓ to extract the (chain of) events prescribed by T . The conclusion records the delegated type T via splitting (Γ, x : e lin ! T.L) • (y : T ) as y may be used (dually to T ) in Γ .

The description of rule (T-UOut) follows the same lines, the only differences is that a shared type captures the output and there is no continuation usage for channel x. We rule out uses of x in the continuation to exclude processes that offer the input in the continuation of an output (at the cost of excluding processes that perform more than one shared output over the same channel in sequence). Our rationale for shared communications is that at least one (replicated) shared input matches all corresponding outputs, so the input cannot be activated after the output (to avoid cluttering the rules this led us to also exclude two outputs in sequence, a configuration which is not problematic per se). Rule (T-UIn) types shared inputs that are necessarily replicated, so as to support the rationale that a shared input is able to match all respective inputs. Since more than one copy of the continuation of the input may be simultaneously active we require the resources shared by all copies to be shared outputs (Γ un ).

The reason why we exclude (nested) shared inputs, as explained earlier, is to avoid the situation where a shared output is blocked due to a shared input (of lesser order) that is blocking the matching shared input (of greater order) which is not matched. To avoid forcing that all shared inputs are matched we exclude nested shared inputs in general. Notice however that the argument type T may be linear or shared, in which case T may actually specify a shared input (a nested input that is activated via interaction). Since the behaviour of the name received in the input is only "published" via a corresponding output, this particular case of nested shared inputs is naturally supported.

The main restriction of the presented work is the absence of a general form of recursion, which, conceivably, involves considering the repetition of the overall ordering throughout the unfolding, handled e.g., via a dedicated typing context that we believe can be engineered in conformance to our approach.

Results. We may now present our results, namely that typing is preserved under reduction (Theorem 1) and that a specific class of well-typed processes (those where all communications are matched) enjoy progress (Theorem 2). We start by mentioning some auxiliary results, namely that we may show that conformance is ensured between the typing context and the strict partial order in all derivations, a sanity check that ensures the conditions imposed by our rules (e.g., picking freshness of events) are enough to keep conformance invariant in a derivation. We may also show two standard results used in the proof of Theorem 1, namely that typing is preserved under structural equivalence and under name substitution.

Before presenting our first main result (Theorem 1) we introduce two auxiliary notions that characterise reduction of contexts and of strict partial orders. As expected from a behavioural type system, as processes evolve so must the types that characterise the processes. Reduction for contexts is defined as follows.

• → • Γ, x : e lin p T.L → Γ, x : L Γ 1 → Γ 2 =⇒ Γ 1 , x: T → Γ 2 , x: T A context reduces if it
holds an assumption on a linear type prefix, which reduces to the continuation so as to mimic the analogous behaviour in processes. Also, the empty context reduces (to the empty context) so as to capture synchronisations in processes on restricted channels and on channels with shared usage, thus introducing reflexivity in context reduction since no change is required to capture such synchronisations. Reduction for partial orders is defined as follows.

≺ → ≺

e ∈ supp(≺) =⇒ ≺ → ≺\ e Strict partial order reduction is also reflexive. This allows to capture synchronisations that depend on shared inputs. Notice that the ordering for shared inputs is kept invariant via reduction (since the replicated process is kept throughout reduction), thus capturing synchronisations that depend on shared inputs (as they will take place repeatedly for each activation of the continuation of the shared input). Reduction is also defined by removing an event of the ordering, so as to capture one shot synchronisations. Since such synchronisations may depend on shared outputs, they are not necessarily associated with the minimum event in the ordering. We may now present our first main result, where Γ

1 ; ≺ 1 → Γ 2 ; ≺ 2 denotes Γ 1 → Γ 2 and ≺ 1 →≺ 2 .
Theorem 1 (Preservation). If Γ 1 ; ≺ 1 P 1 and P 1 → P 2 then Γ 1 ; ≺ 1 → Γ 2 ; ≺ 2 and Γ 2 ; ≺ 2 P 2 .

The proof follows by induction on the length of the derivation of P 1 → P 2 in expected lines. The theorem says that typing is preserved under process reduction, up to a reduction in the context and ordering. Fidelity is an immediate consequence of Theorem 1, as usual. We now turn our attention to the result on progress. In order to define "live" processes (processes that should reduce) we introduce the (standard) notion of active contexts, noted C

[•], defined as C[•] ::= • | (P | C[•]) | (νx)C[•]. A context C[•]
is a process with a hole • under a number of parallel compositions and restrictions. We say a process P is active if it has a (non-replicated) communication prefix in an active context, defined as follows active(P )

∃C[•], x, y, Q. P ≡ C[x!y.Q] ∨ P ≡ C[x?y.Q].
Notice the definition of active process rules out replicated inputs. So, we consider stable processes (processes that do not reduce but are not errors) to be processes where a number of (replicated) shared inputs are active. We now state our second main result that says an active and well-typed (matched ) process reduces.

Theorem 2 (Progress). If active(P ), Γ ; ≺ P and matched (Γ ) then P → P .

The proof follows by induction on the size of ≺. The proof invariant is that for every event either there is a synchronisation pair of lesser order or every active prefix of lesser order is a replicated (shared) input. Theorem 2 attests our typing discipline ensures progress of active processes, including processes that interleave communications on received channels.

Concluding Remarks

We have presented a typing discipline for the analysis of progress in sessionbased communication-centred systems. Our work exploits notions introduced in [3] (e.g., the τ polarity) and in [START_REF] Baltazar | A type system for flexible role assignment in multiparty communicating systems[END_REF] (e.g., the splitting relation), allowing to type systems specified in standard π-calculus. This is in contrast with related approaches, where session channels are equipped with polarities (see, e.g., [START_REF] Gay | Subtyping for session types in the pi calculus[END_REF]) or where channels have two endpoints (see, e.g., [START_REF] Vasconcelos | Fundamentals of session types[END_REF]), or or where sessions are established via specialised initiation primitives (see, e.g., [START_REF] Honda | Language primitives and type discipline for structured communication-based programming[END_REF]). Also, we uniformly handle communication of linear and shared channels (when they are the object of the communication) via lin and un annotations introduced in [START_REF] Vasconcelos | Fundamentals of session types[END_REF]. However, this is not the case for communications on linear and shared channels (when they are the subject of the communication).

A cornerstone of our development is the progress analysis technique introduced in [START_REF] Caires | Conversation types[END_REF], where message types already specify the orderings expected for the communicated names, thus providing the basic support for the interleaving of communications on received names. We depart from [START_REF] Caires | Conversation types[END_REF] by unifying the channel usage and event ordering in a single type analysis. Moreover, our orderings build on abstract events and do not refer channel identities (nor labels) differently from [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Caires | Conversation types[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF], which allows us to relate events in received names (via an abstract event) with others. This is crucial to address the interleaving of received names in a more general way, allowing us to address scenarios out of reach of the above mentioned works [START_REF] Bettini | Global progress in dynamically interleaved multiparty sessions[END_REF][START_REF] Caires | Conversation types[END_REF][START_REF] Dezani-Ciancaglini | On progress for structured communications[END_REF]. By combining session types and events in the same type language, inspired by [START_REF] Padovani | From lock freedom to progress using session types[END_REF], we are able to rely on usual session-based reasoning. Our approach differs from the preliminary ideas presented in [START_REF] Padovani | From lock freedom to progress using session types[END_REF] that combines session types with a typing discipline that relies on type simulation [START_REF] Kobayashi | A type system for lock-free processes[END_REF], in that our verification system is completely syntax driven and does not rely on extraimposed conditions (neither on type simulation nor on model-checking).

In our approach, the sound communication dependency structure is captured in a minimal way, via a (strict) partial order of events, which combined with the event-equipped session types, allow us to single out systems that enjoy progress. We acknowledge that our development does not address full-fledged recursion. However, the principles we use can conceivably be lifted to consider recursion, considering the repetition of the event ordering (handled by a dedicated typing context, as usual) or (well-founded) infinite orderings, an engineering exercise we leave to future work. We also plan to use the ideas presented in this paper to type progress in multiparty conversations.

On a pragmatic (vital) level, we may show that the type checking procedure is decidable (considering bound names are type annotated) and we are confident that a type inference procedure can be extracted from our type system. While decidability attests the type system is worth mentioning, type inference makes it more interesting. It supports the verification of systems without burdening the development process, thus contributing to a cost-effective increase of reliability.

Fig. 1 .

 1 Fig. 1. Greeting service code

Fig. 6 .

 6 Fig. 6. Syntax of types and typing contexts

  e + ≺ ≺ ∪{(e, e 1 ) | e 1 ∈ supp(≺)} The relation obtained by removing an element e from ≺ is denoted by ≺\ e. Notice that if ≺ is a strict partial order, then so is ≺\ e. ≺\ e {(e 1 , e 2 ) | (e 1 , e 2 ) ∈≺ ∧ e = e 1 ∧ e 2 = e}

Fig. 7 .Fig. 8 .

 78 Fig. 7. Linear type splitting

Fig. 10 .

 10 Fig. 10. Typing rules

  handle : e 1 un ! (e 2 lin ? String ) service : e 3 un ? (e 4 lin ! String .e 2 lin ? String ) Notice that Server's usage of channel handle is dual to that of Slave (Server outputs ! and Slave receives ?). Notice also that Server and Slave agree that

	Client	(νchat)service!chat.chat?s.chat!"bye"
	Proxy	service?y.(νs)masterservice!s.s!y
	Master	masterservice?z.z?y.y!"hello".handle!y
	Slave	handle?z.z?s
	System	Client | Proxy | Master | Slave
	Fig. 2. Greeting via proxy service code

Acknowledgments We acknowledge support of the project PTDC/EIA-CCO/ 117513/2010 and thank Pedro Baltazar and Luís Caires for fruitful discussions.