Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LoRe: A Programming Model for Verifiably Safe Local-First Software

Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, Mira Mezini

TL;DR

LoRe tackles the challenge of building verifiably safe local-first software by integrating reactive data-flow programming with automated invariant-based verification and synthesized cross-device coordination. The framework represents application state as Source CRDTs and Derived values, with Interactions that atomically affect reactives while invariants guide safety and conflicts identify when coordination is necessary. A modular verification pipeline translates programs to Viper for invariant preservation and confluence proofs, while runtime synchronization uses a token-based protocol to enforce coordinated interactions; graph analysis minimizes verification effort. Case studies on a distributed calendar and local-first TPC-C demonstrate safer development with modular, scalable verification and acceptable performance, underscoring practical impact for edge-first, offline-capable software. Overall, LoRe enables end-to-end safety guarantees across distributed, offline environments by automating coordination only where needed and enabling incremental adoption of safety specifications.

Abstract

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.

LoRe: A Programming Model for Verifiably Safe Local-First Software

TL;DR

LoRe tackles the challenge of building verifiably safe local-first software by integrating reactive data-flow programming with automated invariant-based verification and synthesized cross-device coordination. The framework represents application state as Source CRDTs and Derived values, with Interactions that atomically affect reactives while invariants guide safety and conflicts identify when coordination is necessary. A modular verification pipeline translates programs to Viper for invariant preservation and confluence proofs, while runtime synchronization uses a token-based protocol to enforce coordinated interactions; graph analysis minimizes verification effort. Case studies on a distributed calendar and local-first TPC-C demonstrate safer development with modular, scalable verification and acceptable performance, underscoring practical impact for edge-first, offline-capable software. Overall, LoRe enables end-to-end safety guarantees across distributed, offline environments by automating coordination only where needed and enabling incremental adoption of safety specifications.

Abstract

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.
Paper Structure (28 sections, 2 theorems, 4 equations, 7 figures, 1 table, 1 algorithm)

This paper contains 28 sections, 2 theorems, 4 equations, 7 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. LoRe in a Nutshell
  3. Reactives
  4. Interactions
  5. Invariants and Conflicts
  6. Programming Model
  7. Syntax and Evaluation Semantics
  8. Syntax
  9. Term evaluation
  10. Semantics for interactions and device communication
  11. Verifying Program Safety
  12. Implementation
  13. Graph Analysis
  14. Automated Verification
  15. Translation to Viper's Intermediate Language.
  16. ...and 13 more sections

Key Result

Lemma 1

The locking mechanism ensures for any program execution $P^0 \Longrightarrow \dots \Longrightarrow P^m$ that conflicting interactions are sequentially ordered. Specifically, for any two conflicting interactions $a_1$, $a_2$ with transitions $\langle \sigma{}{_1}, L{_1} \rangle \xRightarrow[a_1]{v_1}

Figures (7)

  • Figure 1: The data-flow graph of the calendar application.
  • Figure 2: Concurrent execution of interactions may cause invariant violations. In this example, device $D_1$ adds a vacation of 20 days to the calendar, while $D_2$ concurrently adds a vacation of 12 days. Given a total amount of 30 available vacation days, this leads to a negative amount of remaining vacation once the devices synchronize.
  • Figure 3: Abstract syntax of LoRe programs.
  • Figure 4: Semantics for reactive term evaluation.
  • Figure 5: Semantics for interactions and device communication.
  • ...and 2 more figures

Theorems & Definitions (7)

  • Definition 1: Validity
  • Definition 2: Safety
  • Definition 3: Invariant Preservation
  • Definition 4: Confluence
  • Definition 5: Initial Program
  • Lemma 1: Correct locking
  • Theorem 1: Soundness