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

Our test harness, DaisyTest , takes four parameters: F, the number of files to
be created initially; T, the number of threads to be created; N, the number
of iterations each thread executes; and R, the seed for the random number
generator. The main thread of DaisyTest first creates F files and T threads.
Next, each child thread makes a sequence of N calls to randomly selected
methods of the DaisyDir class (one of read , write , set attr , or get attr ). These
methods are invoked with arguments randomly selected within the valid range.

8.3.1.1 Inference Results

We ran DaisyTest with F = 5, T = 5, N = 15, and R = 0. This execu-
tion produced a trace of about 70000 events. We used Perracotta to slice the
original trace by threads and obtained six subtraces (five for the child threads
and one for the main thread). We ran Perracotta in approximate mode with
0:70 as the acceptance threshold for p AL . Our analysis only considered the
40 distinct events that occurred more than 10 times in the trace. Perracotta
inferred 70 properties, 52 of which had a satisfaction ratio less than one. We
applied Perracotta's chaining method to infer nine Alternating Chains .
The six shortest chains, with length from one to three events, are uninter-
esting because they correspond to wrapper functions. The other three chains
also contain uninteresting edges due to wrapper functions. Next we applied
Perracotta's call graph based heuristic to eliminate these wrapper properties
and got eight properties.
Several properties provide insight into the temporal behaviors of Daisy.
For example, DaisyDisk.readAllocBit ! DaisyLock.relb (p AL = 0:97) indicates
that reading the allocation bit of a block ( DaisyDisk.readAllocBit ) often alter-
nates with releasing the lock on the block ( DaisyLock.relb ). Because these two
methods are not eliminated by the call graph based heuristic, they represent an
interesting pair of asynchronous operations. These two methods do not neces-
sarily alternate because DaisyLock.relb is called in several places (e.g., Daisy.read
and Daisy.write ) where DaisyDisk.readAllocBit is not called. Another interesting
property is LockManager.acq ! LockManager.rel (p AL = 0:86) that captures an
important locking relationship. The satisfaction ratio of this property is less
than 1:0 because the traces are not sliced by objects.
Next, we used Perracotta to slice the this object and a method's rst ar-
gument. Perracotta inferred two properties with p AL = 1:0: Mutex.acq ! Mu-
tex.rel and LockManager.acq ! LockManager.rel . Slicing on other arguments did
not lead Perracotta to infer more properties. Object slicing missed some use-
ful properties that involve more than one object such as LockManager.acq !
Mutex.rel .
We also ran Perracotta with the two-effect-alternating and the two-cause-
alternating patterns (Section 8.2.4.1). Perracotta inferred an important prop-
erty: RAF.seek ! RAF.readByte j RAF.writeByte . We found a race condition in
Daisy that violates this property using the Java PathFinder model checker
(Section 8.4.1.1).