Showing 1–25 of 25 results for author: Zavattaro, G

A Sound and Complete Characterization of Fair Asynchronous Session Subtyping

Authors: Mario Bravetti, Luca Padovani, Gianluigi Zavattaro

Abstract: Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outp… ▽ More Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outputs with respect to an unbounded number of message inputs. This refinement is useful to capture common patterns in communication protocols that take advantage of asynchrony. However, while the semantic (à la testing) definition of such refinement is straightforward, its characterization has proved to be quite challenging. In fact, only a sound but not complete characterization is known so far. In this paper we close this open problem by presenting a sound and complete characterization of asynchronous fair refinement for session types. We relate this characterization to those given in the literature for synchronous session types by leveraging a novel labelled transition system of session types that embeds their asynchronous semantics. △ Less

Submitted 6 June, 2025; originally announced June 2025.

Decidability Problems for Micro-Stipula

Authors: Giorgio Delzanno, Cosimo Laneve, Arnaud Sangnier, Gianluigi Zavattaro

Abstract: Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model, the combination of state evolution, time reasoning, and nondeterminism gives rise to significant analytical challenges. In particular, we show that determining… ▽ More Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model, the combination of state evolution, time reasoning, and nondeterminism gives rise to significant analytical challenges. In particular, we show that determining whether a clause is never executed is undecidable. We formally prove that this undecidability result holds even for syntactically restricted fragments: namely, the time-ahead fragment, where all time expressions are strictly positive, and the instantaneous fragment, where all time expressions evaluate to zero. On the other hand, we identify a decidable subfragment: within the instantaneous fragment, reachability becomes decidable when the initial states of functions and events are disjoint. △ Less

Submitted 23 April, 2025; originally announced April 2025.

Fair Termination of Asynchronous Binary Sessions

Authors: Luca Padovani, Gianluigi Zavattaro

Abstract: We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for ses… ▽ More We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs. △ Less

Submitted 14 March, 2025; v1 submitted 10 March, 2025; originally announced March 2025.

ACM Class: F.3.1; F.3.2; F.3.3

Adaptable TeaStore

Authors: Simon Bliudze, Giuseppe De Palma, Saverio Giallorenzo, Ivan Lanese, Gianluigi Zavattaro, Brice Arleon Zemtsop Ndadji

Abstract: Adaptability is a fundamental requirement for modern Cloud software architectures to ensure robust performance in the face of diverse known and unforeseen events inherent to distributed systems. State-of-the-art Cloud systems frequently adopt microservices or serverless architectures. Among these, TeaStore is a recognised microservice reference architecture that offers a benchmarking framework for… ▽ More Adaptability is a fundamental requirement for modern Cloud software architectures to ensure robust performance in the face of diverse known and unforeseen events inherent to distributed systems. State-of-the-art Cloud systems frequently adopt microservices or serverless architectures. Among these, TeaStore is a recognised microservice reference architecture that offers a benchmarking framework for modelling and resource management techniques. However, TeaStore's original configuration lacks the flexibility necessary to address the varied scenarios encountered in real-world applications. To overcome this limitation, we propose an enhanced variant of TeaStore that distinguishes between mandatory and optional services while incorporating third-party service integration. Core services such as WebUI, Image Provider, and Persistence are designated as mandatory to maintain essential functionality, whereas optional services, such as Recommender and Auth, extend the architecture's feature set. We outline the design and configuration possibilities of this adaptable TeaStore variant, aimed at enabling a broader spectrum of configurability and operational resilience. △ Less

Submitted 20 December, 2024; originally announced December 2024.

Affinity-aware Serverless Function Scheduling

Authors: Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent work proposed using domain-specific languages to express per-function policies, e.g., policies that enforce the allocation on nodes that enjoy lower latencies to databases and services used by the function. Here, we fo… ▽ More Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent work proposed using domain-specific languages to express per-function policies, e.g., policies that enforce the allocation on nodes that enjoy lower latencies to databases and services used by the function. Here, we focus on affinity-aware scenarios, i.e., where, for performance and functional requirements, the allocation of a function depends on the presence/absence of other functions on nodes. We present aAPP, an extension of a declarative, platform-agnostic language that captures affinity-aware scheduling at the FaaS level. We implement an aAPP-based prototype on Apache OpenWhisk. Besides proving that a FaaS platform can capture affinity awareness using aAPP and improve performance in affinity-aware scenarios, we use our prototype to show that aAPP imposes no noticeable overhead in scenarios without affinity constraints. △ Less

Submitted 23 January, 2025; v1 submitted 19 July, 2024; originally announced July 2024.

Comments: 11 pages, 9 figures, 1 listing. arXiv admin note: substantial text overlap with arXiv:2407.14159

On the Complexity of Reachability Properties in Serverless Function Scheduling

Authors: Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies… ▽ More Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution scheduling (e.g., resource allocation, runtime environments) of stateless functions. Recent developments demonstrate the benefits of using domain-specific languages to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. We present aAPP, an affinity-aware extension of a platform-agnostic function scheduling language. We formalise its scheduling semantics and then study the complexity of statically checking reachability properties, e.g., useful to verify that trusted and untrusted functions cannot be co-located. Analysing different fragments of aAPP, we show that checking reachability of policies without affinity has linear complexity, while affinity makes the problem PSpace. △ Less

Submitted 19 July, 2024; originally announced July 2024.

Comments: 26 pages, 3 figures, 2 listing, appendix

Towards a Function-as-a-Service Choreographic Programming Language: Examples and Applications

Authors: Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: Choreographic Programming (CP) is a language paradigm whereby software artefacts, called choreographies, specify the behaviour of communicating participants. CP is famous for its correctness-by-construction approach to the development of concurrent, distributed systems. In this paper, we illustrate FaaSChal, a proposal for a CP language tailored for the case of serverless Function-as-a-Service (Fa… ▽ More Choreographic Programming (CP) is a language paradigm whereby software artefacts, called choreographies, specify the behaviour of communicating participants. CP is famous for its correctness-by-construction approach to the development of concurrent, distributed systems. In this paper, we illustrate FaaSChal, a proposal for a CP language tailored for the case of serverless Function-as-a-Service (FaaS). In FaaS, developers define a distributed architecture as a collection of stateless functions, leaving to the serverless platform the management of deployment and scaling. We provide a first account of a CP language tailored for the FaaS case via examples that present some of its relevant features, including projection. In addition, we showcase a novel application of CP. We use the choreography as a source to extract information on the infrastructural relations among functions so that we can synthesise policies that strive to minimise their latency while guaranteeing the respect of user-defined constraints. △ Less

Submitted 13 June, 2024; originally announced June 2024.

FunLess: Functions-as-a-Service for Private Edge Cloud Systems

Authors: Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: We present FunLess, a Function-as-a-Service (FaaS) platform tailored for the private edge cloud system. FunLess responds to recent trends that advocate for extending the coverage of serverless computing to private edge cloud systems and enhancing latency, security, and privacy while improving resource usage. Unlike existing solutions that rely on containers for function invocation, FunLess leverag… ▽ More We present FunLess, a Function-as-a-Service (FaaS) platform tailored for the private edge cloud system. FunLess responds to recent trends that advocate for extending the coverage of serverless computing to private edge cloud systems and enhancing latency, security, and privacy while improving resource usage. Unlike existing solutions that rely on containers for function invocation, FunLess leverages WebAssembly (Wasm) as its runtime environment. Wasm's lightweight, sandboxed runtime is crucial to have functions run on constrained devices at the edge. Moreover, the advantages of using Wasm in FunLess include a consistent development and deployment environment for users and function portability (write once, run everywhere) We validate FunLess under different deployment scenarios, characterised by the presence/absence of constrained-resource devices (Raspberry Pi 3B+) and the (in)accessibility of container orchestration technologies - Kubernetes. We compare FunLess with three production-ready, widely adopted open-source FaaS platforms - OpenFaaS, Fission, and Knative. Our benchmarks confirm that FunLess is a proper solution for FaaS private edge cloud systems since it achieves performance comparable to the considered FaaS alternatives while it is the only fully-deployable alternative on constrained-resource devices, thanks to its small memory footprint. △ Less

Submitted 31 May, 2024; originally announced May 2024.

Serverless Scheduling Policies based on Cost Analysis

Authors: Giuseppe De Palma, Saverio Giallorenzo, Cosimo Laneve, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such policies may decrease the performance and the security of the application due to locality issues (e.g., functions executed by workers far from the databases to be accessed). These limitations are partially overcome by the… ▽ More Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such policies may decrease the performance and the security of the application due to locality issues (e.g., functions executed by workers far from the databases to be accessed). These limitations are partially overcome by the adoption of APP, a new platform-agnostic declarative language that allows serverless platforms to support multiple scheduling logics. Defining the "right" scheduling policy in APP is far from being a trivial task since it often requires rounds of refinement involving knowledge of the underlying infrastructure, guesswork, and empirical testing. In this paper, we start investigating how information derived from static analysis could be incorporated into APP scheduling function policies to help users select the best-performing workers at function allocation. We substantiate our proposal by presenting a pipeline able to extract cost equations from functions' code, synthesising cost expressions through the usage of off-the-shelf solvers, and extending APP allocation policies to consider this information. △ Less

Submitted 31 October, 2023; originally announced October 2023.

Comments: In Proceedings TiCSA 2023, arXiv:2310.18720

Journal ref: EPTCS 392, 2023, pp. 40-52

Topology-aware Serverless Function-Execution Scheduling

Authors: Giuseppe De Palma, Saverio Giallorenzo, Jacopo Mauro, Matteo Trentin, Gianluigi Zavattaro

Abstract: Cloud-edge serverless applications or serverless deployments spanning multiple regions introduce the need to govern the scheduling of functions to satisfy their functional constraints or avoid performance degradation. For instance, functions may require to be allocated to specific private (edge) nodes that have access to specialised resources or to nodes with low latency to access a certain databa… ▽ More Cloud-edge serverless applications or serverless deployments spanning multiple regions introduce the need to govern the scheduling of functions to satisfy their functional constraints or avoid performance degradation. For instance, functions may require to be allocated to specific private (edge) nodes that have access to specialised resources or to nodes with low latency to access a certain database to decrease the overall latency of the application. State-of-the-art serverless platforms do not support directly the implementation of topological constraints on the scheduling of functions. We address this problem by presenting a declarative language for defining topology-aware, function-specific serverless scheduling policies, called tAPP. Given a tAPP script, a compatible serverless scheduler can enforce different, co-existing topological constraints without requiring ad-hoc platform deployments. We prove our approach feasible by implementing a tAPP-based serverless platform as an extension of the Apache OpenWhisk serverless platform. We show that, compared to vanilla OpenWhisk, our extension does not negatively impact the performance of generic, non-topology-bound serverless scenarios, while it increases the performance of topology-bound ones. △ Less

Submitted 6 July, 2023; v1 submitted 20 May, 2022; originally announced May 2022.

Microservice Dynamic Architecture-Level Deployment Orchestration (Extended Version)

Authors: Lorenzo Bacchiani, Mario Bravetti, Saverio Giallorenzo, Jacopo Mauro, Iacopo Talevi, Gianluigi Zavattaro

Abstract: In the context of the BI-REX (Big Data Innovation and Research Excellence) competence center SEAWALL (SEAmless loW lAtency cLoud pLatforms) project (scientific coordinator Prof. Maurizio Gabbrielli) we develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfiguration orchestrations. More precisely, we devise an algorithm… ▽ More In the context of the BI-REX (Big Data Innovation and Research Excellence) competence center SEAWALL (SEAmless loW lAtency cLoud pLatforms) project (scientific coordinator Prof. Maurizio Gabbrielli) we develop a novel approach for run-time global adaptation of microservice applications, based on synthesis of architecture-level reconfiguration orchestrations. More precisely, we devise an algorithm for automatic reconfiguration that reaches a target system Maximum Computational Load by performing optimal deployment orchestrations. To conceive and simulate our approach, we introduce a novel integrated timed architectural modeling/execution language based on an extension of the actor-based object-oriented Abstract Behavioral Specification (ABS) language. In particular, we realize a timed extension of SmartDeployer, whose ABS code annotations make it possible to express architectural properties. Our Timed SmartDeployer tool fully integrates time features of ABS and architectural annotations by generating timed deployment orchestrations. We evaluate the applicability of our approach on a realistic microservice application taken from the literature: an Email Pipeline Processing System. We prove its effectiveness by simulating such an application and by comparing architecture-level reconfiguration with traditional local scaling techniques (which detect scaling needs and enact replications at the level of single microservices). Our comparison results show that our approach avoids cascading slowdowns and consequent increased message loss and latency, which affect traditional local scaling. △ Less

Submitted 4 June, 2021; v1 submitted 26 April, 2021; originally announced April 2021.

A Session Subtyping Tool (Extended Version)

Authors: Lorenzo Bacchiani, Mario Bravetti, Julien Lange, Gianluigi Zavattaro

Abstract: Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in session type implementations is the one defined by Gay and Hole for synchronous communication. This might be because there are several notions of asynchronous session… ▽ More Session types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in session type implementations is the one defined by Gay and Hole for synchronous communication. This might be because there are several notions of asynchronous session subtyping, these notions are usually undecidable, and only recently sound (but not complete) algorithmic characterizations for these subtypings have been proposed. But the fact that the definition of asynchronous session subtyping and the theory behind related algorithms are not easily accessible to non-experts may also prevent further integration. The aim of this paper, and of the tool presented therein, is to make the growing body of knowledge about asynchronous session subtyping more accessible, thus promoting its integration in practical applications of session types. △ Less

Submitted 28 April, 2021; v1 submitted 26 April, 2021; originally announced April 2021.

Fair Asynchronous Session Subtyping

Authors: Mario Bravetti, Julien Lange, Gianluigi Zavattaro

Abstract: Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is asynchronous session subtyping, which allows message emissions to be anticipated… ▽ More Session types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is asynchronous session subtyping, which allows message emissions to be anticipated w.r.t. a bounded amount of message consumptions. In this paper we investigate the possibility to anticipate emissions w.r.t. an unbounded amount of consumptions: to this aim we propose to consider fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm which deals with examples that feature potentially unbounded buffering. Finally, we present an implementation of our algorithm and an empirical evaluation of it on synthetic benchmarks. △ Less

Submitted 4 October, 2024; v1 submitted 20 January, 2021; originally announced January 2021.

Journal ref: Logical Methods in Computer Science, Volume 20, Issue 4 (October 7, 2024) lmcs:12368

Microservice Interface Based Deployment Orchestration

Authors: Lorenzo Bacchiani, Mario Bravetti, Saverio Giallorenzo, Jacopo Mauro, Iacopo Talevi, Gianluigi Zavattaro

Abstract: Following previous work on the automated deployment orchestration of component based applications, where orchestrations are expressed in terms of behaviours satisfying component interface functional dependences, we develop a formal model specifically tailored for microservice architectures. The first result that we obtain is decidability of the problem of synthesizing optimal deployment orchestrat… ▽ More Following previous work on the automated deployment orchestration of component based applications, where orchestrations are expressed in terms of behaviours satisfying component interface functional dependences, we develop a formal model specifically tailored for microservice architectures. The first result that we obtain is decidability of the problem of synthesizing optimal deployment orchestrations for microservice architectures, a problem that is, instead, undecidable for generic component-based applications. We, thus, show how optimal deployment orchestrations can be synthesized and how, by using such orchestrations we can devise a procedure for run-time adaptation based on performing global reconfigurations. Finally, we evaluate the applicability of our approach on a realistic microservice architecture taken from the literature. In particular, we use the high-level object-oriented probabilistic and timed process algebra Abstract Behavioural Specification (ABS) to model such a case study and to simulate it. The results of simulation show the advantages of global reconfiguration w.r.t. local adaptation. △ Less

Submitted 29 September, 2020; v1 submitted 4 August, 2020; originally announced August 2020.

Analysis of SLA Compliance in the Cloud -- An Automated, Model-based Approach

Authors: Frank S. de Boer, Elena Giachino, Stijn de Gouw, Reiner Hähnle, Einar Broch Johnsen, Cosimo Laneve, Ka I Pun, Gianluigi Zavattaro

Abstract: Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study.… ▽ More Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study. The approach is based on formal models combined with static analysis tools and generated runtime monitors. As such, it fits well within a methodology combining software development with information technology operations (DevOps). △ Less

Submitted 27 August, 2019; originally announced August 2019.

Comments: In Proceedings VORTEX 2018, arXiv:1908.09302

Journal ref: EPTCS 302, 2019, pp. 1-15

A Sound Algorithm for Asynchronous Session Subtyping and its Implementation

Authors: Mario Bravetti, Marco Carbone, Julien Lange, Nobuko Yoshida, Gianluigi Zavattaro

Abstract: Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent… ▽ More Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm. △ Less

Submitted 3 March, 2021; v1 submitted 30 June, 2019; originally announced July 2019.

Comments: This is an extended version of the CONCUR'19 version

Journal ref: Logical Methods in Computer Science, Volume 17, Issue 1 (March 4, 2021) lmcs:5974

Optimal and Automated Deployment for Microservices

Authors: Mario Bravetti, Saverio Giallorenzo, Jacopo Mauro, Iacopo Talevi, Gianluigi Zavattaro

Abstract: Microservices are highly modular and scalable Service Oriented Architectures. They underpin automated deployment practices like Continuous Deployment and Autoscaling. In this paper, we formalize these practices and show that automated deployment - proven undecidable in the general case - is algorithmically treatable for microservices. Our key assumption is that the configuration life-cycle of a mi… ▽ More Microservices are highly modular and scalable Service Oriented Architectures. They underpin automated deployment practices like Continuous Deployment and Autoscaling. In this paper, we formalize these practices and show that automated deployment - proven undecidable in the general case - is algorithmically treatable for microservices. Our key assumption is that the configuration life-cycle of a microservice is split into two phases: (i) creation, which entails establishing initial connections with already available microservices, and (ii) subsequent binding/unbinding with other microservices. To illustrate the applicability of our approach, we implement an automatic optimal deployment tool and compute deployment plans for a realistic microservice architecture, modeled in the Abstract Behavioral Specification (ABS) language. △ Less

Submitted 28 January, 2019; originally announced January 2019.

On the Boundary between Decidability and Undecidability of Asynchronous Session Subtyping

Authors: Mario Bravetti, Marco Carbone, Gianluigi Zavattaro

Abstract: Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable… ▽ More Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance. △ Less

Submitted 12 February, 2018; v1 submitted 2 March, 2017; originally announced March 2017.

Undecidability of Asynchronous Session Subtyping

Authors: Mario Bravetti, Marco Carbone, Gianluigi Zavattaro

Abstract: Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability of subtyping for session types in asynchronously communicating systems. We first devise a core undecidable subtyping relation that is obtained by imposing limitations on… ▽ More Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability of subtyping for session types in asynchronously communicating systems. We first devise a core undecidable subtyping relation that is obtained by imposing limitations on the structure of types. Then, as a consequence of this initial undecidability result, we show that (differently from what stated or conjectured in the literature) the three notions of asynchronous subtyping defined so far for session types are all undecidable. Namely, we consider the asynchronous session subtyping by Mostrous and Yoshida for binary sessions, the relation by Chen et al. for binary sessions under the assumption that every message emitted is eventually consumed, and the one by Mostrous et al. for multiparty session types. Finally, by showing that two fragments of the core subtyping relation are decidable, we evince that further restrictions on the structure of types make our core subtyping relation decidable. △ Less

Submitted 19 July, 2017; v1 submitted 15 November, 2016; originally announced November 2016.

Comments: 36 pages

Choreographies and Behavioural Contracts on the Way to Dynamic Updates

Authors: Mario Bravetti, Gianluigi Zavattaro

Abstract: We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous address or name based communicatio… ▽ More We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous address or name based communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly relations between behavioural contracts and choreographic descriptions are considered, where a contract for each communicating party is, e.g., derived by projection. The considered relations are induced as the maximal preoders which preserve contract compliance and global traces: we show maximality to hold (permitting services to be discovered/substituted independently for each party) when contract refinement preorders with all the above asymmetric communication means are considered and, instead, not to hold if the standard symmetric CCS/pi-calculus communication is considered (or when directly relating choreographies to behavioral contracts via a preorder, no matter the communication mean). The obtained maximal preorders are then characterized in terms of a new form of testing, called compliance testing, where not only tests must succeed but also the system under test (thus relating to controllability theory), and compared with classical preorders such as may/must testing, trace inclusion, etc. Finally, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention. △ Less

Submitted 13 November, 2014; originally announced November 2014.

Comments: In Proceedings MOD* 2014, arXiv:1411.3453

Journal ref: EPTCS 168, 2014, pp. 12-31

Decidability Problems for Actor Systems

Authors: Frank De Boer, Mahdi Jaghoori, Cosimo Laneve, Gianluigi Zavattaro

Abstract: We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still… ▽ More We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still holds for actors with states when the number of actors is bounded and the state is read-only. △ Less

Submitted 3 December, 2014; v1 submitted 17 September, 2014; originally announced September 2014.

Journal ref: Logical Methods in Computer Science, Volume 10, Issue 4 (December 4, 2014) lmcs:1091

Amending Choreographies

Authors: Ivan Lanese, Fabrizio Montesi, Gianluigi Zavattaro

Abstract: Choreographies are global descriptions of system behaviors, from which the local behavior of each endpoint entity can be obtained automatically through projection. To guarantee that its projection is correct, i.e. it has the same behaviors of the original choreography, a choreography usually has to respect some coherency conditions. This restricts the set of choreographies that can be projected.… ▽ More Choreographies are global descriptions of system behaviors, from which the local behavior of each endpoint entity can be obtained automatically through projection. To guarantee that its projection is correct, i.e. it has the same behaviors of the original choreography, a choreography usually has to respect some coherency conditions. This restricts the set of choreographies that can be projected. In this paper, we present a transformation for amending choreographies that do not respect common syntactic conditions for projection correctness. Specifically, our transformation automatically reduces the amount of concurrency, and it infers and adds hidden communications that make the resulting choreography respect the desired conditions, while preserving its behavior. △ Less

Submitted 1 August, 2013; originally announced August 2013.

Comments: In Proceedings WWV 2013, arXiv:1308.0268

ACM Class: D.1.3; D.3.3; F.3.2

Journal ref: EPTCS 123, 2013, pp. 34-48

Adaptable processes

Authors: Mario Bravetti, Cinzia Di Giusto, Jorge A Perez, Gianluigi Zavattaro

Abstract: We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location… ▽ More We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime; this allows to express a wide range of evolvability patterns for concurrent processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, the latter ensures that if the system enters into a state with errors then a state without errors will be eventually reached. We study the (un)decidability of these two problems in several variants of the calculus, which result from considering dynamic and static topologies of adaptable processes as well as different evolvability patterns. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities. △ Less

Submitted 15 November, 2012; v1 submitted 23 October, 2012; originally announced October 2012.

ACM Class: D.2.4; F.3.1; F.3.2; F.4.3

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 4 (November 19, 2012) lmcs:982

The Cost of Parameterized Reachability in Mobile Ad Hoc Networks

Authors: Giorgio Delzanno, Arnaud Sangnier, Riccardo Traverso, Gianluigi Zavattaro

Abstract: We investigate the impact of spontaneous movement in the complexity of verification problems for an automata-based protocol model of networks with selective broadcast communication. We first consider reachability of an error state and show that parameterized verification is decidable with polynomial complexity. We then move to richer queries and show how the complexity changes when considering pro… ▽ More We investigate the impact of spontaneous movement in the complexity of verification problems for an automata-based protocol model of networks with selective broadcast communication. We first consider reachability of an error state and show that parameterized verification is decidable with polynomial complexity. We then move to richer queries and show how the complexity changes when considering properties with negation or cardinality constraints. △ Less

Submitted 27 February, 2012; originally announced February 2012.

Parameterized Verification of Safety Properties in Ad Hoc Network Protocols

Authors: Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro

Abstract: We summarize the main results proved in recent work on the parameterized verification of safety properties for ad hoc network protocols. We consider a model in which the communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broad… ▽ More We summarize the main results proved in recent work on the parameterized verification of safety properties for ad hoc network protocols. We consider a model in which the communication topology of a network is represented as a graph. Nodes represent states of individual processes. Adjacent nodes represent single-hop neighbors. Processes are finite state automata that communicate via selective broadcast messages. Reception of a broadcast is restricted to single-hop neighbors. For this model we consider a decision problem that can be expressed as the verification of the existence of an initial topology in which the execution of the protocol can lead to a configuration with at least one node in a certain state. The decision problem is parametric both on the size and on the form of the communication topology of the initial configurations. We draw a complete picture of the decidability and complexity boundaries of this problem according to various assumptions on the possible topologies. △ Less

Submitted 9 August, 2011; originally announced August 2011.

Comments: In Proceedings PACO 2011, arXiv:1108.1452

Journal ref: EPTCS 60, 2011, pp. 56-65