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 T yCO, 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