| Abstract |
| 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 faults, leaks, and communication errors. The type system is essentially linear, but we show that linearity alone is inadequate. On the one hand, it is too strict when dealing with heap-allocated objects; on the other hand, it leaves room for scenarios where well-typed processes leak significant amounts of memory. We address these problems using dedicated types for keeping track of dereferenced pointers and by basing the type system upon an original variant of session types. |
@inproceedings{BonoMessaPadovani11,
volume = {6602},
author = {Viviana Bono and Chiara Messa and Luca Padovani},
series = {LNCS},
booktitle = {Proceedings of the European Symposium on Programming (ESOP'11)},
url = {http://www.di.unito.it/~padovani/Papers/TypingCopylessMessagePassing.pdf},
abstract = { 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 faults, leaks, and
communication errors. The type system is essentially linear, but
we show that linearity alone is inadequate. On the one hand, it is
too strict when dealing with heap-allocated objects; on the other
hand, it leaves room for scenarios where well-typed processes leak
significant amounts of memory. We address these problems using
dedicated types for keeping track of dereferenced pointers and by
basing the type system upon an original variant of session types.
},
title = {{Typing Copyless Message Passing}},
publisher = {Springer},
year = {2011},
pages = {57-76},
doi = {10.1007/978-3-642-19718-5\_4},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)
