Re: Typing non-uniform concurrent objects

I would like to announce my PhD thesis, available from:


Comments welcome. 

     Antonio Ravara 
Typing Non-Uniform Concurrent Objects. 

Concurrent objects can offer services non-uniformly, according to
synchronisation constraints, that is, the availability of a service
depends on the internal state of the object. Interfaces-as-types is an
approach not suitable to model non-uniform service availability, and
the message-not-understood communication error is very restrictive.
Hence, we propose a looser definition of communication error by
demanding only that messages requesting a method not enabled, but that
may be accepted at some time in the future, do not cause errors.

This new notion detects messages that are never accepted, either
because the requested method does not exists at all, or because the
object is blocked and cannot change its state to accept the request.

We formalise non-uniform concurrent objects in TyCO, a name-passing
object calculus, and we ensure program safety (the absence of run-time
errors) via a type system. Types are terms of a process algebra which
describe some dynamic aspects of the behaviour of objects, thus, the
approach is centred on behaviours-as-types.

The type system assigns terms of the algebra to the names of
processes, and ensures that typable processes are neither locally
blocked nor run into communication errors.