Background

The concurrent object-calculus can serve a semantics basis of concurrent, object-oriented languages, featuring message passing, object creation and aliasing, and especially multithreading. For instance it can be used to present multi-threading features as known from Java. Being a typical ``/object/’‘-calculus, it lacks, however, the notion of classes as a device to generate multiple instances from the same source code.

A standard approach to define semantics is observational: what can an external observer distinguish experimenting with the program. Including classes has quite some bearing on the semantics. With the observer-component or environment-program dichotomy separating also classes, the environment can instantiate component classes into component objects, and also the component can use environment classes for instantiation. Being able to instantiate objects inside the component and thus with the initial handle to the object at hand, the environment suddenly has, to a certain extent, control which of other objects in the component can in principle be in connection with new reference. So the environment has the power to separate the heap-space of the component into isolated portions and with this knowledge, certain observations become a priori impossible, for instance two objects belonging to separate parts of the heap cannot occur in the same communication label at the interface between component and environment. Thus, to characterize exactly the observable behavior, the semantics must not only be aware of the sequence of messages at the component-interface, but also of the potential connectivity of objects in the component.

Problem setting

As mentioned in the background section, a faithful semantic account of the observable behavior in a calculus with classes must take object connectivity into account. In effect, what counts is a worst-case estimation of the connectivity between objects. A mathematical justification of this intuition requires to show that the worst-case estimation of connectivity can exactly be realized in the calculus. This problem is thus constructive as it requires to come up with an distributed algorithm that implements the connectivity.

In the Diplomarbeit, a particular solution should be worked out. Unlike the solution sketched in the literature, the solution should be centralized: the connectivity for a group (``clique’’) of objects be maintained and managed by some special object (or object group). This object broker stores all identities belonging to the clique and distributes them appropriately when needed. Furthermore, it must be able to create new brokers, as new cliques may appear, and it must be possible for brokers, to combine their knowledge.

The Diplomarbeit should work-out the sketched ideas in the setting of the concurrent object-calculus. Concretely, it could address (a subset of) the following points:

  1. describe informally a centralized algorithm in detail

  2. implement the broker ideas in the concurrent object-calculus. The formalization should reflect the dynamicity of the clique-situation:

    • creation of new object cliques and
    • merging of cliques.

    As fall-back options, one can imagine to concentrate on only the single-threaded case, or to ignore creation and/or merging.

  3. Make an (informal?) correctness argument. One possible way is to argue that the distributed implementation and the centralized are equivalent

The tasks are arranged in increasing complexity, The first 2 points should be more or less straightforward generalizations of the available prior work. However, depending on the amount of formality in the encoding, part 2 can already be quite demanding. The same holds for part 3 (and more so, depending on the degree of formality).

Requirements

The work is theoretical in nature. The candidate should be interested in semantical and formal aspects of programming languages. Preferably, the Diplomarbeit is done in English.

Context

The work is embedded in the research project MobiJ, a German-Dutch cooperation between the Universities of Kiel, Freiburg, Leiden, and the Centrum voor Wiskunde en Informatica in Amsterdam, addressing formal aspects of concurrent and mobile components (modeling, semantics, proof theory, and mechanical verification support More loosely, the work is connected also to the larger European IST project OMEGA.