First Summer School on Distributed and Replicated Environments (DARE 2023)

Abstract of the opening session.

Slides

In this lecture we focus on the problem of conflict resolution in the context of data management systems. We overview different contexts in which conflict resolution is a key issue, from groupware to geo-replicated and local-first systems, and discuss the requirements and techniques used, from simple last-writer-wins registers to CRDTs.

Slides

In the first part of this talk, I will address what it means for a distributed program to be both efficient and correct. A distributed program is a set of processes that communicate in order to reach some common goal. Our approach to correctness is to identify, for a given application, the invariants that the program must satisfy, i.e., the properties over the program's variables that must remain true in every execution. Our approach to efficiency is characterize the minimal amount of coordination between processes that is required to guarantee those invariants, thereby maximizing parallelism and autonomy between processes. Along the way, I categorize different classes of invariants, and for each class, a protocol that guarantees it. Some classes can be enforced by each process independently; some require asynchronous coordination in the form of causal-order delivery of messages; and some (but by no means all) do require the full power of consensus. The first two classes are at the same time available and partition-tolerant; for the last one (the focus of the CAP Theorem) the programmer must make a decision, choosing between availability and partition-tolerance. Finally, we will discuss program analysis techniques for safely characterizing the amount of required coordination. In the second part of the talk, I will present Varda, a new programming language for distributed applications. Varda aims to reduce the amount of work and to improve the safety of distributed programming. Varda is designed to enable the safe composition of components, including black-box "off-the-shelf" (OTS) components. As a running example, we consider the incremental development of a sharded, geo-distributed key-value store, using OTSs such as Redis, Kafka, and RabbitMQ. A component's interface is a well-defined protocol, i.e., a set of typed messages that satisfy both a given grammar and some given invariants (an OTS is sandboxed to verify the protocol at run time). To ensure safety, two components may communicate only if their protocols are mutually compatible and they are in the same scope. The developer may evolve such a composition by interposing proxies, transparently to the existing components. The Varda compiler enforces the safety constraints, generates boiler-plate code, and applies high-level optimisations.

Slides

In distributed systems, processes need to cooperate by exchanging information. Broadcast algorithms are a fundamental abstraction for this information exchange. This lecture will discuss different variants of broadcast algorithms and their properties concerning process failure and message ordering. We will further see how to implement and reason about these algorithms in a compositional way.

Slides

Distributed systems are difficult to design, implement, and test. They must ensure correctness in the concurrent execution of a distributed set of processes, different delivery orderings of asynchronous messages, and in the existence of network and process failures. Unforeseen interleavings of concurrent events and faults can result in expected malfunctioning or outages, and it is important to detect and diagnose them. In this tutorial, we will discuss concurrency and fault-tolerance bugs in distributed systems and introduce state-of-the-art testing techniques for efficiently detecting concurrency and fault-tolerance bugs in distributed system implementations.

Slides

Distributed systems are inherently complex and exposed to failures in their components. While distributed algorithms try to do their best in handling node and network failures, it is often not possible to mask them. In the presence of failures, systems that thrive for high availability need to allow users to always submit operations and observe the local state (ensuring local-first), leading to potential divergence. Designs with Conflict-free Replicated Data Types (CRDTs) have been used extensively to guarantee that it is possible to converge to a state that reflects concurrent operations.

Slides

TODO:

Slides

Replicated list objects form the foundation of lots of collaborative software, such as multi-user text editors, spreadsheets, or graphics software. Each user needs to be able to update their own copy of the document without waiting for a network round-trip, and concurrent edits by different users need to be merged together. Although researchers have studied this problem for over 30 years, many published algorithms are broken in various ways. I will present our recent work on Fugue, a CRDT algorithm for replicated lists that avoids the interleaving problems exhibited by most other algorithms, and also talk about some of the other problems that have arisen in the history of research on collaborative text editors.

Slides

In this presentation, we embark on an exploration of the landscape of software verification, with a particular emphasis on its application in the domain of distributed programs, especially, on replicated data types. Our journey begins with an in-depth analysis of various verification strategies, spanning the spectrum from traditional paper-based proofs to fully mechanized proofs. Within the realm of mechanized proofs, we categorize the techniques into three distinct classes: interactive, auto-active, and automated verification strategies, offering a brief overview of each. In this first part of the talk, the focus lies within the domain of automated verification strategies, where we delve into the potent capabilities of SMT (Satisfiability Modulo Theories) solving. We elucidate how harnessing SMT solvers can transform software verification into an automated and efficient process for certain types of programs. In the second part of the talk, I will introduce VeriFx, a high-level functional object-oriented programming language specially designed to empower developers with automated verification features. We will dive deep into the language design of VeriFx, especially its functional collections, to understand how it leverages the Z3 SMT solver to enable automated verification without sacrificing on expressiveness. Finally, we will transition from the technical underpinnings and pivot our focus to the programmer’s perspective. I will guide you through the process of implementing and verifying conflict-free replicated data types (CRDTs) using VeriFx, offering a hands-on glimpse into the application of automated verification techniques. By the end of this talk, you will have a deeper understanding of the tools and strategies available for ensuring the correctness and reliability of distributed software.

Slides

In the first part of this talk, I will address what it means for a distributed program to be both efficient and correct. A distributed program is a set of processes that communicate in order to reach some common goal. Our approach to correctness is to identify, for a given application, the invariants that the program must satisfy, i.e., the properties over the program's variables that must remain true in every execution. Our approach to efficiency is characterize the minimal amount of coordination between processes that is required to guarantee those invariants, thereby maximizing parallelism and autonomy between processes. Along the way, I categorize different classes of invariants, and for each class, a protocol that guarantees it. Some classes can be enforced by each process independently; some require asynchronous coordination in the form of causal-order delivery of messages; and some (but by no means all) do require the full power of consensus. The first two classes are at the same time available and partition-tolerant; for the last one (the focus of the CAP Theorem) the programmer must make a decision, choosing between availability and partition-tolerance. Finally, we will discuss program analysis techniques for safely characterizing the amount of required coordination. In the second part of the talk, I will present Varda, a new programming language for distributed applications. Varda aims to reduce the amount of work and to improve the safety of distributed programming. Varda is designed to enable the safe composition of components, including black-box "off-the-shelf" (OTS) components. As a running example, we consider the incremental development of a sharded, geo-distributed key-value store, using OTSs such as Redis, Kafka, and RabbitMQ. A component's interface is a well-defined protocol, i.e., a set of typed messages that satisfy both a given grammar and some given invariants (an OTS is sandboxed to verify the protocol at run time). To ensure safety, two components may communicate only if their protocols are mutually compatible and they are in the same scope. The developer may evolve such a composition by interposing proxies, transparently to the existing components. The Varda compiler enforces the safety constraints, generates boiler-plate code, and applies high-level optimisations.

Slides

We all know that a web server should never trust data sent by clients, because clients might be malicious, tell lies, and try to break the system. In the case of a web app, the server is trusted to check the validity of data from clients, but what do we do in peer-to-peer systems where there is no such server that we can depend on? We have to rely on protocols, but unfortunately many replication protocols assume that peers are trusted; a malicious peer can easily break them. Byzantine Fault Tolerance (BFT) is often associated with blockchains, but it is relevant for other types of replication as well. In this lecture I will show CRDTs can be made Byzantine fault tolerant.

Slides

Abstract of the opening session.

Slides

The following students presented posters at the session: - Geo Johns Antony (IMT Atlantique) - Tim Baccaert (Vrije Universiteit Brussel) - Dina Borrego (NOVA University of Lisbon) - Julian Haas (TU Darmstadt) - Mirko Kohler (TU Darmstadt) - Christian Kuessner (TU Darmstadt) - Aaron Munsters (Vrije Universiteit Brussel) - Ana Ribeiro (NOVA University of Lisbon) - Mateo Sanabria (Universidad de los Andes) - Jana Toljaga (Institut Polytechnique de Paris) - Weihong Wang (KU Leuven) - George Zakhour (University of St. Gallen) The jury formed by a representation of DARE organizers and invited speakers (Prof. Baquero, Prof. Ferreira, Prof. Gonzalez Boix, Dr. Kleppmann and Prof. Kulahcioglu Ozkan) deemed the following three works as the best posters: - Aaron Munsters - CoAST: a conflict-free replicated abstract syntax tree (best poster award winner) - Julian Haas - LoRe : local first reactive programming with verified safety guarantees (runner-up) - George Zakhour - Propel: type checking CRDT convergence with Propel (runner-up)

Slides

TODO: museum visit

Slides

Today's huge memories make it possible to store and process large data structures in memory instead of in a database. Hence, accesses to this data should be optimized, which is normally relegated either to the runtimes and compilers or is left to the developers, who often lack the knowledge about optimization strategies. As arrays are often part of the language, developers frequently use them as an underlying storage mechanism. Thus, optimization of arrays may be vital to improve performance of data-intensive applications. While compilers can apply numerous optimizations to speed up accesses, it would also be beneficial to adapt the actual layout of the data in memory to improve cache utilization. However, runtimes and compilers typically do not perform such memory layout optimizations.
In this work, we present an approach to dynamically perform memory layout optimizations on arrays of objects to transform them into a columnar memory layout, a storage layout frequently used in analytical applications that enables faster processing of read-intensive workloads. By integration into a state-of-the-art JavaScript runtime, our approach can speed up queries for large workloads by up to 9x, where the initial transformation overhead is amortized over time.

Slides

Abstract of the opening session.

Slides

Chats allow to broadcast information among a group of persons. In this practical session, we will experiment how different broadcast algorithms influence the order in which messages are delivered to the chat participants. To this end, you will learn the basics of processes and message passing in Elixir (https://elixir-lang.org/) and implement a simple chat application.

In this practical session we will verify a number of CRDTs using VeriFx, a new functional object-oriented programming language that can perform automated proofs.