blob: 6a67174cf367cc471206f31ddd771e2aadf409c8 (
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
|
class Philosopher module Philosophers {
var left: Fork;
var right: Fork;
method init(f1: Fork, f2: Fork)
requires f1!=null && f2!=null;
requires acc(this.*);
ensures valid;
ensures getLeft()==f1 && getRight()==f2;
{
left := f1;
right := f2;
fold valid;
}
method run()
requires valid;
requires acc(getLeft().mu, 10);
requires acc(getRight().mu, 10);
requires maxlock << getLeft().mu;
requires maxlock << getRight().mu;
requires getLeft().mu << getRight().mu;
{
while(true)
invariant valid && acc(getLeft().mu, 10) && acc(getRight().mu, 10) && maxlock << getLeft().mu && maxlock << getRight().mu && getLeft().mu << getRight().mu;
{
unfold valid;
acquire left;
acquire right;
//eat
release left;
release right;
fold valid;
}
}
function getLeft(): Fork
requires valid;
ensures result!=null;
{
unfolding valid in left
}
function getRight(): Fork
requires valid;
ensures result!=null;
{
unfolding valid in right
}
predicate valid {
acc(left) && acc(right) && left!=null && right!=null
}
}
class Fork module Dining {
invariant true;
}
class Program module Main {
method main(){
// create forks
var f1 := new Fork;
var f2 := new Fork;
var f3 := new Fork;
share f1;
share f2 above f1;
share f3 above f1, f2;
// create philosophers
var aristotle := new Philosopher;
call aristotle.init(f1, f2);
var plato := new Philosopher;
call plato.init(f2, f3);
var kant := new Philosopher;
call kant.init(f1, f3);
assert f2.mu << f3.mu;
// start eating
fork tk0 := aristotle.run();
fork tk1 := plato.run();
fork tk2 := kant.run();
// everyone's done
join tk0;
join tk1;
join tk2;
}
}
|
