blob: cc3ecfb4102353cc9147fcefc94b65b18b563a50 (
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
|
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
}
|
