Behavioural Types for Local-First Software
Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. This paper introduces an execution model based on log shipping to mitigate this. More precisely, we present specify systems from a global viewpoint, which are projected to machines that yield local specifications.
We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification.
The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.
Wed 19 JulDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00
|Behavioural Types for Local-First Software|
Roland Kuhn Actyx AG, Hernan Melgratti University of Buenos Aires, Argentina, Emilio Tuosto Gran Sasso Science Institute, L'Aquila, ItalyDOI
|Algebraic Replicated Data Types: Programming Secure Local-First Software|
Christian Kuessner Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Anna-Katharina Wickert TU Darmstadt, Germany, Mira Mezini TU DarmstadtDOI Pre-print
|Modular Verification of State-Based CRDTs in Separation Logic|
Abel Nieto Aarhus University, Arnaud Daby-Seesaram ENS Paris Saclay, Léon Gondelman Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus UniversityDOI
|VeriFx: Correct Replicated Data Types for the Masses|
Kevin De Porre Vrije Universiteit Brussel, Carla Ferreira NOVA University Lisbon, Elisa Gonzalez Boix Vrije Universiteit BrusselDOI
|Nested Pure Operation-Based CRDTs|
|LoRe: A Programming Model for Verifiably Safe Local-First Software|
Julian Haas Technische Universität Darmstadt, Ragnar Mogk Technische Universität Darmstadt, Elena Yanakieva University of Kaiserslautern-Landau, Annette Bieniusa Kaiserslautern, Mira Mezini TU DarmstadtDOI Pre-print