|
1 (* Title: HOL/UNITY/Alloc |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Specification of Chandy and Charpentier's Allocator |
|
7 *) |
|
8 |
|
9 Alloc = Follows + Comp + |
|
10 |
|
11 (*simplifies the expression of some specifications*) |
|
12 constdefs |
|
13 sub :: ['a, 'a=>'b] => 'b |
|
14 "sub i f == f i" |
|
15 |
|
16 (*Duplicated from HOL/ex/NatSum.thy. |
|
17 Maybe type should be [nat=>int, nat] => int**) |
|
18 consts sum :: [nat=>nat, nat] => nat |
|
19 primrec |
|
20 "sum f 0 = 0" |
|
21 "sum f (Suc n) = f(n) + sum f n" |
|
22 |
|
23 |
|
24 (*This function merely sums the elements of a list*) |
|
25 consts tokens :: nat list => nat |
|
26 primrec |
|
27 "tokens [] = 0" |
|
28 "tokens (x#xs) = x + tokens xs" |
|
29 |
|
30 |
|
31 consts |
|
32 NbT :: nat (*Number of tokens in system*) |
|
33 Nclients :: nat (*Number of clients*) |
|
34 |
|
35 |
|
36 record clientState = |
|
37 giv :: nat list (*client's INPUT history: tokens GRANTED*) |
|
38 ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) |
|
39 rel :: nat list (*client's OUTPUT history: tokens RELEASED*) |
|
40 |
|
41 record allocState = |
|
42 allocGiv :: nat => nat list (*allocator's local copy of "giv" for i*) |
|
43 allocAsk :: nat => nat list (*allocator's local copy of "ask" for i*) |
|
44 allocRel :: nat => nat list (*allocator's local copy of "rel" for i*) |
|
45 |
|
46 record systemState = allocState + |
|
47 client :: nat => clientState (*states of all clients*) |
|
48 |
|
49 |
|
50 constdefs |
|
51 |
|
52 (** Resource allocation system specification **) |
|
53 |
|
54 (*spec (1)*) |
|
55 system_safety :: systemState program set |
|
56 "system_safety == |
|
57 Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients |
|
58 <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}" |
|
59 |
|
60 (*spec (2)*) |
|
61 system_progress :: systemState program set |
|
62 "system_progress == INT i : lessThan Nclients. |
|
63 INT h. |
|
64 {s. h <= (ask o sub i o client)s} LeadsTo |
|
65 {s. h pfix_le (giv o sub i o client) s}" |
|
66 |
|
67 (** Client specification (required) ***) |
|
68 |
|
69 (*spec (3)*) |
|
70 client_increasing :: clientState program set |
|
71 "client_increasing == |
|
72 UNIV guarantees Increasing ask Int Increasing rel" |
|
73 |
|
74 (*spec (4)*) |
|
75 client_bounded :: clientState program set |
|
76 "client_bounded == |
|
77 UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" |
|
78 |
|
79 (*spec (5)*) |
|
80 client_progress :: clientState program set |
|
81 "client_progress == |
|
82 Increasing giv |
|
83 guarantees |
|
84 (INT h. {s. h <= giv s & h pfix_ge ask s} |
|
85 LeadsTo |
|
86 {s. tokens h <= (tokens o rel) s})" |
|
87 |
|
88 (** Allocator specification (required) ***) |
|
89 |
|
90 (*spec (6)*) |
|
91 alloc_increasing :: allocState program set |
|
92 "alloc_increasing == |
|
93 UNIV |
|
94 guarantees |
|
95 (INT i : lessThan Nclients. Increasing (sub i o allocAsk))" |
|
96 |
|
97 (*spec (7)*) |
|
98 alloc_safety :: allocState program set |
|
99 "alloc_safety == |
|
100 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
|
101 guarantees |
|
102 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
|
103 <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
|
104 |
|
105 (*spec (8)*) |
|
106 alloc_progress :: allocState program set |
|
107 "alloc_progress == |
|
108 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
|
109 Increasing (sub i o allocRel)) |
|
110 Int |
|
111 Always {s. ALL i : lessThan Nclients. |
|
112 ALL k : lessThan (length (allocAsk s i)). |
|
113 allocAsk s i ! k <= NbT} |
|
114 Int |
|
115 (INT i : lessThan Nclients. |
|
116 INT h. {s. h <= (sub i o allocGiv)s & h pfix_ge (sub i o allocAsk)s} |
|
117 LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) |
|
118 guarantees |
|
119 (INT i : lessThan Nclients. |
|
120 INT h. {s. h <= (sub i o allocAsk) s} LeadsTo |
|
121 {s. h pfix_le (sub i o allocGiv) s})" |
|
122 |
|
123 (** Network specification ***) |
|
124 |
|
125 (*spec (9.1)*) |
|
126 network_ask :: systemState program set |
|
127 "network_ask == INT i : lessThan Nclients. |
|
128 Increasing (ask o sub i o client) guarantees |
|
129 ((sub i o allocAsk) Fols (ask o sub i o client))" |
|
130 |
|
131 (*spec (9.2)*) |
|
132 network_giv :: systemState program set |
|
133 "network_giv == INT i : lessThan Nclients. |
|
134 Increasing (sub i o allocGiv) guarantees |
|
135 ((giv o sub i o client) Fols (sub i o allocGiv))" |
|
136 |
|
137 (*spec (9.3)*) |
|
138 network_rel :: systemState program set |
|
139 "network_rel == INT i : lessThan Nclients. |
|
140 Increasing (rel o sub i o client) guarantees |
|
141 ((sub i o allocRel) Fols (rel o sub i o client))" |
|
142 |
|
143 end |