archives

Trust, but verify: Optimistic Effect Analysis for Reusable Code


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Long, Yuheng and Rajan, Hridesh (2012) Trust, but verify: Optimistic Effect Analysis for Reusable Code. Technical Report 12-02, Computer Science, Iowa State University.

Full text available as:Adobe PDF

This is the latest version of this eprint.

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.

Commentary on:Trust, but verify: Optimistic Effect Analysis for Reusable Code
Keywords:types and effects, concurrency, safety
Subjects:Computer Systems Organization: COMPUTER SYSTEM IMPLEMENTATION: General
Software: PROGRAMMING TECHNIQUES (E): Concurrent Programming
Software: PROGRAMMING TECHNIQUES (E): Object-oriented Programming
Software: SOFTWARE ENGINEERING (K.6.3): Design Tools and Techniques
Software: SOFTWARE ENGINEERING (K.6.3): Coding Tools and Techniques
Software: PROGRAMMING LANGUAGES
Software: PROGRAMMING LANGUAGES: General
Software: PROGRAMMING LANGUAGES: Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3)
Software: PROGRAMMING LANGUAGES: Language Constructs and Features (E.2)
ID code:00000684
Deposited by:Yuheng Long on 22 October 2012

Available Versions of This Paper



Contact site administrator at: ssg@cs.iastate.edu