ABS Workshop 2023
Welcome to the website of the Fifth International ABS Workshop/Fifth Workshop on Asynchronous Programming Models, which will be held 4th – 6th October in Lyon, France, hosted by ENS de Lyon. Information about prior iterations can be found here.
Venue
The workshop will be held at a side-building of the monod site (see map)
Salle Condorcet
1 place de l’École
ENS de Lyon
Travel information is provided here. There is no registration fee. The workshop will provide free snacks and coffee for the breaks, but lunches have to be bought by the participants.
Programme and State-of-the-Art of Active Objects
You can find the collection of preprints for the State-of-the-Art of Active Object volume here. The proceedings are now published by Springer as LNCS 14360 here.
Wednesday, 04.10.23
| Time | Title | Presenter |
|---|---|---|
| 09:30 - 10:00 | Active Objects in OCaml based on Algebraic Effects Algebraic effects are a long-studied programming language allowing to implement complex control flow in a structured way. With OCaml 5, such features are finally available in a mainstream programming language, giving us a great opportunity to experiment with varied concurrency constructs implemented as simple libraries. We explore how to implement concurrency features such as futures and active objects using algebraic effects, both in theory and in practice. On the practical side, we present a library of active objects implemented in OCaml, with futures, cooperative scheduling of active objects, and thread-level parallelism. On the theoretical side, we formalize and prove the compilation of a future calculus that models our library into an effect calculus similar to the primitives available in OCaml. |
Ludovic Henrio |
| 10:30 - 11:00 | Type-Based Verification of Delegated Control in Hybrid Systems We present a post-region-based verification system for distributed hybrid models using the Hybrid Active Object concurrency model. The post-region of a method is the set of states where the physical process must be shown to be proven safe after a discrete process of this method terminates. Prior systems computed the post-region locally and, thus, were limited to systems where each object ensures its own safety. The system presented here uses a type-and-effect system to structure the interactions between objects and compute post-regions globally. Furthermore, we are able to handle hybrid systems, where control is delegated and the object and method that shape the post-region change over time. This is crucial to model cloud-based systems, where processes are dynamically started and distributed among multiple server instances. |
Eduard Kamburjan |
| 10:30 - 11:00 | Break | |
| 11:00 - 11:30 | Specification Guided Distributed Programming with Multiparty Session Types Session types are a type-theoretic approach to specifying communication protocols so that they can be verified by type-checking. This year marks 30 years since the first paper on session types, by Kohei Honda at CONCUR 1993. Since then the topic has attracted increasing interest, and and a substantial community and literature have developed. This talk explains the origin of session types and summarises resent developments in programming language extensions with session types. |
Nobuko Yoshida |
| 11:30 - 12:00 | Integrating Data Privacy Compliance in Active Object Languages As users are more and more required to share their personal data, it becomes increasingly important for applications to comply with users’ consent for the handling of their personal data. Ensuring compliance with such consent requires reasoning globally about both the flow of information and the interaction of different parties handling personal data. In this direction, privacy by design principles cultivate a philosophy that endorses the development of systems with built-in abilities to demonstrate compliance with data privacy to guarantee the protection of personal data. However, there is an apparent mismatch in adopting such imprecise principles into explicit methods that support systematic solutions that integrates data privacy in system design. In this presentation, we present an integration of privacy concepts into a core active object language, to explore how the chosen language semantics can ensure personal data handling according to users’ privacy consent. |
Chinmayi Baramashetru |
| 12:00 - 13:30 | Lunch | |
| 13:30 - 14:00 | Integrated Timed Architectural Modeling/Execution Language We discuss an integrated approach for the design, specification, automatic deployment and simulation of microservice-based applications based on the ABS language. In particular, the integration of architectural modeling inspired to TOSCA (component types/port dependencies/architectural invariants) with the ABS language (static and dynamic aspects of ABS, including component properties, e.g. speed, and their use in timed/probabilistic simulations) via dedicated annotations. This is realized by integration of the ABS toolchain with a dedicated tool, called Timed SmartDepl. Such a tool, at ABS code compile time, solves (starting from the provided architectural specification) the optimal deployment problem and produces ABS deployment orchestrations to be used in the context of timed simulations. Moreover, the potentialities and the expressive power of this approach are confirmed by further integration with external tools, e.g.: the Zephyrus tool, used by Timed SmartDepl to solve the optimal deployment problem via constraint solving, and a machine learning based predictive module, that generates in advance data to be used in a timed ABS simulation exploiting such predicted data (e.g., simulating the usage, during the day, of predicted data generated during the preceding night). |
Lorenzo Bacchiani |
| 14:00 - 14:30 | Behaviour-Oriented Concurrency in Verona Behaviour-oriented Concurrency is a new concurrency paradigm inspired by the actor model, join calculus and structural lock correlation. Programs in behaviour-oriented concurrency are expressed as tasks joining on data organised into isolated regions. Akin to actor-based concurrency, data is always accessed by a single thread of control, but in contrast to actor-based concurrency, data is decoupled from specific threads of control. Through a combination of region isolation, which can be guaranteed statically and dynamically, and scheduling, behaviour-oriented concurrency guarantees data-race freedom and deadlock-freedom. |
Tobias Wrigstad |
| 14:30 - 15:00 | Break | |
| 15:00 - 15:30 | Trace-based Deductive Verification Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a mod- ular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts. |
Marco Scaletta |
| 15:30 - 16:00 | Context-aware Trace Contracts Recent work generalized state-based method contracts to trace contracts, which permit to specify internal behavior of a procedure as a trace, such as calls or state changes. In this talk, we generalize trace contracts to context-aware trace contracts that allow to specify the call context through trace formulas, which cannot be specified with the state-based Hoare-style contracts common in deductive verification. In particular, the behavior of concurrent, asynchronous procedures depends on the call context, because of the global protocol that governs scheduling. We propose a program logic of context-aware trace contracts for specifying global behavior of asynchronous programs. We provide a sound proof system and transfer Liskov’s principle of behavioral subtyping to the analysis of asynchronous procedures. |
Eduard Kamburjan |
Thursday, 05.10.23
| Time | Title | Presenter |
|---|---|---|
| 09:30 - 10:00 | A Survey of Actor-Like Programming Models for Serverless Computing Serverless computing promises to significantly simplify cloud computing by providing Functions-as-a-Service where invocations of functions, triggered by events, are automatically scheduled for execution on compute nodes. Notably, the serverless computing model does not require the manual provisioning of virtual machines; instead, FaaS enables load-based billing and auto-scaling according to the workload, reducing costs and making scheduling more efficient. While early serverless programming models only supported stateless functions and severely restricted program composition, recently proposed systems offer greater flexibility by adopting ideas from actors, active objects, and dataflow programming. This paper presents a survey of actor-like programming abstractions for stateful serverless computing, and provides a characterization of their properties and highlights their origin. |
Jonas Spenger |
| 10:00 - 10:30 | Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent Systems Programming distributed and concurrent systems is notoriously hard. Active objects, which encapsulate operations, state and the execution thread, have been investigated by researchers to alleviate this issue. In a distributed system, message exchange among active objects or actors often coincides with network boundaries, and determines a major modularization direction for the application. Yet, certain application functionalities naturally crosscut such modularization direction. For those, structuring the application architecture around network boundaries is purely accidental and does not help reasoning about programs. Recently, multitier programming has been proposed as a programming paradigm that enables code that belongs to different peers to be developed together, in the same compilation unit. The compiler then splits the code and generates the required deployment components. In this work we explore the relation between multitier programming and active objects. Multitier programming can be considered a programming paradigm based on active objects with a focus on application domains where functionalities span multiple active objects, and allows such functionalities to be encapsulated into single object. A number of features of active objects are directly visible to programmers also in the multi- tier programming, resulting in an interesting combination of language abstractions available to developers. |
Guido Salvaneschi/Pascal Weisenburger |
| 10:30 - 11:00 | Break | |
| 11:00 - 11:30 | Actors Upgraded for Variability, Adaptability, and Determinism Rebeca modeling language is designed as an imperative actor-based language with the goal of providing an easy-to-use language for modeling concurrent and distributed systems, with formal verification support. Rebeca has been extended to support time and probability. We extend Rebeca further with inheritance, polymorphism, interface declaration, and annotation mechanisms. These features allow us to handle variability within the model, support non-disruptive model evolution, and define method priorities. This enables Rebeca to be used more effectively in different domains, like in Software Product Lines, and holistic analysis of Cyber-Physical Systems. We develop specialized analysis techniques to support these extensions, partly integrated into Afra, the model checking tool of Rebeca. |
Marjan Sirjani |
| 11:30 - 12:00 | Enforced Dependencies for Active Objects We present an active object-based language that records required and provided method completions ahead of method invocations. With this language, a programmer can use method declarations to specify the dependencies between different types of tasks. The type system makes sure that the programmer declares how to fulfil the prerequisites. Program execution corresponds to a non-deterministic simulation, consisting primarily of calls and returns. We present the grammar, dynamic semantics in the form of operational semantics rules, and a rule-based type system that checks the dependencies. The absence of cyclic task dependency can be checked at the level of method declaration. |
Violet Ka I Pun |
| 12:00 - 13:30 | Lunch | |
| 13:30 - 14:00 | Simulating User Journeys with Active Objects The servitization of business makes companies increasingly dependent on providing a carefully designed user experience for their service offerings. User journeys allow services to be modeled from the user’s perspective, but are today mainly constructed and analyzed manually. Recent work analyzing user journeys as games allow optimal service- provider strategies to be automatically derived, assuming a restricted user behavior. Complementing this work, we here develop an actor-based modeling framework for user journeys that is parametric in user behavior and service-provider strategies, using the active-object modeling language ABS. Strategies for the service provider, such as those derived for user journey games, can be automatically imported into the framework. Our work enables prescriptive simulation-based analysis, as strategies can be evaluated and compared in scenarios with rich user behavior. |
Paul Kobialka |
| 14:00 - 14:45 | Embedding aggregated programming constructs in the functional layer of ABS This talk provides a brief introduction to Aggregate Programming (AP) [1] – an emerging approach to the engineering of complex coordination for distributed systems, based on viewing system interactions in terms of information propagating through collectives of devices, rather than in terms of individual devices and their interaction with their peers and environment. The foundation of this approach is the distillation of a number of prior approaches, both formal and pragmatic, proposed under the umbrella of field-based coordination, and culminating into the Field Calculus (FC) [2] and its recently proposed extension called the eXchange Calculus (XC) [3] – two core calculi capturing the essential elements of AP, much as lambda-calculus captures the essence of functional programming and Featherweight Java the essence of class-based object-oriented programming. The talk aims to trigger a discussion on the issue posed in the title. [1] Jacob Beal, Danilo Pianini, Mirko Viroli (2015). Aggregate Programming for the Internet of Things. Computer 48(9): 22-30. https://doi.org/10.1109/MC.2015.261 [2] Giorgio Audrito, Mirko Viroli, Ferruccio Damiani, Danilo Pianini, Jacob Beal (2019). A Higher-Order Calculus of Computational Fields. ACM Trans. Comput. Log. 20(1): 5:1-5:55. https://doi.org/10.1145/3285956 [3] Giorgio Audrito, Roberto Casadei, Ferruccio Damiani, Guido Salvaneschi, Mirko Viroli (2022). Functional Programming for Distributed Systems with XC. ECOOP 2022: 20:1-20:28. https://doi.org/10.4230/LIPIcs.ECOOP.2022.20 |
Ferruccio Damiani |
| 14:45 - | Semi-guided Walk in Lyon and Restaurant |
Friday, 06.10.23
| Time | Title | Presenter |
|---|---|---|
| 09:30 - 10:00 | Actor-based Designs for Distributed Self-organisation Programming Self-organisation and collective adaptation are highly desired features for several kinds of large-scale distributed systems including robotic swarms, computational ecosystems, wearable collectives, and Internet-of-Things systems. These kinds of distributed processes, addressing functional and non-functional aspects of complex socio-technical systems, can emerge in an engineered/controlled way from (re)active decentralised activity and interaction across all physical and logical system devices. In the paperin the ABS SOTA volume, we study how the Actors programming model can be adopted to support collective self-organising behaviours. Specifically, we analyse the features of the Actors model that are instrumental for implementing the adaptive coordination of large-scale systems, and discuss potential actor-based designs. Then, we discuss an incarnation of the approach in the aggregate computing paradigm, which stands as a comprehensive engineering approach for self-organisation. This is based on Akka, and can be fully programmed in the Scala programming language thanks to the ScaFi aggregate computing toolkit. |
Ferruccio Damiani |
| 10:00 - 10:30 | Predicting Resource Consumption of Kubernetes Container Systems using Resource Models Cloud computing has radically changed the way organisations operate their software by allowing them to achieve high availability of services at affordable cost. Containerized microservices is an enabling technology for this change, and advanced container orchestration platforms such as Kubernetes are used for service management. Despite the flourishing ecosystem of monitoring tools for such orchestration platforms, service management is still mainly a manual effort. The modeling of cloud computing systems is an essential step towards automatic management, but the modeling of cloud systems of such complexity remains challenging and, as yet, unaddressed. In fact modeling resource consumption will be a key to comparing the outcome of possible deployment scenarios. This paper considers how to derive resource models for cloud systems empirically. We do so based on models of deployed services in a formal modeling language with explicit CPU and memory resources; once the adherence to the real system is good enough, formal properties can be verified in the model. Targeting a likely microservices application, we present a model of Kubernetes developed in Real-Time ABS. We report on leveraging data collected empirically from small deployments to simulate the execution of higher intensity scenarios on larger deployments. We discuss the challenges and limitations that arise from this approach, and identify constraints under which we obtain satisfactory accuracy. |
Einar Broch Johnsen |
| 10:30 - 11:00 | Break | |
| 11:00 - 11:30 | Automatic Data Dependence Analysis by Deductive Verification Parallelization of programs relies on sound and precise analysis of data dependences in the code, specifically, when dealing with loops. State-of-art tools tend to over- and, occasionally, to under-approximate dependences. The former misses parallelization opportunities, the latter can change the behavior of the parallelized program. We have developed a sound and highly precise approach to generate data dependences based on deductive verification. We implemented our approach in KeY. The evaluation shows that our approach can generate highly precise data dependences for representative code taken from HPC applications. |
Asmae Heydari Tabar |
| 11:30 - 11:45 | Current Work, Recent Releases and Status of ABS | Eduard Kamburjan/Rudolf Schlatte |
| 11:30 - 11:45 | Closing | |
| 12:00 - 13:30 | Lunch |
Organizers
If there are any inquiries or questions, feel free to contact the organizers:
- Local Organization: Ludovic Henrio
- General Organization: Eduard Kamburjan