Trust, but verify: Optimistic Effect Analysis for Reusable Code







Deposit Papers 


Long, Yuheng (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

There is a later version of this eprint available: Click here to view it.


Effect analyses can provide valuable assistance in concurrent software development. Such an analysis could compute sets of memory accesses (effects) of concurrent tasks to determine if these effects interfere. If such an analysis is formulated as a pure static analysis; for soundness, it must conservatively handle prevalent object-oriented features such as dynamic dispatch; by either assuming whole program analysis, or by requiring specifications on supertypes to restrict the effects of all subtypes. The first assumption is often in conflict with important modularity properties of languages like Java such as dynamic class loading, linking and evolution. The second requirement could be restrictive. A purely dynamic variant of such analysis would typically not make these assumptions, however, it would detect conflicts after they have already occurred and may be expensive. We contribute a novel optimistic effect analysis that enables safe concurrency and solves these problems. Our analysis relies on the notion of open effects. An open effect is unknown statically but made concrete post-compilation. Our 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 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: 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:00000680
Deposited by:Yuheng Long

Available Versions of This Paper

Contact site administrator at: