Exception handling for copyless messaging

• Copyless message passing is a communication paradigm at odds with traditional exception handling.
• We propose a formal process model where try–catch blocks are transactions.
• We devise a type system to prevent communication errors, memory leaks and faults.
• We use types for reducing the cost of state restoration in case of exceptions.

Copyless messaging is a communication paradigm in which only pointers to messages are exchanged between sender and receiver processes. Because of its intrinsically low overhead, copyless messaging is suitable for the efficient implementation of communication-intensive software systems where processes have access to a shared address space. Unfortunately, the very nature of the paradigm fosters the proliferation of programming errors due to the explicit use of pointers and to the sharing of data. In this paper we study a type discipline for copyless messaging that, together with some minimal support from the runtime system, is able to guarantee the absence of communication errors, memory faults, and memory leaks in the presence of exceptions. To formalize the semantics of processes we draw inspiration from software transactional memories: in our case a transaction is a process that is meant to accomplish some exchange of messages and that should either be executed completely, or should have no observable effect if aborted by an exception.