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

Marco Carbone 1 Fabrizio Montesi 1, 2
2 FOCUS - Foundations of Component-based Ubiquitous Systems
CRISAM - Inria Sophia Antipolis - Méditerranée , DISI - Dipartimento di Informatica - Scienza e Ingegneria [Bologna]
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.
Type de document :
Communication dans un congrès
POPL - 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - 2013, 2013, Rome, Italy. ACM, pp.263-274, 2013
Liste complète des métadonnées

https://hal.inria.fr/hal-00909320
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:46:41
Dernière modification le : jeudi 11 janvier 2018 - 16:24:58

Identifiants

  • HAL Id : hal-00909320, version 1

Collections

Citation

Marco Carbone, Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. POPL - 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - 2013, 2013, Rome, Italy. ACM, pp.263-274, 2013. 〈hal-00909320〉

Partager

Métriques

Consultations de la notice

80