Title:          Application of Process Types

Address:        Christof Peter
                Technische Universitaet Wien, Institut fuer Computersprachen
                Argentinierstrasse 8, A-1040 Vienna, Austria
Tel.:           ++43 (0)1 58801 185 14
Fax.:           ++43 (0)1 58801 185 98
E-mail:         christof@complang.tuwien.ac.at
Nationality:    Austria
Starting Date:  1997
Keywords:       Distribution, Typing, Language Concepts, Formal Calculus,
                Coordination, Middleware

Languages like C++, Java and Ada have shown that strong, static typing 
provides a good basis for programming. In distributed environments, 
there are well known calculi like the pi-calculus [MiPW92] or Vasconcelos' 
TyCO-calculus [Vasc94]. Static type systems for these calculi also exist. 
But their expressiveness is limited, because most of them are not able to
express  the sequencing of messages which is an important part of the
behavior of  objects. For example, a buffer object may receive "get"
messages only when  there are elements in the buffer object (which can be
added with "put"). This behavior could be ensured with preconditions, but
usually they cannot be checked statically and are of limited use in
concurrent systems. 

Process Types [Punt97] are based on a concept which allows to express
the sequencing of messages in the type information. This is done by
providing changeable state information in the types. When a message is 
sent, information about the state change of the message's receiver is 
provided by the type. The sender of the message can update its information
about the state of the receiver. This updating of information about the 
states of objects can be done by the compiler (process types provide a 
mechanism giving enough information to avoid problems with aliasing). 
Therefore, process types offer an expressive type system ensuring that 
there are no "message-not-understood" errors.

My research is concentrated on applications of the process type concept:

1) Examine a matching relationship for process types: Process types provide
   the subtyping relationship and genericity for re-use. But binary methods 
   can be re-used only with a higher-order subtyping mechanism like matching.
2) Using process types for deadlock detection: With asynchronous message 
   passing, an object is blocked when it is waiting for an answer (i.e. a
   message) from another object, but it receives no answer. If there are
   cycles of blocking objects, a deadlock occurs. An extension of process
   types allows us to express that a request shall imply an answer. This
   property can be guaranteed statically and, therefore, an important reason
   for deadlocks can be detected.
3) Integrate process types into CORBA: The interface definition language of
   CORBA provides only few information about the behavior of an object. A 
   goal of my research is to examine what possibilities of process types may 
   be used to enhance the interface information, but still provide static 
   type checking.

 
[MiPW92] R. Milner and J. Parrow and D. Walker, "A Calculus of Mobile 
         Processes (Parts I and II)", Information and Computation, 1992
[Vasc94] Vasco T. Vasconcelos, "Typed Concurrent Objects", Proceedings 
         ECOOP'94,
[Punt97] Franz Puntigam, "Coordination Requirements Expressed in Types 
         for Active Objects", ECOOP'97