Automatic Inference and Effective Application of Temporal Specifications - Mining Software Specifications: Methodologies and Applications - page 281

1 public class Alt {
2 private final static byte[ ][ ] rule = { { 1, 2 }, { 2, 0 }, { 2, 2 } };
3 private byte currState;
4 public Alt() {
5 currState = 0;
6 }
7 public synchronized void update(int event) {
8 Verify.beginAtomic();
9 currState = rule[currState][event];
10 assert (currState != 2);
11 Verify.endAtomic();
12 }
13 public synchronized void checkExitState() {
14 assert (currState == 0);
15 }
16 }

FIGURE 8.22: The Java code for monitoring Alternating properties.

8.4.1.1 Daisy

Section 8.3.1 introduced Daisy, a prototype Unix-like file system [18]. We
applied Java PathFinder (JPF) [78] to verify the 22 inferred properties shown
in Table 8.6. Java PathFinder is an explicit-state model checker for Java pro-
grams [78]. It checks deadlocks, race conditions, unhandled exceptions, and
user-specified assertions. It can scale to a program of about 10,000 lines. Upon
finding a violation of a property, it produces an execution path illustrating the
problem. It has been used to find complex concurrent bugs in real systems [78].
Setup. We developed a Java class, Alt , for checking the Alternating tem-
plate (Figure 8.22). We encode a safety property as an assertion on the FSM's
state, which says the current state cannot be an error state (line 10). Our
instrumentor instruments Daisy so that it calls the update method whenever
the P or S event occurs. Our instrumentor also inserts a call to the checkEx-
itState method (line 13-15) to ensure that the current state is in an accepting
state before the program terminates (to catch bugs such as when a lock is not
released).
JPF did not support many Java native classes such as RandomAccessFile
( RAF ). We created an array to emulate RAF . We also created a simpler test
harness, DaisyTestSimple , which creates one file and two threads. Each thread
either reads from or writes to the created le once. We used JPF's Verify.random
in place of Java's random number generator so that JPF would automatically
explore all possible results of the random number generator.
In our preliminary experiments, JPF did not finish analyzing several prop-
erties within 24 hours. JPF allows users to indicate a sequence of statements
as an atomic segment by enclosing the statements between Verify.beginAtomic
and Verify.endAtomic . This significantly reduces the number of states JPF