Reasoning about explicit resource management

Abstract

We investigate the behaviour and efficiency of concurrent processes with explicit resource management. Our study is based on a π-calculus variant called Rπ [4] where the only resources available are channels, which must be explicitly allocated before they can be used and can be deallocated when no longer required. A substructural type system guarantees the safe allocation and deallocation of channels, as well as safe channel reuse through strong updates. In this paper we use this type system to give compositional proof techniques for reasoning about the behaviour and efficiency of Rπ processes.