一句话：提出 LoRe 编程模型与编译器，自动验证 local-first 应用的安全性质，并按需引入强一致性协调。
本地优先软件在本地管理私有数据，同时支持经不可靠网络连接的多方协作，并常与用户及外部环境交互；其去中心化与交互不可预测性使正确性推理十分困难，现有开发方案缺乏自动安全保证。LoRe 是一种编程模型与编译器：它把响应式编程的声明式数据流与静态分析、验证技术结合，精确判定会违反安全不变式的并发交互，并仅在需要时通过协调引入强一致性。作者提出形式化证明原则，并在原型实现中自动生成经过验证的可执行代码。评估表明，相比现有方法，LoRe 简化了安全本地优先软件的开发，且验证时间可接受。
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.
@article{paperbot2680,
title = {LoRe: A Programming Model for Verifiably Safe Local-first Software},
author = {Julian Haas and Ragnar Mogk and Elena Yanakieva and Annette Bieniusa and Mira Mezini},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {46},
number = {1},
year = {2024},
doi = {10.1145/3633769}
}