skip to main content
10.1145/2429069.2429101acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
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)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
  • (2024)Alice or Bob?: Process polymorphism in choreographiesJournal of Functional Programming10.1017/S095679682300011434Online publication date: 23-Jan-2024
  • (2024)Branching pomsets: Design, expressiveness and applications to choreographiesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100919136(100919)Online publication date: Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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]

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

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

Qualifiers

  • Research-article

Conference

POPL '13
Sponsor:

Acceptance Rates

Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

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)Choral: Object-oriented Choreographic ProgrammingACM Transactions on Programming Languages and Systems10.1145/363239846:1(1-59)Online publication date: 16-Jan-2024
  • (2024)Alice or Bob?: Process polymorphism in choreographiesJournal of Functional Programming10.1017/S095679682300011434Online publication date: 23-Jan-2024
  • (2024)Branching pomsets: Design, expressiveness and applications to choreographiesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100919136(100919)Online publication date: Jan-2024
  • (2024)The Concurrent Calculi Formalisation BenchmarkCoordination Models and Languages10.1007/978-3-031-62697-5_9(149-158)Online publication date: 17-Jun-2024
  • (2024)A Probabilistic Choreography Language for PRISMCoordination Models and Languages10.1007/978-3-031-62697-5_2(20-37)Online publication date: 17-Jun-2024
  • (2024)Bridging Between Active Objects: Multitier Programming for Distributed, Concurrent SystemsActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_4(92-122)Online publication date: 29-Jan-2024
  • (2023)Choreographic Programming of Isolated TransactionsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.378.5378(49-60)Online publication date: 13-Apr-2023
  • (2023)HasChor: Functional Choreographic Programming for All (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36078497:ICFP(541-565)Online publication date: 31-Aug-2023
  • (2023)Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint ProjectionProceedings of the ACM on Programming Languages10.1145/35860317:OOPSLA1(112-142)Online publication date: 6-Apr-2023
  • (2023)LEMMA2JolieScience of Computer Programming10.1016/j.scico.2023.102956228:COnline publication date: 1-Jun-2023
  • 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