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

Marco Carbone, Fabrizio Montesi [2013].
In proceedings of POPL 2013, pp. 263-274.

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-bydesign), provides type inference, and supports session mobility. We give a notion of Endpoint Projection (EPP) which generates correct entity code (as π-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.

Links

wikidata.org

Additional notes

None

Cite (BibTeX)

Click to expand

@inproceedings{DBLP:conf/popl/CarboneM13,
  author       = {Marco Carbone and
                  Fabrizio Montesi},
  editor       = {Roberto Giacobazzi and
                  Radhia Cousot},
  title        = {Deadlock-freedom-by-design: multiparty asynchronous global programming},
  booktitle    = {The 40th Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of
                  Programming Languages, {POPL} '13, Rome, Italy - January 23 - 25,
                  2013},
  pages        = {263--274},
  publisher    = {{ACM}},
  year         = {2013},
  url          = {https://doi.org/10.1145/2429069.2429101},
  doi          = {10.1145/2429069.2429101},
  timestamp    = {Thu, 24 Jun 2021 16:19:31 +0200},
  biburl       = {https://dblp.org/rec/conf/popl/CarboneM13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):