title: Detecting synchronisation errors: a comparison between StaVe and JPF
topics: Case studies and Applications
committee: Marieke Huisman ,
Dilian Gurov (KTH Sweden) ,
Cyrille Artho (KTH Sweden)


StaVe is a tool developed in a collaboration between the University of Twente and KTH Sweden. Goal of the tool is to automatically detect synchronization errors, caused by wrong use of condition variables, i.e., the wait-notify mechanism. StaVe requires a few annotations that describe the synchronization patterns, and then proceeds fully automatically. An advantage of this approach is that it covers all possible paths, but annotations might be difficult to write correctly and completely.

In this project, we would like to validate the use of StaVe and compare it to other available tools, notably Java PathFinder.
Java PathFinder is a tool that automatically analyzes all possible
outcomes of a multi-threaded program (for a given test case). It has
been developed over the last two decades by many researchers, at NASA
and universities over the world, and has also been supported by Google
Summer of Code for many years.
Unlike STaVe, Java Pathfinder does not require annotations; however, it
needs at least one test case, which STaVe does not need.

We have collected several concurrent programs that could be interesting
as examples. These include a concurrent blocking queue that allows
insertion/removal of multiple elements atomically, producer/consumer
programs, and a chat server.

We would like to investigate these examples and find answers to the following questions:

  1. What is the annotation overhead for the given examples?
  2. What is the performance of Java Pathfinder vs. STaVe?
  3. How difficult is it to write a suitable test suite (for Java Pathfinder)?
  4. What types of errors can be found by Java Pathfinder (for example, deadlocks)? Are there specific synchronization problems that require extensions such as property listeners to be detected by Java Pathfinder?

The following steps are expected for this project:
1. Learning JPF + STaVe

    Work your way through 2 - 3 simple examples and try to get them to
work with STaVe and JPF. (Some of the examples may already work on one
of the two platforms.)

2. Adapt/extend existing examples

    Spend the rest of the first 1/3 to 1/2 of your project to adapt more
examples. Seed defects to test how well JPF and STaVe find them.

3. (JPF) Are there patterns that can be generalized?

    It would be very interesting if we find common patterns behind some
wait/notify problems, so we can provide a tool (perhaps as an extension
of JPF) that can find these, *without* a specific test oracle.

    For example, if one thread overwrites data of another thread (after
waking up from wait), is this a sign of a problem? Often, such things
are not certainly defects but there may be a high probability of a problem.

4. (STaVe) Likewise, are there cases where annotations for STaVe can
easily be inferred?

Here are some resources:


Benchmarks are available under

svn --username anonymous co svn://svn-smc.cs.byu.edu/smc-lab/concurrency-benchmarks/Java



* The idea of computation graphs is related in the sense that these
graphs provide an abstract view of the structure of the concurrent
program. For STaVe, annotations provide similar information.
   Habanero programs are more structured than general Java so the graph
can be computed automatically, which is not the case with Java.

* Other papers by Eric Mercer may also be interesting.