| Monday | Tuesday | Wednesday | Thursday | Friday | |
|---|---|---|---|---|---|
| 9:00 | Registration & welcome | Guido Salvaneschi | Carlos Baquero | Tom Van Cutsem | Kevin De Porre |
| 10:30 | Coffee break | Coffee break | Coffee break | Coffee break | Coffee break |
| 10:50 | Nuno Preguiça | José Orlando Pereira | Alexey Gotsman | Carlos Baquero | Kevin De Porre |
| 12:30 | Lunch | Lunch | Lunch | Lunch | Lunch |
| 13:30 | Ragnar Mogk | José Orlando Pereira | Alexey Gotsman | Burcu Ozkan | Project Preparation & Closing |
| 15:00 | Coffee break | Coffee break | Coffee break | Lisbon city tour | |
| 15:20 | Ragnar Mogk | Annette Bieniusa | Poster Session | ||
| Welcome reception | Dinner in Lisbon |
Hands-on Lecture Other
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.
Protocol RDTs extend the concept of replicated data types by treating programs—not just data—as the replicated entity. This approach captures both state and behaviour, enabling systems to enforce application-level correctness under weak consistency. The talk presents the foundations of Protocol RDTs and demonstrates how they enable expressive, coordination-free distributed programming.
Distributed systems are notoriously hard to design, implement, and deploy. In this talk, we argue that programming languages are a fundamental tool to tackle the complexity of distributed systems. We first discuss concrete examples of how abstractions offered by programming languages have been fundamental in solving problems in distributed systems. Then we discuss recent research results in this area, such as abstractions for data consistency and behavioral types for distributed applications. Finally, we outline promising research directions.
State-of-the-art analytical processing relies on advanced query optimisation and parallelism across processors and clusters. Meanwhile, geo-distributed and local-first systems achieve high availability by encapsulating eventual consistency in replicated data types. However, these approaches are difficult to combine, limiting analytical performance on highly available data. This talk offers a hands-on introduction to analytical processing and Conflict-free Replicated Data Views as a solution for enabling high-performance analytics under high availability.
State-based CRDTs can be synchronised by exchanging full states among two replicas. When they share similar content, this leads to the transmission of redundant state. By splitting monolithic CRDT states into sets of smaller CRDTs, that can be joined together to reconstruct the original state, we can harvest existing solutions for distributed set reconciliation. We show this process and then benchmark different set reconciliation approaches in terms of transmitted data and encoding/decoding speeds.
Transaction isolation specifications determine which database states transactions can observe during their execution, and thus, which results queries are allowed to return. This isolation corresponds to the letter “I” in the famous ACID acronym. Different “ACID” systems actually provide a spectrum of isolation levels, which expose the concurrency inside the database to the application programmer to a lesser or greater extent. Examples of such levels are serializability, snapshot isolation, and read committed.
Historically, the definitions of isolation levels have often been ambiguous or tied to database implementation internals. As a result, transaction isolation remains a difficult topic even for seasoned database professionals. This is a problem because understanding the isolation level provided by a given database is necessary to use it correctly. In this tutorial, I will explain the concept of transaction isolation and highlight pitfalls to be wary of when navigating the spectrum of isolation levels while also explaining some of the levels provided by modern database systems.
Blockchain and distributed ledger technology (DLT) are key enabling technologies for building open, resilient and secure distributed transaction processing systems. This introductory lecture will provide you with an up-to-date view on both the foundations and open challenges in the field. We will cover: the origins of Blockchain, the cryptographic building blocks of blockchains, how blockchain networks process transactions, consensus in blockchain networks: Proof-of-Work, Proof-of-Stake and BFT Consensus, “permissioned” versus “permissionless” blockchain networks, programming blockchains using smart contracts and latest trends.
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.
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.
