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

has to check. To improve performance, we enclosed the initialization code
of DaisyTestSimple and the monitoring code in atomic segments (line 8-11 in
Figure 8.22).
Results. When JPF finds a counterexample, it might be a bug. For ex-
ample, consider the RAF.seek ! (RAF.read j RAF.write) property (number 22 in
Table 8.6), which says whenever RAF.seek is called, RAF.read or RAF.write must
be called before the next invocation of RAF.seek . JPF detected a violation of
this property, where RAF.seek was called twice without a call to either RAF.read
or RAF.write in-between. Diagnosing this problem revealed a race condition in
Daisy that was also detected by several other verification tools [18]. After one
thread moves the file pointer to location A, another thread starts executing
and moves the file pointer to location B. If the first thread is scheduled to
execute again, it would write to an incorrect position.
A counterexample can also result from a faulty property inferred from in-
adequate execution. For example, Perracotta inferred DaisyLock.acqi(inodeno)
! DaisyLock.reli(inodeno) (number 17 in Table 8.6). These two methods oper-
ate on the lock of the inode whose inode number equals inodeno . Although this
property appears to be valid, JPF found a counterexample. Inspecting the
code revealed a subtle and interesting aspect of Daisy. DaisyLock.acqi(inodeno)
calls LockManager.acq(lockno) that calls Mutex.acq() corresponding to the Mu-
tex object that has the lockno . Similarly, DaisyLock.reli(inodeno) calls LockMan-
ager.rel(lockno) that calls Mutex.rel() corresponding to the Mutex object that
has the lockno . Therefore, as long as the implementation of Mutex guarantees
synchronized access to an inode , an upper level class (e.g., DaisyLock ) does not
have to ensure synchronization. JPF detected counterexamples to properties
8 to 12 and 16 to 19 in Table 8.6 for a similar reason. Although such coun-
terexamples do not reveal bugs, they provide insight into some important yet
subtle properties of Daisy.
Furthermore, the counterexample of Mutex.acq() ! Mutex.rel() (number 19
in Table 8.6) revealed a limitation of our inference technique. Figure 8.23 shows
the implementation of the two methods. Recall that our instrumentor monitors
the entrance of a method. Hence, the Mutex.acq() event corresponds to entry
of the acq() method of the Mutex class (line 4). Similarly, Mutex.rel() event
corresponds to entry of the rel() method of the Mutex class (line 14). Therefore,
Mutex.acq() does not have to alternate with Mutex.rel() because Mutex.acq() does
not correspond to the start of the critical section (line 12).

8.4.1.2 Windows

We use the ESP verifier [19] to verify the inferred properties of the Win-
dows kernel from Section 8.3.3. ESP is a validation tool for typestate prop-
erties [77]. Typestates are more expressive than ordinary types: for an object
created during program execution, its ordinary type is invariant through the
lifetime of the object, but its typestate may be updated by certain operations.
ESP allows a user to write a custom specification encoded in a finite state