Transcript Mining Parametric Specifications

Mining Parametric Specifications
Choonghwan Lee
Feng Chen
Grigore Roşu
University of Illinois at Urbana-Champaign
1
Formal Specifications
• Useful … when available
• Static analyses
• Model checkers
• Program verifiers
• We don’t like to write them
Overview
•
•
•
•
•
Parametric Specifications
Problem, Goal and Challenges
Our Contributions
jMiner: Implementation and Experiments
Conclusion
Parametric Specifications
• Specifications referring to object instances
• The following property should hold for all
collections c and all iterators i :
1
• Generalize typestates
3
2
4
Monitoring Parametric
Specifications
• Parametric Property Monitoring Systems
•
•
•
•
•
•
Tracematches (Oxford; de Moor et al.)
PQL (Stanford; Lam et al.)
PTQL (Berkeley/Standford/Novell; Aiken at al.)
RuleR (Manchester; Barringer et al.)
MOP (UIUC; Rosu et al.)
many others …
Parametric Property
Monitoring
• Given a program execution Exec and a
specification Prop, does Exec satisfy Prop?
update(𝒄)
Program
hasNext(𝒊)
iterator(𝒄, 𝒊)
1
execute &
observe
update(c
iterator(c
i23) 23
hasNext(i
)23) next(i
) 23) 23)
17)hasNext(i
17, next(i
23next(i
Violation!
2
next(𝒊)
3
4
6
Problem and Goal
• Problem: specifications are rarely available
• Goal: infer parametric specifications from
program executions
Programs
1
3
2
execute &
observe
update(c
iterator(c
i23) 23
hasNext(i
)23) update(i
17)hasNext(i
17, next(i
23)
23)
infer
4
7
Challenge 1 – Trace Slicing
• Unfortunate interaction interleavings may
yield faulty specifications
execute &
observe
hasNext
Thread 1
Thread 2
...
Iterator i1 = ...;
i1.hasNext(); next
...
Iterator i2 = ...;
hasNext
next
next
hasNext
hasNext
i2.hasNext();
i1.next();
infer
i1.hasNext();
i2.next();
Wrong!
i2.hasNext();
8
Challenge 2 – Filtering Events
• Event specification is tedious and requires
expert knowledge
Method
Interesting?
Vector.add()
Vector.capacity()
Vector.contains()
Vector.elementAt()
Vector.remove()
Vector.iterator()
about 30 more methods …
9
Contribution 1 – Trace slicer
• Unfortunate interaction interleavings may
yield faulty specifications
→ Trace slicer
• Given parametric trace and event specification,
extract all independent interactions
• Each resulting trace slice correspond to exactly
one interaction and is non-parametric
10
Trace Slicing
• Parameters must be recorded in the trace.
execute &
observe
hasNext(i
hasNext 1)
Thread 1
Thread 2
...
trace slice i1
Iterator i1 = ...;
i1.hasNext();
hasNext
...
trace slice i2
Iterator i2 = ...;
hasNext(i
hasNext 2)
next(i
next 1)
next(i
next 2)
hasNext(i
hasNext 1)
hasNext(i
hasNext 2)
hasNext
i2.hasNext();
i1.next();
trace slicer
next
next
i2.next();
i1.hasNext();hasNext
hasNext
i2.hasNext();
11
Multiple Parameters
execute &
observe
add(c0)
iterator(c0, i1)
hasNext(i1)
iterator(c0, i2)
hasNext(i2)
add(c0)
Thread 1
Thread 2
...
trace slice (c0, i1) ...trace slice (c0, i2)
Collection c1 = c0; Collection c2 = c0;
add
c1.add(...); add
Iterator i1 =
...
iterator
c1.iterator();
hasNext
i1.hasNext();
Iterator i2 =
trace slicer
iterator
...
c2.iterator();
hasNext
i2.hasNext();
add
add
c2.add(...);
12
Trace Slicing is Hard
• Doesn’t it reduce to computing the
connected components of a graph?
⟨𝑄:q0, 𝑅:r1⟩
⟨𝑃:p0, 𝑄:q0⟩
⟨𝑅:r1, 𝑆:s0⟩
conflict on 𝑅
⟨𝑄:q0, 𝑅:r2⟩
13
Complexity of Trace Slicing
• In the worst case, the number of trace
slices is
𝑛 𝑚
≈
𝑚
• 𝑛: number of events in the execution trace
• 𝑚: number of parameters
• In terms of 𝑛 only, it becomes
≈
𝑛
𝑒𝑒
14
Trace Slicing Seems to Work
• Worst case is more of a theoretical nature
• In practice, rarely more than 3 parameters
• And rarely all combinations appear in traces
• Trace slicing algorithm (see the paper)
• Implemented in jMiner
• The slowest component of jMiner
• Reasonable performance in practice
• Millions of trace slices in typical program executions
Parametric Specification Learning
• (Non-parametric) trace slices from multiple
applications are then passed to any
conventional property learner that does
not handle parameters; e.g.,
• k-tail [Biermann & Feldman, 1972]
• sk-strings [Raman et al., 1997]
• Learns a finite state automaton (FSA) from strings
16
A conventional FSA learner
• A conventional FSA learner infers an FSA
from the set of given strings.
trace
slice
i1 i
trace
slice
2
hasNext
hasNext
next
next
hasNext
hasNext
train
train
FSA learner
infer
hasNext
next
17
Contribution 2 – Event Learner
• Event specification is tedious and requires
expert knowledge
→ Event Specification Learner
• Idea: Use unit tests! Most of these were
created precisely to test interactions
• Given target package and unit tests, discovers
sets of methods likely to obey some protocols
• This can be done either statically or
dynamically. We do it dynamically
18
Why
unit
test
cases?
Java Compilers expand for-each loops
for (Iterator<Integer> it = list.iterator(); it.hasNext(); )
{
Inferred Event Specification
int i = it.next();
...
CheckForComodification.java
from OpenJDK
6’s test cases
AbstractList.add(𝑙𝑖𝑠𝑡)
}
AbstractList.remove(𝑙𝑖𝑠𝑡)
public class CheckForComodification { AbstractList.iterator(𝑙𝑖𝑠𝑡,𝑖𝑡)
private static final int LENGTH = 10;
Iterator.hasNext(𝑖𝑡)
public static void main(String[] args)
throws Exception {
Iterator.next(𝑖𝑡)
List<Integer> list = new ArrayList<Integer>();
for (int i = 0; i < LENGTH; i++) list.add(i);
try {
for (int i : list)
if (i == LENGTH - 2) list.remove(i);
}
catch(ConcurrentModificationException e) { return; }
throw new RuntimeException("No CMException");
}
}
• Interactions are well isolated.
19
IMPLEMENTATION – JMINER
Parametric
Specification
Package
name
Unit tests
Trace Slice
Trace Slice
Trace Slice
FSA Learner
Trace Slicer
Event Spec.
Learner
Event
Event
Specification
Event
Specification
Specification
Execution
Execution
Trace
Execution
Trace
Trace
20
Experiments with JMINER
• Mining parametric specifications in four
OpenJDK 6 packages
•
•
•
•
java.util
java.io
java.lang
java.net
• We show java.io here. See the paper for
the other packages
21
Event Specification Learning
• OpenJDK6’s unit test cases were used; e.g.,
“java.io”
OpenJDK 6’s Unit
test cases for java.io
145 event specifications
in 24 minutes.
Event Specification
Learner
Event Specification
Event Specification
Event Specification
22
Trace slicing
• We used DaCapo [Blackburn et al., 2006]
and Apache JAMES for execution traces
for each
Execution Trace from
Execution Trace from
a DaCapo
execution
Execution
Trace from
a DaCapo execution
a DaCapo execution
For all the 145 event specifications,
trace slicing took 115 minutes.
Event Specification
Trace Slicer
Trace Slice
Trace Slice
Trace Slice
23
Parametric Specification Learning
• Based on sk-strings algorithm [Raman et
al., 1997]
Trace Slice
Trace Slice
Trace Slice
Specification Learner
Parametric
Specification
Among 145 event specifications,
66 specifications were inferred in 24 minutes.
24
Example – Collection-Iterator
update(𝒄)
0
<init>(𝒄)
𝒄
Collection
𝒊
Iterator
hasNext(𝒊)
iterator(𝒄, 𝒊)
1
2
next(𝒊)
3
4
update(𝒄)
25
Example – Reader
read(𝒓)
0
𝒓
<init>(𝒓)
1
close(𝒓)
2
Reader
26
Example – ServerSocket
0
<init>(𝒍)
close(𝒆)
7
𝒍
ServerSocket
𝒆
Socket
𝒊
InputStream
𝒐
OutputStream
accept(𝒍, 𝒆)
1
read(𝒊)
6
getInputStream(𝒆, 𝒊)
2
3
write(𝒐)
write(𝒐)
read(𝒊)
5
write(𝒐)
4
close(𝒆)
27
Related Work
POPL’02 - Ammons, Bodik, Larus
ICSE’06 - Yang, Evans, Bhardwaj, Bhat, Das
IEEE TSE’07 - Henkel, Reichenbach, Diwan
FSE‘07 - Acharya, Xie, Pei, Xu
FSE’08 - Gabel, Su
ICSE’08 - Lorenzoli, Mariani, Pezz
ASE’09 - Pradel, Gross
ECOOP’09 - Zhong, Xie, Zhang, Pei, Mei
…
Conclusion
• Parametric specification mining technique
• Precise – invulnerable to any interleaving
• Generic – any learner can be employed
• Automatic – no expert knowledge is required
• Ongoing and future work
• Mine entire OpenJDK
• Monitor mined specifications to find bugs
• Better learners
29