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

Chain #1
Enter:Buffer.add():[main] 
Exit:Buffer.add():[main]

Chain #2
Enter:Buffer.take():[Thread-1] 
Exit:Buffer.take():[Thread-1]

Chain #3
Enter:Producer.main():[main] 
Enter:Consumer.run():[Thread-1] 
Enter:Buffer.stop():[main] 
Exit:Buffer.stop():[main] 
Exit:Producer.main():[main] 
Exit:Consumer.run():[Thread-1]

FIGURE 8.16: Alternating chains for the Producer-Consumer program.

the number of redundant cliques is in (C p1

n i ). Therefore, the for loop is

in in i (n i + C p1

n i )). To construct the ith maximal clique, the algorithm's

complexity is in ( P n i

n i ))) = (n i 2 n i + n 3 i ). Therefore, the
worst-case complexity of our chaining algorithm is still exponential. The com-
plexity of the chaining algorithm varies by the density of the property graph.
In practice, the density of the property graph tends to be small (typically
around 10% in our experiments). Therefore, the performance of our algorithm
is acceptable in practice.
Figure 8.16 shows the three chains constructed for the Producer-Consumer
program. The longest chain (#3) has six events and represents an important
property: After the Producer calls the stop method, the Consumer eventually
stops. Each of the other two chains has only two events and is uninteresting
because these Alternating properties correspond to the trivial fact that entering
a method alternates with exiting the method.

p=1 (n i (n i + C p1

8.2.8 Perracotta
We adapted a Java instrumentation tool and implemented the inference
engine in a prototype tool called Perracotta. In addition to implementing the
inference algorithm, Perracotta also implements the two selection heuristics,
the chaining method, and the context-handling techniques.

8.2.8.1 Instrumentation

To instrument Java programs, we adapted the Java Runtime Analysis
Toolkit (JRat) [48]. JRat has two important components: an instrumentor
and a runtime system. The instrumentor component uses the Byte Code En-
gineering Library (BCEL) to parse and insert hooks into Java bytecode [6].
When an instrumented Java application executes, the hooks generate events