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

1 class Mutex {
2 boolean locked;
3 ……
4 synchronized void acq() {
5 while (locked) {
6 try {
7 this.wait();
8 } catch (Exception e) {
9 System.out.println(e);
10 }
11 }
12 locked = true;
13 }
14 synchronized void rel() {
15 locked = false;
16 this.notify();
17 }
18 }
FIGURE 8.23: The Mutex class in Daisy.
machine to describe typestate transitions. Based on the specification, ESP in-
struments the target program with the state-changing events. It then employs
an inter-procedural data-flow analysis algorithm to compute the typestate
behavior at every program point [70]. ESP handles inter-procedural analysis
through the use of partial transfer functions via function summaries.
From the 56 inferred properties (see Table 8.5), we randomly selected 10
locking properties and checked them using ESP. ESP found one previously
unknown deadlock bug in the NTFS file system. The property is a typical
locking discipline property: Acquiring a specific type of kernel Mutex must be
followed by releasing the same Mutex . Figure 8.24 shows a snippet of the buggy
code (the function names have been changed to protect Microsoft's proprietary
information). Whenever GetData is called from PushNewInfo , the Mutex will be
acquired twice (line 3 and 13), causing the system to deadlock. ESP clearly
showed this execution path. To fix it, the second argument on line 6 should be
changed to TRUE . The Windows development team confirmed that this was a
real bug and subsequently fixed the problem.
For all 10 properties, ESP produced false positives. The number of false
positives was large for some properties. For example, ESP found 600 coun-
terexamples of one property. We manually examined several counterexamples
that all turned out to be false positives due to known limitations of ESP. Man-
ually examining all counterexamples would take too much time and might not
be worthwhile as previous experience indicated the false positive rate could
be high. Instead, we wrote a simple Perl script to recognize the syntactical
pattern of known false positives, ran the script on the counterexamples, and
only manually examined those counterexamples that the script did not rec-