Behavioural Separation with Parallel Usages for a Core Object-Oriented Language

Abstract

This report extends work on the Mungo language with behavioural separation. Mungo is an object-oriented calculus that employs typestates with a behavioural type system to ensure the absence of null-dereferencing. The typestates are expressed with usages, which are protocols that specify the admissible sequences of method calls on objects.Previous type systems for Mungo have all had a linearity constraint on objects. We lessen this constraint by extending the usage specifications with a parallel usage construct, where the parallel constituents describe separate local behaviour. We use the parallel usage to reason about aliasing, as a parallel usage describes a separation of the heap where we can reason about each constituent in isolation. Furthermore, parallel usages allow for arbitrary interleaving of local protocols, solving a problem of exponential growth of the size of usages, for unrelated linear fields in classes. We show that the new type system, with support for behavioural separation, retains the properties of previously presented type systems for Mungo, namely the safety and progress results, as well as protocol fidelity. Finally, we present an implementation of the Mungo language with support for parallel usages, along with a suite of examples.

Publication
Master Thesis
Mathias Jakobsen
Mathias Jakobsen
PhD Student

Mathias is a PhD Student at the School of Computing Science, University of Glasgow.

Related