Multiparty Compatibility for Concurrent Objects

TL;DR

This paper introduces a method to automatically verify compatibility and compliance of concurrent objects' state machines using multiparty compatibility from session types, enhancing system reliability.

Contribution

It applies multiparty compatibility concepts to concurrent objects, providing an untyped language for automatic checking and a testing-based validation approach.

Findings

Automatic compatibility and compliance checking is feasible

Simple objects can be exhaustively validated

Complex objects benefit from partial testing methods

Abstract

Objects and actors are communicating state machines, offering and consuming different services at different points in their lifecycle. Two complementary challenges arise when programming such systems. When objects interact, their state machines must be "compatible", so that services are requested only when they are available. Dually, when objects refine other objects, their state machines must be "compliant", so that services are honoured whenever they are promised. In this paper we show how the idea of multiparty compatibility from the session types literature can be applied to both of these problems. We present an untyped language in which concurrent objects are checked automatically for compatibility and compliance. For simple objects, checking can be exhaustive and has the feel of a type system. More complex objects can be partially validated via test cases, leading to a methodology closer to continuous testing. Our proof-of-concept implementation is limited in some important respects, but demonstrates the potential value of the approach and the relationship to existing software development practices.