blob: f4cc25d20329cb431b0df50b70ffdaa847cee910 (
plain)
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
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
|
class Node {
var left: Node;
var right: Node;
var parent: Node;
var anc: set<Node>;
var desc: set<Node>;
var sense: bool;
var pc: int;
function validDown(): bool
reads this, desc;
{
this !in desc &&
null !in desc &&
left != right && // not needed, but speeds up verification
(right != null ==> right in desc && left !in right.desc) &&
(left != null ==>
left in desc &&
(right != null ==> desc == {left,right} + left.desc + right.desc) &&
(right == null ==> desc == {left} + left.desc) &&
left.validDown()) &&
(left == null ==>
(right != null ==> desc == {right} + right.desc) &&
(right == null ==> desc == {})) &&
(right != null ==> right.validDown()) &&
(blocked() ==> forall m :: m in desc ==> m.blocked()) &&
(after() ==> forall m :: m in desc ==> m.blocked() || m.after())
// (left != null && right != null ==> left.desc !! right.desc) // not needed
}
function validUp(): bool
reads this, anc;
{
this !in anc &&
null !in anc &&
(parent != null ==> parent in anc && anc == { parent } + parent.anc && parent.validUp()) &&
(parent == null ==> anc == {}) &&
(after() ==> forall m :: m in anc ==> m.after())
}
function valid(): bool
reads this, desc, anc;
{ validUp() && validDown() && desc !! anc }
function before(): bool
reads this;
{ !sense && pc <= 2 }
function blocked(): bool
reads this;
{ sense }
function after(): bool
reads this;
{ !sense && 3 <= pc }
method barrier()
requires valid();
requires before();
modifies this, left, right;
{
//A
pc := 1;
if(left != null) {
while(!left.sense)
modifies left;
invariant validDown(); // this seems necessary to get the necessary unfolding of functions
invariant valid();
decreases *; // to by-pass termination checking for this loop
{
// this loop body is supposed to model what the "left" thread
// might do to its node. This body models a transition from
// "before" to "blocked" by setting sense to true. A transition
// all the way to "after" is not permitted; this would require
// a change of pc.
// We assume that "left" preserves the validity of its subtree,
// which means in particular that it goes to "blocked" only if
// all its descendants are already blocked.
left.sense := *;
assume left.blocked() ==> forall m :: m in left.desc ==> m.blocked();
}
}
if(right != null) {
while(!right.sense)
modifies right;
invariant validDown(); // this seems necessary to get the necessary unfolding of functions
invariant valid();
decreases *; // to by-pass termination checking for this loop
{
// analogous to the previous loop
right.sense := *;
assume right.blocked() ==> forall m :: m in right.desc ==> m.blocked();
}
}
//B
pc := 2;
if(parent != null) {
sense := true;
}
//C
pc := 3;
while(sense)
modifies this;
invariant validUp(); // this seems necessary to get the necessary unfolding of functions
invariant valid();
invariant left == old(left);
invariant right == old(right);
invariant sense ==> parent != null;
decreases *; // to by-pass termination checking for this loop
{
// this loop body is supposed to model what the "parent" thread
// might do to its node. The body models a transition from
// "blocked" to "after" by setting sense to false.
// We assume that "parent" initiates this transition only
// after it went to state "after" itself.
sense := *;
assume !sense ==> parent.after();
}
//D
pc := 4;
if(left != null) {
left.sense := false;
}
//E
pc := 5;
if(right != null) {
right.sense := false;
}
//F
pc := 6;
}
}
|
