1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
// JBMC, concurrency tests that make use of
// the java.lang.Runnable model
import java.lang.Thread;
import org.cprover.CProver;
public class A
{
// calling start from outside.
// expected verfication success.
public void me3()
{
C c = new C();
Thread tmp = new Thread(c);
tmp.start();
c.setX();
}
// calling start from outside, no race-condition on B.x
// expected verfication success.
public void me4()
{
B b = new B();
Thread tmp = new Thread(b);
tmp.start();
}
// expected verfication failed
public void me2()
{
B b = new B();
b.me();
}
// expected verfication success.
public void me()
{
C c = new C();
c.me();
}
}
class B implements Runnable
{
int x = 0;
@Override
public void run()
{
x = 44;
int local_x = x;
assert(local_x == 44);
}
public void me()
{
Thread tmp = new Thread(this);
tmp.start();
x = 10;
}
}
class C implements Runnable
{
int x = 0;
@Override
public void run()
{
x = 44;
int local_x = x;
assert(local_x == 44 || x == 10);
}
public void me()
{
Thread tmp = new Thread(this);
tmp.start();
setX();
}
public void setX()
{
x = 10;
}
}
|
