Towards a Better
Collaboration of Static and
Dynamic Analyses for
Testing Concurrent Programs
Jun Chen and Steve MacDonald
David R. Cheriton School of Computer Science
University of Waterloo
Introduction
Finding concurrent bugs statically
Alias analysis, escape analysis, may happen in parallel
analysis
Chord - false positives
Finding concurrent bugs dynamically
Lockset algorithm
Eraser – false negatives/positives
Instrumenting
Contest – false negatives
Explicit State Model Checking
JPF – state space explosion
PADTAD 2008
2
Static + Dynamic Analysis
Static analysis prunes out irrelevant program
artefacts. Dynamic analysis tests rest of
problem space.
Advantage: Reduces the problem space of
dynamic analysis.
Static analysis tends to be conservative. The
remaining problem space might still remain
large.
What if static analysis is used to actively
guide the dynamic analysis to test potential
bugs?
PADTAD 2008
3
Rationale
Explore interleaving (state space) DFS/BFS.
You may run of memory or CPU time before
hitting a bug.
Instead of searching exhaustively, the
computational resources should always be
dedicated to actively finding a possible bug.
PADTAD 2008
4
Finding a Concurrent Bug
What you could learn from static analysis:
Point of interests:
MHP Reads/Writes (possible data races)
Competing monitor entries (possible general
races)
What you could not know from static analysis:
Accessibility of the read/write assignments.
A feasible path could enable concurrent accesses
Precise alias relationship among reads/writes &
monitor entries
If such feasible path exists, are the read/writes or
monitor entries still relevant?
PADTAD 2008
5
Finding a Concurrent Bug
Strategy:
Scan the program using static analysis
Identify a potential pair of MHP read/write.
Compute a path to enable them.
Drive the program execution along the path.
Adjust/append the path along the way.
Which branch or polymorphism call edge is taken at
runtime.
After concurrent accesses have been reached, are
they relevant (true alias)? If not, pick another possible
pair to test.
PADTAD 2008
6
Finding a Concurrent Bug
Advantage
Avoids exhaustive search (either DFS or BFS)
Supporting mechanism
Tight collaboration between static and
dynamic analysis
Iterative information exchange between two
components.
PADTAD 2008
7
An Example
Thread t1 :
Manager (Account P1, Account B1)
P1.deposit(20);
3 accounts:
2 BusinessAccount B1, B2
1 PersonalAccount P1
P1.transfer(20, B1);
transfer
transfer
Thread t2:
Thread t3:
Manager (Account B1, Account B2)
Manager (Account B2, Account P1)
B2.deposit(20);
B1.deposit(20);
B1.transfer(20, B2);
transfer
PADTAD 2008
B2.transfer(20, P1);
8
An Example
Personal
Account
sync transfer(amt,
account) {
bal -= amt;
Business
Account
sync transfer(amt,
account) {
bal -= amt;
//unprotected
sync(account) {
account.bal += amt;
Account
sync deposit(amt) {
bal += amt;
}
account.bal += amt;
}
}
}
Data Race:
A unprotected access of account’s bal field
from the transfer() method of the Personal
Account, while account is depositing.
PADTAD 2008
9
Static Analysis
Static analysis:
MHP read/writes
PersonalAccount::transfer(): account.bal += amt;
AND
Account::deposit(): bal += amt;
This pair might happen between any two threads
due to imprecise alias and call graph analysis.
Alias analysis will resolve every reference of account in
each thread to all three instances of account created in
main().
Call graph analysis will report every account.transfer()
might produce two call edges for two different subtype
of Account.
PADTAD 2008
10
Using Dynamic Information
Analysis of:
PersonalAccount::transfer(): account.bal +=amt;
AND
Account::deposit(): bal +=amt;
T1(P.deposit)
T1(P.transfer)
T2(B.transfer)
False CFG
T3(B.transfer)
False CFG
T2(B.deposit)
T3(B.deposit)
True Alias
True CFG
False Alias
True CFG
False CFG
False CFG
PADTAD 2008
11
Static Analysis
Instead of having dynamic analysis run randomly, we
statically compute a path to test a read/write pair.
Let us assume, we pick pair
T1: PersonalAccount::transfer(): account.bal += amt;
T2: Account::deposit(): bal += amt;
The path will enable w(account.bal) and r(bal) to
become next-to-execute instruction in t1 and t2
respectively.
PADTAD 2008
12
Static Analysis + Dynamic Method
Resolving
T1:
P1.deposit(20);
P1.transfer(20, B1);
deposit(amt) {
bal += amt;
}
transfer(amt, account)
??
Execute program to
here, and look into the
heap to determine the
runtime type of the
callee.
PersonalAccount::transfer() BusinessAccount::transfer()
PADTAD 2008
13
Static Analysis + Dynamic Alias
Checking
T1:
P1.deposit(20);
P1.transfer(20, B1);
T2:
B1.deposit(20);
B1.transfer(20, B2);
deposit(amt) {
bal += amt;
}
deposit(amt) {
tmp = r(bal)
tmp += amt;
w(bal);
}
transfer(amt, account) {
bal -= amt;
//unprotected
tmp = r(account.bal);
tmp += amt;
w(account.bal);
}
Execute threads up to
blue statements, and get
the runtime memory
address of bal.
In this case, aliased.
PADTAD 2008
14
Static Analysis + Dynamic Alias
Checking
T1:
P1.deposit(20);
P1.transfer(20, B1);
T3:
B2.deposit(20);
B2.transfer(20, P1);
deposit(amt) {
bal += amt;
}
deposit(amt) {
tmp = r(bal)
tmp += amt;
w(bal);
}
transfer(amt, account) {
bal -= amt;
//unprotected
tmp = r(account.bal);
tmp += amt;
w(account.bal);
}
Execute threads up to
blue statements, and get
the runtime memory
address of bal.
In this case, not aliased.
PADTAD 2008
15
Implementation
Static Modules
Soot
MHP
Dynamic Modules
runtime control
flow edge
CFG
fulfilling paths
Value Schedule
Generator
Model Checker
JPF
runtime feasibility
runtime alias
relationships
PADTAD 2008
16
A Simple Experiment
Test Case:
AccountSubtype (4 Business, 1 Personal)
Environment:
Intel P4 2.0; Memory 1.5GB
Overall
states
JPF 4.1
Dynamic method
resolving states
Permutation
70279
Instruction
1,783,821
Alias, cfg
193
186
7
34,056
no-alias, cfg
240
186
54
70,316
no-cfg, alias
7
7
58,992
95
95
104,613
no-alias, no-cfg
PADTAD 2008
17
Conclusions
We’ve presented a collaboration scheme
between static and dynamic analysis
Static analysis guides dynamic analysis
Correct static analysis using dynamic analysis
Iterative scheme
Preliminary results show some improvement
over existing JPF
PADTAD 2008
18
Questions?
PADTAD 2008
19