blob: 418bcd12af3ac997cd999508e9eec59cdaadd0ef (
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
|
/*
Note: This example seems to be completely broken. The failing assertion
about locking/unlocking too much causes an inconsistency and all following
assertions pass by default.
It seems that the specification, in particular the loop invariant in method
Add, is wrong. (see also http://boogie.codeplex.com/workitem/10207)
-- August 2011, Stefan Heule
*/
class Client {
method Main(d: Data)
requires d != null
{
var a := new AssociationList
call a.Init()
call a.Add(5, d)
call a.Add(10, d)
var t: Data
call t := a.Get(10)
}
}
class AssociationList {
var head: Node // sentinel
invariant rd(head) && head != null
invariant rd(mu) && rd(head.mu) && this << head
method Init()
requires acc(head) && acc(mu) && mu == lockbottom
ensures acc(mu) && waitlevel << this
{
head := new Node
head.next := null
share head
share this between waitlevel and head
}
method Add(key: int, value: Data)
requires value != null
requires rd(mu) && waitlevel << this
ensures rd(mu)
{
acquire this
var p: Node := head
acquire p
release this
var n := new Node
n.key := key
n.value := value
n.next := p.next
p.next := n
share n between p and n.next
release p
}
method Get(key: int) returns (d: Data)
requires rd(mu) && waitlevel << this
ensures rd(mu)
{
d := null
acquire this
var p: Node := head
acquire p
release this
if (p.next != null) {
acquire p.next
if (p.next.key == key) {
d := p.next.value
} else {
var done := false
while (!done)
// invariant: holds p and p.next
invariant p != null && rd(p.key) && rd(p.value) && acc(p.next) && acc(p.mu,50) && p.next != null
invariant acc(p.next.mu) && p << p.next
invariant rd(p.next.key) && rd(p.next.value) && acc(p.next.next)
invariant p.next.next != null ==>
acc(p.next.next.mu,50) && p.next << p.next.next
invariant holds(p) && holds(p.next) && waitlevel == p.next.mu
invariant p.next.next != null ==> waitlevel << p.next.next
lockchange p, p.next.next
{
if (p.next.next == null) {
done := true // key not present
} else {
acquire p.next.next
if (p.next.next.key == key) {
done := true // key is present
d := p.next.next.value
// move p.next.next closer to the head by one step
var t: Node := p.next
p.next := t.next
t.next := p.next.next
p.next.next := t
reorder t between p.next and t.next
release t
} else {
var t: Node := p
p := p.next
release t
}
}
}
}
release p.next
}
release p
}
}
class Data { }
class Node
{
var key: int
var value: Data
var next: Node
invariant rd(key) && rd(value) && acc(next) && acc(mu,50)
invariant next != null ==> acc(next.mu,50) && this << next
}
|
