Fabrizio Montesi

Matteo Acclavio, Fabrizio Montesi, Marco Peressotti

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.

Viktor Strate Kløvedal, Dan Plyukhin, Marco Peressotti et al.

In service-oriented architecture, services coordinate in one of two ways: directly, using point-to-point communication, or indirectly, through an intermediary called the orchestrator. Orchestrators tend to be more popular because their local state is a 'single source of truth' for the status of ongoing workflows, which simplifies fault recovery and rollback for distributed transactions that use the 'saga' pattern. But orchestration is not always an option because of hardware constraints and security policies. Without a central orchestrator, resilient saga transactions are hard to implement correctly. A natural idea is to use choreographic programming, a paradigm that brings the 'global view' of orchestrators to a decentralised setting. Unfortunately, choreographic programming relies on strong assumptions about network reliability and service uptime that often do not hold. Recent work weakens some of these assumptions with 'failure-aware' language features, but these features make programs more complex. We propose a complementary approach: to co-design the programming interface with a customizable runtime that can replay computation to mask faults. Our approach keeps programs simple, does not require modifying the compiler, and lends itself to a clean separation of concerns in formal proofs. We present Accompanist, a resilient runtime for the Choral choreographic programming language. With Accompanist, programmers can implement decentralised saga transactions as choreographic programs and deploy the compiled code to 'sidecars' that run alongside services in a pre-existing codebase. Our key assumptions are that choreographic programs should be deterministic, transactions within a saga should be idempotent, and messages should be written to a durable message queue. Based on these assumptions, we present a formal model and prove that target code is correct-by-construction.

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti et al.

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.

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti et al.

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.

Fabrizio Montesi, Marco Peressotti, Valentino Picotti

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.

Claudio Guidi, Ivan Lanese, Manuel Mazzara et al.

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.

Fabrizio Montesi, Janine Weber

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.

Nicola Dragoni, Saverio Giallorenzo, Alberto Lluch Lafuente et al.

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.

Alexander Tchitchigin, Larisa Safina, Manuel Mazzara et al.

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.