Typing Copyless Message Passing

Viviana Bono; Luca Padovani

doi:10.2168/LMCS-8(1:17)2012

Viviana Bono ; Luca Padovani - Typing Copyless Message Passing

lmcs:798 - Logical Methods in Computer Science, March 2, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:17)2012

Typing Copyless Message PassingArticle

Authors: Viviana Bono ; Luca Padovani

We present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS. The calculus is equipped with a type system ensuring that well-typed processes are free from memory faults, memory leaks, and communication errors. The type system is essentially linear, but we show that linearity alone is inadequate, because it leaves room for scenarios where well-typed processes leak significant amounts of memory. We address these problems basing the type system upon an original variant of session types.

Comment: 50 pages

https://doi.org/10.2168/LMCS-8(1:17)2012

Source: arXiv.org:1202.2086

Volume: Volume 8, Issue 1

Secondary volumes: Selected Papers of the 20th European Symposium on Programming (ESOP 2011)

Published on: March 2, 2012

Imported on: September 21, 2011

Keywords: Computer Science - Programming Languages, F.1.2, F.3.3, F.3.1, D.4.4

Licence: arXiv.org - Non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

68Q85 - Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Sources:

[1] zbMATH Open.

Bibliographic References

19 Documents citing this article

Bernardo Almeida;Andreia Mordido;Peter Thiemann;Vasco T. Vasconcelos, 2022, Polymorphic lambda calculus with context-free session types, Information and Computation, 289, pp. 104948, 10.1016/j.ic.2022.104948, https://doi.org/10.1016/j.ic.2022.104948.

Ankush Das;Henry DeYoung;Andreia Mordido;Frank Pfenning, 2021, Nested Session Types, Lecture notes in computer science, pp. 178-206, 10.1007/978-3-030-72019-3_7, https://doi.org/10.1007/978-3-030-72019-3_7.

Filipe Casal;Andreia Mordido;Vasco T. Vasconcelos, 2021, Mixed sessions, Theoretical Computer Science, 897, pp. 23-48, 10.1016/j.tcs.2021.08.005, https://doi.org/10.1016/j.tcs.2021.08.005.

Vasco T. Vasconcelos;Filipe Casal;Bernardo Almeida;Andreia Mordido, 2020, Mixed Sessions, Lecture notes in computer science, pp. 715-742, 10.1007/978-3-030-44914-8_26, https://doi.org/10.1007/978-3-030-44914-8_26.

Giuseppe Castagna;Mariangiola Dezani-Ciancaglini;Elena Giachino;Luca Padovani, 2019, Foundations of Session Types, Institutional Research Information System University of Turin (University of Turin), 13, pp. 1-3, 10.1145/3354166.3356340, http://hdl.handle.net/2318/1712465.

Alceste Scalas;Nobuko Yoshida, 2018, Multiparty session types, beyond duality, Journal of Logical and Algebraic Methods in Programming, 97, pp. 55-84, 10.1016/j.jlamp.2018.01.001, https://doi.org/10.1016/j.jlamp.2018.01.001.

LUCA PADOVANI, 2016, A simple library implementation of binary sessions, Institutional Research Information System University of Turin (University of Turin), 27, 10.1017/s0956796816000289, http://hdl.handle.net/2318/1634956.

Sam Lindley;J. Garrett Morris, 2016, Talking bananas: structural recursion for session types, ACM SIGPLAN Notices, 51, 9, pp. 434-447, 10.1145/3022670.2951921.

Sam Lindley;J. Garrett Morris, 2016, Talking bananas: structural recursion for session types, Edinburgh Research Explorer, pp. 434-447, 10.1145/2951913.2951921, http://dl.acm.org/citation.cfm?id=2951921.

Giovanni Bernardi;Matthew Hennessy, 2014, Using Higher-Order Contracts to Model Session Types (Extended Abstract), Lecture notes in computer science, pp. 387-401, 10.1007/978-3-662-44584-6_27.

Giovanni Bernardi;Ornela Dardha;Simon J. Gay;Dimitrios Kouzapas, 2014, On Duality Relations for Session Types, ENLIGHTEN (Jurnal Bimbingan dan Konseling Islam), pp. 51-66, 10.1007/978-3-662-45917-1_4.

Luca Padovani, 2014, Deadlock and lock freedom in the linear π-calculus, pp. 1-10, 10.1145/2603088.2603116, https://inria.hal.science/hal-00932356.

Étienne Lozes;Jules Villard, 2014, Shared contract-obedient channels, 100, pp. 28-60, 10.1016/j.scico.2014.09.008, https://hal.science/hal-01905136.

Luca Padovani, 2013, From Lock Freedom to Progress Using Session Types, Electronic Proceedings in Theoretical Computer Science, 137, pp. 3-19, 10.4204/eptcs.137.2, https://doi.org/10.4204/eptcs.137.2.

Luís Caires;Jorge A. Pérez;Frank Pfenning;Bernardo Toninho, 2013, Behavioral Polymorphism and Parametricity in Session-Based Communication, Lecture notes in computer science, pp. 330-349, 10.1007/978-3-642-37036-6_19.

Svetlana Jakšić;Luca Padovani, 2013, Exception handling for copyless messaging, Science of Computer Programming, 84, pp. 22-51, 10.1016/j.scico.2013.05.001.

Viviana Bono;Luca Padovani;Andrea Tosatto, 2013, Polymorphic Types for Leak Detection in a Session-Oriented Functional Language, Lecture notes in computer science, pp. 83-98, 10.1007/978-3-642-38592-6_7, https://doi.org/10.1007/978-3-642-38592-6_7.

Svetlana Jakšić;Luca Padovani, 2012, Exception handling for copyless messaging, Institutional Research Information System University of Turin (University of Turin), pp. 151-162, 10.1145/2370776.2370796, http://hdl.handle.net/2318/126473.

Étienne Lozes;Jules Villard, 2012, Shared Contract-Obedient Endpoints, Electronic Proceedings in Theoretical Computer Science, 104, pp. 17-31, 10.4204/eptcs.104.3, https://doi.org/10.4204/eptcs.104.3.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 3221 times.

This article's PDF has been downloaded 664 times.