SpringerLink
Log in

Certified Compilation of Choreographies with hacc

  • Conference paper
  • First Online:
Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13910))

  • 174 Accesses

Abstract

Programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. Choreographic programming addresses this challenge by equip** developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP).

While choreographic programming prevents manual mistakes in the implementation of communications, the correctness of a choreographic programming framework crucially hinges on the correctness of its complex compiler, which has motivated formalisation of theories of choreographic programming in theorem provers. In this paper, we build upon one of these formalisations to construct a toolchain that produces executable code from a choreography.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    CC includes runtime terms, needed for the semantics. Programmers should not write them explicitly, so we do not include them in our datatype.

  2. 2.

    In Coq, also includes the set of processes involved in each procedure. In theory, this set might not be computable, as there may be infinitely many procedures. This cannot happen in hand-written choreographies, so our wrapper computes this set.

References

  1. Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. ACM SIGPLAN Notices 48(1), 263–274 (2013). https://doi.org/10.1145/2429069.2429101

    Article  MATH  Google Scholar 

  2. Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38–66 (2020). https://doi.org/10.1016/j.tcs.2019.07.005. https://doi.org/10.1016/j.tcs.2019.07.005

  3. Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: Cerone, A., Ölveczky, P.C. (eds.) ICTAC 2021. LNCS, vol. 12819, pp. 115–133. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-85315-0_8

    Chapter  Google Scholar 

  4. Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a turing-complete choreographic language in coq. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving, ITP 2021, 29 June to 1 July 2021, Rome, Italy (Virtual Conference). LIPIcs, vol. 193, pp. 15:1–15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.ITP.2021.15

  5. Cruz-Filipe, L., Montesi, F., Peressotti, M.: A formal theory of choreographic programming. CoRR abs/2209.01886 (2022). https://doi.org/10.48550/ar**v.2209.01886. https://doi.org/10.48550/ar**v.2209.01886

  6. Hirsch, A.K., Garg, D.: Pirouette: higher-order typed functional choreographies. Proc. ACM Program. Lang. 6(POPL), 1–27 (2022). https://doi.org/10.1145/3498684. https://doi.org/10.1145/3498684

  7. Leesatapornwongsa, T., Lukman, J.F., Lu, S., Gunawi, H.S.: TaxDC: A taxonomy of non-deterministic concurrency bugs in datacenter distributed systems. In: Proceedings of ASPLOS, pp. 517–530 (2016)

    Google Scholar 

  8. Montesi, F.: Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen (2013). http://www.fabriziomontesi.com/files/choreographic-programming.pdf

  9. Montesi, F.: Introduction to Choreographies. Cambridge University Press, Cambridge (2023)

    Book  Google Scholar 

  10. Montesi, F., Guidi, C., Zavattaro, G.: Service-oriented programming with Jolie. In: Bouguettaya, A., Sheng, Q.Z., Daniel, F. (eds.) Web Services Foundations, pp. 81–107. Springer, Cham (2014). https://doi.org/10.1007/978-1-4614-7518-7_4

    Chapter  Google Scholar 

  11. Myreen, M.O., Owens, S.: Proof-producing synthesis of ML from higher-order logic. In: International Conference on Functional Programming (ICFP), pp. 115–126. ACM Press (2012). https://doi.org/10.1145/2364527.2364545. https://cakeml.org/icfp12/index.html

  12. Pohjola, J.Å., Gómez-Londoño, A., Shaker, J., Norrish, M.: Kalas: A verified, end-to-end compiler for a choreographic language. In: Andronick, J., de Moura, L. (eds.) 13th International Conference on Interactive Theorem Proving, ITP 2022, 7-10 August 2022, Haifa, Israel. LIPIcs, vol. 237, pp. 27:1–27:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.ITP.2022.27

  13. Scalas, A., Yoshida, N.: Less is more: multiparty session types revisited. Proc. ACM Program. Lang. 3(POPL), 30:1–30:29 (2019). https://doi.org/10.1145/3290343

Download references

Acknowledgements

This work was partially supported by Villum Fonden, grant no. 29518, and the Independent Research Fund Denmark, grant no. 0135-00219.

Author information

Authors and Affiliations

  1. Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark

    Luís Cruz-Filipe, Lovro Lugović & Fabrizio Montesi

Authors
  1. Luís Cruz-Filipe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lovro Lugović
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Fabrizio Montesi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lovro Lugović .

Editor information

Editors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Marieke Huisman

  2. NOVA School of Science and Technology and NOVA LINCS, Caparica, Portugal

    António Ravara

Rights and permissions

Reprints and permissions

Copyright information

© 2023 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Cruz-Filipe, L., Lugović, L., Montesi, F. (2023). Certified Compilation of Choreographies with hacc. In: Huisman, M., Ravara, A. (eds) Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2023. Lecture Notes in Computer Science, vol 13910. Springer, Cham. https://doi.org/10.1007/978-3-031-35355-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-35355-0_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-35354-3

  • Online ISBN: 978-3-031-35355-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation