Document Open Access Logo

Mailbox Types for Unordered Interactions

Authors Ugo de'Liguoro , Luca Padovani

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2018.15.pdf
  • Filesize: 0.6 MB
  • 28 pages

Document Identifiers

Author Details

Ugo de'Liguoro
  • Università di Torino, Dipartimento di Informatica, Torino, Italy
Luca Padovani
  • Università di Torino, Dipartimento di Informatica, Torino, Italy

Cite As Get BibTex

Ugo de'Liguoro and Luca Padovani. Mailbox Types for Unordered Interactions. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 15:1-15:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ECOOP.2018.15

Abstract

We propose a type system for reasoning on protocol conformance and deadlock freedom in networks of processes that communicate through unordered mailboxes. We model these networks in the mailbox calculus, a mild extension of the asynchronous pi-calculus with first-class mailboxes and selective input. The calculus subsumes the actor model and allows us to analyze networks with dynamic topologies and varying number of processes possibly mixing different concurrency abstractions. Well-typed processes are deadlock free and never fail because of unexpected messages. For a non-trivial class of them, junk freedom is also guaranteed. We illustrate the expressiveness of the calculus and of the type system by encoding instances of non-uniform, concurrent objects, binary sessions extended with joins and forks, and some known actor benchmarks.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type structures
  • Theory of computation → Process calculi
  • Software and its engineering → Concurrent programming structures
  • Software and its engineering → Message passing
Keywords
  • actors
  • concurrent objects
  • first-class mailboxes
  • unordered communication protocols
  • behavioral types
  • protocol conformance
  • deadlock freedom
  • junk freedom

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, 1986. Google Scholar
  2. Davide Ancona, Viviana Bono, Mario Bravetti, Joana Campos, Giuseppe Castagna, Pierre-Malo Deniélou, Simon J. Gay, Nils Gesbert, Elena Giachino, Raymond Hu, Einar Broch Johnsen, Francisco Martins, Viviana Mascardi, Fabrizio Montesi, Rumyana Neykova, Nicholas Ng, Luca Padovani, Vasco T. Vasconcelos, and Nobuko Yoshida. Behavioral Types in Programming Languages. Foundations and Trends in Programming Languages, 3:95-230, 2016. URL: http://dx.doi.org/10.1561/2500000031.
  3. Joe Armstrong. Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf, 2013. Google Scholar
  4. Janusz A. Brzozowski. Derivatives of Regular Expressions. Journal of ACM, 11(4):481-494, 1964. URL: http://dx.doi.org/10.1145/321239.321249.
  5. Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In Proceedings of FORTE'16, LNCS 9688, pages 74-95. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-39570-8_6.
  6. Luís Caires and Frank Pfenning. Session Types as Intuitionistic Linear Propositions. In Proceedings of CONCUR'10, LNCS 6269, pages 222-236. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15375-4_16.
  7. Minas Charalambides, Peter Dinges, and Gul A. Agha. Parameterized, concurrent session types for asynchronous multi-actor interactions. Science of Computer Programming, 115-116:100-126, 2016. URL: http://dx.doi.org/10.1016/j.scico.2015.10.006.
  8. Dominik Charousset, Raphael Hiesgen, and Thomas C. Schmidt. Revisiting actor programming in C++. Computer Languages, Systems & Structures, 45:105-131, 2016. URL: http://dx.doi.org/10.1016/j.cl.2016.01.002.
  9. Arghya Chatterjee, Branko Gvoka, Bing Xue, Zoran Budimlic, Shams Imam, and Vivek Sarkar. A distributed selectors runtime system for java applications. In Proceedings of PPPJ'16, pages 3:1-3:11. ACM, 2016. URL: http://dx.doi.org/10.1145/2972206.2972215.
  10. Maria Christakis and Konstantinos Sagonas. Detection of asynchronous message passing errors using static analysis. In Proceedings of PADL'11, LNCS 6539, pages 5-18. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-18378-2_3.
  11. John Conway. Regular Algebra and Finite Machines. William Clowes &Sons Ltd, 1971. Google Scholar
  12. Mario Coppo, Mariangiola Dezani-Ciancaglini, Nobuko Yoshida, and Luca Padovani. Global Progress for Dynamically Interleaved Multiparty Sessions. Mathematical Structures in Computer Science, 26:238-302, 2016. URL: http://dx.doi.org/10.1017/S0960129514000188.
  13. Bruno Courcelle. Fundamental Properties of Infinite Trees. Theoretical Computer Science, 25:95-169, 1983. URL: http://dx.doi.org/10.1016/0304-3975(83)90059-2.
  14. Silvia Crafa. Behavioural types for actor systems. Technical Report 1206.1687, arXiv, 2012. URL: http://arxiv.org/abs/1206.1687.
  15. Silvia Crafa and Luca Padovani. The Chemical Approach to Typestate-Oriented Programming. ACM Transactions on Programming Languages and Systems, 39:13:1-13:45, 2017. URL: http://dx.doi.org/10.1145/3064849.
  16. Ornela Dardha, Elena Giachino, and Davide Sangiorgi. Session types revisited. Information and Computation, 256:253-286, 2017. URL: http://dx.doi.org/10.1016/j.ic.2017.06.002.
  17. Ugo de'Liguoro and Luca Padovani. Mailbox types for unordered interactions. CoRR, abs/1801.04167, 2018. URL: http://arxiv.org/abs/1801.04167.
  18. Javier Esparza, Stefan Kiefer, and Michael Luttenberger. Newtonian program analysis. Journal of the ACM, 57(6):33:1-33:47, 2010. URL: http://dx.doi.org/10.1145/1857914.1857917.
  19. Simon Fowler. An Erlang implementation of multiparty session actors. In Proceedings of ICE'16, EPTCS 223, pages 36-50, 2016. URL: http://dx.doi.org/10.4204/EPTCS.223.3.
  20. Simon Fowler, Sam Lindley, and Philip Wadler. Mixing metaphors: Actors as channels and channels as actors. In Proceedings of ECOOP'17, LIPIcs 74, pages 11:1-11:28, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.ECOOP.2017.11.
  21. Simon J. Gay and Malcolm Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2-3):191-225, 2005. URL: http://dx.doi.org/10.1007/s00236-005-0177-z.
  22. Elena Giachino, Ludovic Henrio, Cosimo Laneve, and Vincenzo Mastandrea. Actors may synchronize, safely! In Proceedings PPDP'16, pages 118-131. ACM, 2016. URL: http://dx.doi.org/10.1145/2967973.2968599.
  23. Philipp Haller. On the integration of the actor model in mainstream technologies: the scala perspective. In Proceedings of AGERE! 2012, pages 1-6. ACM, 2012. URL: http://dx.doi.org/10.1145/2414639.2414641.
  24. Philipp Haller and Frank Sommers. Actors in Scala - concurrent programming for the multi-core era. Artima, 2011. Google Scholar
  25. Jiansen He, Philip Wadler, and Philip Trinder. Typecasting actors: From akka to takka. In Proceedings of the Fifth Annual Scala Workshop (SCALA'14), pages 23-33. ACM, 2014. URL: http://dx.doi.org/10.1145/2637647.2637651.
  26. Carl Hewitt, Peter Bishop, and Richard Steiger. A Universal Modular ACTOR Formalism for Artificial Intelligence. In Proceedings of IJCAI'73, pages 235-245. William Kaufmann, 1973. Google Scholar
  27. Kohei Honda. Types for Dyadic Interaction. In Proceedings of CONCUR'93, volume LNCS 715, pages 509-523. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-57208-2_35.
  28. Mark W. Hopkins and Dexter Kozen. Parikh’s Theorem in Commutative Kleene Algebra. In Proceedings of LICS'99, pages 394-401. IEEE, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782634.
  29. Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. Foundations of Session Types and Behavioural Contracts. ACM Computing Surveys, 49(1):3:1-3:36, 2016. URL: http://dx.doi.org/10.1145/2873052.
  30. Atsushi Igarashi and Naoki Kobayashi. A generic type system for the pi-calculus. Theoretical Computer Science, 311(1-3):121-163, 2004. URL: http://dx.doi.org/10.1016/S0304-3975(03)00325-6.
  31. Shams Mahmood Imam and Vivek Sarkar. Integrating task parallelism with actors. SIGPLAN Notices, 47(10):753-772, 2012. URL: http://dx.doi.org/10.1145/2398857.2384671.
  32. Shams Mahmood Imam and Vivek Sarkar. Savina - an actor benchmark suite: Enabling empirical evaluation of actor libraries. In Proceedings of AGERE! 2014, pages 67-80. ACM, 2014. URL: http://dx.doi.org/10.1145/2687357.2687368.
  33. Shams Mahmood Imam and Vivek Sarkar. Selectors: Actors with multiple guarded mailboxes. In Proceedings of AGERE! 2014, pages 1-14. ACM, 2014. URL: http://dx.doi.org/10.1145/2687357.2687360.
  34. Naoki Kobayashi. A Type System for Lock-Free Processes. Information and Computation, 177(2):122-159, 2002. URL: http://dx.doi.org/10.1006/inco.2002.3171.
  35. Naoki Kobayashi. Type systems for concurrent programs. Technical report, Tohoku University, 2007. Short version appeared in 10th Anniversary Colloquium of UNU/IIST, 2002. URL: http://www.kb.ecei.tohoku.ac.jp/~koba/papers/tutorial-type-extended.pdf.
  36. Naoki Kobayashi and Cosimo Laneve. Deadlock analysis of unbounded process networks. Information and Computation, 252:48-70, 2017. URL: http://dx.doi.org/10.1016/j.ic.2016.03.004.
  37. Naoki Kobayashi and Akinori Yonezawa. Type-theoretic foundations for concurrent object-oriented programming. In Proceedings of OOPSLA'94, pages 31-45. ACM, 1994. URL: http://dx.doi.org/10.1145/191080.191088.
  38. Naoki Kobayashi and Akinori Yonezawa. Asynchronous communication model based on linear logic. Formal Aspects of Computing, 7(2):113-149, 1995. URL: http://dx.doi.org/10.1007/BF01211602.
  39. Sam Lindley and J. Garrett Morris. A semantics for propositions as sessions. In Proceedings of ESOP'15, LNCS 9032, pages 560-584. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-662-46669-8_23.
  40. Vincenzo Mastandrea. Deadlock analysis with behavioral types for actors. In Proceedings of ICTCS'16, volume 1720 of CEUR Workshop Proceedings, pages 257-262, 2016. URL: http://ceur-ws.org/Vol-1720/short7.pdf.
  41. Dimitris Mostrous and Vasco T. Vasconcelos. Session typing for a featherweight Erlang. In Proceedings of COORDINATION'11, LNCS 6721, pages 95-109. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-21464-6_7.
  42. Elie Najm, Abdelkrim Nimour, and Jean-Bernard Stefani. Guaranteeing liveness in an object calculus through behavioural typing. In Proceedings of FORTE'99, volume 156, pages 203-221. Kluwer, 1999. Google Scholar
  43. Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. Logical Methods in Computer Science, 13(1), 2017. URL: http://dx.doi.org/10.23638/LMCS-13(1:17)2017.
  44. Luca Padovani. Deadlock and Lock Freedom in the Linear π-Calculus. In Proceedings of CSL-LICS'14, pages 72:1-72:10. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603116.
  45. Luca Padovani. Deadlock-Free Typestate-Oriented Programming. Programming Journal, 2, 2018. URL: http://dx.doi.org/10.22152/programming-journal.org/2018/2/15.
  46. Luca Padovani. MC², the Mailbox Calculus Checker, 2018. URL: http://www.di.unito.it/~padovani/Software/MCC/index.html.
  47. Benjamin C. Pierce and Davide Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409-453, 1996. Google Scholar
  48. Franz Puntigam. Strong types for coordinating active objects. Concurrency and Computation: Practice and Experience, 13(4):293-326, 2001. URL: http://dx.doi.org/10.1002/cpe.570.
  49. Franz Puntigam and Christof Peter. Types for active objects with static deadlock prevention. Fundamenta Informaticae, 48(4):315-341, 2001. URL: http://content.iospress.com/articles/fundamenta-informaticae/fi48-4-02.
  50. António Ravara and Vasco T. Vasconcelos. Typing non-uniform concurrent objects. In Proceedings of CONCUR'00, LNCS 1877, pages 474-488. Springer, 2000. URL: http://dx.doi.org/10.1007/3-540-44618-4_34.
  51. Davide Sangiorgi and David Walker. The Pi-Calculus - A theory of mobile processes. Cambridge University Press, 2001. Google Scholar
  52. Sriram Srinivasan and Alan Mycroft. Kilim: Isolation-typed actors for java. In Proceedings of ECOOP'08, LNCS 5142, pages 104-128. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70592-5_6.
  53. Samira Tasharofi, Peter Dinges, and Ralph E. Johnson. Why do scala developers mix the actor model with other concurrency models? In Proceedings of ECOOP'13, LNCS 7920, pages 302-326. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39038-8_13.
  54. Carlos A. Varela and Gul Agha. Programming dynamically reconfigurable open systems with SALSA. SIGPLAN Notices, 36(12):20-34, 2001. URL: http://dx.doi.org/10.1145/583960.583964.
  55. Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384-418, 2014. URL: http://dx.doi.org/10.1017/S095679681400001X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact