Open Effects: A Hybrid Type-and-Effect System to Tackle Open World Assumption and its Application to Optimistic Concurrency

Abstract

<p>This work tackles the challenge of applying a type-and-effect system to reason about object-oriented programs with an open world assumption. An open world assumption challenges the design of a type-and-effect system when (1) all subclasses of a class are not known, and (2) an upper bound on effects of all subclasses is not available, e.g. when an effect specification is not available for that class – a common phenomenon in modern OO programs. The main problem is in the computation of the effects of a dynamically dispatched method invocation, because all possible dynamic types of its receiver are not known statically, and no static upper bound in the form of effect specification is available. Our new concept open effects solves these problems. The basic idea is to take a programmer-guided hybrid approach. Instead of using a predefined upper bound, our type-and-effect system takes the effects of a programmer-selected dynamically dispatched method call as open effects that encapsulate statically known information about the call, e.g. static type of receiver. The static part of our type-and-effect systems treats open effects as unknown, but the dynamic part of our type-and-effect systems reifies open effects. We also apply open effects to create a sound trust-but-verify type-and-effect system, to better enable concurrent execution of dynamically dispatched method invocations. If a programmer annotates the receiver of a certain method invocation as open, then the type system trusts the programmer and assigns an open effect to the method. The open effect is, optimistically, not supposed to conflict with other effects. Such optimistic assumptions are verified statically, if possible, or at runtime otherwise. Performance evaluations of an open effects-based type system for concurrency, on various benchmarks, show that it incurs negligible annotation and runtime overheads.</p>