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.