JPF tutorial

Introductory JPF exercises

The goal of these exercises is to make you familiar with JPF.

Note that Java Pathfinder currently requires Java 8 to be installed.

If you are using the lab computers, you can switch to OpenJDK version 8 as follows:

module add openjdk/8

export JAVA_HOME="/usr/lib/jvm/java-8-openjdk-amd64"
export PATH="$JAVA_HOME/bin:$PATH"

You have to activate version 8 of Java in each shell/terminal that you use.

Dining Philosophers

Dining Philosophers Download Dining Philosophers.

1. Untar the archive:

   tar -xzf diningphil.tar.gz

2. Run JPF, look at the error trace. Write down a summary of the error trace as a table. Each row represents a transition or a sequence of transition, and each column represents a thread. Write the key actions of each thread in the right table cells. You can compile and run the code using:

   cd diningphil/src
   ./build.sh && ./run.sh

3. Create a lock dependency graph that illustrates the deadlock. (This can be an extra file or ASCII art inside the last part).
4. Propose a possible fix for the program, and create a patch.

Deliverables: Upload the error trace summary, the lock graph, and the patch in Canvas.

Bounded Queue

Bounded Queue Download Bounded Queue.

Note that in the exercise, the queue size is only 2, which is the same as the message size. The queue therefore becomes full after just one "put".

1. Untar the archive:

   tar -xzf queue.tar.gz

   Note that in this case, the tar archive creates three subdirectories, to make it easier to look at each version: queue, queue-do_wait, and queue-notify.

2. Analyze the error trace of JPF when checking queue-do_wait. Create a summary of the error trace, as shown in the lecture slides. You can compile and run the code using:

   cd queue-do_wait/src
   ./build.sh && ./run.sh QueueTest

3. Analyze the error trace of JPF when checking queue-notify. Create a summary of the error trace, as shown in the lecture slides. You can compile and run the code using:

   cd queue-notify/src
   ./build.sh && ./run.sh ProdCons

4. The related test (QueueTest) does not fail in this case! Reason why this simpler test succeeds. Run the other test in JPF using

   ./run.sh QueueTest # also in queue-notify/src

   Hint: to check if a statement is reached, you can add assert(false) and see if JPF returns an error trace that reaches that statement.

Deliverable: Upload the two error trace summaries, and a description of why the last test does not fail, to Canvas.

Time server

Time server Download Time server.

1. Untar the archive:

   tar -xzf daytime.tar.gz

2. Look at the error trace. In this case, the error trace indicates

   java.lang.UnsatisfiedLinkError: cannot find native java.net.PlainSocketImpl.initProto

3. This error means that JPF cannot execute a given native method (more about that in week 6). As a solution to this problem, you can provide a model class. A model class implements a simplified version of the native code. In this case, a model class is already provided in src/env. All you have to do is to change the import statements in question, e.g., replace

   import java.net.ServerSocket;

   with

   import env.java.net.ServerSocket;

4. Now, JPF executes the example without error. However, there are actually flaws. They occur if a network connection fails. This is not fully explored in the given model classes, but you can find examples. For example, look at this code in Socket.close:

   if (Verify.getBoolean()) {
     throw new IOException("Simulated exception when closing connection.");
   }

   Add similar code in ServerSocket.accept and run JPF again!
5. Now you will find a bug.

Deliverable: Fix the bug and upload a patch.