Document Open Access Logo

Nondeterministic Asynchronous Dataflow in Isabelle/HOL

Authors Rafael Castro Gonçalves Silva , Laouen Fernet , Dmitriy Traytel

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.ITP.2025.30.pdf
  • Filesize: 1.07 MB
  • 20 pages
HTML5 Logo HTML (experimental)
LIPIcs.ITP.2025.30.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Computing methodologies → Distributed algorithms
  • Software and its engineering → Data flow languages
Keywords
  • dataflow
  • verification
  • coinduction
  • Isabelle/HOL

Metrics

Abstract

We formalize nondeterministic asynchronous dataflow networks in Isabelle/HOL. Dataflow networks are comprised of operators that are capable of communicating with the network, performing silent computations, and making nondeterministic choices. We represent operators using a shallow embedding as codatatypes. Using this representation, we define standard asynchronous dataflow primitives, including sequential and parallel composition and a feedback operator. These primitives adhere to a number of laws from the literature, which we prove by coinduction using weak bisimilarity as our equality. Albeit coinductive and nondeterministic, our model is executable via code extraction to Haskell.

Cite As Get BibTex

Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic Asynchronous Dataflow in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ITP.2025.30

Author Details

Rafael Castro Gonçalves Silva
  • Department of Computer Science, University of Copenhagen, Denmark
Laouen Fernet
  • Department of Computer Science, University of Copenhagen, Denmark
Dmitriy Traytel
  • Department of Computer Science, University of Copenhagen, Denmark

Funding

This work is supported by an Independent Research Fund Denmark Sapere Aude grant (3120-00057B, titled DISCOVER) and a Novo Nordisk Foundation start package grant (NNF20OC0063462).

Acknowledgements

We thank Asta H. From for numerous discussions on the representation of operators that were instrumental for arriving at the end product presented in this paper and Jan A. Bergstra, Cornelis A. Middelburg, and Gheorghe Stefanescu for discussing their axiom A1 for merge with us and for encouraging words on the merits of formal verification. Thomas Hildebrandt pointed us to Milner’s classic on weak bisimilarity. The ITP reviewers provided helpful textual suggestions.

Supplementary Materials

References

  1. Jesper Bengtson. Formalising process calculi. PhD thesis, Uppsala University, 2010. Google Scholar
  2. Jan A. Bergstra and Jan Willem Klop. Process algebra for synchronous communication. Inf. Control., 60(1-3):109-137, 1984. URL: https://doi.org/10.1016/S0019-9958(84)80025-X.
  3. Jan A. Bergstra, Cornelis A. Middelburg, and Gheorghe Stefanescu. Network algebra for asynchronous dataflow. Int. J. Comput. Math., 65(1-2):57-88, 1997. URL: https://doi.org/10.1080/00207169708804599.
  4. Jan A. Bergstra, Cornelis A. Middelburg, and Gheorghe Stefanescu. Network algebra for synchronous dataflow. CoRR, abs/1303.0382, 2013. URL: https://arxiv.org/abs/1303.0382.
  5. Jasmin Christian Blanchette, Aymeric Bouzy, Andreas Lochbihler, Andrei Popescu, and Dmitriy Traytel. Friends with benefits - implementing corecursion in foundational proof assistants. In Hongseok Yang, editor, ESOP 2017, volume 10201 of LNCS, pages 111-140. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_5.
  6. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_7.
  7. Timothy Bourke, Lélio Brun, Pierre-Évariste Dagand, Xavier Leroy, Marc Pouzet, and Lionel Rieg. A formally verified compiler for Lustre. In Albert Cohen and Martin T. Vechev, editors, PLDI 2017, pages 586-601. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062358.
  8. J Dean Brock and William B Ackerman. Scenarios: A model of non-determinate computation. In Formalization of Programming Concepts: International Colloquium Peniscola, Spain, April 19-25, 1981 Proceedings, pages 252-259. Springer, 1981. URL: https://doi.org/10.1007/3-540-10699-5_102.
  9. Manfred Broy and Gheorghe Stefanescu. The algebra of stream processing functions. Theor. Comput. Sci., 258(1-2):99-129, 2001. URL: https://doi.org/10.1016/S0304-3975(99)00322-9.
  10. Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified progress tracking for Timely Dataflow. In Liron Cohen and Cezary Kaliszyk, editors, ITP 2021, volume 193 of LIPIcs, pages 10:1-10:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.ITP.2021.10.
  11. Mihai Budiu, Tej Chajed, Frank McSherry, Leonid Ryzhyk, and Val Tannen. DBSP: automatic incremental view maintenance for rich query languages. Proc. VLDB Endow., 16(7):1601-1614, 2023. URL: https://doi.org/10.14778/3587136.3587137.
  12. Paris Carbone, Asterios Katsifodimos, Stephan Ewen, Volker Markl, Seif Haridi, and Kostas Tzoumas. Apache Flink: Stream and batch processing in a single engine. IEEE Data Eng. Bull., 38(4):28-38, 2015. URL: http://sites.computer.org/debull/A15dec/p28.pdf.
  13. Paul Caspi, Daniel Pilaud, Nicolas Halbwachs, and John Plaice. Lustre: A declarative language for programming synchronous systems. In POPL 1987, pages 178-188. ACM Press, 1987. URL: https://doi.org/10.1145/41625.41641.
  14. Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. Choice trees: Representing nondeterministic, recursive, and impure programs in Coq. Proc. ACM Program. Lang., 7(POPL):1770-1800, 2023. URL: https://doi.org/10.1145/3571254.
  15. Simon Foster, Chung-Kil Hur, and Jim Woodcock. Formally verified simulations of state-rich processes using interaction trees in Isabelle/HOL. In Serge Haddad and Daniele Varacca, editors, CONCUR 2021, volume 203 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPICS.CONCUR.2021.20.
  16. Florian Haftmann, Alexander Krauss, Ondrej Kuncar, and Tobias Nipkow. Data refinement in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP 2013, volume 7998, pages 100-115. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_10.
  17. Florian Haftmann and Tobias Nipkow. Code generation via higher-order rewrite systems. In Matthias Blume, Naoki Kobayashi, and Germán Vidal, editors, FLOPS 2010, volume 6009 of LNCS, pages 103-117. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12251-4_9.
  18. Brian Huffman and Ondrej Kuncar. Lifting and transfer: A modular design for quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, CPP 2013, volume 8307 of LNCS, pages 131-146. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03545-1_9.
  19. Bengt Jonsson. A fully abstract trace model for dataflow and asynchronous networks. Distributed Computing, 7:197-212, 1994. URL: https://doi.org/10.1007/BF02280834.
  20. Cezary Kaliszyk and Christian Urban. Quotients revisited for Isabelle/HOL. In William C. Chu, W. Eric Wong, Mathew J. Palakal, and Chih-Cheng Hung, editors, SAC 2011, pages 1639-1644. ACM, 2011. URL: https://doi.org/10.1145/1982185.1982529.
  21. Martin Kleppmann and Jay Kreps. Kafka, Samza and the Unix philosophy of distributed data. IEEE Data Eng. Bull., 38(4):4-14, 2015. URL: http://sites.computer.org/debull/A15dec/p4.pdf.
  22. Ondřej Kunčar. Types, abstraction and parametric polymorphism in higher-order logic. PhD thesis, Fakultät für Informatik, Technische Universität München, 2016. Google Scholar
  23. Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, and Mae Milano. Flo: A semantic foundation for progressive stream processing. Proc. ACM Program. Lang., 9(POPL):241-270, 2025. URL: https://doi.org/10.1145/3704845.
  24. Andreas Lochbihler and Pascal Stoop. Lazy algebraic types in Isabelle/HOL, 2018. Google Scholar
  25. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  26. Derek Gordon Murray, Frank McSherry, Rebecca Isaacs, Michael Isard, Paul Barham, and Martín Abadi. Naiad: a timely dataflow system. In Michael Kaminsky and Mike Dahlin, editors, SOSP 2013, pages 439-455. ACM, 2013. URL: https://doi.org/10.1145/2517349.2522738.
  27. Lawrence C. Paulson. A Fixedpoint Approach to (Co)Inductive and (Co)Datatype Definitions, pages 187-211. MIT Press, Cambridge, MA, USA, 2000. Google Scholar
  28. Damien Pous. Weak bisimulation up to elaboration. In Christel Baier and Holger Hermanns, editors, CONCUR 2006, volume 4137 of LNCS, pages 390-405. Springer, 2006. URL: https://doi.org/10.1007/11817949_26.
  29. Damien Pous. New up-to techniques for weak bisimulation. Theor. Comput. Sci., 380(1-2):164-180, 2007. URL: https://doi.org/10.1016/J.TCS.2007.02.060.
  30. Rafael Castro Gonçalves Silva and Dmitriy Traytel. Time-aware stream processing in Isabelle/HOL. In Tobias Nipkow, Lawrence C. Paulson, and Makarius Wenzel, editors, Isabelle workshop 2024, pages 1-19, 2024. URL: https://files.sketis.net/Isabelle_Workshop_2024/Isabelle_2024_paper_8.pdf (accessed: July 1, 2025).
  31. Rafael Castro Gonçalves Silva, Laouen Fernet, and Dmitriy Traytel. Nondeterministic asynchronous dataflow in Isabelle/HOL artifact, June 2025. URL: https://doi.org/10.5281/zenodo.15737868.
  32. Makarius Wenzel et al. The Isabelle/Isar reference manual, 2004. Google Scholar
  33. Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. Proc. ACM Program. Lang., 4(POPL):51:1-51:32, 2020. URL: https://doi.org/10.1145/3371119.
  34. Matei Zaharia, Tathagata Das, Haoyuan Li, Timothy Hunter, Scott Shenker, and Ion Stoica. Discretized streams: fault-tolerant streaming computation at scale. In Michael Kaminsky and Mike Dahlin, editors, SOSP 2013, pages 423-438. ACM, 2013. URL: https://doi.org/10.1145/2517349.2522737.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact