Document Open Access Logo

Behavioural Types for Local-First Software

Authors Roland Kuhn , Hernán Melgratti , Emilio Tuosto

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.15.pdf
  • Filesize: 1.09 MB
  • 28 pages

Document Identifiers

Author Details

Roland Kuhn
  • Actyx AG, Kassel, Germany
Hernán Melgratti
  • University of Buenos Aires, Argentina
  • Conicet, Buenos Aires, Argentina
Emilio Tuosto
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

Research partly supported by the EU H2020 RISE programme under the Marie Skłodowska-Curie grant agreement No 778233, by MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems), by the PRO3 MUR project Software Quality, and by the PNRR MUR project VITALITY (ECS00000041), Spoke 2 ASTRA - Advanced Space Technologies and Research Alliance. machine-runner and machine-check partly funded by the European Union (TaRDIS, 101093006).

Acknowledgements

The authors thank the anonymous reviewers for their useful and insightful comments and Daniela Marottoli for her help in the initial phase of this project.

Cite AsGet BibTex

Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.15

Abstract

Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. Our model elaborates on the Actyx industrial platform and provides the basis for tool support: we sketch an implemented prototype which proves this work a viable step towards reasoning about local-first and peer-to-peer software systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Software and its engineering → Distributed systems organizing principles
  • Software and its engineering → Distributed programming languages
Keywords
  • Distributed coordination
  • local-first software
  • behavioural types
  • publish-subscribe
  • asynchronous communication

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

  • The extended version of this paper [Roland Kuhn et al., 2023] contains more examples, a comparison between our model and state machine replication [Schneider, 1990], more details on the Actyx middleware, and a discussion on the limitation of our approach.
  • Extended Version https://arxiv.org/abs/2305.04848

Supplementary Materials

References

  1. Actyx AG. Actyx developer website, 2020-2022. accessed 2022/07/06. URL: https://developer.actyx.com.
  2. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J Gay, Nils Gesbert, Elena Giachino, Raymond Hu, et al. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95-230, 2016. Google Scholar
  3. Valter Balegas, Sérgio Duarte, Carla Ferreira, Rodrigo Rodrigues, and Nuno M. Preguiça. IPA: invariant-preserving applications for weakly consistent replicated databases. Proc. VLDB Endow., 12(4):404-418, 2018. URL: https://doi.org/10.14778/3297753.3297760.
  4. Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang., 1(1–2):1-150, October 2014. URL: https://doi.org/10.1561/2500000011.
  5. Sebastian Burckhardt, Manuel Fähndrich, Daan Leijen, and Benjamin P. Wood. Cloud types for eventual consistency. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming, pages 283-307, Berlin, Heidelberg, 2012. Springer. Google Scholar
  6. Sebastian Burckhardt, Daan Leijen, Jonathan Protzenko, and Manuel Fähndrich. Global Sequence Protocol: A Robust Abstraction for Replicated Shared State. In John Tang Boyland, editor, 29th European Conference on Object-Oriented Programming (ECOOP 2015), volume 37 of Leibniz International Proceedings in Informatics (LIPIcs), pages 568-590, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2015.568.
  7. Giuseppe Castagna, Nils Gesbert, and Luca Padovani. A theory of contracts for web services. ACM Transactions on Programming Languages and Systems (TOPLAS), 31(5):1-61, 2009. Google Scholar
  8. David Castro-Perez, Raymond Hu, Sung-Shik Jongmans, Nicholas Ng, and Nobuko Yoshida. Distributed programming using role-parametric session types in go: statically-typed endpoint apis for dynamically-instantiated communication structures. Proc. ACM Program. Lang., 3(POPL):29:1-29:30, 2019. URL: https://doi.org/10.1145/3290342.
  9. Bruno Courcelle. Fundamental properties of infinite trees. Theor. Comput. Sci., 25:95-169, 1983. URL: https://doi.org/10.1016/0304-3975(83)90059-2.
  10. Ornela Dardha and Jorge A. Pérez. Comparing type systems for deadlock freedom. J. Log. Algebraic Methods Program., 124:100717, 2022. URL: https://doi.org/10.1016/j.jlamp.2021.100717.
  11. Pierre-Malo Deniélou and Nobuko Yoshida. Dynamic multirole session types. In Thomas Ball and Mooly Sagiv, editors, POPL, pages 435-446. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926435.
  12. Pierre-Malo Deniélou, Nobuko Yoshida, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. Log. Methods Comput. Sci., 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:6)2012.
  13. Mariangiola Dezani-Ciancaglini and Ugo de'Liguoro. Sessions and session types: An overview. In WS-FM, volume 6194 of LNCS, pages 1-28. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-14458-5_1.
  14. Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, April 1985. URL: https://doi.org/10.1145/3149.214121.
  15. Simon Gay and Antonio Ravara, editors. Behavioural Types: from Theory to Tools. Automation, Control and Robotics. River, 2009. Google Scholar
  16. Seth Gilbert and Nancy Lynch. Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News, 33(2):51-59, June 2002. URL: https://doi.org/10.1145/564585.564601.
  17. Alexey Gotsman and Sebastian Burckhardt. Consistency Models with Global Operation Sequencing and their Composition. In Andréa W. Richa, editor, 31st International Symposium on Distributed Computing (DISC 2017), volume 91 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.DISC.2017.23.
  18. Alexey Gotsman, Hongseok Yang, Carla Ferreira, Mahsa Najafzadeh, and Marc Shapiro. 'Cause i'm strong enough: reasoning about consistency choices in distributed systems. In POPL 2016, pages 371-384, 2016. Google Scholar
  19. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. In Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on principles of programming languages, pages 273-284, 2008. Google Scholar
  20. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM (JACM), 63(1):1-67, 2016. Google Scholar
  21. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of session types and behavioural contracts. ACM Comput. Surv., 49(1):3:1-3:36, 2016. Google Scholar
  22. David R Jefferson. Virtual time. ACM Transactions on Programming Languages and Systems (TOPLAS), 7(3):404-425, 1985. Google Scholar
  23. Sung-Shik Jongmans and Nobuko Yoshida. Exploring type-level bisimilarity towards more expressive multiparty session types. In Peter Müller, editor, Programming Languages and Systems, pages 251-279, Cham, 2020. Springer International Publishing. Google Scholar
  24. Gowtham Kaki, Kapil Earanky, KC Sivaramakrishnan, and Suresh Jagannathan. Safe replication through bounded concurrency verification. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1-27, 2018. Google Scholar
  25. 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, pages 154-178, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3359591.3359737.
  26. Roland Kuhn. Local-first cooperation: Autonomy at the edge, secured by crypto, 100% available, 2021. accessed 2021/06/20. URL: https://www.infoq.com/articles/local-first-cooperation/.
  27. Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural types for local-first software, 2023. URL: https://arxiv.org/abs/2305.04848.
  28. Roland Kuhn, Hernán Melgratti, and Emilio Tuosto. Behavioural Types for Local-First Software (Artifact). Dagstuhl Artifacts Series, 9(2):14:1-14:5, 2023. URL: https://doi.org/10.4230/DARTS.9.2.14.
  29. Rupak Majumdar, Marcus Pirron, Nobuko Yoshida, and Damien Zufferey. Motion session types for robotic interactions (brave new idea paper). In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. Google Scholar
  30. Microsoft. Typescript: Javascript with syntax for types, 2012-2023. accessed 2023/02/02. URL: https://www.typescriptlang.org/.
  31. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  32. Fred B Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Computing Surveys (CSUR), 22(4):299-319, 1990. Google Scholar
  33. Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Stabilization, Safety, and Security of Distributed Systems, pages 386-400. Springer, 2011. Google Scholar
  34. Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In SSS 2011, pages 386-400, 2011. URL: https://doi.org/10.1007/978-3-642-24550-3_29.
  35. KC Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative programming over eventually consistent data stores. In PLDI 2015, pages 413-424. ACM, 2015. Google Scholar
  36. Ecma TC39. Ecma-404, 2017. accessed 2023/02/13, alternative RFC8259. URL: https://www.ecma-international.org/publications-and-standards/standards/ecma-404/.
  37. Ecma TC39. Decorators, 2022. accessed 2023/02/02. URL: https://github.com/tc39/proposal-decorators.
  38. Lewis Tseng. Eventual consensus: Applications to storage and blockchain : (extended abstract). In 2019 57th Annual Allerton Conference on Communication, Control, and Computing (Allerton), pages 840-846, 2019. URL: https://doi.org/10.1109/ALLERTON.2019.8919675.
  39. Vasco T. Vasconcelos. Fundamentals of session types. Inf. and Comp., 217:52-70, 2012. URL: https://doi.org/10.1016/j.ic.2012.05.002.
  40. Chao Wang, Constantin Enea, Suha Orhun Mutluergil, and Gustavo Petri. Replication-aware linearizability. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 980-993, 2019. Google Scholar
  41. Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, and Raymond Hu. Parameterised multiparty session types. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings, volume 6014 of Lecture Notes in Computer Science, pages 128-145. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_10.
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