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
|
class List {
ghost var sum: int
var head: Node
invariant acc(head) && head != null
invariant rd(head.val) && head.val == -1
invariant rd(mu) && acc(head.mu,50) && this << head
invariant acc(sum,20) && acc(head.sum, 50) && sum == head.sum
method Main()
{
var list := new List
call list.Init()
call list.Insert(8)
call list.Insert(12)
call list.Insert(4)
assert list.sum == 24
}
method Init()
requires acc(mu) && mu == lockbottom && acc(head) && acc(sum)
ensures rd(mu,*) && waitlevel << this
ensures acc(sum,80) && sum == 0
{
var t := new Node
t.val := -1
t.next := null
t.sum := 0
share t
head := t
sum := 0
share this between waitlevel and t
}
method Insert(x: int)
requires rd(mu) && waitlevel << this
requires acc(sum,80) && 0 <= x
ensures rd(mu)
ensures acc(sum,80) && sum == old(sum) + x
{
acquire this
assert waitlevel == this.mu;
sum := sum + x
var p: Node := head
acquire p
p.sum := p.sum + x
release this
while (p.next != null && p.next.val < x)
invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)
invariant holds(p) && waitlevel == p.mu
invariant !old(holds(p)) && !old(rd holds(p))
invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val
invariant acc(p.sum, 50)
invariant p.next == null ==> p.sum == x
invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum + x
invariant p.val <= x
lockchange p
{
var nx: Node := p.next
acquire nx
nx.sum := nx.sum + x
release p
p := nx
}
var t := new Node
t.val := x
t.next := p.next
if (t.next == null) { t.sum := 0 } else { t.sum := p.next.val + p.next.sum }
share t between p and p.next
p.next := t
release p
}
method Delete(x: int) returns (wasPresent: bool)
requires rd(mu) && waitlevel << this
requires acc(sum,80) && 0 <= x
ensures acc(sum,80) && (wasPresent ==> sum == old(sum) - x) && (!wasPresent ==> sum == old(sum))
{
ghost const c
acquire this
sum := sum - c
var p: Node := head
acquire p
p.sum := p.sum - c
release this
while (p.next != null && p.next.val < x)
invariant p != null && acc(p.next) && rd(p.val) && acc(p.mu,50)
invariant holds(p) && waitlevel == p.mu && !assigned(c)
invariant !old(holds(p)) && !old(rd holds(p))
invariant p.next != null ==> acc(p.next.mu,50) && p << p.next
invariant p.next != null ==> rd(p.next.val) && p.val <= p.next.val
invariant acc(p.sum, 50)
invariant p.next == null ==> p.sum == 0 - c
invariant p.next != null ==> acc(p.next.sum, 50) && p.sum == p.next.val + p.next.sum - c
invariant p.val <= x
lockchange p
{
var nx: Node := p.next
acquire nx
nx.sum := nx.sum - c
release p
p := nx
}
if (p.next != null && p.next.val == x) {
wasPresent := true
c := x
var nx: Node := p.next
acquire nx
p.next := nx.next
unshare nx
} else {
wasPresent := false
c := 0
}
release p
}
}
class Node {
ghost var sum: int
var val: int
var next: Node
invariant acc(next) && rd(val)
invariant next != null ==> rd(next.val) && val <= next.val
invariant acc(sum, 50)
invariant next == null ==> sum == 0
invariant next != null ==> acc(next.sum, 50) && sum == next.val + next.sum
invariant acc(mu,50) && (next != null ==> acc(next.mu,50) && this << next)
}
|
