License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.12
URN: urn:nbn:de:0030-drops-182056
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18205/
Go to the corresponding LIPIcs Volume Portal

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

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

pdf-format:
LIPIcs-ECOOP-2023-12.pdf (0.8 MB)

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.

BibTeX - Entry

@InProceedings{haas_et_al:LIPIcs.ECOOP.2023.12,
  author =	{Haas, Julian and Mogk, Ragnar and Yanakieva, Elena and Bieniusa, Annette and Mezini, Mira},
  title =	{{LoRe: A Programming Model for Verifiably Safe Local-First Software (Extended Abstract)}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{12:1--12:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18205},
  URN =		{urn:nbn:de:0030-drops-182056},
  doi =		{10.4230/LIPIcs.ECOOP.2023.12},
  annote =	{Keywords: Local-First Software, Reactive Programming, Invariants, Consistency, Automated Verification}
}

Keywords: Local-First Software, Reactive Programming, Invariants, Consistency, Automated Verification
Collection: 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Issue Date: 2023
Date of publication: 11.07.2023
Supplementary Material: Software (Source Code): https://github.com/stg-tud/LoRe
Software (ECOOP 2023 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.9.2.11

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI