LoRe: A Programming Model for Verifiably Safe Local-First Software
Local-first software manages and processes private data locally while still enabling collaboration between multiple parties connected via partially unreliable networks. Such software typically involves interactions with users and the execution environment (the outside world). The unpredictability of such interactions paired with their decentralized nature make reasoning about the correctness of local-first software a challenging endeavor. Yet, existing solutions to develop local-first software do not provide support for automated safety guarantees and instead expect developers to reason about concurrent interactions in an environment with unreliable network conditions.
We propose LoRe, a programming model and compiler that automatically verifies developer-supplied safety properties for local-first applications. LoRe combines the declarative data flow of reactive programming with static analysis and verification techniques to precisely determine concurrent interactions that violate safety invariants and to selectively employ strong consistency through coordination where required. We propose a formalized proof principle and demonstrate how to automate the process in a prototype implementation that outputs verified executable code. Our evaluation shows that LoRe simplifies the development of safe local-first software when compared to state-of-the-art approaches and that verification times are acceptable.
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