Document Open Access Logo

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

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

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.12.pdf
  • Filesize: 0.8 MB
  • 15 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

Funding

This work was funded by the German Federal Ministry of Education and Research together with the Hessen State Ministry for Higher Education (ATHENE), the German Research Foundation (SFB 1053), and the German Federal Ministry for Economic Affairs and Climate Action project SafeFBDC (01MK21002K).

Cite AsGet BibTex

Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, and Mira Mezini. LoRe: A Programming Model for Verifiably Safe Local-First Software (Extended Abstract). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 12:1-12:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.12

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
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Deepthi Devaki Akkoorath, Alejandro Z. Tomsic, Manuel Bravo, Zhongmiao Li, Tyler Crain, Annette Bieniusa, Nuno Preguiça, and Marc Shapiro. Cure: Strong Semantics Meets High Availability and Low Latency. In 2016 IEEE 36th International Conference on Distributed Computing Systems (ICDCS), 2016. URL: https://doi.org/10.1109/ICDCS.2016.98.
  2. Peter Alvaro, Neil Conway, Joseph M Hellerstein, and David Maier. Blazes: Coordination analysis for distributed programs. In 2014 IEEE 30th International Conference on Data Engineering. IEEE, March 2014. URL: https://doi.org/10.1109/ICDE.2014.6816639.
  3. Peter Alvaro, Neil Conway, Joseph M Hellerstein, and William R Marczak. Consistency Analysis in Bloom: A CALM and Collected Approach. In CIDR. Citeseer, 2011. URL: http://cidrdb.org/cidr2011/Papers/CIDR11_Paper35.pdf.
  4. Peter Bailis, Alan Fekete, Michael J Franklin, Ali Ghodsi, Joseph M Hellerstein, and Ion Stoica. Coordination Avoidance in Database Systems. Proceedings of the VLDB Endowment, 8(3):185-196, November 2014. URL: https://doi.org/10.14778/2735508.2735509.
  5. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno Preguiça. IPA: Invariant-Preserving Applications for Weakly Consistent Replicated Databases. Proceedings of the VLDB Endowment, 12(4):404-418, December 2018. URL: https://doi.org/10.14778/3297753.3297760.
  6. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguiça, Mahsa Najafzadeh, and Marc Shapiro. Putting consistency back into eventual consistency. Proceedings of the Tenth European Conference on Computer Systems - EuroSys '15, pages 1-16, 2015. URL: https://doi.org/10.1145/2741948.2741972.
  7. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, Nuno Preguiça, Mahsa Najafzadeh, and Marc Shapiro. Towards Fast Invariant Preservation in Geo-replicated Systems. ACM SIGOPS Operating Systems Review, 49(1):121-125, January 2015. URL: https://doi.org/10.1145/2723872.2723889.
  8. Kevin De Porre, Carla Ferreira, Nuno M. Preguiça, and Elisa Gonzalez Boix. Ecros: building global scale systems from sequential code. Proceedings of the ACM on Programming Languages, 5(OOPSLA):1-30, 2021. URL: https://doi.org/10.1145/3485484.
  9. Kevin De Porre, Florian Myter, Christophe De Troyer, Christophe Scholliers, Wolfgang De Meuter, and Elisa Gonzalez Boix. Putting order in strong eventual consistency. In Distributed Applications and Interoperable Systems, pages 36-56, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-22496-7_3.
  10. Moritz Dinser. An empirical study on reactive programming. Master’s thesis, Technische Universität Darmstadt, 2021. URL: http://tubama.ulb.tu-darmstadt.de/id/eprint/30079.
  11. Joscha Drechsler, Ragnar Mogk, Guido Salvaneschi, and Mira Mezini. Thread-Safe Reactive Programming. Proceedings of the ACM on Programming Languages, 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276477.
  12. Victor B F Gomes, Martin Kleppmann, Dominic P Mulligan, and Alastair R Beresford. Verifying Strong Eventual Consistency in Distributed Systems. Proceedings of the ACM on Programming Languages, 1(OOPSLA):109:1-109:28, October 2017. URL: https://doi.org/10.1145/3133933.
  13. Julian Haas, Ragnar Mogk, Elena Yanakieva, Annette Bieniusa, and Mira Mezini. Lore: A programming model for verifiably safe local-first software, 2023. URL: https://arxiv.org/abs/2304.07133.
  14. Farzin Houshmand and Mohsen Lesani. Hamsaz: Replication Coordination Analysis and Synthesis. Proceedings of the ACM on Programming Languages, 3(POPL):74:1-74:32, January 2019. URL: https://doi.org/10.1145/3290387.
  15. Gowtham Kaki, Kapil Earanky, K C Sivaramakrishnan, and Suresh Jagannathan. Safe Replication through Bounded Concurrency Verification. Proceedings of the ACM on Programming Languages, 2(OOPSLA), October 2018. URL: https://doi.org/10.1145/3276534.
  16. Gowtham Kaki, Swarn Priya, K C Sivaramakrishnan, and Suresh Jagannathan. Mergeable replicated data types. Proceedings of the ACM on Programming Languages, 3(OOPSLA):154:1-154:29, October 2019. URL: https://doi.org/10.1145/3360580.
  17. Martin Kleppmann, Adam Wiggins, Peter van Hardenberg, and Mark McGranaghan. Local-first software: You own your data, in spite of the cloud. In Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, New York, NY, USA, October 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3359591.3359737.
  18. Rusty Klophaus. Riak Core: Building Distributed Applications without Shared State. In ACM SIGPLAN Commercial Users of Functional Programming, New York, NY, USA, 2010. Association for Computing Machinery. URL: https://doi.org/10.1145/1900160.1900176.
  19. Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, and Guido Salvaneschi. Rethinking Safe Consistency in Distributed Object-Oriented Programming. Proceedings of the ACM on Programming Languages, 4(OOPSLA):188:1-188:30, 2020. URL: https://doi.org/10.1145/3428256.
  20. Shadaj Laddad, Conor Power, Mae Milano, Alvin Cheung, and Joseph M. Hellerstein. Katara: Synthesizing CRDTs with verified lifting. Proceedings of the ACM on Programming Languages, 6(OOPSLA2):173:1349-173:1377, October 2022. URL: https://doi.org/10.1145/3563336.
  21. Nicholas V Lewchenko, Arjun Radhakrishna, Akash Gaonkar, and Pavol Černý. Sequential Programming for Replicated Data Stores. Proceedings of the ACM on Programming Languages, 3(ICFP):106:1-106:28, July 2019. URL: https://doi.org/10.1145/3341710.
  22. Cheng Li, João Leitão, Allen Clement, Nuno M. Preguiça, Rodrigo Rodrigues, and Viktor Vafeiadis. Automating the Choice of Consistency Levels in Replicated Systems. In 2014 USENIX Annual Technical Conference (USENIX ATC 14), Philadelphia, PA, 2014. USENIX Association. URL: https://www.usenix.org/conference/atc14/technical-sessions/presentation/li_cheng_2.
  23. Cheng Li, Daniel Porto, Allen Clement, Johannes Gehrke, Nuno Preguic, and Rodrigo Rodrigues. Making Geo-Replicated Systems Fast as Possible, Consistent when Necessary. OSDI'12 Proceedings of the 10th USENIX conference on Operating Systems Design and Implementation, pages 265-278, 2012. URL: https://www.usenix.org/conference/osdi12/technical-sessions/presentation/li.
  24. Christopher Meiklejohn and Peter Van Roy. Lasp: A Language for Distributed, Coordination-free Programming. In Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, pages 184-195, New York, NY, USA, 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2790449.2790525.
  25. Mae Milano and Andrew C Myers. MixT: A Language for Mixing Consistency in Geodistributed Transactions. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3192366.3192375.
  26. Ragnar Mogk, Lars Baumgärtner, Guido Salvaneschi, Bernd Freisleben, and Mira Mezini. Fault-tolerant Distributed Reactive Programming. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018), volume 109, Dagstuhl, Germany, 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.1.
  27. Ragnar Mogk, Joscha Drechsler, Guido Salvaneschi, and Mira Mezini. A Fault-tolerant Programming Model for Distributed Interactive Applications. Proceedings of the ACM on Programming Languages, 3(OOPSLA):144:1-144:29, October 2019. URL: https://doi.org/10.1145/3360570.
  28. P Müller, M Schwerhoff, and A J Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 9583, Berlin, Heidelberg, 2016. Springer-Verlag. URL: https://doi.org/10.1007/978-3-662-49122-5_2.
  29. Florian Myter, Christophe Scholliers, and Wolfgang De Meuter. A CAPable Distributed Programming Model. In Proceedings of the 2018 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2018, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3276954.3276957.
  30. Sreeja S Nair, Gustavo Petri, and Marc Shapiro. Proving the Safety of Highly-Available Distributed Objects. In Programming Languages and Systems, pages 544-571, Cham, 2020. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-44914-8_20.
  31. Petru Nicolaescu, Kevin Jahns, Michael Derntl, and Ralf Klamma. Near real-time peer-to-peer shared editing on extensible data types. In Proceedings of the 19th International Conference on Supporting Group Work, Sanibel Island, FL, USA, November 13 - 16, 2016. Association for Computing Machinery, 2016. URL: https://doi.org/10.1145/2957276.2957310.
  32. Nuno Preguiça. Conflict-free Replicated Data Types: An Overview. ArXiv, June 2018. URL: https://doi.org/10.48550/arXiv.1806.10254.
  33. Guido Salvaneschi, Sebastian Proksch, Sven Amann, Sarah Nadi, and Mira Mezini. On the Positive Effect of Reactive Programming on Software Comprehension: An Empirical Study. IEEE Transactions on Software Engineering, 43(12), 2017. URL: https://doi.org/10.1109/TSE.2017.2655524.
  34. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. A comprehensive study of convergent and commutative replicated data types. Research Report RR-7506, Inria endash Centre Paris-Rocquencourt ; INRIA, January 2011. URL: https://hal.inria.fr/inria-00555588.
  35. KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative Programming over Eventually Consistent Data Stores. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '15, pages 413-424, New York, NY, USA, June 2015. Association for Computing Machinery. URL: https://doi.org/10.1145/2737924.2737981.
  36. TPC. TPC-C Specification 5.11.0, 2021. URL: http://tpc.org/TPC_Documents_Current_Versions/pdf/tpc-c_v5.11.0.pdf.
  37. Viper. Viperproject/silicon Github Repository. Viper Project, April 2021. URL: https://github.com/viperproject/silicon.
  38. Michael Whittaker and Joseph M Hellerstein. Interactive Checks for Coordination Avoidance. Proceedings of the VLDB Endowment, 12(1):14-27, September 2018. URL: https://doi.org/10.14778/3275536.3275538.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact