Thursday, 7 November 15:30-17:00
Chair: David Bacon
Static program analysis is the basis for most of the powerful optimization techniques behind modern high-performance programming languages. In this session, static analysis is applied to solve a wide range of problems, from traditional compiler optimization to automated verification of program properties. The first paper shows that it is usually possible to eliminate almost all dynamically executed write barriers from a program by using static information about allocation order combined with code reordering techniques. The second paper extends the authors' previous work on race-free Java to the problem of statically preventing deadlocks. Finally, the third paper shows how high-level program properties can be specified as annotations to Java programs and then checked automatically.
Write Barrier Removal by Static Analysis
We present a new static analysis for removing unnecessary write barriers in programs that use generational garbage collection. To our knowledge, this is the first analysis for this purpose. Our algorithm uses an interprocedural, flow-sensitive pointer analysis to locate assignments that always create a reference from a younger object to an older object, then transforms the program to eliminate the write barriers normally associated with such assignments. To enhance the effectiveness of the technique, we have implemented two transformations that reorder object allocations. These transformations can dramatically increase the number of write barriers that our algorithm is able to eliminate. Results from our implemented system show that our technique can eliminate the majority of the write barriers in most of the programs in our benchmark set, producing modest performance improvements of up to 8% of the overall execution time. Moreover, by dynamically instrumenting the executable, we are able to show that for all but two of our nine benchmark programs, our analysis is close to optimal in the sense that it eliminates the write barriers for almost all assignments that do not, in the observed execution, create a reference from an older object to a younger object.
Ownership Types for Safe Programming: Preventing Data Races and Deadlocks
This paper presents a new static type system for multithreaded programs; well-typed programs in our system are guaranteed to be free of data races and deadlocks. Our type system allows programmers to partition the locks into a fixed number of equivalence classes and specify a partial order among the equivalence classes. The type checker then statically verifies that whenever a thread holds more than one lock, the thread acquires the locks in the descending order. Our system also allows programmers to use recursive tree-based data structures to describe the partial order. For example, programmers can specify that nodes in a tree must be locked in the tree-order. Our system allows mutations to the data structure that change the partial order at runtime. The type checker statically verifies that the mutations do not introduce cycles in the partial order, and that the changing of the partial order does not lead to deadlocks. We do not know of any other sound static system for preventing deadlocks that allows changes to the partial order at runtime.
An Analyzable Annotation Language
The Alloy Annotation Language (AAL) is a language for annotating Java code based on the Alloy modeling language. It offers a syntax similar to the Java Modeling Language (JML), and the same opportunities for generation of run-time assertions. In addition, however, AAL offers the possibility of fully automatic compile-time analysis. Several kinds of analyses are supported, including: checking the code of a method against its specification; checking that the specification of a method in a subclass is compatible with the specification in the superclass; and checking properties relating method calls on different objects, such as that the equals methods of a class (and its overridings) induce an equivalence. Using partial models in place of code, it is also possible to analyze object-oriented designs in the abstract: investigating, for example, a view relationship amongst objects. The paper gives examples of annotations and such analyses. It presents (informally) a systematic translation of annotations into Alloy, a simple first-order logic with relational operators. By doing so, it makes Alloy's automatic analysis, which is based on state-of-the-art SAT solvers, applicable to the analysis of object-oriented programs, and demonstrates the power of a simple logic as the basis for an annotation language.