键入无复制消息传递
Typing Copyless Message Passing
摘要：
我们提出了一个演算，模拟一种形式的进程交互的基础上无拷贝的消息传递，在风格的奇点OS。演算配备了一个类型系统，确保良好的类型的进程是免费的内存故障，内存泄漏，和通信错误。类型系统本质上是线性的，但是我们证明了仅仅线性是不够的，因为它为类型良好的进程泄漏大量内存的情况留下了空间。我们解决这些问题的基础上的会话类型的原始变体的类型系统。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
