Document Open Access Logo

Compositional Design, Implementation, and Verification of Swarms

Authors Florian Furbach , Lucas Clorius , Roland Kuhn , Hernán Melgratti , Alceste Scalas , Emilio Tuosto

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2026.7.pdf
  • Filesize: 1.56 MB
  • 30 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed computing models
  • Software and its engineering → Distributed programming languages
  • Software and its engineering → Formal software verification
Keywords
  • Swarms
  • Swarm Protocols
  • Concurrency
  • Distributed Coordination
  • Local-first Software
  • Behavioural Types
  • Publish-Subscribe
  • Asynchronous Communication

Metrics

Abstract

Swarm protocols are a recently introduced formalism for specifying, implementing, and verifying peer-to-peer systems called swarms. A swarm consists of distributed agents called machines that communicate by asynchronous event propagation. Following a local-first model, each machine can progress without requiring continuous connectivity to other machines. Existing models of swarms are not compositional, making the modular development of large and complex swarm applications as well as the reuse of code difficult. We address these issues by presenting novel theory and techniques for the compositional specification, verification, and implementation of swarms. These results enable the correct compositional reuse of pre-existing swarm protocols and machine implementations. We implement these contributions in a companion software artifact which enables the automatic integration of independently designed and verified swarm components.

Cite As Get BibTex

Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional Design, Implementation, and Verification of Swarms. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 7:1-7:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ECOOP.2026.7

Author Details

Florian Furbach
  • University of Surrey, Guildford, UK
  • Technical University of Denmark, Kgs. Lyngby, Denmark
Lucas Clorius
  • Technical University of Denmark, Kgs. Lyngby, Denmark
Roland Kuhn
  • RKSW UG, Kassel, Germany
Hernán Melgratti
  • University of Buenos Aires, Argentina
  • Conicet, Buenos Aires, Argentina
Alceste Scalas
  • Technical University of Denmark, Kgs. Lyngby, Denmark
Emilio Tuosto
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

Research partially supported by the Horizon Europe grant 101093006 (TaRDIS) and by the Italian Ministero dell'Università e della Ricerca "Dipartimenti di eccellenza" initiative.

Acknowledgements

This work was inspired by the discussions at the Dagstuhl Seminar 24051 "Next Generation Protocols for Heterogeneous Systems" [Stephanie Balzer et al., 2024]. We thank the organisers of the meeting and Schloss Dagstuhl - Leibniz Center for Informatics for making this work possible.

Supplementary Materials

References

  1. Actyx AG. Actyx decentralized event database, streaming and processing engine, 2024. URL: https://github.com/Actyx/Actyx.
  2. Actyx AG. @actyx/machine-runner library, 2024. accessed 13-12-2024. URL: https://www.npmjs.com/package/@actyx/machine-runner.
  3. Actyx AG. Actyx developer website. https://developer.actyx.com, 2024. [Online; accessed on 29 October 2024].
  4. Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. The MIT Press, December 1986. URL: https://doi.org/10.7551/mitpress/1086.001.0001.
  5. 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. URL: https://doi.org/10.1561/2500000031.
  6. Ozalp Babaoglu and Keith Marzullo. Consistent global states of distributed systems: Fundamental concepts and mechanisms. Distributed Systems, 53, 1993. Google Scholar
  7. 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.
  8. Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next generation protocols for heterogeneous systems (dagstuhl seminar 24051). Dagstuhl Reports, 14(1):108-129, 2024. URL: https://doi.org/10.4230/DAGREP.14.1.108.
  9. Franco Barbanera, Ugo de'Liguoro, and Rolf Hennicker. Connecting open systems of communicating finite state machines. J. Log. Algebraic Methods Program., 109, 2019. URL: https://doi.org/10.1016/j.jlamp.2019.07.004.
  10. Franco Barbanera, Mariangiola Dezani-Ciancaglini, Lorenzo Gheri, and Nobuko Yoshida. Multicompatibility for multiparty-session composition. In Proceedings of the 25th International Symposium on Principles and Practice of Declarative Programming, pages 1-15, 2023. URL: https://doi.org/10.1145/3610612.3610614.
  11. Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese, and Emilio Tuosto. Composition and decomposition of multiparty sessions. J. Log. Algebraic Methods Program., 119:100620, 2021. URL: https://doi.org/10.1016/j.jlamp.2020.100620.
  12. Franco Barbanera, Ivan Lanese, and Emilio Tuosto. On composing communicating systems. In Clément Aubert, Cinzia Di Giusto, Larisa Safina, and Alceste Scalas, editors, Proceedings 15th Interaction and Concurrency Experience, ICE 2022, Lucca, Italy, 17th June 2022, volume 365 of EPTCS, pages 53-68, 2022. URL: https://doi.org/10.4204/EPTCS.365.4.
  13. Franco Barbanera, Ivan Lanese, and Emilio Tuosto. Composition of synchronous communicating systems. J. Log. Algebraic Methods Program., 135:100890, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100890.
  14. Sebastian Burckhardt. Principles of eventual consistency. Found. Trends Program. Lang., 1(1–2):1-150, October 2014. URL: https://doi.org/10.1561/2500000011.
  15. 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. URL: https://doi.org/10.1007/978-3-642-31057-7_14.
  16. 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 für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2015.568.
  17. 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.
  18. 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.
  19. Luís Cruz-Filipe, Eva Graversen, Lovro Lugović, Fabrizio Montesi, and Marco Peressotti. Modular Compilation for Higher-Order Functional Choreographies. In 37th European Conference on Object-Oriented Programming (ECOOP 2023), volume 263 of Leibniz International Proceedings in Informatics (LIPIcs), pages 7:1-7:37, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.7.
  20. Ugo de'Liguoro, Hernán C. Melgratti, and Emilio Tuosto. Towards refinable choreographies. J. Log. Algebraic Methods Program., 127:100776, 2022. URL: https://doi.org/10.1016/j.jlamp.2022.100776.
  21. 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.
  22. 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.
  23. Criterion Developers. Criterion documentation, 2025. Accessed 18-02-2026. URL: https://docs.rs/criterion/0.7.0/criterion.
  24. Patrick Th. Eugster, Pascal Felber, Rachid Guerraoui, and Anne-Marie Kermarrec. The many faces of publish/subscribe. ACM Comput. Surv., 35(2):114-131, June 2003. URL: https://doi.org/10.1145/857076.857078.
  25. Florian Furbach, Lucas Clorius, Roland Kuhn, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Compositional design, implementation, and verification of swarms (technical report), 2026. URL: https://doi.org/10.48550/arXiv.2604.16097.
  26. Simon Gay and Antonio Ravara, editors. Behavioural Types: from Theory to Tools. Automation, Control and Robotics. River, 2009. Google Scholar
  27. Lorenzo Gheri and Nobuko Yoshida. Hybrid multiparty session types: Compositionality for protocol specification through endpoint projection. Proc. ACM Program. Lang., 7(OOPSLA), April 2023. URL: https://doi.org/10.1145/3586031.
  28. 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.
  29. 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 für Informatik. URL: https://doi.org/10.4230/LIPIcs.DISC.2017.23.
  30. 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. URL: https://doi.org/10.1145/2837614.2837625.
  31. Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. A universal modular ACTOR formalism for artificial intelligence. In Nils J. Nilsson, editor, Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973, IJCAI'73, pages 235-245, San Francisco, CA, USA, 1973. William Kaufmann. URL: http://ijcai.org/Proceedings/73/Papers/027B.pdf.
  32. 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. URL: https://doi.org/10.1145/1328438.1328472.
  33. Kohei Honda, Nobuko Yoshida, and Marco Carbone. Multiparty asynchronous session types. Journal of the ACM (JACM), 63(1):1-67, 2016. URL: https://doi.org/10.1145/2827695.
  34. 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. URL: https://doi.org/10.1145/2873052.
  35. 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. URL: https://doi.org/10.1007/978-3-030-44914-8_10.
  36. 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. URL: https://doi.org/10.1145/3276534.
  37. Martin Kleppmann, Adam Wiggins, Peter van Hardenberg, and Mark McGranaghan. Local-first software: you own your data, in spite of the cloud. In Hidehiko Masuhara and Tomas Petricek, editors, Proceedings of the 2019 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2019, Athens, Greece, October 23-24, 2019, Onward! 2019, pages 154-178, New York, NY, USA, 2019. ACM. URL: https://doi.org/10.1145/3359591.3359737.
  38. Roland Kuhn. Local-first cooperation: Autonomy at the edge, secured by crypto, 100% available. https://www.infoq.com/articles/local-first-cooperation/, 2021. [Online; accessed on 29 October 2024].
  39. Roland Kuhn and Alan Darmasaputra. Behaviorally typed state machines in typescript for heterogeneous swarms. In René Just and Gordon Fraser, editors, Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2023, Seattle, WA, USA, July 17-21, 2023, ISSTA 2023, pages 1475-1478, New York, NY, USA, 2023. ACM. URL: https://doi.org/10.1145/3597926.3604917.
  40. Roland Kuhn, Hernán C. Melgratti, and Emilio Tuosto. Behavioural types for local-first software. In Karim Ali and Guido Salvaneschi, editors, 37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States, volume 263 of LIPIcs, pages 15:1-15:28. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.15.
  41. Fabrizio Montesi. Introduction to Choreographies. Cambridge University Press, 2023. URL: https://doi.org/10.1017/9781108981491.
  42. Fabrizio Montesi and Nobuko Yoshida. Compositional choreographies. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013. Proceedings, Lecture Notes in Computer Science, pages 425-439. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_30.
  43. D Stott Parker, Gerald J Popek, Gerard Rudisin, Allen Stoughton, Bruce J Walker, Evelyn Walton, Johanna M Chow, David Edwards, Stephen Kiser, and Charles Kline. Detection of mutual inconsistency in distributed systems. IEEE transactions on Software Engineering, SE-9(3):240-247, 1983. URL: https://doi.org/10.1109/TSE.1983.236733.
  44. David Lorge Parnas. On the criteria to be used in decomposing systems into modules. Communications of the ACM, 15(12):1053-1058, 1972. URL: https://doi.org/10.1145/361598.361623.
  45. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  46. Fred B. Schneider. Implementing fault-tolerant services using the state machine approach: A tutorial. ACM Comput. Surv., 22(4):299-319, 1990. URL: https://doi.org/10.1145/98163.98167.
  47. 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.
  48. Gan Shen, Shun Kashiwa, and Lindsey Kuper. HasChor: Functional Choreographic Programming for All. Proceedings of the ACM on Programming Languages, 7(ICFP):541-565, 2023. URL: https://doi.org/10.1145/3607849.
  49. K. C. Sivaramakrishnan, Gowtham Kaki, and Suresh Jagannathan. Declarative programming over eventually consistent data stores. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 413-424. ACM, ACM, 2015. URL: https://doi.org/10.1145/2737924.2737981.
  50. Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. Composable partial multiparty session types for open systems. Software and Systems Modeling, 22(2):473-494, 2023. URL: https://doi.org/10.1007/s10270-022-01040-x.
  51. 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. URL: https://doi.org/10.1145/3314221.3314617.
  52. 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.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact