Coordination models and languages : 23rd IFIP WG 6.1 international conference, COORDINATION 2021 : held as part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021 : Valletta, Malta, June 14-18, 2021 : proceed

This book constitutes the refereed proceedings of the 23rd IFIP WG 6.1 International Conference on Coordination Models and Language, COORDINATION 2021, held in Valletta, Malta, in June 2021, as part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021. The 15 regular papers, 2 short papers, and 1 tutorial paper presented in this book were carefully reviewed and selected from 31 submissions. COORDINATION provides a well-established forum for the growing community of researchers interested in coordination models and languages, architectures, verification and implementation techniques necessary to cope with the complexity induced by the demands of today's software development. The tool papers describe experience reports, technological artefacts, and innovative prototypes, as well as educational tools in the scope of the research topics of the conference. Due to the Corona pandemic this event was held virtually. Foreword Preface Organization Let it Flow: Reactive Computations for Consistent-by-Design Distributed Applications (Abstract of Invited Talk) Contents Tutorial Modeling and Analyzing Resource-Sensitive Actors: A Tutorial Introduction 1 Introduction 2 The ABS Language 2.1 A Simple ABS Model 3 Specifying Time and Resource Behavior 3.1 Example: Phone Services on New Year's Eve 4 Advanced Synchronization Patterns 4.1 Coordinating Multiple Processes via Object State 4.2 Synchronizing on Multiple Processes via Futures 5 Visualizations via the Model API 5.1 Exporting Objects and Methods 5.2 Adding a Custom Visualization 6 Record and Replay of Simulations 7 Case Studies and Other Analysis Tools A Installing the ABS Compiler References Communications: Types and Implemenations Manifestly Phased Communication via Shared Session Types 1 Introduction 2 Background 2.1 Linear Session Types 2.2 Shared Session Types 3 Equi-Synchronizing Rules Out Phasing 4 Subtyping 5 Phasing 5.1 Subsynchronizing Constraint 6 Metatheory 6.1 Process Typing 6.2 Processes and Configuration 6.3 Configuration Typing 6.4 Dynamics 6.5 Theorems 7 Related Work 8 Conclusion References Deconfined Global Types for Asynchronous Sessions 1 Introduction 2 A Core Calculus for Multiparty Sessions 3 Configuration Types 4 Type System 5 An Algorithm for Input/Output Matching 6 Conclusion and Future Work References Relating Functional and Imperative Session Types 1 Introduction 2 Motivation 3 VGR: Imperative Session Types 4 Linear Functional Session Types 5 Translation: Imperative to Functional 6 Translation: Functional to Imperative 6.1 Untyped Translation 6.2 Typed Backwards Translation 7 Related Work 8 Conclusion References Safe Session-Based Asynchronous Coordination in Rust 1 Introduction 2 Overview 3 Evaluation 4 Related and Future Work References A Session Subtyping Tool 1 Introduction 2 Session Subtyping 2.1 Session Types and Their Automata Representation 2.2 Synchronous Session Subtyping 2.3 Asynchronous Session Subtyping 2.4 Fair Asynchronous Session Subtyping 3 Main Functionalities of the Tool 3.1 Extensibility of the Tool 3.2 Configuration of Tool Algorithms 4 Conclusion References Towards Probabilistic Session-Type Monitoring 1 Introduction 2 Methodology 2.1 Probabilistic Session Types (PSTs) 2.2 Monitoring Sessions 3 The Tool 4 Conclusions and Discussion 4.1 Related Work 4.2 Future Work References Java Typestate Checker 1 Introduction 2 Related Work 3 Motivating Example 4 What Is the Tool Good For? 5 Future Work References Asynchronous Global Types in Co-logic Programming 1 Introduction 2 Global Types for Asynchronous Sessions 3 Co-logic Programming 4 Query Language 5 Prolog Implementation 6 Conclusion References Large-Scale Decentalised Systems Tuple-Based Coordination in Large-Scale Situated Systems 1 Introduction 2 Background and Related Work 2.1 Tuple-Based Coordination in Pervasive Systems and Space(-Time) 2.2 Spatial Tuples 3 A Model for Spatiotemporal Tuple-Based Coordination 3.1 Requirements 3.2 Computational Space-Time Model 3.3 Specifications for Spatio-Temporal Tuple Operators 3.4 Spatiotemporal Tuple-Based Coordination 4 Spatiotemporal Tuples as Aggregate Processes 4.1 Aggregate Processes 4.2 Implementing Spatiotemporal Tuples via Aggregate Processes 5 Evaluation 5.1 Simulation-Based Evaluation 5.2 Case Study: Rescue Scenario with Breadcrumbs 6 Conclusion and Future Work References A Theory of Automated Market Makers in DeFi 1 Introduction 2 A Formal Model of Automated Market Makers 2.1 AMM States 2.2 AMM Semantics 3 Structural Properties of AMMs 4 Properties of AMM Incentives 4.1 Exchange Rates 4.2 General Properties of Swap Invariants 4.3 The Arbitrage Game 4.4 Incentivizing Deposits and Swaps 5 Related Work 6 Conclusions References ReGraDa: Reactive Graph Data 1 Introduction 2 ReGraDa: Programming with Reactive Graph Data 3 Formal Syntax of ReGraDa 4 Semantics 4.1 Enabledness 4.2 Effects 4.3 Transitions 5 From ReGraDa to Cypher 6 Empirical Experiments 7 Conclusions and Future Work References Modelling: Structures and Implementations The Structure of Concurrent Process Histories 1 Introduction 1.1 Contributions and Related Work 1.2 Organization and Prerequisites 2 Monoidal Categories as Resource Theories 3 Single Object Double Categories 4 Cornerings and Crossings 5 Concurrency Through Cornering 6 Conclusions and Future Work References A Clean and Efficient Implementation of Choreography Synthesis for Behavioural Contracts 1 Introduction 2 Design 3 Specification 4 Implementation 5 Evaluation 6 Related Work 7 Conclusion References A Practical Tool-Chain for the Development of Coordination Scenarios 1 Introduction to the Peer Model Tool-Chain 2 Peer Model in a Nutshell 2.1 Core Concepts 2.2 Newly Introduced Concepts 3 Implementation of the Toolchain 4 Use Case Example 5 Evaluation 6 Conclusion and Future Work References Microservices Microservice Dynamic Architecture-Level Deployment Orchestration 1 Introduction 2 Preliminaries 2.1 The Microservice Model 2.2 Abstract Behavioral Specification Language 2.3 SmartDeployer 3 Timed Architectural Modeling/Execution Language 3.1 Case Study and Timed Characteristics of Microservice Systems 3.2 Microservice MF and MCL Calculation 3.3 Timed SmartDeployer 3.4 Modeling Service MCL 4 Global Run-Time Adaptation 4.1 Calculation of Scaling Configurations 4.2 Scaling Algorithms 5 Simulation with ABS 5.1 Simulation Results 6 Related Work and Conclusion References Jolie and LEMMA: Model-Driven Engineering and Programming Languages Meet on Microservices 1 Introduction 2 A Structured Comparison of Jolie and LEMMA 2.1 Application Programming Interfaces (APIs) 2.2 Access Points 2.3 Behaviours 3 Cross-Fertilisation and Conclusion References ScaFi-Web: A Web-Based Application for Field-Based Coordination Programming 1 Introduction 2 Motivation and Related Work 3 The ScaFi Aggregate Programming Toolchain 3.1 Field Calculus and the ScaFi DSL 3.2 The Channel Example 3.3 ScaFi Programming in Practice 4 ScaFi-Web 4.1 Architecture Details 4.2 Usage Scenarios 4.3 Roadmap to Monitoring and Control of Deployed Systems 5 Conclusion and Future Work References Author Index