Trust, but verify: Optimistic Effect Analysis for Reusable Code

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

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

Abstract

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.

Available Versions of This Paper

• Trust, but verify: Optimistic Effect Analysis for Reusable Code (deposited 01 May 2012) [Currently displayed]
  • Open Effects: Optimistic Effects for Dynamic Dispatch (deposited 16 October 2012)
  • Trust, but verify: Optimistic Effect Analysis for Reusable Code (deposited 08 May 2012)
    • Trust, but verify: Optimistic Effect Analysis for Reusable Code (deposited 22 October 2012)
    • Trust, but verify: Optimistic Effect Analysis for Reusable Code (deposited 16 October 2012)