summaryrefslogtreecommitdiff
path: root/Chalice/examples/dining-philosophers.chalice
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;
  }
}