A type safe state abstraction for coordination in Java-like languages

The state of a concurrent object, intended as some abstraction over the values of the fields of the object, usually determines its coordination behavior. Therefore, state is always in the programmer's mind, even though implicitly. We suggest a feature for Java-like languages, which makes the state of a concurrent object explicit and supports the expression of the object's behavior depending on the state it is currently in. Namely, an object will be in one of the states declared in its class. The state determines the presence of fields and methods. State transition statements explicitly change the state of an object, and thus change the availability of fields and methods. When a thread calls a method which is declared in the object's class but absent from its current state, it waits, until the state of the object changes to a state which does contain that method. This directly expresses coordination. We claim that this feature makes it easier to understand and develop concurrent programs, and substantiate our claim through the discussion of some popular examples of concurrent programs written using this feature. We develop a type and effect system, which guarantees that, during execution of a method invoked on a concurrent object o: (1) No attempt will be made to access fields not available in the current state of o, and (2) No method invoked on a receiver (syntactically) different from this may cause the invocation of a method on o. The latter guarantee helps to enforce the former and prevents a family of accidental violations of the intended coordination protocol.