Previous Up Next
1 Introduction

The join calculus is a simple name-passing calculus, related to the pi calculus but with a functional flavor [10, 9]. In this calculus, communication channels are statically defined: channels are created together with a set of reaction rules that specify, once and for all, how messages sent on these names will be synchronized and processed. These design choices favor the integration of concurrency and distribution within a programming language. Indeed, a typed language based on join calculus has been implemented as an extension of OCaml [17], called JoCaml [11, 15]. However, the above integration does not address object-oriented features. Precisely, JoCaml objects are just imported from OCaml and therefore they are sequential. The main contribution of this work is an extension of the join calculus with object oriented features that is compatible with the JoCaml implementation.

Although the join calculus does not have a primitive notion of object, definitions encapsulate the details of synchronization much as concurrent objects. Applying the well-known objects-as-records paradigm to the join calculus, we obtain a simple language of objects with asynchronous message passing. Method calls, locks, and states are handled in a uniform manner, using labeled messages. There is no primitive notion of functions, calling sequences, or threads (they can all be encoded using continuation messages). Our language---the objective join calculus---allows fine-grained internal concurrency, as each object may send and receive several messages in parallel.

For every object of our language, message synchronization is defined and compiled as a whole. This allows an efficient compilation of message delivery into automata [16] and simplifies reasoning on objects. However, the complete definition of object can be overly restrictive for the programmer. This suggests some compile-time mechanism for assembling partial definitions. To this end, we promote partial definitions into classes. Classes can be combined and transformed to form new classes. They can also be closed to create objects.

Objects can be created by instantiating definition patterns called classes, and in turn complex classes can be built from simpler ones. To make this approach effective, the assembly of classes should rely on a small set of operators with a clear semantics and should support a typing discipline. In a concurrency setting, such promises can be rather hard to achieve.

The class language is layered on top of the core objective calculus, with a semantics that reduces classes into plain object definitions. We thus retain strong static properties for all objects at run-time. Some operators are imported from sequential languages and adapted to a concurrent setting. For instance, multiple inheritance is expressed as a disjunction of join definitions, but some disjunctions have no counterpart in a sequential language. In addition, we propose a new operator, called selective refinement. Selective refinement applies to a parent class and rewrites the parent reaction rules according to their synchronization patterns. Selective refinement treats synchronization concretely, but it handles the parent processes abstractly. The design of our class language follows from common programming patterns in the join calculus. We also illustrate this design by coding some standard problematic examples that mix synchronization and inheritance.

Our approach to computing classes is compatible with the JoCaml implementation of the join calculus [15], which relies on runtime representation of synchronization patterns as bitfields [16] and, on the contrary compiles processes into functional closures. As a consequence, synchronization patterns can be scanned and produced at runtime, while processes cannot be scanned (but still can be produced), as required by our operators on classes.

We then define a type system for objects and classes. We introduce types at the end of the paper only, to separate design issues and typing issues. The type system improves on our previous work on polymorphism in the join calculus [12]. As discussed in [12], message synchronization potentially weakens polymorphism. With classes, however, message synchronization may not be entirely determined as we type partial definitions. In order to preserve polymorphism, we thus rely on synchronization information in class types.

In addition to standard safety properties, the type system enforces privacy. Indeed, the untyped objective join calculus lacks expressiveness as regards encapsulation1. In order to restrict access to the internal state of objects, we distinguish public and private labels. Then, the type system guarantees that private labels are accessed only from the body of a class used to create the object. The correctness of the type system is established for an operational semantics supplemented with privacy information.

As concern class operators, there is a trade-off between expressiveness and simplicity of both the static and dynamic semantics. In this paper, we favor expressiveness, while preserving type soundness and compositionality (with respect to compilation). As a consequence, we get a better understanding of inheritance and concurrency, and a touchstone for other design choices. Most of the complexity of our class operators stays within selective refinement. However, selective refinement is often used in rather simple patterns. This leaves place for simpler design choices (some of them will be discussed in Section 5).

The paper is organized as follows. In Section 2, we present the objective join calculus and develop a few examples. In Section 3, we supplement the language with classes and give a rewriting semantics for the class language. In Section 4 we present more involved examples of inheritance and concurrency. In Section 5, we discuss other design choices. In Section 6, we provide a static semantics for our calculus and state its correctness. In Section 7, we discuss related works and possible extensions. Appendix A presents cross-encodings between the plain and objective join calculus. Appendix B gathers the main typing proofs.


Previous Up Next