|
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 = AllocBase + PPROD + |
|
10 |
|
11 (** State definitions. OUTPUT variables are locals **) |
|
12 |
|
13 record clientState = |
|
14 giv :: nat list (*client's INPUT history: tokens GRANTED*) |
|
15 ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) |
|
16 rel :: nat list (*client's OUTPUT history: tokens RELEASED*) |
|
17 |
|
18 record 'a clientState_d = |
|
19 clientState + |
|
20 dummy :: 'a (*dummy field for new variables*) |
|
21 |
|
22 constdefs |
|
23 (*DUPLICATED FROM Client.thy, but with "tok" removed*) |
|
24 (*Maybe want a special theory section to declare such maps*) |
|
25 non_dummy :: 'a clientState_d => clientState |
|
26 "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)" |
|
27 |
|
28 (*Renaming map to put a Client into the standard form*) |
|
29 client_map :: "'a clientState_d => clientState*'a" |
|
30 "client_map == funPair non_dummy dummy" |
|
31 |
|
32 |
|
33 record allocState = |
|
34 allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*) |
|
35 allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*) |
|
36 allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*) |
|
37 |
|
38 record 'a allocState_d = |
|
39 allocState + |
|
40 dummy :: 'a (*dummy field for new variables*) |
|
41 |
|
42 record 'a systemState = |
|
43 allocState + |
|
44 client :: nat => clientState (*states of all clients*) |
|
45 dummy :: 'a (*dummy field for new variables*) |
|
46 |
|
47 |
|
48 constdefs |
|
49 |
|
50 (** Resource allocation system specification **) |
|
51 |
|
52 (*spec (1)*) |
|
53 system_safety :: 'a systemState program set |
|
54 "system_safety == |
|
55 Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients) |
|
56 <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}" |
|
57 |
|
58 (*spec (2)*) |
|
59 system_progress :: 'a systemState program set |
|
60 "system_progress == INT i : lessThan Nclients. |
|
61 INT h. |
|
62 {s. h <= (ask o sub i o client)s} LeadsTo |
|
63 {s. h pfixLe (giv o sub i o client) s}" |
|
64 |
|
65 system_spec :: 'a systemState program set |
|
66 "system_spec == system_safety Int system_progress" |
|
67 |
|
68 (** Client specification (required) ***) |
|
69 |
|
70 (*spec (3)*) |
|
71 client_increasing :: 'a clientState_d program set |
|
72 "client_increasing == |
|
73 UNIV guarantees Increasing ask Int Increasing rel" |
|
74 |
|
75 (*spec (4)*) |
|
76 client_bounded :: 'a clientState_d program set |
|
77 "client_bounded == |
|
78 UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}" |
|
79 |
|
80 (*spec (5)*) |
|
81 client_progress :: 'a clientState_d program set |
|
82 "client_progress == |
|
83 Increasing giv guarantees |
|
84 (INT h. {s. h <= giv s & h pfixGe ask s} |
|
85 LeadsTo {s. tokens h <= (tokens o rel) s})" |
|
86 |
|
87 (*spec: preserves part*) |
|
88 client_preserves :: 'a clientState_d program set |
|
89 "client_preserves == preserves giv Int preserves clientState_d.dummy" |
|
90 |
|
91 (*environmental constraints*) |
|
92 client_allowed_acts :: 'a clientState_d program set |
|
93 "client_allowed_acts == |
|
94 {F. AllowedActs F = |
|
95 insert Id (UNION (preserves (funPair rel ask)) Acts)}" |
|
96 |
|
97 client_spec :: 'a clientState_d program set |
|
98 "client_spec == client_increasing Int client_bounded Int client_progress |
|
99 Int client_allowed_acts Int client_preserves" |
|
100 |
|
101 (** Allocator specification (required) ***) |
|
102 |
|
103 (*spec (6)*) |
|
104 alloc_increasing :: 'a allocState_d program set |
|
105 "alloc_increasing == |
|
106 UNIV guarantees |
|
107 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
|
108 |
|
109 (*spec (7)*) |
|
110 alloc_safety :: 'a allocState_d program set |
|
111 "alloc_safety == |
|
112 (INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
|
113 guarantees |
|
114 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients) |
|
115 <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}" |
|
116 |
|
117 (*spec (8)*) |
|
118 alloc_progress :: 'a allocState_d program set |
|
119 "alloc_progress == |
|
120 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
|
121 Increasing (sub i o allocRel)) |
|
122 Int |
|
123 Always {s. ALL i<Nclients. |
|
124 ALL elt : set ((sub i o allocAsk) s). elt <= NbT} |
|
125 Int |
|
126 (INT i : lessThan Nclients. |
|
127 INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
|
128 LeadsTo |
|
129 {s. tokens h <= (tokens o sub i o allocRel)s}) |
|
130 guarantees |
|
131 (INT i : lessThan Nclients. |
|
132 INT h. {s. h <= (sub i o allocAsk) s} |
|
133 LeadsTo |
|
134 {s. h pfixLe (sub i o allocGiv) s})" |
|
135 |
|
136 (*NOTE: to follow the original paper, the formula above should have had |
|
137 INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s} |
|
138 LeadsTo |
|
139 {s. tokens h i <= (tokens o sub i o allocRel)s}) |
|
140 thus h should have been a function variable. However, only h i is ever |
|
141 looked at.*) |
|
142 |
|
143 (*spec: preserves part*) |
|
144 alloc_preserves :: 'a allocState_d program set |
|
145 "alloc_preserves == preserves allocRel Int preserves allocAsk Int |
|
146 preserves allocState_d.dummy" |
|
147 |
|
148 (*environmental constraints*) |
|
149 alloc_allowed_acts :: 'a allocState_d program set |
|
150 "alloc_allowed_acts == |
|
151 {F. AllowedActs F = |
|
152 insert Id (UNION (preserves allocGiv) Acts)}" |
|
153 |
|
154 alloc_spec :: 'a allocState_d program set |
|
155 "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int |
|
156 alloc_allowed_acts Int alloc_preserves" |
|
157 |
|
158 (** Network specification ***) |
|
159 |
|
160 (*spec (9.1)*) |
|
161 network_ask :: 'a systemState program set |
|
162 "network_ask == INT i : lessThan Nclients. |
|
163 Increasing (ask o sub i o client) guarantees |
|
164 ((sub i o allocAsk) Fols (ask o sub i o client))" |
|
165 |
|
166 (*spec (9.2)*) |
|
167 network_giv :: 'a systemState program set |
|
168 "network_giv == INT i : lessThan Nclients. |
|
169 Increasing (sub i o allocGiv) |
|
170 guarantees |
|
171 ((giv o sub i o client) Fols (sub i o allocGiv))" |
|
172 |
|
173 (*spec (9.3)*) |
|
174 network_rel :: 'a systemState program set |
|
175 "network_rel == INT i : lessThan Nclients. |
|
176 Increasing (rel o sub i o client) |
|
177 guarantees |
|
178 ((sub i o allocRel) Fols (rel o sub i o client))" |
|
179 |
|
180 (*spec: preserves part*) |
|
181 network_preserves :: 'a systemState program set |
|
182 "network_preserves == |
|
183 preserves allocGiv Int |
|
184 (INT i : lessThan Nclients. preserves (rel o sub i o client) Int |
|
185 preserves (ask o sub i o client))" |
|
186 |
|
187 (*environmental constraints*) |
|
188 network_allowed_acts :: 'a systemState program set |
|
189 "network_allowed_acts == |
|
190 {F. AllowedActs F = |
|
191 insert Id |
|
192 (UNION (preserves allocRel Int |
|
193 (INT i: lessThan Nclients. preserves(giv o sub i o client))) |
|
194 Acts)}" |
|
195 |
|
196 network_spec :: 'a systemState program set |
|
197 "network_spec == network_ask Int network_giv Int |
|
198 network_rel Int network_allowed_acts Int |
|
199 network_preserves" |
|
200 |
|
201 |
|
202 (** State mappings **) |
|
203 sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState" |
|
204 "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s |
|
205 in (| allocGiv = allocGiv s, |
|
206 allocAsk = allocAsk s, |
|
207 allocRel = allocRel s, |
|
208 client = cl, |
|
209 dummy = xtr|)" |
|
210 |
|
211 |
|
212 sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState" |
|
213 "sysOfClient == %(cl,al). (| allocGiv = allocGiv al, |
|
214 allocAsk = allocAsk al, |
|
215 allocRel = allocRel al, |
|
216 client = cl, |
|
217 systemState.dummy = allocState_d.dummy al|)" |
|
218 |
|
219 consts |
|
220 Alloc :: 'a allocState_d program |
|
221 Client :: 'a clientState_d program |
|
222 Network :: 'a systemState program |
|
223 System :: 'a systemState program |
|
224 |
|
225 rules |
|
226 Alloc "Alloc : alloc_spec" |
|
227 Client "Client : client_spec" |
|
228 Network "Network : network_spec" |
|
229 |
|
230 defs |
|
231 System_def |
|
232 "System == rename sysOfAlloc Alloc Join Network Join |
|
233 (rename sysOfClient |
|
234 (plam x: lessThan Nclients. rename client_map Client))" |
|
235 |
|
236 |
|
237 (** |
|
238 locale System = |
|
239 fixes |
|
240 Alloc :: 'a allocState_d program |
|
241 Client :: 'a clientState_d program |
|
242 Network :: 'a systemState program |
|
243 System :: 'a systemState program |
|
244 |
|
245 assumes |
|
246 Alloc "Alloc : alloc_spec" |
|
247 Client "Client : client_spec" |
|
248 Network "Network : network_spec" |
|
249 |
|
250 defines |
|
251 System_def |
|
252 "System == rename sysOfAlloc Alloc |
|
253 Join |
|
254 Network |
|
255 Join |
|
256 (rename sysOfClient |
|
257 (plam x: lessThan Nclients. rename client_map Client))" |
|
258 **) |
|
259 |
|
260 |
|
261 end |