CSAIL Research Abstracts - 2005 link to http://publications.csail.mit.edu/abstracts/abstracts05/index.html link to http://www.csail.mit.edu
bullet Introduction bullet Architecture, Systems
& Networks
bullet Language, Learning,
Vision & Graphics
bullet Physical, Biological
& Social Systems
bullet Theory bullet

horizontal line

Static Deadlock Detection for Java Libraries

Amy Williams, William Thies & Michael D. Ernst

Introduction

Deadlock is a condition under which the progress of a program is halted as each thread in a set attempts to acquire a lock already held by another thread in the set. Because deadlock prevents an entire program from working, it is a serious problem.

Finding and fixing deadlock is difficult. Testing does not always expose deadlock because it is infeasible to test all possible interleavings of a program's threads. In addition, once deadlock is exhibited by a program, reproducing the deadlock scenario can be troublesome, thus making the source of the deadlock difficult to determine. One must know how the threads were interleaved to know which set of locks are in contention.

We propose a method for static deadlock detection in Java libraries. Our method determines whether it is possible to deadlock the library by calling some set of its public methods. If deadlock is possible, it provides the names of the methods involved.

To our knowledge, the problem of detecting deadlock in libraries has not been investigated previously. This problem poses unique challenges because, lacking client code, very little alias information is available. Library methods often synchronize over parameters or this, values for which no alias information is available.

Analysis Synopsis

Our deadlock detector uses an interprocedural analysis to track possible sequences of lock acquisitions within a Java library. It builds a graph called the lock-order graph that captures locking information for an entire library. This graph represents the order in which locks are acquired via calls to the library's public methods. Cycles in this graph indicate possibilities of deadlock.

To build the graph, the analysis iterates over the methods in the library, building a lock-order graph for each of them. All possible locking configurations of a method are modeled, including locks acquired transitively via calls to other methods. At a call site, the callee's graph is inserted into the caller. After each method's lock-order graph has reached a fixed point, the public methods' lock-order graphs are merged into a single graph for the library.

The lock-order graph's nodes represent a partition of objects into may-alias sets. Types are used as an approximation to may-alias information when a more specific partitioning is unavailable. Our full algorithm includes finer-grained partitioning techniques [4].

An edge in the graph indicates nested locking of objects along some code path. That is, it indicates the possibility of locking first an object from the source node, then an object from the destination node.

An example is given below; the Java code on the left yields the lock-order graph in the middle, and the client code on the right can lead to deadlock. The labels on the nodes of the graph are the types used for may-alias sets.

class A {
  public void foo(B b1, A a1) {
    synchronized (b1) {
      synchronized (a1) {
        ...
      }
    }
  }

  public synchronized void bar(B b2) {
    synchronized (b2) {
      ...
    }
  }
}
         
Lock-order graph corresponding to the Java source code
         
A a = new A();
B b = new B();
thread 1: a.foo(b, a);
thread 2: a.bar(b);
Lock-order graph for class A
Client code that can invoke deadlock
Current Results

We implemented our analysis and evaluated it on 20 libraries comprising 1279 kLOC. We verified 15 libraries to be free from deadlock, and found deadlocks in 13 distinct classes from 4 libraries, including 5 from the JDK.

An example deadlock from the AWT in the JDK may be invoked using the following code:

DropTarget a = new DropTarget(), b = new DropTarget();
Component aComp = new Button(), bComp = new Button();

aComp.setDropTarget(a);
bComp.setDropTarget(b);

thread 1: a.setComponent(bComp);
thread 2: b.setComponent(aComp);

The setComponent() method locks its receiver and, if the Component argument passed to it has a valid DropTarget, that DropTarget is locked as well. Thus, a.setComponent(bComp); locks a followed by bComp's DropTarget, or b; likewise, b.setCompoent(aComp); locks b then a. Since the two threads lock these objects in reverse order, deadlock can occur. We have verified this deadlock case using the above code.

Related Work

Several researchers have developed static deadlock detection tools for Java using representations similar to our lock-order graph [1,3]. These analyses use unsound heuristics to prune their results; the primary difference between our analysis and theirs is that they do not report all deadlock possibilities.

Another technique for detecting or preventing deadlock use model checking. Demartini, Iosif, and Sisto [2] use model checking to find deadlock in Java programs. Their tool is limited to a maximum number of modeled objects or threads, ours models an unbounded number of threads an objects for library code (rather than a single program).

Research Support

This work is supported in part by NSF grant CCR-0133580, the MIT-Oxygen Project, and DARPA contract FA8750-04-2-0254.

References

[1] Cyrille Artho and Armin Biere. Applying Static Analysis to Large-Scale, Multi-Threaded Java Programs. In Australian Software Engineering Conference, 2001.

[2] Claudio Demartini, Radu Iosif, and Riccardo Sisto. A Deadlock Detection Tool for Concurrent Java Programs. In Software -- Practice and Experience, 1999.

[3] Christoph von Praun. Detecting Synchronization Defects in Multi-Threaded Object-Oriented Programs. PhD thesis, Swiss Federal Institute of Technology Zurich, 2004.

[4] Amy Williams, William Thies, and Michael D. Ernst. Static Deadlock Detection for Java Libraries. In European Conference on Object-Oriented Programming, Glasgow, Scotland, UK, July, 2005 (to appear).

horizontal line

MIT logo Computer Science and Artificial Intelligence Laboratory (CSAIL)
The Stata Center, Building 32 - 32 Vassar Street - Cambridge, MA 02139 - USA
tel:+1-617-253-0073 - publications@csail.mit.edu
(Note: On July 1, 2003, the AI Lab and LCS merged to form CSAIL.)