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

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



PDF
Thumbnail PDF

Artifact Description

DARTS.9.2.11.pdf
  • Filesize: 0.51 MB
  • 2 pages

Document Identifiers

Author Details

Julian Haas
  • Technische Universität Darmstadt, Germany
Ragnar Mogk
  • Technische Universität Darmstadt, Germany
Elena Yanakieva
  • University of Kaiserslautern-Landau, Germany
Annette Bieniusa
  • University of Kaiserslautern-Landau, Germany
Mira Mezini
  • Technische Universität Darmstadt, Germany

Cite As Get BibTex

Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, and Mira Mezini. LoRe: A Programming Model for Verifiably Safe Local-First Software (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/DARTS.9.2.11

Artifact

  MD5 Sum: e27898622113ac3de4936bafda3151fa (Get MD5 Sum)

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Distributed programming languages
  • Software and its engineering → Data flow languages
  • Software and its engineering → Consistency
  • Theory of computation → Pre- and post-conditions
  • Theory of computation → Program specifications
  • Computer systems organization → Peer-to-peer architectures
Keywords
  • Local-First Software
  • Reactive Programming
  • Invariants
  • Consistency
  • Automated Verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail