Showing 1–49 of 49 results for author: Montesi, F

Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)

Authors: Matteo Acclavio, Giulia Manara, Fabrizio Montesi

Abstract: We introduce a novel approach to studying properties of processes in the π-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free π-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-fre… ▽ More We introduce a novel approach to studying properties of processes in the π-calculus based on a processes-as-formulas interpretation, by establishing a correspondence between specific sequent calculus derivations and computation trees in the reduction semantics of the recursion-free π-calculus. Our method provides a simple logical characterisation of deadlock-freedom for the recursion- and race-free fragment of the π-calculus, supporting key features such as cyclic dependencies and an independence of the name restriction and parallel operators. Based on this technique, we establish a strong completeness result for a nontrivial choreographic language: all deadlock-free and race-free finite π-calculus processes composed in parallel at the top level can be faithfully represented by a choreography. With these results, we show how the paradigm of computation-as-derivation extends the reach of logical methods for the study of concurrency, by bridging important gaps between logic, the expressiveness of the π-calculus, and the expressiveness of choreographic languages. △ Less

Submitted 26 May, 2025; v1 submitted 15 January, 2025; originally announced January 2025.

Comments: Extended version of the paper "Formulas as Processes, Deadlock-Freedom as Choreographies", accepted at ESOP2025

Journal ref: In: Vafeiadis, V. (eds) Programming Languages and Systems. ESOP 2025. Lecture Notes in Computer Science, vol 15694

A Conceptual Framework for API Refactoring in Enterprise Application Architectures

Authors: Fabrizio Montesi, Marco Peressotti, Valentino Picotti, Olaf Zimmermann

Abstract: Enterprise applications are often built as service-oriented architectures, where the individual services are designed to perform specific functions and interact with each other by means of well-defined APIs (Application Programming Interfaces). The architecture of an enterprise application evolves over time, in order to adapt to changing business requirements. This evolution might require changes… ▽ More Enterprise applications are often built as service-oriented architectures, where the individual services are designed to perform specific functions and interact with each other by means of well-defined APIs (Application Programming Interfaces). The architecture of an enterprise application evolves over time, in order to adapt to changing business requirements. This evolution might require changes to the APIs offered by services, which can be achieved through appropriate API refactorings. Previous studies on API refactoring focused on the effects on API definitions, with general considerations on related forces and smells. So far, instead, the development strategy for realising these refactorings has received little attention. This paper addresses exactly this aspect. We introduce a conceptual framework for the implementation of API refactorings. Our framework elicits that there are important trade-offs and choices, which significantly affect the efficiency, maintainability, and isolation properties of the resulting architecture. We validate our framework by implementing several refactorings that introduce established API patterns with different choices, which illustrates the guiding principles offered by our framework. Our work also elicits, for the first time, how certain programming language features can reduce friction in applying API refactoring and open up more architectural choices. △ Less

Submitted 10 July, 2024; originally announced July 2024.

On Propositional Dynamic Logic and Concurrency

Authors: Matteo Acclavio, Fabrizio Montesi, Marco Peressotti

Abstract: Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are re… ▽ More Dynamic logic is a powerful approach to reasoning about programs and their executions, obtained by extending classical logic with modalities that can express program executions as formulas. However, the use of dynamic logic in the setting of concurrency has proved problematic because of the challenge of capturing interleaving. This challenge stems from the fact that, traditionally, programs are represented by their sets of traces. These sets are then expressed as elements of a Kleene algebra, for which it is not possible to decide equality in the presence of the commutations required to model interleaving. In this work, we generalise propositional dynamic logic (PDL) to a logic framework we call operational propositional dynamic logic (OPDL), which departs from tradition by distinguishing programs from their traces. Traces are generated by an arbitrary operational semantics that we take as a parameter, making our approach applicable to different program syntaxes and semantics. To develop our framework, we provide the first proof of cut-elimination for a finitely-branching non-wellfounded sequent calculus for PDL. Thanks to this result we can effortlessly prove adequacy for PDL, and extend these results to OPDL. We conclude by discussing OPDL for two representative cases of concurrency: the Calculus of Communicating Systems (CCS), where interleaving is obtained by parallel composition, and Choreographic Programming, where interleaving is obtained by out-of-order execution. △ Less

Submitted 26 May, 2025; v1 submitted 27 March, 2024; originally announced March 2024.

Ozone: Fully Out-of-Order Choreographies

Authors: Dan Plyukhin, Marco Peressotti, Fabrizio Montesi

Abstract: Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a… ▽ More Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order -- for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs). In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered data messages. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency and increase throughput by overlapping communication with computation. △ Less

Submitted 12 July, 2024; v1 submitted 30 January, 2024; originally announced January 2024.

Comments: To appear ECOOP 2024. 26 pages, 22 Figures, 3 pages appendix

Reasoning about Choreographic Programs

Authors: Luís Cruz-Filipe, Eva Graversen, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographie… ▽ More Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties. This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation. △ Less

Submitted 27 April, 2023; originally announced April 2023.

Alice or Bob?: Process Polymorphism in Choreographies

Authors: Eva Graversen, Andrew K. Hirsch, Fabrizio Montesi

Abstract: We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type a… ▽ More We present PolyChor$λ$, a language for higher-order functional \emph{choreographic programming} -- an emerging paradigm by which programmers write the desired cooperative behaviour of a system of communicating processes and then compile it into distributed implementations for each process, a translation called \emph{endpoint projection}. Unlike its predecessor, Chor$λ$, PolyChor$λ$ has both type and \emph{process} polymorphism inspired by System F$_ω$. That is, PolyChor$λ$ is the first (higher-order) functional choreographic language which gives programmers the ability to write generic choreographies and determine the participants at runtime. This novel combination of features also allows PolyChor$λ$ processes to communicate \emph{distributed values}, leading to a new and intuitive way to write delegation. While some of the functional features of PolyChor$λ$ give it a weaker correspondence between the semantics of choreographies and their endpoint-projected concurrent systems than some other choreographic languages, we still get the hallmark end result of choreographic programming: projected programs are deadlock-free by design. △ Less

Submitted 8 March, 2023; originally announced March 2023.

Comments: In submission to JFP

Real-World Choreographic Programming: Full-Duplex Asynchrony and Interoperability

Authors: Lovro Lugović, Fabrizio Montesi

Abstract: In the paradigm of choreographic programming, the overall behaviour of a distributed system is coded as a choreography from a global viewpoint. The choreography can then be automatically projected (compiled) to a correct implementation for each participant. This paradigm is interesting because it relieves the programmer from manually writing the separate send and receive actions performed by parti… ▽ More In the paradigm of choreographic programming, the overall behaviour of a distributed system is coded as a choreography from a global viewpoint. The choreography can then be automatically projected (compiled) to a correct implementation for each participant. This paradigm is interesting because it relieves the programmer from manually writing the separate send and receive actions performed by participants, which simplifies development and avoids communication mismatches. However, the applicability of choreographic programming in the real world remains largely unexplored. The reason is twofold. First, while there have been several proposals of choreographic programming languages, none of these languages have been used to implement a realistic, widely-used protocol. Thus there is a lack of experience on how realistic choreographic programs are structured and on the relevance of the different features explored in theoretical models. Second, applications of choreographic programming shown so far are intrusive, in the sense that each participant must use exactly the code projected from the choreography. This prevents using the code generated from choreographies with existing third-party implementations of some participants, something that is very beneficial for testing or might even come as a requirement. This paper addresses both problems. In particular, we carry out the first development in choreographic programming of a widespread real-world protocol: the Internet Relay Chat (IRC) client--server protocol. The development is based on Choral, an object-oriented higher-order choreographic programming language (choreographies can be parametric on choreographies and carry state). We find that two of Choral's features are key to our implementation: higher-order choreographies are used for modelling the complex interaction patterns that arise due to IRC's asynchronous nature, while user-definable communication semantics are relevant for achieving interoperability with third-party implementations. In the process we also discover a missing piece: the capability of statically detecting that choices on alternative distributed behaviours are appropriately communicated by means of message types, for which we extend the Choral compiler with an elegant solution based on subtyping. Our Choral implementation of IRC arguably represents a milestone for choreographic programming, since it is the first empirical evidence that the paradigm can be used to faithfully codify protocols found `in the wild'. We observe that the choreographic approach reduces the interaction complexity of our program, compared to the traditional approach of writing separate send and receive actions. To check that our implementation is indeed interoperable with third-party software, we test it against publicly available conformance tests for IRC and some of the most popular IRC client and server software. We also evaluate the performance and scalability of our implementation by performing performance tests. Our experience shows that even if choreographic programming is still in its early life, it can already be applied to a realistic setting. △ Less

Submitted 29 December, 2023; v1 submitted 7 March, 2023; originally announced March 2023.

Journal ref: The Art, Science, and Engineering of Programming, 2024, Vol. 8, Issue 2, Article 8

Certified Compilation of Choreographies with hacc

Authors: Luís Cruz-Filipe, Lovro Lugović, Fabrizio Montesi

Abstract: Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures f… ▽ More Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP). While choreographic programming prevents manual mistakes in the implementation of communications, the correctness of a choreographic programming framework crucially hinges on the correctness of its complex compiler, which has motivated formalisation of theories of choreographic programming in theorem provers. In this paper, we build upon one of these formalisations to construct a toolchain that produces executable code from a choreography. △ Less

Submitted 7 March, 2023; originally announced March 2023.

Now It Compiles! Certified Automatic Repair of Uncompilable Protocols

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces pr… ▽ More Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment. △ Less

Submitted 28 February, 2023; originally announced February 2023.

A Formal Theory of Choreographic Programming

Authors: Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these… ▽ More Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works. In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure. Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages. △ Less

Submitted 5 September, 2022; originally announced September 2022.

From Infinity to Choreographies: Extraction for Unbounded Systems

Authors: Bjørn Angel Kjær, Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographies are formal descriptions of distributed systems, which focus on the way in which participants communicate. While they are useful for analysing protocols, in practice systems are written directly by specifying each participant's behaviour. This created the need for choreography extraction: the process of obtaining a choreography that faithfully describes the collective behaviour of al… ▽ More Choreographies are formal descriptions of distributed systems, which focus on the way in which participants communicate. While they are useful for analysing protocols, in practice systems are written directly by specifying each participant's behaviour. This created the need for choreography extraction: the process of obtaining a choreography that faithfully describes the collective behaviour of all participants in a distributed protocol. Previous works have addressed this problem for systems with a predefined, finite number of participants. In this work, we show how to extract choreographies from system descriptions where the total number of participants is unknown and unbounded, due to the ability of spawning new processes at runtime. This extension is challenging, since previous algorithms relied heavily on the set of possible states of the network during execution being finite. △ Less

Submitted 18 July, 2022; originally announced July 2022.

Implementing Choreography Extraction

Authors: Luis Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi, Larisa Safina

Abstract: Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their… ▽ More Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification and synthesis of correct-by-construction software. They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most software does not come with choreographies yet, which prevents their application. To attack this problem, previous work investigated choreography extraction, which automatically constructs a choreography that describes the behaviour of a given set of programs or protocol specifications. We propose a new extraction methodology that improves on the state of the art: we can deal with programs that are equipped with state and internal computation and time complexity is dramatically better. We also implement this theory and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introduce some optimisations, and perform a systematic practical evaluation. △ Less

Submitted 6 May, 2022; v1 submitted 5 May, 2022; originally announced May 2022.

Comments: arXiv admin note: text overlap with arXiv:1910.11741

Model-Driven Generation of Microservice Interfaces: From LEMMA Domain Models to Jolie APIs

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher

Abstract: We formally define and implement a translation from domain models in the LEMMA modelling framework to microservice APIs in the Jolie programming language. Our tool enables a software development process whereby microservice architectures can first be designed with the leading method of Domain-Driven Design, and then corresponding data types and service interfaces (APIs) in Jolie are automatically… ▽ More We formally define and implement a translation from domain models in the LEMMA modelling framework to microservice APIs in the Jolie programming language. Our tool enables a software development process whereby microservice architectures can first be designed with the leading method of Domain-Driven Design, and then corresponding data types and service interfaces (APIs) in Jolie are automatically generated. Developers can extend and use these APIs as guides in order to produce compliant implementations. Our tool thus contributes to enhancing productivity and improving the design adherence of microservices. △ Less

Submitted 23 February, 2022; originally announced February 2022.

Functional Choreographic Programming

Authors: Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the genera… ▽ More Choreographic programming is an emerging programming paradigm for concurrent and distributed systems, whereby developers write the communications that should be enacted and then a distributed implementation is automatically obtained by means of a compiler. Theories of choreographic programming typically come with strong theoretical guarantees about the compilation process, most notably: the generated implementations operationally correspond to their source choreographies and are deadlock-free. Currently, the most advanced incarnation of the paradigm is Choral, an object-oriented choreographic programming language that targets Java. Choral deviated significantly from known theories of choreographies, and introduced the possibility of expressing higher-order choreographies (choreographies parameterised over choreographies) that are fully distributed. As a consequence, it is unclear if the usual guarantees of choreographies can still hold in the more general setting of higher-order ones. We introduce Chorλ, the first functional choreographic programming language: it introduces a new formulation of the standard communication primitive found in choreographies as a function, and it is based upon the λ-calculus. Chorλ is the first theory that explains the core ideas of higher-order choreographic programming (as in Choral). Bridging the gap between practice and theory requires developing a new evaluation strategy and typing discipline for λ terms that accounts for the distributed nature of computation in choreographies. We illustrate the expressivity of Chorλ with a series of examples, which include reconstructions of the key examples from the original presentation of Choral. Our theory supports the expected properties of choreographic programming and bridges the gap between the communities of functional and choreographic programming. △ Less

Submitted 17 August, 2022; v1 submitted 5 November, 2021; originally announced November 2021.

Linear Logic, the $π$-calculus, and their Metatheory: A Recipe for Proofs as Processes

Authors: Fabrizio Montesi, Marco Peressotti

Abstract: Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear logic and the $π$-calculus. To date, Proofs as Processes is still a partial success. Caires and Pfenning [2010] showed that linear propositions correspond to session types, which prescribe the observable behaviour of p… ▽ More Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear logic and the $π$-calculus. To date, Proofs as Processes is still a partial success. Caires and Pfenning [2010] showed that linear propositions correspond to session types, which prescribe the observable behaviour of processes. Further, Carbone et al. [2018] demonstrated that adopting devices from hypersequents [Avron 1991] shapes proofs such that they correspond to the expected syntactic structure of processes in the $π$-calculus. What remains is reconstructing the expected metatheory of session types and the $π$-calculus. In particular, the hallmark of session types, session fidelity, still has to be reconstructed: a correspondence between the observable behaviours of processes and their session types, in terms of labelled transitions. In this article, we present $π$LL, a new process calculus rooted in linear logic. The key novelty of $π$LL is that it comes with a carefully formulated design recipe, based on a dialgebraic view of labelled transition systems. Thanks to our recipe, $π$LL offers the expected transition systems of session types, which we use to establish session fidelity. We use $π$LL to carry out the first thorough investigation of the metatheoretical properties enforced by linear logic on the observable behaviour of processes, uncovering connections with similarity and bisimilarity. We also prove that $π$LL and our recipe form a robust basis for the further exploration of Proofs as Processes, by considering different features: polymorphism, process mobility, and recursion. △ Less

Submitted 22 June, 2021; originally announced June 2021.

Jolie & LEMMA: Model-Driven Engineering and Programming Languages Meet on Microservices

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, Sabine Sachweh

Abstract: In the field of microservices, Model-Driven Engineering has emerged as a powerful methodology for architectural design, and new programming languages have introduced language abstractions to deal with microservice development more effectively. In this article, we present the first preliminary investigation of how the two approaches can be married, taking the LEMMA framework and the Jolie programmi… ▽ More In the field of microservices, Model-Driven Engineering has emerged as a powerful methodology for architectural design, and new programming languages have introduced language abstractions to deal with microservice development more effectively. In this article, we present the first preliminary investigation of how the two approaches can be married, taking the LEMMA framework and the Jolie programming language as respective representatives. By developing a conceptual metamodel for Jolie, we elicit a strong link between the two approaches, which shows that there is much to gain. We discuss a few low-hanging fruits that come from our finding and present some interesting future directions that arise from our new viewpoint. △ Less

Submitted 6 April, 2021; originally announced April 2021.

Sliceable Monolith: Monolith First, Microservices Later

Authors: Fabrizio Montesi, Marco Peressotti, Valentino Picotti

Abstract: We propose Sliceable Monolith, a new methodology for developing microservice architectures and perform their integration testing by leveraging most of the simplicity of a monolith: a single codebase and a local execution environment that simulates distribution. Then, a tool compiles a codebase for each microservice and a cloud deployment configuration. The key enabler of our approach is the techno… ▽ More We propose Sliceable Monolith, a new methodology for developing microservice architectures and perform their integration testing by leveraging most of the simplicity of a monolith: a single codebase and a local execution environment that simulates distribution. Then, a tool compiles a codebase for each microservice and a cloud deployment configuration. The key enabler of our approach is the technology-agnostic service definition language offered by Jolie. △ Less

Submitted 17 July, 2021; v1 submitted 17 March, 2021; originally announced March 2021.

Certifying Choreography Compilation

Authors: Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreograph… ▽ More Choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion. △ Less

Submitted 26 August, 2021; v1 submitted 21 February, 2021; originally announced February 2021.

Formalising a Turing-Complete Choreographic Language in Coq

Authors: Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

Abstract: Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our… ▽ More Theory of choreographic languages typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of them lead to long reviewing processes, and occasionally to errors being found in published proofs. In this work, we take a published proof of Turing completeness of a choreographic language and formalise it in Coq. Our development includes formalising the choreographic language and its basic properties, Kleene's theory of partial recursive functions, the encoding of these functions as choreographies, and proving this encoding correct. With this effort, we show that theorem proving can be a very useful tool in the field of choreographic languages: besides the added degree of confidence that we get from a mechanised proof, the formalisation process led us to a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages. △ Less

Submitted 4 February, 2021; originally announced February 2021.

Choral: Object-Oriented Choreographic Programming

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti

Abstract: We present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies ar… ▽ More We present Choral, the first choreographic programming language based on mainstream abstractions. The key idea in Choral is a new notion of data type, which allows for expressing that data is distributed over different roles. We use this idea to reconstruct the paradigm of choreographic programming through object-oriented abstractions. Choreographies are classes, and instances of choreographies are objects with states and behaviours implemented collaboratively by roles. Choral comes with a compiler that, given a choreography, generates an implementation for each of its roles. These implementations are libraries in pure Java, whose types are under the control of the Choral programmer. Developers can then modularly compose these libraries in their own programs, in order to participate correctly in choreographies. Choral is the first incarnation of choreographic programming offering such modularity, which finally connects more than a decade of research on the paradigm to practical software development. The integration of choreographic and object-oriented programming yields other powerful advantages, where the features of one paradigm benefit the other in ways that go beyond the sum of the parts. The high-level abstractions and static checks from the world of choreographies can be used to write concurrent and distributed object-oriented software more concisely and correctly. We obtain a much more expressive choreographic language from object-oriented abstractions than in previous work. For example, object passing makes Choral the first higher-order choreographic programming language, whereby choreographies can be parameterised over other choreographies without any need for central coordination. Together with subtyping and generics, this allows Choral to elegantly support user-defined communication mechanisms and middleware. △ Less

Submitted 19 October, 2023; v1 submitted 19 May, 2020; originally announced May 2020.

Implementing choreography extraction

Authors: Luís Cruz-Filipe, Fabrizio Montesi, Larisa Safina

Abstract: Choreography extraction deals with the generation of a choreography (a global description of communication behaviour) from a set of local process behaviours. In this work, we implement a previously proposed theory for extraction and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introdu… ▽ More Choreography extraction deals with the generation of a choreography (a global description of communication behaviour) from a set of local process behaviours. In this work, we implement a previously proposed theory for extraction and show that, in spite of its theoretical exponential complexity, it is usable in practice. We discuss the data structures needed for an efficient implementation, introduce some optimizations, and perform a systematic practical evaluation. △ Less

Submitted 25 October, 2019; originally announced October 2019.

Ephemeral Data Handling in Microservices - Technical Report

Authors: Saverio Giallorenzo, Fabrizio Montesi, Larisa Safina, Stefano Pio Zingaro

Abstract: In modern application areas for software systems --- like eHealth, the Internet-of-Things, and Edge Computing --- data is encoded in heterogeneous, tree-shaped data-formats, it must be processed in real-time, and it must be ephemeral, i.e., not persist in the system. While it is preferable to use a query language to express complex data-handling logic, their typical execution engine, a database ex… ▽ More In modern application areas for software systems --- like eHealth, the Internet-of-Things, and Edge Computing --- data is encoded in heterogeneous, tree-shaped data-formats, it must be processed in real-time, and it must be ephemeral, i.e., not persist in the system. While it is preferable to use a query language to express complex data-handling logic, their typical execution engine, a database external from the main application, is unfit in scenarios of ephemeral data-handling. A better option is represented by integrated query frameworks, which benefit from existing development support tools (e.g., syntax and type checkers) and execute within the application memory. In this paper, we propose one such framework that, for the first time, targets tree-shaped, document-oriented queries. We formalise an instantiation of MQuery, a sound variant of the widely-used MongoDB query language, which we implemented in the Jolie language. Jolie programs are microservices, the building blocks of modern software systems. Moreover, since Jolie supports native tree data-structures and automatic management of heterogeneous data-encodings, we can provide a uniform way to use MQuery on any data-format supported by the language. We present a non-trivial use case from eHealth, use it to concretely evaluate our model, and to illustrate our formalism. △ Less

Submitted 25 April, 2019; originally announced April 2019.

Taking Linear Logic Apart

Authors: Wen Kokke, Fabrizio Montesi, Marco Peressotti

Abstract: Process calculi based on logic, such as $π$DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the $π$-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. (2019) introduced Hypersequent Cl… ▽ More Process calculi based on logic, such as $π$DILL and CP, provide a foundation for deadlock-free concurrent programming. However, in previous work, there is a mismatch between the rules for constructing proofs and the term constructors of the $π$-calculus: the fundamental operator for parallel composition does not correspond to any rule of linear logic. Kokke et al. (2019) introduced Hypersequent Classical Processes (HCP), which addresses this mismatch using hypersequents (collections of sequents) to register parallelism in the typing judgements. However, the step from CP to HCP is a big one. As of yet, HCP does not have reduction semantics, and the addition of delayed actions means that CP processes interpreted as HCP processes do not behave as they would in CP. We introduce HCP-, a variant of HCP with reduction semantics and without delayed actions. We prove progress, preservation, and termination, and show that HCP- supports the same communication protocols as CP. △ Less

Submitted 15 April, 2019; originally announced April 2019.

Comments: In Proceedings Linearity-TLLA 2018, arXiv:1904.06159

ACM Class: D.3.1; D.3.2; F.3.2; F.4.1

Journal ref: EPTCS 292, 2019, pp. 90-103

No more, no less - A formal model for serverless computing

Authors: Maurizio Gabbrielli, Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Marco Peressotti, Stefano Pio Zingaro

Abstract: Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution an… ▽ More Serverless computing, also known as Functions-as-a-Service, is a recent paradigm aimed at simplifying the programming of cloud applications. The idea is that developers design applications in terms of functions, which are then deployed on a cloud infrastructure. The infrastructure takes care of executing the functions whenever requested by remote clients, dealing automatically with distribution and scaling with respect to inbound traffic. While vendors already support a variety of programming languages for serverless computing (e.g. Go, Java, Javascript, Python), as far as we know there is no reference model yet to formally reason on this paradigm. In this paper, we propose the first formal programming model for serverless computing, which combines ideas from both the $λ$-calculus (for functions) and the $π$-calculus (for communication). To illustrate our proposal, we model a real-world serverless system. Thanks to our model, we are also able to capture and pinpoint the limitations of current vendor technologies, proposing possible amendments. △ Less

Submitted 1 May, 2019; v1 submitted 19 March, 2019; originally announced March 2019.

Better Late Than Never: A Fully Abstract Semantics for Classical Processes

Authors: Wen Kokke, Fabrizio Montesi, Marco Peressotti

Abstract: We present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of… ▽ More We present Hypersequent Classical Processes (HCP), a revised interpretation of the "Proofs as Processes" correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by $\otimes$ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini's theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide. △ Less

Submitted 6 November, 2018; originally announced November 2018.

Multiparty Classical Choreographies

Authors: Marco Carbone, Luis Cruz-Filipe, Fabrizio Montesi, Agata Murawska

Abstract: We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multipar… ▽ More We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logic-driven compilation of choreographies with replicated processes. △ Less

Submitted 2 December, 2018; v1 submitted 15 August, 2018; originally announced August 2018.

Comments: Post-proceedings paper presented at the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), Frankfurt am Main, Germany, 4-6 September 2018 (arXiv:1808.03326) The paper was improved and extended (+2 pages). Now more details are provided on the work

Report number: LOPSTR/2018/24

Connectors meet Choreographies

Authors: Farhad Arbab, Luís Cruz-Filipe, Sung-Shik Jongmans, Fabrizio Montesi

Abstract: We present Cho-Reo-graphies (CR), a new language model that unites two powerful programming paradigms for concurrent software based on communicating processes: Choreographic Programming and Exogenous Coordination. In CR, programmers specify the desired communications among processes using a choreography, and define how communications should be concretely animated by connectors given as constraint… ▽ More We present Cho-Reo-graphies (CR), a new language model that unites two powerful programming paradigms for concurrent software based on communicating processes: Choreographic Programming and Exogenous Coordination. In CR, programmers specify the desired communications among processes using a choreography, and define how communications should be concretely animated by connectors given as constraint automata (e.g., synchronous barriers and asynchronous multi-casts). CR is the first choreography calculus where different communication semantics (determined by connectors) can be freely mixed; since connectors are user-defined, CR also supports many communication semantics that were previously unavailable for choreographies. We develop a static analysis that guarantees that a choreography in CR and its user-defined connectors are compatible, define a compiler from choreographies to a process calculus based on connectors, and prove that compatibility guarantees deadlock-freedom of the compiled process implementations. △ Less

Submitted 24 April, 2018; originally announced April 2018.

Classical Transitions

Authors: Fabrizio Montesi, Marco Peressotti

Abstract: We introduce the calculus of Classical Transitions (CT), which extends the research line on the relationship between linear logic and processes to labelled transitions. The key twist from previous work is registering parallelism in typing judgements, by generalising linear logic judgements from one sequents to many (hypersequents). This allows us to bridge the gap between the structures of operato… ▽ More We introduce the calculus of Classical Transitions (CT), which extends the research line on the relationship between linear logic and processes to labelled transitions. The key twist from previous work is registering parallelism in typing judgements, by generalising linear logic judgements from one sequents to many (hypersequents). This allows us to bridge the gap between the structures of operators used as proof terms in previous work and those of the standard π-calculus (in particular parallel operator and restriction). The proof theory of CT allows for new proof transformations, which we show correspond to a labelled transition system (LTS) for processes. We prove that CT enjoys subject reduction and progress. △ Less

Submitted 2 March, 2018; originally announced March 2018.

Comments: IMADA-preprint

Classical Higher-Order Processes

Authors: Fabrizio Montesi

Abstract: Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session types and propositions in linear logic. Desirable properties such as type preservation under reductions and progress come for free from the metatheory of… ▽ More Classical Processes (CP) is a calculus where the proof theory of classical linear logic types communicating processes with mobile channels, a la pi-calculus. Its construction builds on a recent propositions as types correspondence between session types and propositions in linear logic. Desirable properties such as type preservation under reductions and progress come for free from the metatheory of linear logic. We contribute to this research line by extending CP with code mobility. We generalise classical linear logic to capture higher-order (linear) reasoning on proofs, which yields a logical reconstruction of (a variant of) the Higher-Order pi-calculus (HOpi). The resulting calculus is called Classical Higher-Order Processes (CHOP). We explore the metatheory of CHOP, proving that its semantics enjoys type preservation and progress (terms do not get stuck). We also illustrate the expressivity of CHOP through examples, derivable syntax sugar, and an extension to multiparty sessions. Lastly, we define a translation from CHOP to CP, which encodes mobility of process code into reference passing. △ Less

Submitted 8 February, 2018; originally announced February 2018.

Choreographies for Reactive Programming

Authors: Marco Carbone, Fabrizio Montesi, Hugo Torres Vieira

Abstract: Modular programming is a cornerstone in software development, as it allows to build complex systems from the assembly of simpler components, and support reusability and substitution principles. In a distributed setting, component assembly is supported by communication that is often required to follow a prescribed protocol of interaction. In this paper, we present a language for the modular develop… ▽ More Modular programming is a cornerstone in software development, as it allows to build complex systems from the assembly of simpler components, and support reusability and substitution principles. In a distributed setting, component assembly is supported by communication that is often required to follow a prescribed protocol of interaction. In this paper, we present a language for the modular development of distributed systems, where the assembly of components is supported by a choreography that specifies the communication protocol. Our language allows to separate component behaviour, given in terms of reactive data ports, and choreographies, specified as first class entities. This allows us to consider reusability and substitution principles for both components and choreographies. We show how our model can be compiled into a more operational perspective in a provably-correct way, and we present a typing discipline that addresses communication safety and progress of systems, where a notion of substitutability naturally arises. △ Less

Submitted 24 January, 2018; originally announced January 2018.

A Promising Future: Omission Failures in Choreographic Programming

Authors: Eva Graversen, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic programming promises a simple approach to the coding of concurrent and distributed systems: write the collective communication behaviour of a system of processes as a choreography, and then the programs for these processes are automatically compiled by a provably-correct procedure known as endpoint projection. While this promise prompted substantial research, a theory that can deal w… ▽ More Choreographic programming promises a simple approach to the coding of concurrent and distributed systems: write the collective communication behaviour of a system of processes as a choreography, and then the programs for these processes are automatically compiled by a provably-correct procedure known as endpoint projection. While this promise prompted substantial research, a theory that can deal with realistic communication failures in a distributed network remains elusive. In this work, we provide the first theory of choreographic programming that addresses realistic communication failures taken from the literature of distributed systems: processes can send or receive fewer messages than they should (send and receive omission), and the network can fail at transporting messages (omission failure). Our theory supports the programming of strategies for failure recovery, and a novel static analysis (called robustness) to check for delivery guarantees (at-most-once and exactly-once). Our key technical innovation is a deconstruction of the usual communication primitive in choreographies to allow for independent implementations of the send and receive actions of a communication, while still retaining the static guarantee that these actions will correlate correctly (the essence of choreographic programming). This has two main benefits. First, each side of a communication can adopt its own failure recovery strategy, as in realistic protocols. Second, initiating new communications does not require any (unrealistic) synchronisation over unreliable channels: senders and receivers agree by construction on how each message should be identified. We validate our design via a series of examples -- including two-phase commit, which so far eluded choreographic programming -- and an implementation of our ideas in the choreographic programming language Choral. △ Less

Submitted 17 March, 2025; v1 submitted 14 December, 2017; originally announced December 2017.

Comments: IMADA-preprint

On Asynchrony and Choreographies

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only argued informally. In this w… ▽ More Choreographic Programming is a paradigm for the development of concurrent software, where deadlocks are prevented syntactically. However, choreography languages are typically synchronous, whereas many real-world systems have asynchronous communications. Previous attempts at enriching choreographies with asynchrony rely on ad-hoc constructions, whose adequacy is only argued informally. In this work, we formalise the properties that an asynchronous semantics for choreographies should have: messages can be sent without the intended receiver being ready, and all sent messages are eventually received. We explore how out-of-order execution, used in choreographies for modelling concurrency, can be exploited to endow choreographies with an asynchronous semantics. Our approach satisfies the properties we identified. We show how our development yields a pleasant correspondence with FIFO-based asynchronous messaging, modelled in a process calculus, and discuss how it can be adopted in more complex choreography models. △ Less

Submitted 29 November, 2017; originally announced November 2017.

Comments: In Proceedings ICE 2017, arXiv:1711.10708

Journal ref: EPTCS 261, 2017, pp. 76-90

Communications in Choreographies, Revisited

Authors: Luís Cruz-Filipe, Fabrizio Montesi, Marco Peressotti

Abstract: Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world sys… ▽ More Choreographic Programming is a paradigm for developing correct-by-construction concurrent programs, by writing high-level descriptions of the desired communications and then synthesising process implementations automatically. So far, choreographic programming has been explored in the monadic setting: interaction terms express point-to-point communications of a single value. However, real-world systems often rely on interactions of polyadic nature, where multiple values are communicated among two or more parties, like multicast, scatter-gather, and atomic exchanges. We introduce a new model for choreographic programming equipped with a primitive for grouped interactions that subsumes all the above scenarios. Intuitively, grouped interactions can be thought of as being carried out as one single interaction. In practice, they are implemented by processes that carry them out in a concurrent fashion. After formalising the intuitive semantics of grouped interactions, we prove that choreographic programs and their implementations are correct and deadlock-free by construction. △ Less

Submitted 28 November, 2017; originally announced November 2017.

That's Enough: Asynchrony with Standard Choreography Primitives

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographies are widely used for the specification of concurrent and distributed software architectures. Since asynchronous communications are ubiquitous in real-world systems, previous works have proposed different approaches for the formal modelling of asynchrony in choreographies. Such approaches typically rely on ad-hoc syntactic terms or semantics for capturing the concept of messages in tr… ▽ More Choreographies are widely used for the specification of concurrent and distributed software architectures. Since asynchronous communications are ubiquitous in real-world systems, previous works have proposed different approaches for the formal modelling of asynchrony in choreographies. Such approaches typically rely on ad-hoc syntactic terms or semantics for capturing the concept of messages in transit, yielding different formalisms that have to be studied separately. In this work, we take a different approach, and show that such extensions are not needed to reason about asynchronous communications in choreographies. Rather, we demonstrate how a standard choreography calculus already has all the needed expressive power to encode messages in transit (and thus asynchronous communications) through the primitives of process spawning and name mobility. The practical consequence of our results is that we can reason about real-world systems within a choreography formalism that is simpler than those hitherto proposed. △ Less

Submitted 27 November, 2017; v1 submitted 23 November, 2017; originally announced November 2017.

Microservices: a Language-based Approach

Authors: Claudio Guidi, Ivan Lanese, Manuel Mazzara, Fabrizio Montesi

Abstract: Microservices is an emerging development paradigm where software is obtained by composing autonomous entities, called (micro)services. However, microservice systems are currently developed using general-purpose programming languages that do not provide dedicated abstractions for service composition. Instead, current practice is focused on the deployment aspects of microservices, in particular by u… ▽ More Microservices is an emerging development paradigm where software is obtained by composing autonomous entities, called (micro)services. However, microservice systems are currently developed using general-purpose programming languages that do not provide dedicated abstractions for service composition. Instead, current practice is focused on the deployment aspects of microservices, in particular by using containerization. In this chapter, we make the case for a language-based approach to the engineering of microservice architectures, which we believe is complementary to current practice. We discuss the approach in general, and then we instantiate it in terms of the Jolie programming language. △ Less

Submitted 26 April, 2017; originally announced April 2017.

The Paths to Choreography Extraction

Authors: Luís Cruz-Filipe, Kim S. Larsen, Fabrizio Montesi

Abstract: Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most existing… ▽ More Choreographies are global descriptions of interactions among concurrent components, most notably used in the settings of verification (e.g., Multiparty Session Types) and synthesis of correct-by-construction software (Choreographic Programming). They require a top-down approach: programmers first write choreographies, and then use them to verify or synthesize their programs. However, most existing software does not come with choreographies yet, which prevents their application. To attack this problem, we propose a novel methodology (called choreography extraction) that, given a set of programs or protocol specifications, automatically constructs a choreography that describes their behavior. The key to our extraction is identifying a set of paths in a graph that represents the symbolic execution of the programs of interest. Our method improves on previous work in several directions: we can now deal with programs that are equipped with a state and internal computation capabilities; time complexity is dramatically better; we capture programs that are correct but not necessarily synchronizable, i.e., they work because they exploit asynchronous communication. △ Less

Submitted 20 February, 2017; v1 submitted 31 October, 2016; originally announced October 2016.

Circuit Breakers, Discovery, and API Gateways in Microservices

Authors: Fabrizio Montesi, Janine Weber

Abstract: We review some of the most widely used patterns for the programming of microservices: circuit breaker, service discovery, and API gateway. By systematically analysing different deployment strategies for these patterns, we reach new insight especially for the application of circuit breakers. We also evaluate the applicability of Jolie, a language for the programming of microservices, for these patt… ▽ More We review some of the most widely used patterns for the programming of microservices: circuit breaker, service discovery, and API gateway. By systematically analysing different deployment strategies for these patterns, we reach new insight especially for the application of circuit breakers. We also evaluate the applicability of Jolie, a language for the programming of microservices, for these patterns and report on other standard frameworks offering similar solutions. Finally, considerations for future developments are presented. △ Less

Submitted 21 September, 2016; v1 submitted 19 September, 2016; originally announced September 2016.

Microservices: yesterday, today, and tomorrow

Authors: Nicola Dragoni, Saverio Giallorenzo, Alberto Lluch Lafuente, Manuel Mazzara, Fabrizio Montesi, Ruslan Mustafin, Larisa Safina

Abstract: Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Before presenting the current state-of-the-art in the field, this chapter reviews the history of software architecture, the reasons that led to the diffusion of objects and services first, and microservices later. Finally, open problems and future challenges are introduced.… ▽ More Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Before presenting the current state-of-the-art in the field, this chapter reviews the history of software architecture, the reasons that led to the diffusion of objects and services first, and microservices later. Finally, open problems and future challenges are introduced. This survey primarily addresses newcomers to the discipline, while offering an academic viewpoint on the topic. In addition, we investigate some practical issues and point out some potential solutions. △ Less

Submitted 20 April, 2017; v1 submitted 13 June, 2016; originally announced June 2016.

Choreographies in Practice

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O operations in programs, called choreographies, and then mechanically synthesise distributed implementations in terms of standard process models via a mechanism known as EndPoint Projection (EPP). Despite the promise of… ▽ More Choreographic Programming is a development methodology for concurrent software that guarantees correctness by construction. The key to this paradigm is to disallow mismatched I/O operations in programs, called choreographies, and then mechanically synthesise distributed implementations in terms of standard process models via a mechanism known as EndPoint Projection (EPP). Despite the promise of choreographic programming, there is still a lack of practical evaluations that illustrate the applicability of choreographies to concrete computational problems with standard concurrent solutions. In this work, we explore the potential of choreographies by using Procedural Choreographies (PC), a model that we recently proposed, to write distributed algorithms for sorting (Quicksort), solving linear equations (Gaussian elimination), and computing Fast Fourier Transform. We discuss the lessons learned from this experiment, giving possible directions for the usage and future improvements of choreography languages. △ Less

Submitted 29 February, 2016; originally announced February 2016.

Refinement types in Jolie

Authors: Alexander Tchitchigin, Larisa Safina, Manuel Mazzara, Mohamed Elwakil, Fabrizio Montesi, Victor Rivera

Abstract: Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially maliciou… ▽ More Jolie is the first language for microservices and it is currently dynamically type checked. This paper considers the opportunity to integrate dynamic and static type checking with the introduction of refinement types, verified via SMT solver. The integration of the two aspects allows a scenario where the static verification of internal services and the dynamic verification of (potentially malicious) external services cooperates in order to reduce testing effort and enhancing security. △ Less

Submitted 22 February, 2016; originally announced February 2016.

A Language for the Declarative Composition of Concurrent Protocols

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: A recent study of bugs in real-world concurrent and distributed systems found that, while implementations of individual protocols tend to be robust, the composition of multiple protocols and its interplay with internal computation is the culprit for most errors. Multiparty Session Types and Choreographic Programming are methodologies for developing correct-by-construction concurrent and distribute… ▽ More A recent study of bugs in real-world concurrent and distributed systems found that, while implementations of individual protocols tend to be robust, the composition of multiple protocols and its interplay with internal computation is the culprit for most errors. Multiparty Session Types and Choreographic Programming are methodologies for developing correct-by-construction concurrent and distributed software, based on global descriptions of communication flows. However, protocol composition is either limited or left unchecked. Inspired by these two methodologies, in this work we present a new language model for the safe composition of protocols, called Procedural Choreographies (PC). Protocols in PC are procedures, parameterised on the processes that enact them. Procedures define communications declaratively using global descriptions, and programs are written by invoking and composing these procedures. An implementation in terms of a process model is then mechanically synthesised, guaranteeing correctness and deadlock-freedom. We study PC in the settings of synchronous and asynchronous communications, and illustrate its expressivity with some representative examples. △ Less

Submitted 24 October, 2016; v1 submitted 11 February, 2016; originally announced February 2016.

Data-driven Workflows for Microservices

Authors: Larisa Safina, Manuel Mazzara, Fabrizio Montesi

Abstract: Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Jolie is a programming language based on the microservices paradigm: the main building block of Jolie systems are services, in contrast to, e.g., functions or objects. The primitives offered by the Jolie language elicit many of the recurring patterns found in microservices,… ▽ More Microservices is an architectural style inspired by service-oriented computing that has recently started gaining popularity. Jolie is a programming language based on the microservices paradigm: the main building block of Jolie systems are services, in contrast to, e.g., functions or objects. The primitives offered by the Jolie language elicit many of the recurring patterns found in microservices, like load balancers and structured processes. However, Jolie still lacks some useful constructs for dealing with message types and data manipulation that are present in service-oriented computing. In this paper, we focus on the possibility of expressing choices at the level of data types, a feature well represented in standards for Web Services, e.g., WSDL. We extend Jolie to support such type choices and show the impact of our implementation on some of the typical scenarios found in microservice systems. This shows how computation can move from a process-driven to a data-driven approach, and leads to the preliminary identification of recurring communication patterns that can be shaped as design patterns. △ Less

Submitted 9 November, 2015; originally announced November 2015.

Comments: 8 pages, 4 figures

Applied Choreographies

Authors: Saverio Giallorenzo, Fabrizio Montesi, Maurizio Gabbrielli

Abstract: Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographies. Previous work used choreographies for the synthesis of programs. Alas, there is no formalisation that provides a chain of correctness from choreogr… ▽ More Choreographic Programming is a correct-by-construction paradigm where a compilation procedure synthesises deadlock-free, concurrent, and distributed communicating processes from global, declarative descriptions of communications, called choreographies. Previous work used choreographies for the synthesis of programs. Alas, there is no formalisation that provides a chain of correctness from choreographies to their implementations. This problem originates from the gap between existing theoretical models, which abstract communications using channel names (à la CCS/π-calculus), and their implementations, which use low-level mechanisms for message routing. As a solution, we propose the theoretical framework of Applied Choreographies. In the framework, developers write choreographies in a language that follows the standard syntax and name-based communication semantics of previous works. Then, they use a compilation procedure to transform a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof in three stages, respectively dealing with: a) the translation of name-based communications into their SOC equivalents (namely, using correlation mechanisms based on message data); b) the projection of a choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes); c) the translation of partial choreographies and the distribution of choreography-level state into SOC processes. We provide results of behavioural correspondence for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful and deadlock-free service-oriented implementation. △ Less

Submitted 14 December, 2020; v1 submitted 13 October, 2015; originally announced October 2015.

A Core Model for Choreographic Programming

Authors: Luís Cruz-Filipe, Fabrizio Montesi

Abstract: Choreographic Programming is a programming paradigm for building concurrent programs that are deadlock-free by construction, as a result of programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographi… ▽ More Choreographic Programming is a programming paradigm for building concurrent programs that are deadlock-free by construction, as a result of programming communications declaratively and then synthesising process implementations automatically. Despite strong interest on choreographies, a foundational model that explains which computations can be performed with the hallmark constructs of choreographies is still missing. In this work, we introduce Core Choreographies (CC), a model that includes only the core primitives of choreographic programming. Every computable function can be implemented as a choreography in CC, from which we can synthesise a process implementation where independent computations run in parallel. We discuss the design of CC and argue that it constitutes a canonical model for choreographic programming. △ Less

Submitted 9 October, 2018; v1 submitted 12 October, 2015; originally announced October 2015.

Kickstarting Choreographic Programming

Authors: Fabrizio Montesi

Abstract: We present an overview of some recent efforts aimed at the development of Choreographic Programming, a programming paradigm for the production of concurrent software that is guaranteed to be correct by construction from global descriptions of communication behaviour. We present an overview of some recent efforts aimed at the development of Choreographic Programming, a programming paradigm for the production of concurrent software that is guaranteed to be correct by construction from global descriptions of communication behaviour. △ Less

Submitted 10 February, 2015; v1 submitted 9 February, 2015; originally announced February 2015.

Process-aware web programming with Jolie

Authors: Fabrizio Montesi

Abstract: We extend the Jolie programming language to capture the native modelling of process-aware web information systems, i.e., web information systems based upon the execution of business processes. Our main contribution is to offer a unifying approach for the programming of distributed architectures on the web, which can capture web servers, stateful process execution, and the composition of services v… ▽ More We extend the Jolie programming language to capture the native modelling of process-aware web information systems, i.e., web information systems based upon the execution of business processes. Our main contribution is to offer a unifying approach for the programming of distributed architectures on the web, which can capture web servers, stateful process execution, and the composition of services via mediation. We discuss applications of this approach through a series of examples that cover, e.g., static content serving, multiparty sessions, and the evolution of web systems. Finally, we present a performance evaluation that includes a comparison of Jolie-based web systems to other frameworks and a measurement of its scalability. △ Less

Submitted 21 April, 2016; v1 submitted 14 October, 2014; originally announced October 2014.

Comments: IMADA-preprint-cs

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

Merging Multiparty Protocols in Multiparty Choreographies

Authors: Marco Carbone, Fabrizio Montesi

Abstract: Choreography-based programming is a powerful paradigm for defining communication-based systems from a global viewpoint. A choreography can be checked against multiparty protocol specifications, given as behavioural types, that may be instantiated indefinitely at runtime. Each protocol instance is started with a synchronisation among the involved peers. We analyse a simple transformation from… ▽ More Choreography-based programming is a powerful paradigm for defining communication-based systems from a global viewpoint. A choreography can be checked against multiparty protocol specifications, given as behavioural types, that may be instantiated indefinitely at runtime. Each protocol instance is started with a synchronisation among the involved peers. We analyse a simple transformation from a choreography with a possibly unbounded number of protocol instantiations to a choreography instantiating a single protocol, which is the merge of the original ones. This gives an effective methodology for obtaining new protocols by composing existing ones. Moreover, by removing all synchronisations required for starting protocol instances, our transformation reduces the number of communications and resources needed to execute a choreography. △ Less

Submitted 26 February, 2013; originally announced February 2013.

Comments: In Proceedings PLACES 2012, arXiv:1302.5798

ACM Class: D.3.1, F.3.2

Journal ref: EPTCS 109, 2013, pp. 21-27

Reasoning About a Service-oriented Programming Paradigm

Authors: Claudio Guidi, Fabrizio Montesi

Abstract: This paper is about a new way for programming distributed applications: the service-oriented one. It is a concept paper based upon our experience in developing a theory and a language for programming services. Both the theoretical formalization and the language interpreter showed us the evidence that a new programming paradigm exists. In this paper we illustrate the basic features it is characte… ▽ More This paper is about a new way for programming distributed applications: the service-oriented one. It is a concept paper based upon our experience in developing a theory and a language for programming services. Both the theoretical formalization and the language interpreter showed us the evidence that a new programming paradigm exists. In this paper we illustrate the basic features it is characterized by. △ Less

Submitted 22 June, 2009; originally announced June 2009.

Journal ref: EPTCS 2, 2009, pp. 67-81