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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 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.
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
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
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
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
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
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
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
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)
Montesi, F.: Choreographic Programming. Ph.D. Thesis, IT University of Copenhagen (2013). http://www.fabriziomontesi.com/files/choreographic-programming.pdf
Montesi, F.: Introduction to Choreographies. Cambridge University Press, Cambridge (2023)
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
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
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
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
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
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 IFIP International Federation for Information Processing
About this paper
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)