Java PathFinder

A lot of information about JPF can be found here.

More information can be found here.

Although it describes an old version of JPF, this manual may be useful.

To configure JPF, you may want to use a jpf.properties file containing

search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
search.heuristic.class = 
  gov.nasa.jpf.search.heuristic.BFSHeuristic

to use a breadth-first traversal of the state space (rather than a depth-first traversal which is the default). To check for race conditions, you may want to add

jpf.listener = gov.nasa.jpf.tools.precise.PreciseRaceDetector

to your jpf.properties file.

To check some properties of our solution to the readers-writers problem by means of JPF, we modified our solution as follows (the attribute writers and assertions have been added).

/**
 * This class represents a database.  There are many competing
 * threads wishing to read and write.  It is acceptable to have
 * multiple processes reading at the same time, but if one thread
 * is writing then no other process may either read or write.
 */
public class Database
{
  private int readers; // number of active readers
  private int writers; // number of active writers
 
  /**
     Initializes this database.
  */
  public Database()
  {
    this.readers = 0;
  }
 
  /**
     Read from this database.
 
     @param number Number of the reader.
  */
  public void read(int number)
  {
    synchronized(this)
    {
      this.readers++;
      System.out.println("Reader " + number + " starts reading.");
    }
 
    final int DELAY = 5000;
    try
    {
       Thread.sleep((int) (Math.random() * DELAY));
    }
    catch (InterruptedException e) {}
 
    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);
 
    synchronized(this)
    {
      System.out.println("Reader " + number + " stops reading.");
      this.readers--;
      if (this.readers == 0)
      {
        this.notifyAll();
      }
    }
  }
 
  /**
     Writes to this database.
 
     @param number Number of the writer.
  */
  public synchronized void write(int number)
  {
    while (this.readers != 0)
    {
      try
      {
        this.wait();
      }
      catch (InterruptedException e) {}
    }
    System.out.println("Writer " + number + " starts writing.");
    this.writers++;
 
    final int DELAY = 5000;
    try
    {
      Thread.sleep((int) (Math.random() * DELAY));
    }
    catch (InterruptedException e) {}
 
    assert((this.writers == 1 && this.readers == 0) || this.writers == 0);
 
    this.writers--;
    System.out.println("Writer " + number + " stops writing.");
    this.notifyAll();
  }
}