Differences

This shows you the differences between two versions of the page.

--- jpf:start [2007/11/23 13:51] – created franck
+++ jpf:start [2008/01/21 20:37] (current) – franck
@@ Line 1: / Line 1: @@
 ====== Java PathFinder ======
+A lot of information about JPF can be found
+[[http://javapathfinder.sourceforge.net/|here]].
+More information can be found
+[[http://www.cse.yorku.ca/~sergey/jpf/|here]].
+Although it describes an old version of JPF,
+[[http://www.havelund.com/Publications/jpf-manual.ps|this]]
+manual may be useful.
+To configure JPF, you may want to use a
+jpf.properties file containing
+<code>
+search.class = gov.nasa.jpf.search.heuristic.HeuristicSearch
+search.heuristic.class =
+  gov.nasa.jpf.search.heuristic.BFSHeuristic
+</code>
+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\\
+<code>
+jpf.listener = gov.nasa.jpf.tools.precise.PreciseRaceDetector
+</code>
+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).
+<code java>
+/**
+ * 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();
+  }
+}
+</code>