Marco Carbone
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.
Supplemental Material
- BPMN. http://www.omg.org/spec/BPMN/2.0/.Google Scholar
- italianaSoftware. http://www.italianasoftware.com/.Google Scholar
- Jolie language. http://www.jolie-lang.org/.Google Scholar
- SOAP Specifications. http://www.w3.org/TR/soap/.Google Scholar
- WS-Addressing. http://www.w3.org/TR/ws-addr-core/.Google Scholar
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Briais and U. Nestmann. A formal semantics for protocol narrations. Theoretical Computer Science, 389(3):484--511, 2007. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- L. Caires and H. T. Vieira. Conversation types. Theoretical Computer Science, 411(51-52):4399--4440, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- M. Carbone. Session-based choreography with exceptions. In Proc. of PLACES, volume 241, pages 35--55. ENTCS, 2008. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Chor. Programming Language. http://www.chor-lang.org/.Google Scholar
- P.-M. Deniélou and N. Yoshida. Dynamic multirole session types. In Proc. of POPL, pages 435--446. ACM, 2011. Google ScholarDigital Library
- P.-M. Deniélou and N. Yoshida. Multiparty session types meet communicating automata. In Proc. of ESOP, LNCS, pages 194--213. Springer-Verlag, 2012. Google ScholarDigital Library
- Eclipse. The Eclipse IDE. http://www.eclipse.org/.Google Scholar
- Enea. ENEA: Italian National agency for new technologies, Energy and sustainable economic development. http://www.enea.it/.Google Scholar
- 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.Google ScholarCross Ref
- K. Honda, N. Yoshida, and M. Carbone. Multiparty asynchronous session types. In Proc. of POPL, volume 43(1), pages 273--284. ACM, 2008. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- R. Hu, N. Yoshida, and K. Honda. Session-based distributed programming in java. In ECOOP, pages 516--541, 2008. Google ScholarDigital Library
- International Telecommunication Union. Recommendation Z.120: Message Sequence Chart, 1996.Google Scholar
- 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. Google ScholarDigital Library
- M. Merro and D. Sangiorgi. On asynchrony in name-passing calculi. Mathematical Structures in Computer Science, 14(5):715--767, 2004. Google ScholarDigital Library
- F. Montesi and M. Carbone. Programming services with correlation sets. In ICSOC, pages 125--141, 2011. Google ScholarDigital Library
- F. Montesi, C. Guidi, and G. Zavattaro. Composing Services with JOLIE. In Proc. of ECOWS, pages 13--22, 2007. Google ScholarDigital Library
- OASIS. Web Services Business Process Execution Language. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.html.Google Scholar
- OOI. Ocean Observatories. http://www.oceanobservatories.org.Google Scholar
- OpenID. Specifications. http://openid.net/developers/specs/.Google Scholar
- PI4SOA. http://www.pi4soa.org, 2008.Google Scholar
- B. C. Pierce. Types and Programming Languages. MIT Press, MA, USA, 2002. Google ScholarDigital Library
- Qualit-E. Funded by Cognizant. http://www.cognizant.com/.Google Scholar
- Savara. JBoss Community. http://www.jboss.org/savara/.Google Scholar
- W3C WS-CDL Working Group. Web services choreography description language version 1.0. http://www.w3.org/TR/ws-cdl-10/, 2004.Google Scholar
- 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. Google ScholarDigital Library
Index Terms
- Deadlock-freedom-by-design: multiparty asynchronous global programming
Recommendations
Deadlock-freedom-by-design: multiparty asynchronous global programming
POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesOver 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 ...
Static lock capabilities for deadlock freedom
TLDI '12: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementationWe present a technique --- lock capabilities --- for statically verifying that multithreaded programs with locks will not deadlock. Most previous work on deadlock prevention requires a strict total order on all locks held simultaneously by a thread, but ...
Types for Active Objects with Static Deadlock Prevention
Process types statically ensure the acceptability of all messages sent to an object even if the set of acceptable messages changes dynamically. As proposed so far, process types do not ensure the return of answers; deadlocks may prevent objects from ...
Comments