Article

A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming

Authors:

Sung-Shik Jongmans,

Petra van den BosAuthors Info & Claims

Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings

Pages 520 - 547

https://doi.org/10.1007/978-3-030-99336-8_19

Published: 05 April 2022 Publication History

Abstract

Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if/while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.

References

[1]

Apt, K.R., Olderog, E.: Fifty years of hoare’s logic. Formal Aspects Comput. 31(6), 751–807 (2019)

[2]

Baeten, J.C.M., Bravetti, M.: A ground-complete axiomatisation of finite-state processes in a generic process algebra. Mathematical Structures in Computer Science 18(6), 1057–1089 (2008)

[3]

Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: POPL. pp. 191–202. ACM (2012)

[4]

Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The vercors tool set: Verification of parallel and concurrent software. In: IFM. Lecture Notes in Computer Science, vol. 10510, pp. 102–110. Springer (2017)

[5]

Bocchi, L., Honda, K., Tuosto, E., Yoshida, N.: A theory of design-by-contract for distributed multiparty interactions. In: CONCUR. Lecture Notes in Computer Science, vol. 6269, pp. 162–176. Springer (2010)

[6]

Brookes, S.: A semantics for concurrent separation logic. Theor. Comput. Sci. 375(1-3), 227–270 (2007)

[7]

Carbone, M., Cruz-Filipe, L., Montesi, F., Murawska, A.: Multiparty classical choreographies. In: LOPSTR. Lecture Notes in Computer Science, vol. 11408, pp. 59–76. Springer (2018)

[8]

Carbone, M., Honda, K., Yoshida, N.: Structured communication-centred programming for web services. In: ESOP. Lecture Notes in Computer Science, vol. 4421, pp. 2–17. Springer (2007)

[9]

Carbone, M., Honda, K., Yoshida, N.: Structured communication-centered programming for web services. ACM Trans. Program. Lang. Syst. 34(2), 8:1–8:78 (2012)

[10]

Carbone, M., Montesi, F.: Deadlock-freedom-by-design: multiparty asynchronous global programming. In: POPL. pp. 263–274. ACM (2013)

[11]

Carbone, M., Montesi, F., Schürmann, C.: Choreographies, logically. In: CONCUR. Lecture Notes in Computer Science, vol. 8704, pp. 47–62. Springer (2014)

[12]

Carbone, M., Montesi, F., Schürmann, C.: Choreographies, logically. Distributed Comput. 31(1), 51–67 (2018)

[13]

Coppo, M., Dezani-Ciancaglini, M., Yoshida, N., Padovani, L.: Global progress for dynamically interleaved multiparty sessions. Mathematical Structures in Computer Science 26(2), 238–302 (2016)

[14]

Cruz-Filipe, L., Larsen, K.S., Montesi, F.: The paths to choreography extraction. In: FoSSaCS. Lecture Notes in Computer Science, vol. 10203, pp. 424–440 (2017)

[15]

Cruz-Filipe, L., Montesi, F.: Choreographies in practice. In: FORTE. Lecture Notes in Computer Science, vol. 9688, pp. 114–123. Springer (2016)

[16]

Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. In: FACS. Lecture Notes in Computer Science, vol. 10231, pp. 17–35 (2016)

[17]

Cruz-Filipe, L., Montesi, F.: Encoding asynchrony in choreographies. In: SAC. pp. 1175–1177. ACM (2017)

[18]

Cruz-Filipe, L., Montesi, F.: Procedural choreographic programming. In: FORTE. Lecture Notes in Computer Science, vol. 10321, pp. 92–107. Springer (2017)

[19]

Cruz-Filipe, L., Montesi, F.: A core model for choreographic programming. Theor. Comput. Sci. 802, 38–66 (2020)

[20]

Cruz-Filipe, L., Montesi, F., Peressotti, M.: Communications in choreographies, revisited. In: SAC. pp. 1248–1255. ACM (2018)

[21]

Cruz-Filipe, L., Montesi, F., Peressotti, M.: Certifying choreography compilation. In: ICTAC. Lecture Notes in Computer Science, vol. 12819, pp. 115–133. Springer (2021)

[22]

Cruz-Filipe, L., Montesi, F., Peressotti, M.: Formalising a turing-complete choreographic language in coq. In: ITP. LIPIcs, vol. 193, pp. 15:1–15:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

[23]

Deniélou, P., Yoshida, N.: Dynamic multirole session types. In: POPL. pp. 435–446. ACM (2011)

[24]

Deniélou, P., Yoshida, N.: Multiparty compatibility in communicating automata: Characterisation and synthesis of global session types. In: ICALP (2). Lecture Notes in Computer Science, vol. 7966, pp. 174–186. Springer (2013)

[25]

Deniélou, P., Yoshida, N., Bejleri, A., Hu, R.: Parameterised multiparty session types. Logical Methods in Computer Science 8(4) (2012)

[26]

Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)

[27]

Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor. Comput. Sci. 328(1-2), 19–37 (2004)

[28]

Giallorenzo, S., Montesi, F., Gabbrielli, M.: Applied choreographies. In: FORTE. Lecture Notes in Computer Science, vol. 10854, pp. 21–40. Springer (2018)

[29]

Giallorenzo, S., Montesi, F., Peressotti, M., Richter, D., Salvaneschi, G., Weisenburger, P.: Multiparty languages: The choreographic and multitier cases (pearl). In: ECOOP. LIPIcs, vol. 194, pp. 22:1–22:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

[30]

van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)

[31]

Hildebrandt, T.T., Slaats, T., López, H.A., Debois, S., Carbone, M.: Declarative choreographies and liveness. In: FORTE. Lecture Notes in Computer Science, vol. 11535, pp. 129–147. Springer (2019)

[32]

Hinrichsen, J.K., Bengtson, J., Krebbers, R.: Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4(POPL), 6:1–6:30 (2020)

[33]

Hoare, C.A.R.: Parallel programming: An axiomatic approach. Comput. Lang. 1(2), 151–160 (1976)

[34]

Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: ESOP. Lecture Notes in Computer Science, vol. 1381, pp. 122–138. Springer (1998)

[35]

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. pp. 273–284. ACM (2008)

[36]

Hurlin, C.: Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. (Spécification et vérification de programmes orientés objets en logique de séparation). Ph.D. thesis, University of Nice Sophia Antipolis, France (2009)

[37]

Itai, A., Rodeh, M.: Symmetry breaking in distributive networks. In: FOCS. pp. 150–158. IEEE Computer Society (1981)

[38]

Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60–87 (1990)

[39]

Jongmans, S.S., van den Bos, P.: A Predicate Transformer for Choreographies (Full Version). Tech. Rep. OUNL-CS-2022-01, Open University of the Netherlands (2022)

[40]

Jongmans, S.S., van den Bos, P.: A Predicate Transformer for Choreographies (Technical Report). Tech. Rep. OUNL-CS-2022-02, Open University of the Netherlands (2022)

[41]

López, H.A., Marques, E.R.B., Martins, F., Ng, N., Santos, C., Vasconcelos, V.T., Yoshida, N.: Protocol-based verification of message-passing parallel programs. In: OOPSLA. pp. 280–298. ACM (2015)

[42]

Montesi, F., Yoshida, N.: Compositional choreographies. In: CONCUR. Lecture Notes in Computer Science, vol. 8052, pp. 425–439. Springer (2013)

[43]

Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: compile-time API generation of distributed protocols with refinements in f#. In: CC. pp. 128–138. ACM (2018)

[44]

O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1-3), 271–307 (2007)

[45]

Peleg, D.: Time-optimal leader election in general networks. J. Parallel Distributed Comput. 8(1), 96–99 (1990)

[46]

Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies - safe runtime updates of distributed applications. In: COORDINATION. Lecture Notes in Computer Science, vol. 9037, pp. 67–82. Springer (2015)

[47]

Preda, M.D., Gabbrielli, M., Giallorenzo, S., Lanese, I., Mauro, J.: Dynamic choreographies: Theory and implementation. Log. Methods Comput. Sci. 13(2) (2017)

[48]

Preda, M.D., Giallorenzo, S., Lanese, I., Mauro, J., Gabbrielli, M.: AIOCJ: A choreographic framework for safe adaptive distributed applications. In: SLE. Lecture Notes in Computer Science, vol. 8706, pp. 161–170. Springer (2014)

[49]

Rensink, A., Wehrheim, H.: Process algebra with action dependencies. Acta Informatica 38(3), 155–234 (2001)

[50]

Sangiorgi, D., Walker, D.: The Pi-Calculus - a theory of mobile processes. Cambridge University Press (2001)

[51]

Toninho, B., Yoshida, N.: Certifying data in multiparty session types. J. Log. Algebraic Methods Program. 90, 61–83 (2017)

[52]

Zhou, F., Ferreira, F., Hu, R., Neykova, R., Yoshida, N.: Statically verified refinements for multiparty protocols. Proc. ACM Program. Lang. 4(OOPSLA), 148:1–148:30 (2020)

Cited By

Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
Armborst LBos Pvan den Haak LHuisman MRubbens RŞakar ÖTasche P(2024)The VerCors Verifier: A Progress ReportComputer Aided Verification10.1007/978-3-031-65630-9_1(3-18)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_1
van den Bos PJongmans S(2023)VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsFormal Methods10.1007/978-3-031-27481-7_19(321-339)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_19
Show More Cited By

Index Terms

A Predicate Transformer for Choreographies: Computing Preconditions in Choreographic Programming

Index terms have been assigned to the content through auto-classification.

Recommendations

Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...
Automatic predicate abstraction of C programs
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation

Model checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

Programming Languages and Systems: 31st European Symposium on Programming, ESOP 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings

Apr 2022

617 pages

ISBN:978-3-030-99335-1

DOI:10.1007/978-3-030-99336-8

Editor:
Ilya Sergey
National University of Singapore, Singapore, Singapore

© The Author(s) 2022.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 05 April 2022

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 30 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Giallorenzo SMontesi FPeressotti M(2024)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
https://dl.acm.org/doi/10.1145/3632398
Armborst LBos Pvan den Haak LHuisman MRubbens RŞakar ÖTasche P(2024)The VerCors Verifier: A Progress ReportComputer Aided Verification10.1007/978-3-031-65630-9_1(3-18)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65630-9_1
van den Bos PJongmans S(2023)VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsFormal Methods10.1007/978-3-031-27481-7_19(321-339)Online publication date: 6-Mar-2023
https://dl.acm.org/doi/10.1007/978-3-031-27481-7_19
Coto ABarbanera FLanese IRossi DTuosto E(2022)On Formal Choreographic Modelling: A Case Study in EU Business ProcessesLeveraging Applications of Formal Methods, Verification and Validation. Verification Principles10.1007/978-3-031-19849-6_13(205-219)Online publication date: 22-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19849-6_13
Cruz-Filipe LGraversen ELugović LMontesi FPeressotti M(2022)Functional Choreographic ProgrammingTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_15(212-237)Online publication date: 27-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-17715-6_15

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents