Trust, but verify: Optimistic Effect Analysis for Reusable Code

Date
2012-07-10
Authors
Long, Yuheng
Rajan, Hridesh
Rajan, Hridesh
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

We present an optimistic effect system for enabling safe concurrency in modern object-oriented languages with an open world assumption. New to our effect system is the notion of open effects. An open effect is a placeholder effect. It is produced by method calls when the dynamic type of the receiver object is unknown. An open effect is assumed to be blank (i.e., noninterfering effect) statically but verified to be truly so when the dynamic type of the receiver is known. An open effect-based analysis has several benefits. It is modular and so it allows analysis of partial programs and libraries. It is more precise than a comparable static analysis. It also has a small annotation overhead, and does not require specification on super type methods to restrict overriding in subclasses. We have formalized our analysis and proven that it is sound and that it enables deterministic semantics. We have also extended the OpenJDK Java compiler with support for open effects and tested its effectiveness on several reusable library classes where it shows only about 0.13-7.65\% overhead and good speedup.

Description
Keywords
types and effects, concurrency, safety
Citation
Collections