Channels as Objects in Concurrent Object-Oriented Programming

TL;DR

This paper introduces a formal concurrent object-oriented language that uses usage types to specify protocols, object states, and method calls, enabling static verification of client code adherence in concurrent settings.

Contribution

It extends session types by removing channel operations, unifies object categories, and formalizes a type system for verifying method call correctness in concurrent object-oriented programming.

Findings

Formal language with usage types for protocols and object states

Type system enforces correct method calls and client adherence

Unified category for linear and shared objects, enabling evolution

Abstract

There is often a sort of a protocol associated to each class, stating when and how certain methods should be called. Given that this protocol is, if at all, described in the documentation accompanying the class, current mainstream object-oriented languages cannot provide for the verification of client code adherence against the sought class behaviour. We have defined a class-based concurrent object-oriented language that formalises such protocols in the form of usage types. Usage types are attached to class definitions, allowing for the specification of (1) the available methods, (2) the tests clients must perform on the result of methods, and (3) the object status - linear or shared - all of which depend on the object's state. Our work extends the recent approach on modular session types by eliminating channel operations, and defining the method call as the single communication primitive in both sequential and concurrent settings. In contrast to previous works, we define a single category for objects, instead of distinct categories for linear and for shared objects, and let linear objects evolve into shared ones. We introduce a standard sync qualifier to prevent thread interference in certain operations on shared objects. We formalise the language syntax, the operational semantics, and a type system that enforces by static typing that methods are called only when available, and by a single client if so specified in the usage type. We illustrate the language via a complete example.