A type safe state abstraction for coordination in Java-like languages
A type safe state abstraction for coordination in Java-like languages
复制标题
用于协调类 Java 语言的类型安全状态抽象
作者：
Ferruccio Damiani;Elena Giachino;P. Giannini;S. Drossopoulou
并发对象的状态，作为对象字段值的某种抽象，通常决定其协调行为。因此，状态总是在程序员的头脑中，即使是隐式的。我们建议一个类似Java的语言，这使得一个并发对象的状态显式，并支持对象的行为取决于它目前所处的状态的表达式的功能。也就是说，对象将处于其类中声明的状态之一。状态确定字段和方法的存在。状态转换语句显式更改对象的状态，从而更改字段和方法的可用性。当一个线程调用一个在对象的类中声明但在当前状态中不存在的方法时，它会等待，直到对象的状态改变为包含该方法的状态。这直接体现了协调性。我们声称，这一特点使它更容易理解和开发并发程序，并通过讨论一些流行的并发程序使用这一特点的例子来证实我们的说法。我们开发了一个类型和效果系统，它保证，在执行一个方法调用并发对象$${ t o}$$：（1）不会尝试访问在$${}的当前状态下不可用的字段 t o}$$，以及（2）在不同于$${ t this}$$可能会导致调用$${ t o}$$.后一种保证有助于执行前一种保证，并防止一系列意外违反预期协调协议的行为。
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 $${ t o}$$: (1) No attempt will be made to access fields not available in the current state of $${ t o}$$, and (2) No method invoked on a receiver (syntactically) different from $${ t this}$$ may cause the invocation of a method on $${ t o}$$. The latter guarantee helps to enforce the former and prevents a family of accidental violations of the intended coordination protocol.