Wed 19 Jul 2023 14:30 - 14:45 at Amazon Auditorium (Gates G20) - ECOOP 2: Replication Chair(s): Eric Jul

Modern distributed applications increasingly replicate data to guarantee high availability and optimal user experience. Conflict-free Replicated Data Types (CRDTs) are a family of data types specially designed for highly available systems that guarantee some form of eventual consistency. Designing CRDTs is very difficult because it requires devising designs that guarantee convergence in the presence of conflicting operations. Even though design patterns and structured frameworks have emerged to aid developers with this problem, they mostly focus on statically structured data; nesting and dynamically changing the structure of a CRDT remains to be an open issue.

This paper explores support for nested CRDTs in a structured and systematic way. To this end, we define an approach for building nested CRDTs based on the work of pure operation-based CRDTs, resulting in nested pure operation-based CRDTs. We add constructs to control the nesting of CRDTs into a pure operation-based CRDT framework and show how several well-known CRDT designs can be defined in our framework. We provide an implementation of nested pure operation-based CRDTs as an extension to the Flec, an existing TypeScript-based framework for pure operation-based CRDTs. We validate our approach, 1) by implementing a portfolio of nested data structures, 2) by implementing and verifying our approach in the VeriFx language, and 3) by implementing a real-world application scenario and comparing its network usage against an implementation in the closest related work, Automerge. We show that the framework is general enough to nest well-known CRDT designs like maps and lists, and its performance in terms of network traffic is comparable to the state of the art.

Wed 19 Jul

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 15:00
ECOOP 2: ReplicationResearch Papers at Amazon Auditorium (Gates G20)
Chair(s): Eric Jul University of Oslo
13:30
15m
Talk
Behavioural Types for Local-First Software
Research Papers
Roland Kuhn Actyx AG, Hernan Melgratti University of Buenos Aires, Argentina, Emilio Tuosto Gran Sasso Science Institute, L'Aquila, Italy
DOI
13:45
15m
Talk
Algebraic Replicated Data Types: Programming Secure Local-First Software
Research Papers
Christian Kuessner Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Anna-Katharina Wickert TU Darmstadt, Germany, Mira Mezini TU Darmstadt
DOI Pre-print
14:00
15m
Talk
Modular Verification of State-Based CRDTs in Separation Logic
Research Papers
Abel Nieto Aarhus University, Arnaud Daby-Seesaram ENS Paris Saclay, Léon Gondelman Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
DOI
14:15
15m
Talk
VeriFx: Correct Replicated Data Types for the Masses
Research Papers
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA University Lisbon, Elisa Gonzalez Boix Vrije Universiteit Brussel
DOI
14:30
15m
Talk
Nested Pure Operation-Based CRDTs
Research Papers
Jim Bauwens Vrije Universiteit Brussel, Elisa Gonzalez Boix Vrije Universiteit Brussel
DOI
14:45
15m
Talk
LoRe: A Programming Model for Verifiably Safe Local-First Software
Research Papers
Julian Haas Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Elena Yanakieva University of Kaiserslautern-Landau, Annette Bieniusa Kaiserslautern, Mira Mezini TU Darmstadt
DOI Pre-print