Towards reasoning about concurrent objects

Heinz W. Schmidt and Jian Chen
Department Software Development
Monash University, Melbourne
P.O. Box 197, Caulfield East, 3145, Australia
e-mail: [email protected]

Abstract

Embedded specifications in object-oriented languages such as Eiffel are based on a rigorous approach towards validation, compatibility and reusability of sequential programs. Such specifications are not limited to functional and interface aspects but extend to complexity and, more generally, quantitative aspects in a straightforward way.

However concurrent object-oriented languages are still in their infancy. Concurrent objects have inherently imperative" facets, such as object identity, persistence and sharing. Several concurrency extensions to object-oriented languages have been proposed as well as object-oriented extensions to concurrent languages. Any such marriage requires a trade-off in a space of desirable qualities whose dimensions are not completely independent.

This paper summarises our work on a type system, calculus and an operational model for reasoning about concurrent objects. We are extending earlier work on sequential objects in such a way that method codes read like sequential codes and generate concurrency and synchronisation only implicitly. However concurrency and synchronisation are explicit in type signatures and interface specifications to be able to reason about concurrent interfaces, their correct implementation, and the preservation of system stability.
The concepts are presented as an extension to Eiffel-like object-oriented languages.

1 Introduction

Modern imperative object-oriented design methods and languages, such as Eiffel [5] or Sather [6, 7, 8], address system design, quality management and reusable library documentation by a rigorous approach to interface specification. Hoare logic assertions are embedded in such programs and become immediately useful in systematic testing, documentation and validation. Even if incomplete in many practical cases, they become central elements for understanding, assessing and integrating reusable components, as reasoning can be limited to partial specifications in a methodology called design-by-contract" [4].
If these assertions capture the full specifications, relative to which correctness and conformance of the implementation is to be checked, it turns out that design by contract can be proven the basis of a fully incremental and compositional approach to class library safety and stability. Walker and the first author sketched a type system and sufficient conditions for such an approach [9]. The present paper softens these constraints and sketches underlying formal semantics. These semantics and type system extensions are for concurrent objects extend previous work [11, 10] on reasoning about complexity of sequential object-oriented computations.
While concurrent objects are one of the more active fields of research in computer science at present, a marriage of concurrency and objects necessitates trade-offs particularly between provability (of global properties) and local control (of encapsulated objects), compositionally and efficiency, concurrency and sharing. Partly, the so-called inheritance anomaly is causing