skip to main content
research-article

Deadlock-freedom-by-design: multiparty asynchronous global programming

Published: 23 January 2013 Publication History

Abstract

Over the last decade, global descriptions have been successfully employed for the verification and implementation of communicating systems, respectively as protocol specifications and choreographies. In this work, we bring these two practices together by proposing a purely-global programming model. We show a novel interpretation of asynchrony and parallelism in a global setting and develop a typing discipline that verifies choreographies against protocol specifications, based on multiparty sessions. Exploiting the nature of global descriptions, our type system defines a new class of deadlock-free concurrent systems (deadlock-freedom-by-design), provides type inference, and supports session mobility. We give a notion of Endpoint Projection (EPP) which generates correct entity code (as pi-calculus terms) from a choreography. Finally, we evaluate our approach by providing a prototype implementation for a concrete programming language and by applying it to some examples from multicore and service-oriented programming.

Supplementary Material

JPG File (r1d2_talk5.jpg)
MP4 File (r1d2_talk5.mp4)

References

[1]
BPMN. http://www.omg.org/spec/BPMN/2.0/.
[2]
italianaSoftware. http://www.italianasoftware.com/.
[3]
Jolie language. http://www.jolie-lang.org/.
[4]
SOAP Specifications. http://www.w3.org/TR/soap/.
[5]
WS-Addressing. http://www.w3.org/TR/ws-addr-core/.
[6]
P. Baltazar, L. Caires, V. T. Vasconcelos, and H. T. Vieira. A Type System for Flexible Role Assignment in Multiparty Communicating Systems. In Proc. of TGC, 2012. To appear.
[7]
L. Bettini, M. Coppo, L. D'Antoni, M. D. Luca, M. Dezani-Ciancaglini, and N. Yoshida. Global progress in dynamically interleaved multiparty sessions. In CONCUR, volume 5201 of LNCS, pages 418--433. Springer, 2008.
[8]
K. Bhargavan, R. Corin, P.-M. Denielou, C. Fournet, and J. J. Leifer. Cryptographic protocol synthesis and verification for multiparty sessions. In Proc. of CSF, pages 124--140, 2009.
[9]
S. Briais and U. Nestmann. A formal semantics for protocol narrations. Theoretical Computer Science, 389(3):484--511, 2007.
[10]
N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro. Choreography and orchestration conformance for system design. In Proc. of Coordination, volume 4038 of LNCS, pages 63--81. Springer-Verlag, 2006.
[11]
L. Caires and H. T. Vieira. Conversation types. Theoretical Computer Science, 411(51-52):4399--4440, 2010.
[12]
C. Caleiro, L. Vigan`o, and D. A. Basin. On the semantics of Alice & Bob specifications of security protocols. Theor. Comput. Sci., 367(1-2):88--122, 2006.
[13]
M. Carbone. Session-based choreography with exceptions. In Proc. of PLACES, volume 241, pages 35--55. ENTCS, 2008.
[14]
M. Carbone and F. Montesi. Typed multiparty global programming. Technical Report 149, IT University of Copenhagen, 2011. http://www.itu.dk/people/fabr/papers/multichor.
[15]
M. Carbone, K. Honda, and N. Yoshida. Structured communicationcentred programming for web services. In Proc. of ESOP, volume 4421 of LNCS, pages 2--17. Springer-Verlag, 2007.
[16]
Chor. Programming Language. http://www.chor-lang.org/.
[17]
P.-M. Deniélou and N. Yoshida. Dynamic multirole session types. In Proc. of POPL, pages 435--446. ACM, 2011.
[18]
P.-M. Deniélou and N. Yoshida. Multiparty session types meet communicating automata. In Proc. of ESOP, LNCS, pages 194--213. Springer-Verlag, 2012.
[19]
Eclipse. The Eclipse IDE. http://www.eclipse.org/.
[20]
Enea. ENEA: Italian National agency for new technologies, Energy and sustainable economic development. http://www.enea.it/.
[21]
X. Fu, T. Bultan, and J. Su. Realizability of conversation protocols with message contents. International Journal on Web Service Res., 2 (4):68--93, 2005.
[22]
K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In Proc. of POPL, volume 43(1), pages 273--284. ACM, 2008.
[23]
K. Honda, A. Mukhamedov, G. Brown, T.-C. Chen, and N. Yoshida. Scribbling interactions with a formal foundation. In Proc. of ICDCIT, volume 6536 of LNCS, pages 55--75. Springer, 2011.
[24]
R. Hu, N. Yoshida, and K. Honda. Session-based distributed programming in java. In ECOOP, pages 516--541, 2008.
[25]
International Telecommunication Union. Recommendation Z.120: Message Sequence Chart, 1996.
[26]
I. Lanese, C. Guidi, F. Montesi, and G. Zavattaro. Bridging the gap between interaction- and process-oriented choreographies. In Proc. of SEFM, pages 323--332. IEEE, 2008.
[27]
M. Merro and D. Sangiorgi. On asynchrony in name-passing calculi. Mathematical Structures in Computer Science, 14(5):715--767, 2004.
[28]
F. Montesi and M. Carbone. Programming services with correlation sets. In ICSOC, pages 125--141, 2011.
[29]
F. Montesi, C. Guidi, and G. Zavattaro. Composing Services with JOLIE. In Proc. of ECOWS, pages 13--22, 2007.
[30]
OASIS. Web Services Business Process Execution Language. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html.
[31]
OOI. Ocean Observatories. http://www.oceanobservatories.org.
[32]
OpenID. Specifications. http://openid.net/developers/specs/.
[33]
PI4SOA. http://www.pi4soa.org, 2008.
[34]
B. C. Pierce. Types and Programming Languages. MIT Press, MA, USA, 2002.
[35]
Qualit-E. Funded by Cognizant. http://www.cognizant.com/.
[36]
Savara. JBoss Community. http://www.jboss.org/savara/.
[37]
W3C WS-CDL Working Group. Web services choreography description language version 1.0. http://www.w3.org/TR/ws-cdl-10/, 2004.
[38]
N. Yoshida, P.-M. Deniélou, A. Bejleri, and R. Hu. Parameterised multiparty session types. In FOSSACS'10, volume 6014 of LNCS, pages 128--145, 2010.

Cited By

View all
  • (2024)Towards a Framework for Transitioning from Monolith to ServerlessThe Combined Power of Research, Education, and Dissemination10.1007/978-3-031-73887-6_13(167-182)Online publication date: 23-Oct-2024
  • (2023)Certified Compilation of Choreographies with haccFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-35355-0_3(29-36)Online publication date: 19-Jun-2023
  • (2023)VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsFormal Methods10.1007/978-3-031-27481-7_19(321-339)Online publication date: 3-Mar-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. choreography
  2. concurrency
  3. sessions
  4. types

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)43
  • Downloads (Last 6 weeks)9
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Towards a Framework for Transitioning from Monolith to ServerlessThe Combined Power of Research, Education, and Dissemination10.1007/978-3-031-73887-6_13(167-182)Online publication date: 23-Oct-2024
  • (2023)Certified Compilation of Choreographies with haccFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-35355-0_3(29-36)Online publication date: 19-Jun-2023
  • (2023)VeyMont: Parallelising Verified Programs Instead of Verifying Parallel ProgramsFormal Methods10.1007/978-3-031-27481-7_19(321-339)Online publication date: 3-Mar-2023
  • (2022)A Type Discipline for Message Passing Parallel ProgramsACM Transactions on Programming Languages and Systems10.1145/3552519Online publication date: 10-Aug-2022
  • (2022)A Predicate Transformer for ChoreographiesProgramming Languages and Systems10.1007/978-3-030-99336-8_19(520-547)Online publication date: 29-Mar-2022
  • (2021)Prioritise the Best VariationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-030-78089-0_6(100-119)Online publication date: 8-Jun-2021
  • (2020)CHOReVOLUTION: Service choreography in practiceScience of Computer Programming10.1016/j.scico.2020.102498(102498)Online publication date: Jun-2020
  • (2020)A microservice composition approach based on the choreography of BPMN fragmentsInformation and Software Technology10.1016/j.infsof.2020.106370127(106370)Online publication date: Nov-2020
  • (2020)Choreography AutomataCoordination Models and Languages10.1007/978-3-030-50029-0_6(86-106)Online publication date: 10-Jun-2020
  • (2020)Exploring Type-Level Bisimilarity towards More Expressive Multiparty Session TypesProgramming Languages and Systems10.1007/978-3-030-44914-8_10(251-279)Online publication date: 27-Apr-2020
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media