18 Search Results for "Montesi, Fabrizio"

Volume

OASIcs, Volume 78

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Microservices 2017/2019, February 19-21, 2019, University of Applied Sciences and Arts Dortmund, Germany

Editors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Document
DOI: 10.4230/OASIcs.Microservices.2020-2022.3
Modular Choreographies: Bridging Alice and Bob Notation to Java

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

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)

Abstract
We present Modular Choreographies, a new choreographic programming language that features modular functions. Modular Choreographies is aimed at simplicity: its communication abstraction follows the simple tradition from the "Alice and Bob" notation. We develop a compiler toolchain that translates choreographies into modular Java libraries, which developers can use to participate correctly in choreographies. The key novelty is to compile through the Choral language, which was previously proposed to define object-oriented choreographies: our toolchain compiles Modular Choreographies to Choral, and then leverages the existing Choral compiler to generate Java code. Our work is the first to bridge the simplicity of traditional choreographic programming languages with the requirement of generating modular libraries in a mainstream language (Java).
Cite as

Luís Cruz-Filipe, Anne Madsen, Fabrizio Montesi, and Marco Peressotti. Modular Choreographies: Bridging Alice and Bob Notation to Java. In Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:OASIcs.Microservices.2020-2022.3,
  author =	{Cruz-Filipe, Lu{\'\i}s and Madsen, Anne and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Modular Choreographies: Bridging Alice and Bob Notation to Java}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{3:1--3:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.3},
  URN =		{urn:nbn:de:0030-drops-194650},
  doi =		{10.4230/OASIcs.Microservices.2020-2022.3},
  annote =	{Keywords: Choreographic Programming, Choreographies, Modularity}
}
Document
DOI: 10.4230/OASIcs.Microservices.2020-2022.6
Model-Driven Code Generation for Microservices: Service Models

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

Published in: OASIcs, Volume 111, Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)

Abstract
We formally define and implement a translation of domain and service models expressed in the LEMMA modelling ecosystem for microservice architectures to source code in the Jolie microservice programming language. Specifically, our work extends previous efforts on the generation of Jolie code to the inclusion of the LEMMA service modelling layer. We also contribute an implementation of our translation, given as an extension of the LEMMA2Jolie tool, which enables the practical application of our encoding. As a result, LEMMA2Jolie now supports a software development process whereby microservice architectures can first be designed by microservice developers in collaboration with domain experts in LEMMA, and then be automatically translated into Jolie APIs. Our tool can thus be used to enhance productivity and improve design adherence.
Cite as

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, and Florian Rademacher. Model-Driven Code Generation for Microservices: Service Models. In Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022). Open Access Series in Informatics (OASIcs), Volume 111, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:OASIcs.Microservices.2020-2022.6,
  author =	{Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian},
  title =	{{Model-Driven Code Generation for Microservices: Service Models}},
  booktitle =	{Joint Post-proceedings of the Third and Fourth International Conference on Microservices (Microservices 2020/2022)},
  pages =	{6:1--6:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-306-5},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{111},
  editor =	{Dorai, Gokila and Gabbrielli, Maurizio and Manzonetto, Giulio and Osmani, Aomar and Prandini, Marco and Zavattaro, Gianluigi and Zimmermann, Olaf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2020-2022.6},
  URN =		{urn:nbn:de:0030-drops-194688},
  doi =		{10.4230/OASIcs.Microservices.2020-2022.6},
  annote =	{Keywords: Microservices, Model-driven Engineering, Code Generation, Jolie APIs}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.11
Now It Compiles! Certified Automatic Repair of Uncompilable Protocols

Authors: Luís Cruz-Filipe and Fabrizio Montesi

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

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 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.
Cite as

Luís Cruz-Filipe and Fabrizio Montesi. Now It Compiles! Certified Automatic Repair of Uncompilable Protocols. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2023.11,
  author =	{Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio},
  title =	{{Now It Compiles! Certified Automatic Repair of Uncompilable Protocols}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.11},
  URN =		{urn:nbn:de:0030-drops-183867},
  doi =		{10.4230/LIPIcs.ITP.2023.11},
  annote =	{Keywords: choreographic programming, theorem proving, compilation, program repair}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.7
Modular Compilation for Higher-Order Functional Choreographies

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

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Choreographic programming is a paradigm for concurrent and distributed software, whereby descriptions of the intended communications (choreographies) are automatically compiled into distributed code with strong safety and liveness properties (e.g., deadlock-freedom). Recent efforts tried to combine the theories of choreographic programming and higher-order functional programming, in order to integrate the benefits of the former with the modularity of the latter. However, they do not offer a satisfactory theory of compilation compared to the literature, because of important syntactic and semantic shortcomings: compilation is not modular (editing a part might require recompiling everything) and the generated code can perform unexpected global synchronisations. In this paper, we find that these shortcomings are not mere coincidences. Rather, they stem from genuine new challenges posed by the integration of choreographies and functions: knowing which participants are involved in a choreography becomes nontrivial, and divergence in applications requires rethinking how to prove the semantic correctness of compilation. We present a novel theory of compilation for functional choreographies that overcomes these challenges, based on types and a careful design of the semantics of choreographies and distributed code. The result: a modular notion of compilation, which produces code that is deadlock-free and correct (it operationally corresponds to its source choreography).
Cite as

Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 7:1-7:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ECOOP.2023.7,
  author =	{Cruz-Filipe, Lu{\'\i}s and Graversen, Eva and Lugovi\'{c}, Lovro and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Modular Compilation for Higher-Order Functional Choreographies}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{7:1--7:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.7},
  URN =		{urn:nbn:de:0030-drops-182005},
  doi =		{10.4230/LIPIcs.ECOOP.2023.7},
  annote =	{Keywords: Choreographies, Concurrency, \lambda-calculus, Type Systems}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.ECOOP.2022.35
Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract)

Authors: David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Decentralized applications (dApps) consist of smart contracts that run on blockchains and clients that model collaborating parties. dApps are used to model financial and legal business functionality. Today, contracts and clients are written as separate programs - in different programming languages - communicating via send and receive operations. This makes distributed program flow awkward to express and reason about, increasing the potential for mismatches in the client-contract interface, which can be exploited by malicious clients, potentially leading to huge financial losses. In this paper, we present Prisma, a language for tierless decentralized applications, where the contract and its clients are defined in one unit. Pairs of send and receive actions that "belong together" are encapsulated into a single direct-style operation, which is executed differently by sending and receiving parties. This enables expressing distributed program flow via standard control flow and renders mismatching communication impossible. We prove formally that our compiler preserves program behavior in presence of an attacker controlling the client code. We systematically compare Prisma with mainstream and advanced programming models for dApps and provide empirical evidence for its expressiveness and performance. The design space of dApp programming and other multi-party languages depends on one major choice: a local model versus a global model. In a local model, parties are defined in separate programs and their interactions are encoded via send and receive effects. In a global language, parties are defined within one shared program and interactions are encoded via combined send-and-receive operations with no effects visible to the outside world. The global model is followed by tierless [Christian Queinnec, 2000; Cooper et al., 2007; Choi and Chang, 2019; Fowler et al., 2019; Serrano et al., 2006; Serrano and Prunet, 2016; Radanne et al., 2016; Weisenburger et al., 2018] and choreographic [Kohei Honda et al., 2011; Fabrizio Montesi et al., 2014; Saverio Giallorenzo et al., 2020] languages. However, known approaches to dApp programming follow the local model, thus rely on explicitly specifying the client-contract interaction protocol. Moreover, the contract and clients are implemented in different languages, hence, developers have to master two technology stacks. The dominating approach in industry is Solidity [Mix, 2019] for the contract and JavaScript for clients. Solidity relies on expressing the protocol using assertions in the contract code, which are checked at run time [Solidity documentation - common patterns, 2020]. Failing to insert the correct assertions may give parties illegal access to monetary values to the detriment of others [Nikolić et al., 2018; Luu et al., 2016]. In research, contract languages [Ankush Das et al., 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019; Reed Oei et al., 2020; Sam Blackshear et al., 2019] have been proposed that rely on advanced type systems such as session types, type states, and linear types. The global model has not been explored for dApp programming. This is unfortunate given the potential to get by with a standard typing discipline and to avoid intricacies and potential mismatches of a two-language stack. Our work fills this gap by proposing Prisma - the first language that features a global programming model for Ethereum dApps. While we focus on the Ethereum blockchain, we believe our techniques to be applicable to other smart contract platforms. Prisma enables interleaving contract and client logic within the same program and adopts a direct style (DS) notation for encoding send-and-receive operations (with our awaitCl language construct) akin to languages with async/await [Gavin M. Bierman et al., 2012; Scala async rfc]. DS addresses shortcomings with the currently dominant encoding of the protocol’s finite state machines (FSM) [Mix, 2019; Michael J. Coblenz, 2017; Franklin Schrans et al., 2018; Franklin Schrans et al., 2019; Michael J. Coblenz et al., 2019; Michael J. Coblenz et al., 2019]. We argue writing FSM style corresponds to a control-flow graph of basic blocks, which is low-level and more suited to be written by a compiler than by a human. With FSM style, the contract is a passive entity whose execution is driven by clients. whereas the DS encoding allows the contract to actively ask clients for input, fitting dApp execution where a dominant contract controls execution and diverts control to other parties when their input is needed. In the following Prisma snippet, the payout function is a function invoked by the contract when it is time to pay money to a client. In Prisma, variables, methods and classes are separated into two namespaces, one for the contract and one for the clients. The payout method is located on the contract via the annotation @co. The body of the method diverts the control to the client using awaitCl(...) { ... }, hence the contained readLine call is executed on the client. Note that no explicit send/receive operations are needed but the communication protocol is expressed through the program control flow. Only after the check client == toBePayed that the correct client replied, the current contact balance balance() is transferred to the client via transfer. @co def payout(toBePayed: Arr[Address]): Unit = { awaitCl(client => client == toBePayed) { readLine("Press enter for payout") } toBePayed.transfer(balance()) } Overall, Prisma relieves the developer from the responsibility of correctly managing distributed, asynchronous program flows and the heterogeneous technology stack. Instead, the burden is put on the compiler, which distributes the program flow by means of selective continuation-passing-style (CPS) translation and defunctionalisation and inserts guards against malicious client interactions. We needed to develop a CPS translation for the code that runs on the Ethereum Virtual Machine (EVM) since the EVM has no built-in support for concurrency primitives which could be used for asynchronous communication. While CPS translations are well-known, we cannot use them out-of-the-box because the control flow is interwoven with distribution in our case. A CPS translation that does not take distribution into account would allow malicious clients to force the contract to deviate from the intended control flow by sending a spoofed continuation. Thus, it was imperative to prove correctness of our distributed CPS translation to ensure control-flow integrity of the contract.
Cite as

David Richter, David Kretzler, Pascal Weisenburger, Guido Salvaneschi, Sebastian Faust, and Mira Mezini. Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications (Extended Abstract). In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 35:1-35:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2022.35,
  author =	{Richter, David and Kretzler, David and Weisenburger, Pascal and Salvaneschi, Guido and Faust, Sebastian and Mezini, Mira},
  title =	{{Prisma: A Tierless Language for Enforcing Contract-Client Protocols in Decentralized Applications}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{35:1--35:4},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.35},
  URN =		{urn:nbn:de:0030-drops-162632},
  doi =		{10.4230/LIPIcs.ECOOP.2022.35},
  annote =	{Keywords: Domain Specific Languages, Smart Contracts, Scala}
}
Document
Pearl
DOI: 10.4230/LIPIcs.ECOOP.2021.22
Multiparty Languages: The Choreographic and Multitier Cases (Pearl)

Authors: Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Choreographic languages aim to express multiparty communication protocols, by providing primitives that make interaction manifest. Multitier languages enable programming computation that spans across several tiers of a distributed system, by supporting primitives that allow computation to change the location of execution. Rooted into different theoretical underpinnings - respectively process calculi and lambda calculus - the two paradigms have been investigated independently by different research communities with little or no contact. As a result, the link between the two paradigms has remained hidden for long. In this paper, we show that choreographic languages and multitier languages are surprisingly similar. We substantiate our claim by isolating the core abstractions that differentiate the two approaches and by providing algorithms that translate one into the other in a straightforward way. We believe that this work paves the way for joint research and cross-fertilisation among the two communities.
Cite as

Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, David Richter, Guido Salvaneschi, and Pascal Weisenburger. Multiparty Languages: The Choreographic and Multitier Cases (Pearl). In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 22:1-22:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:LIPIcs.ECOOP.2021.22,
  author =	{Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Richter, David and Salvaneschi, Guido and Weisenburger, Pascal},
  title =	{{Multiparty Languages: The Choreographic and Multitier Cases}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{22:1--22:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.22},
  URN =		{urn:nbn:de:0030-drops-140658},
  doi =		{10.4230/LIPIcs.ECOOP.2021.22},
  annote =	{Keywords: Distributed Programming, Choreographies, Multitier Languages}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.15
Formalising a Turing-Complete Choreographic Language in Coq

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

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
The 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, its basic properties, Kleene’s theory of partial recursive functions, the encoding of these functions as choreographies, and a proof that this encoding is 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.
Cite as

Luís Cruz-Filipe, Fabrizio Montesi, and Marco Peressotti. Formalising a Turing-Complete Choreographic Language in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:LIPIcs.ITP.2021.15,
  author =	{Cruz-Filipe, Lu{\'\i}s and Montesi, Fabrizio and Peressotti, Marco},
  title =	{{Formalising a Turing-Complete Choreographic Language in Coq}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{15:1--15:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.15},
  URN =		{urn:nbn:de:0030-drops-139109},
  doi =		{10.4230/LIPIcs.ITP.2021.15},
  annote =	{Keywords: Choreographic Programming, Formalisation, Turing Completeness}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.5
The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service

Authors: Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Serverless computing is a paradigm for programming cloud applications in terms of stateless functions, executed and scaled in proportion to inbound requests. Here, we revisit SKC, a calculus capturing the essential features of serverless programming. By exploring the design space of the language, we refined the integration between the fundamental features of the two calculi that inspire SKC: the λ- and the π-calculus. That investigation led us to a revised syntax and semantics, which support an increase in the expressiveness of the language. In particular, now function names are first-class citizens and can be passed around. To illustrate the new features, we present step-by-step examples and two non-trivial use cases from artificial intelligence, which model, respectively, a perceptron and an image tagging system into compositions of serverless functions. We also illustrate how SKC supports reasoning on serverless implementations, i.e., the underlying network of communicating, concurrent, and mobile processes which execute serverless functions in the cloud. To that aim, we show an encoding from SKC to the asynchronous π-calculus and prove it correct in terms of an operational correspondence. Dedicated to Maurizio Gabbrielli, on his 60th birthday (... rob da mët ! )
Cite as

Saverio Giallorenzo, Ivan Lanese, Fabrizio Montesi, Davide Sangiorgi, and Stefano Pio Zingaro. The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 5:1-5:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{giallorenzo_et_al:OASIcs.Gabbrielli.5,
  author =	{Giallorenzo, Saverio and Lanese, Ivan and Montesi, Fabrizio and Sangiorgi, Davide and Zingaro, Stefano Pio},
  title =	{{The Servers of Serverless Computing: A Formal Revisitation of Functions as a Service}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{5:1--5:21},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.5},
  URN =		{urn:nbn:de:0030-drops-132271},
  doi =		{10.4230/OASIcs.Gabbrielli.5},
  annote =	{Keywords: Serverless computing, Process calculi, Pi-calculus}
}
Document
Complete Volume
DOI: 10.4230/OASIcs.Microservices.2017-2019
OASIcs, Volume 78, Microservices 2017/2019, Complete Volume

Authors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
OASIcs, Volume 78, Microservices 2017/2019, Complete Volume
Cite as

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 1-98, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Proceedings{cruzfilipe_et_al:OASIcs.Microservices.2017-2019,
  title =	{{OASIcs, Volume 78, Microservices 2017/2019, Complete Volume}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{1--98},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019},
  URN =		{urn:nbn:de:0030-drops-118301},
  doi =		{10.4230/OASIcs.Microservices.2017-2019},
  annote =	{Keywords: OASIcs, Volume 78, Microservices 2017/2019, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/OASIcs.Microservices.2017-2019.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Luís Cruz-Filipe, Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti, Florian Rademacher, and Sabine Sachweh

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cruzfilipe_et_al:OASIcs.Microservices.2017-2019.0,
  author =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{0:i--0:xiv},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.0},
  URN =		{urn:nbn:de:0030-drops-118225},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/OASIcs.Microservices.2017-2019.1
Using Microservices to Customize Multi-Tenant SaaS: From Intrusive to Non-Intrusive

Authors: Hui Song, Phu H. Nguyen, and Franck Chauvel

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
Customization is a widely adopted practice on enterprise software applications such as Enterprise resource planning (ERP) or Customer relation management (CRM). Software vendors deploy their enterprise software product on the premises of a customer, which is then often customized for different specific needs of the customer. When enterprise applications are moving to the cloud as mutli-tenant Software-as-a-Service (SaaS), the traditional way of on-premises customization faces new challenges because a customer no longer has an exclusive control to the application. To empower businesses with specific requirements on top of the shared standard SaaS, vendors need a novel approach to support the customization on the multi-tenant SaaS. In this paper, we summarize our two approaches for customizing multi-tenant SaaS using microservices: intrusive and non-intrusive. The paper clarifies the key concepts related to the problem of multi-tenant customization, and describes a design with a reference architecture and high-level principles. We also discuss the key technical challenges and the feasible solutions to implement this architecture. Our microservice-based customization solution is promising to meet the general customization requirements, and achieves a balance between isolation, assimilation and economy of scale.
Cite as

Hui Song, Phu H. Nguyen, and Franck Chauvel. Using Microservices to Customize Multi-Tenant SaaS: From Intrusive to Non-Intrusive. In Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 1:1-1:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{song_et_al:OASIcs.Microservices.2017-2019.1,
  author =	{Song, Hui and Nguyen, Phu H. and Chauvel, Franck},
  title =	{{Using Microservices to Customize Multi-Tenant SaaS: From Intrusive to Non-Intrusive}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{1:1--1:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.1},
  URN =		{urn:nbn:de:0030-drops-118230},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.1},
  annote =	{Keywords: Customization, Software-as-a-Service (SaaS), Microservices, Multi-tenancy, Cloud, Reference Architecture}
}
Document
DOI: 10.4230/OASIcs.Microservices.2017-2019.2
Experience Report: First Steps towards a Microservice Architecture for Virtual Power Plants in the Energy Sector

Authors: Manuel Wickert, Sven Liebehentze, and Albert Zündorf

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
Virtual Power Plants provide energy sector stakeholders a useful abstraction for distributed energy resources by aggregating them. Software systems enabling this are critical infrastructure and must handle a fast-growing number of distributed energy resources. Modern architecture such as Microservice architecture can therefore be a good choice for dealing with such scalable systems where changing market and regulation requirements are part of every day business. In this report, we outline first experiences gained during the change from the existing Virtual Power Plant software monolith to Microservice architecture.
Cite as

Manuel Wickert, Sven Liebehentze, and Albert Zündorf. Experience Report: First Steps towards a Microservice Architecture for Virtual Power Plants in the Energy Sector. In Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{wickert_et_al:OASIcs.Microservices.2017-2019.2,
  author =	{Wickert, Manuel and Liebehentze, Sven and Z\"{u}ndorf, Albert},
  title =	{{Experience Report: First Steps towards a Microservice Architecture for Virtual Power Plants in the Energy Sector}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{2:1--2:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.2},
  URN =		{urn:nbn:de:0030-drops-118247},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.2},
  annote =	{Keywords: Microservices, VPP, Virtual Power Plants, Domain Driven Design}
}
Document
DOI: 10.4230/OASIcs.Microservices.2017-2019.3
Exploring Maintainability Assurance Research for Service- and Microservice-Based Systems: Directions and Differences

Authors: Justus Bogner, Adrian Weller, Stefan Wagner, and Alfred Zimmermann

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
To ensure sustainable software maintenance and evolution, a diverse set of activities and concepts like metrics, change impact analysis, or antipattern detection can be used. Special maintainability assurance techniques have been proposed for service- and microservice-based systems, but it is difficult to get a comprehensive overview of this publication landscape. We therefore conducted a systematic literature review (SLR) to collect and categorize maintainability assurance approaches for service-oriented architecture (SOA) and microservices. Our search strategy led to the selection of 223 primary studies from 2007 to 2018 which we categorized with a threefold taxonomy: a) architectural (SOA, microservices, both), b) methodical (method or contribution of the study), and c) thematic (maintainability assurance subfield). We discuss the distribution among these categories and present different research directions as well as exemplary studies per thematic category. The primary finding of our SLR is that, while very few approaches have been suggested for microservices so far (24 of 223, ∼11%), we identified several thematic categories where existing SOA techniques could be adapted for the maintainability assurance of microservices.
Cite as

Justus Bogner, Adrian Weller, Stefan Wagner, and Alfred Zimmermann. Exploring Maintainability Assurance Research for Service- and Microservice-Based Systems: Directions and Differences. In Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 3:1-3:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bogner_et_al:OASIcs.Microservices.2017-2019.3,
  author =	{Bogner, Justus and Weller, Adrian and Wagner, Stefan and Zimmermann, Alfred},
  title =	{{Exploring Maintainability Assurance Research for Service- and Microservice-Based Systems: Directions and Differences}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{3:1--3:22},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.3},
  URN =		{urn:nbn:de:0030-drops-118255},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.3},
  annote =	{Keywords: Maintainability, Software Evolution, Quality Assurance, Service-Based Systems, SOA, Microservices, Systematic Literature Review}
}
Document
DOI: 10.4230/OASIcs.Microservices.2017-2019.4
Introduction to Microservice API Patterns (MAP)

Authors: Olaf Zimmermann, Mirko Stocker, Daniel Lübke, Cesare Pautasso, and Uwe Zdun

Published in: OASIcs, Volume 78, Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)

Abstract
The Microservice API Patterns (MAP) language and supporting website premiered under this name at Microservices 2019. MAP distills proven, platform- and technology-independent solutions to recurring (micro-)service design and interface specification problems such as finding well-fitting service granularities, rightsizing message representations, and managing the evolution of APIs and their implementations. In this paper, we motivate the need for such a pattern language, outline the language organization and present two exemplary patterns describing alternative options for representing nested data. We also identify future research and development directions.
Cite as

Olaf Zimmermann, Mirko Stocker, Daniel Lübke, Cesare Pautasso, and Uwe Zdun. Introduction to Microservice API Patterns (MAP). In Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019). Open Access Series in Informatics (OASIcs), Volume 78, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{zimmermann_et_al:OASIcs.Microservices.2017-2019.4,
  author =	{Zimmermann, Olaf and Stocker, Mirko and L\"{u}bke, Daniel and Pautasso, Cesare and Zdun, Uwe},
  title =	{{Introduction to Microservice API Patterns (MAP)}},
  booktitle =	{Joint Post-proceedings of the First and Second International Conference on Microservices (Microservices 2017/2019)},
  pages =	{4:1--4:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-137-5},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{78},
  editor =	{Cruz-Filipe, Lu{\'\i}s and Giallorenzo, Saverio and Montesi, Fabrizio and Peressotti, Marco and Rademacher, Florian and Sachweh, Sabine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.Microservices.2017-2019.4},
  URN =		{urn:nbn:de:0030-drops-118268},
  doi =		{10.4230/OASIcs.Microservices.2017-2019.4},
  annote =	{Keywords: application programming interfaces, distributed systems, enterprise application integration, service-oriented computing, software architecture}
}
  • Refine by Author
  • 11 Montesi, Fabrizio
  • 7 Peressotti, Marco
  • 6 Cruz-Filipe, Luís
  • 5 Giallorenzo, Saverio
  • 3 Rademacher, Florian
  • Show More...

  • Refine by Classification
  • 5 Applied computing → Service-oriented architectures
  • 3 Software and its engineering → Cloud computing
  • 2 Computing methodologies → Distributed programming languages
  • 2 Information systems → RESTful web services
  • 2 Software and its engineering → Concurrent programming languages
  • Show More...

  • Refine by Keyword
  • 4 Microservices
  • 3 Choreographies
  • 2 Choreographic Programming
  • 2 Linear Logic
  • 1 Cloud
  • Show More...

  • Refine by Type
  • 17 document
  • 1 volume

  • Refine by Publication Year
  • 9 2020
  • 4 2023
  • 2 2021
  • 1 2015
  • 1 2016
  • Show More...

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact