-
Serverless Scheduling Policies based on Cost Analysis
Authors:
Giuseppe De Palma,
Saverio Giallorenzo,
Cosimo Laneve,
Jacopo Mauro,
Matteo Trentin,
Gianluigi Zavattaro
Abstract:
Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such policies may decrease the performance and the security of the application due to locality issues (e.g., functions executed by workers far from the databases to be accessed). These limitations are partially overcome by the…
▽ More
Current proprietary and open-source serverless platforms follow opinionated, hardcoded scheduling policies to deploy the functions to be executed over the available workers. Such policies may decrease the performance and the security of the application due to locality issues (e.g., functions executed by workers far from the databases to be accessed). These limitations are partially overcome by the adoption of APP, a new platform-agnostic declarative language that allows serverless platforms to support multiple scheduling logics. Defining the "right" scheduling policy in APP is far from being a trivial task since it often requires rounds of refinement involving knowledge of the underlying infrastructure, guesswork, and empirical testing. In this paper, we start investigating how information derived from static analysis could be incorporated into APP scheduling function policies to help users select the best-performing workers at function allocation. We substantiate our proposal by presenting a pipeline able to extract cost equations from functions' code, synthesising cost expressions through the usage of off-the-shelf solvers, and extending APP allocation policies to consider this information.
△ Less
Submitted 31 October, 2023;
originally announced October 2023.
-
Pacta sunt servanda: legal contracts in Stipula
Authors:
Silvia Crafa,
Cosimo Laneve,
Giovanni Sartor
Abstract:
There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal content. We then undertake a foundational study of legal contracts and we distill four main features: agreement, permissions, violations and obligations. We therefore design Stipula, a domain specific language that assists la…
▽ More
There is a growing interest in running legal contracts on digital systems, at the same time, it is important to understand to what extent software contracts may capture legal content. We then undertake a foundational study of legal contracts and we distill four main features: agreement, permissions, violations and obligations. We therefore design Stipula, a domain specific language that assists lawyers in programming legal contracts through specific patterns. The language is based on a small set of abstractions that correspond to common patterns in legal contracts, and that are amenable to be executed either on centralized or on distributed systems. Stipula comes with a formal semantics and an observational equivalence, that provide for a clear account of the contracts' behaviour. The expressive power of the language is illustrated by a set of examples that correspond to template contracts that are often used in practice.
△ Less
Submitted 21 October, 2021;
originally announced October 2021.
-
Analysis of SLA Compliance in the Cloud -- An Automated, Model-based Approach
Authors:
Frank S. de Boer,
Elena Giachino,
Stijn de Gouw,
Reiner Hähnle,
Einar Broch Johnsen,
Cosimo Laneve,
Ka I Pun,
Gianluigi Zavattaro
Abstract:
Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study.…
▽ More
Service Level Agreements (SLA) are commonly used to specify the quality attributes between cloud service providers and the customers. A violation of SLAs can result in high penalties. To allow the analysis of SLA compliance before the services are deployed, we describe in this paper an approach for SLA-aware deployment of services on the cloud, and illustrate its workflow by means of a case study. The approach is based on formal models combined with static analysis tools and generated runtime monitors. As such, it fits well within a methodology combining software development with information technology operations (DevOps).
△ Less
Submitted 27 August, 2019;
originally announced August 2019.
-
Deadlock detection of Java Bytecode
Authors:
Abel Garcia,
Cosimo Laneve
Abstract:
This paper presents a technique for deadlock detection of Java programs. The technique uses ty** rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language -- the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is…
▽ More
This paper presents a technique for deadlock detection of Java programs. The technique uses ty** rules for extracting infinite-state abstract models of the dependencies among the components of the Java intermediate language -- the Java bytecode. Models are subsequently analysed by means of an extension of a solver that we have defined for detecting deadlocks in process calculi. Our technique is complemented by a prototype verifier that also covers most of the Java features.
△ Less
Submitted 13 September, 2017;
originally announced September 2017.
-
Time complexity of concurrent programs
Authors:
Elena Giachino,
Einar Broch Johnsen,
Cosimo Laneve,
Ka I Pun
Abstract:
We study the problem of automatically computing the time complexity of concurrent object-oriented programs. To determine this complexity we use intermediate abstract descriptions that record relevant information for the time analysis (cost of statements, creations of objects, and concurrent operations), called behavioural types. Then, we define a translation function that takes behavioural types a…
▽ More
We study the problem of automatically computing the time complexity of concurrent object-oriented programs. To determine this complexity we use intermediate abstract descriptions that record relevant information for the time analysis (cost of statements, creations of objects, and concurrent operations), called behavioural types. Then, we define a translation function that takes behavioural types and makes the parallelism explicit into so-called cost equations, which are fed to an automatic off-the-shelf solver for obtaining the time complexity.
△ Less
Submitted 16 November, 2015;
originally announced November 2015.
-
A framework for deadlock detection in core ABS
Authors:
Elena Giachino,
Cosimo Laneve,
Michael Lienhardt
Abstract:
We present a framework for statically detecting deadlocks in a concurrent object-oriented language with asynchronous method calls and cooperative scheduling of method activations. Since this language features recursion and dynamic resource creation, deadlock detection is extremely complex and state-of-the-art solutions either give imprecise answers or do not scale. In order to augment precision an…
▽ More
We present a framework for statically detecting deadlocks in a concurrent object-oriented language with asynchronous method calls and cooperative scheduling of method activations. Since this language features recursion and dynamic resource creation, deadlock detection is extremely complex and state-of-the-art solutions either give imprecise answers or do not scale. In order to augment precision and scalability we propose a modular framework that allows several techniques to be combined. The basic component of the framework is a front-end inference algorithm that extracts abstract behavioural descriptions of methods, called contracts, which retain resource dependency information. This component is integrated with a number of possible different back-ends that analyse contracts and derive deadlock information. As a proof-of-concept, we discuss two such back-ends: (i) an evaluator that computes a fixpoint semantics and (ii) an evaluator using abstract model checking.
△ Less
Submitted 16 November, 2015;
originally announced November 2015.
-
Decidability Problems for Actor Systems
Authors:
Frank De Boer,
Mahdi Jaghoori,
Cosimo Laneve,
Gianluigi Zavattaro
Abstract:
We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still…
▽ More
We introduce a nominal actor-based language and study its expressive power. We have identified the presence/absence of fields as a crucial feature: the dynamic creation of names in combination with fields gives rise to Turing completeness. On the other hand, restricting to stateless actors gives rise to systems for which properties such as termination are decidable. This decidability result still holds for actors with states when the number of actors is bounded and the state is read-only.
△ Less
Submitted 3 December, 2014; v1 submitted 17 September, 2014;
originally announced September 2014.
-
Deadlock detection in linear recursive programs
Authors:
Elena Giachino,
Cosimo Laneve
Abstract:
Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale.
We define an algorithm for detecting deadlocks of "linear recursive programs" of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called "mutations", which transform t…
▽ More
Deadlock detection in recursive programs that admit dynamic resource creation is extremely complex and solutions either give imprecise answers or do not scale.
We define an algorithm for detecting deadlocks of "linear recursive programs" of a basic model. The theory that underpins the algorithm is a generalization of the theory of permutations of names to so-called "mutations", which transform tuples by introducing duplicates and fresh names.
Our algorithm realizes the back-end of deadlock analyzers for object-oriented programming languages, once the association programs/basic-model-programs has been defined as front-end.
△ Less
Submitted 28 October, 2013;
originally announced October 2013.
-
Reversibility in Massive Concurrent Systems
Authors:
Luca Cardelli,
Cosimo Laneve
Abstract:
Reversing a (forward) computation history means undoing the history. In concurrent systems, undoing the history is not performed in a deterministic way but in a causally consistent fashion, where states that are reached during a backward computation are states that could have been reached during the computation history by just performing independent actions in a different order.
Reversing a (forward) computation history means undoing the history. In concurrent systems, undoing the history is not performed in a deterministic way but in a causally consistent fashion, where states that are reached during a backward computation are states that could have been reached during the computation history by just performing independent actions in a different order.
△ Less
Submitted 17 August, 2011;
originally announced August 2011.
