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,这是一种编程模型和编译器,用于自动验证基于本地的应用程序的开发人员提供的安全属性。LoRe将响应式编程的声明性数据流与静态分析和验证技术相结合,以准确确定违反安全不变量的并发交互,并有选择地通过协调采用强一致性。我们提出了一个形式化的证明原则,并演示了如何在原型实现中自动化该过程输出已验证的可执行代码。我们的评估显示,与现有的最新方法相比,LoRe简化了开发安全的基于本地优先的软件的过程,并且验证时间是可接受的。