Presentation

Practical Verification of
High-Level Dataraces in
Transactional Memory
Programs
Vasco Pessanha (*) Ricardo J. Dias (*) João Lourenço (*)
Eitan Farchi (+) Diogo Sousa (*)
(*) Universidade Nova de Lisboa
(+) IBM Research Labs at Haifa
CONTEXT
Concurrent Programming
And with TM...?
•  No DeadLocks
•  No Priority Inversion
2
LOW-LEVEL DATARACES
Dataraces
Low-level Dataraces...
@Atomic
public void setX_1() {
access x
}
// Not Atomic
public void setX_2() {
access x
}
3
HIGH-LEVEL DATARACES
¡ A rtho (2003)
§ Views
V(swap) = {{x,y}}
V(reset) = {{x},{y}}
§ Maximal Views
M = V(swap) = {{x,y}}
§ Conflict ó views are
subsets of a Maximal View
and don’t form a chain
public void swap() {
synchronized
(lock) {
atomic
{
read/write(coord.x)
read/write(coord.y)
}
}
public void reset() {
synchronized
(lock) {
atomic
{
write(coord.x)
}
synchronized
(lock) {
atomic
{
write(coord.y)
}
}
V(reset) are subsets of the Maximal View and don’t form a chain
4
OUR APPROACH
¡ E xtend Artho’s Algorithm for the detection of
HLDR
§ 1. Differentiate Reads and Writes
Extension
Artho
• 
V(method)
• 
Vr(method), Vw(method)
• 
M(thread)
• 
Mr(thread), Mw(thread)
• 
Conflits between M and V
• 
Conflits between:
•  Mr and Vw
•  Mw and Vr
•  Mw and Vw
5
OUR APPROACH
¡ E xtend Artho’s Algorithm
§ 1. Differentiate Reads and Writes
§ 2. Complement it with the detections of stale-values
Thread 1
Transaction1
Transaction3
Write(x)
Read(x)
Thread 2
Write(x)
Stale
Value
Transaction2
Thread 1
read(x) Є v1 Є Vr(t1)
write(x) Є v3 Є Vw(t1)
write(x) Є v2 Є Vw(t2)
Thread 2
Not overwritten!
Not read before!
Stale
Value
6
HIGH-LEVEL DATARACES
High-level Dataraces
@Atomic
public int setPair(int v1,
int v2){
x = v1;
y = v2;
}
t1.view1
T1
Pair
X
@Atomic
public int getSum{
return x+y;
}
Y
t2.view1
T2
7
HIGH-LEVEL DATARACES
High-level Dataraces
@Atomic
public int setPair(int v1,
int v2){
x = v1;
y = v2;
}
t1.view1
T1
Pair
X
@Atomic
public int getY{
return y;
}
Y
t2.view1
T2
8
HIGH-LEVEL DATARACES
High-level Dataraces
@Atomic
public int setPair(int v1,
int v2){
x = v1;
y = v2;
}
Pair
X
Y
t1.view1
t2.view2
@Atomic
public int
return
}
@Atomic
public int
return
}
getY{
y;
getSum{
x+y;
t2.view1
T1
T2
9
HIGH-LEVEL DATARACES
High-level Dataraces
@Atomic
public int setPair(int v1,
int v2){
x = v1;
y = v2;
}
Pair
X
Y
t1.view1
public boolean equal{
int x = getX();
int y = getY();
return x == y;
}
t2.view2
t2.view1
T1
T2
10
HIGH-LEVEL DATARACES
¡ V iew compatibility
Conflits between:
Mr and Vw
Mw and Vr
Mw and Vw
¡ V iew safety (high-level datarace free)
11
STALE-VALUES
Stale-Value Errors
public void incX(){
int tmp = getX();
tmp = tmp + 1;
setX(2)
setX(tmp);
}
12
STALE-VALUES
Stale-Value Errors
Teixeira (2010) RwW pattern
public void incX(){
int tmp = getX(); //Read(x)
tmp = tmp + 1;
setX(tmp);
//write(x)
setX(2)
//write(x)
}
13
STALE-VALUES
Stale-Value Errors
Problem...?
@Atomic
T2
T1
incX() //r and w
public void incX(){
incX() //r and w
x = x + 1; //read(x) and write(x)
}
incX() //r and w
STALE-VALUES
Stale-Value Errors
read(x)
(r,x,overwritten?)
write(x)
(w,x,readBefore?)
RwW
(r,x,f)
(w,x,f)
(w,x,?)
@Atomic
public void incX(){
x = x + 1; //(r,x,t), (w,x,t)
}
RwW
STALE-VALUES
Stale-Value Errors
Problem...?
public void specialSet(int v){
int old = getX(); //(r,x,f)
System.out.println(old);
setX(v);
}
//(w,x,f)
setX(2)
//(w,x,f)
MOTH
Instance Type
Analysis
Soot
Views
Analysis
Method Analysis
Collecting Information
Sensor Manager
TM-based Java
ByteCode program
View Consistency
Sensor
Stale Value
Sensor
...
Datarace Detection
24
PROBLEMS (1)
¡ P roblems
§ Dynamic dispatch (interface methods)
private List list;
public void initA() {
list = new LinkedList();
}
public void initB() {
list = new ArrayList();
}
main(){
if(?)
initA();
else
initB();
???
list.add(1);
}
25
PROBLEMS (1)
@Atomic
¡ P roblems
public int
get() {...}
@Atomicdispatch (interface methods)
§ Dynamic
public void add(int e) {...}
public
void inc(){
§ Native
methods
§  e.g.
int x = get();
socket.getOutputStream.write(..)
x++;
add(x);
write(socket)???
}
§ “Conflicts”
main(){ versus “Real Conflicts”
for(...)
add(i);
for(...)
System.out.print(get())
}
26
PROBLEMS (2)
¡ S olutions
§ Dynamic dispatch (interface methods)
§  Analysis of the new expressions
§  Assume the worst cenario (r(obj), w(obj))
§  Ask for user annotations
27
PROBLEMS (2)
¡ S olutions
§ Dynamic dispatch (interface methods)
§ Native methods
§  Assume the worst cenario (r(obj), w(obj))
§  Ask for user annotations
28
PROBLEMS (2)
¡ S olutions
§ Dynamic dispatch (interface methods)
§ Native methods
§ “Conflicts” versus “Real Conflicts”
§  Dataflow and MHP analysis (future work)
§  Dataraces and Warnings
29
RESULTS
Detected 87% of the
dataraces
All 6 false positives are
caused by the Single
Variable Sensor
30
RESULTS
s
e
v
i
t
ga
e
N
e
Fals
Problems with
native methods of
the Socket Class
Dynamic Dispatch
still not working in
some cases
31
RESULTS
s
e
v
i
t
si
o
P
e
Fals
Conflict vs Real
Conflict (DF)
Conflict vs Real
Conflict (DF)
Conflict vs Real
Conflict (DF)
Variant of stale
value pattern
Conflict vs Real
Conflict (MHP)
32
CONCLUSIONS
¡ E xtension of Artho’s initial proposal
§ Distinction on R/W operations
§ Detection of stale values
¡ M oTH is a practical tool to use with
§ Experiments with medium sized Java programs (100’s
of lines) are very promisor
§ Plugin based architecture
¡ O ngoing work to include
§ Data-flow and control flow anaysis
38
THE END
Thank you Ques-ons? 39