1 (* Title: HOL/UNITY/AllocImpl |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Implementation of a multiple-client allocator from a single-client allocator |
|
7 *) |
|
8 |
|
9 AllocImpl = AllocBase + Follows + PPROD + |
|
10 |
|
11 |
|
12 (** State definitions. OUTPUT variables are locals **) |
|
13 |
|
14 (*Type variable 'b is the type of items being merged*) |
|
15 record 'b merge = |
|
16 In :: nat => 'b list (*merge's INPUT histories: streams to merge*) |
|
17 Out :: 'b list (*merge's OUTPUT history: merged items*) |
|
18 iOut :: nat list (*merge's OUTPUT history: origins of merged items*) |
|
19 |
|
20 record ('a,'b) merge_d = |
|
21 'b merge + |
|
22 dummy :: 'a (*dummy field for new variables*) |
|
23 |
|
24 constdefs |
|
25 non_dummy :: ('a,'b) merge_d => 'b merge |
|
26 "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)" |
|
27 |
|
28 record 'b distr = |
|
29 In :: 'b list (*items to distribute*) |
|
30 iIn :: nat list (*destinations of items to distribute*) |
|
31 Out :: nat => 'b list (*distributed items*) |
|
32 |
|
33 record ('a,'b) distr_d = |
|
34 'b distr + |
|
35 dummy :: 'a (*dummy field for new variables*) |
|
36 |
|
37 record allocState = |
|
38 giv :: nat list (*OUTPUT history: source of tokens*) |
|
39 ask :: nat list (*INPUT: tokens requested from allocator*) |
|
40 rel :: nat list (*INPUT: tokens released to allocator*) |
|
41 |
|
42 record 'a allocState_d = |
|
43 allocState + |
|
44 dummy :: 'a (*dummy field for new variables*) |
|
45 |
|
46 record 'a systemState = |
|
47 allocState + |
|
48 mergeRel :: nat merge |
|
49 mergeAsk :: nat merge |
|
50 distr :: nat distr |
|
51 dummy :: 'a (*dummy field for new variables*) |
|
52 |
|
53 |
|
54 constdefs |
|
55 |
|
56 (** Merge specification (the number of inputs is Nclients) ***) |
|
57 |
|
58 (*spec (10)*) |
|
59 merge_increasing :: ('a,'b) merge_d program set |
|
60 "merge_increasing == |
|
61 UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)" |
|
62 |
|
63 (*spec (11)*) |
|
64 merge_eqOut :: ('a,'b) merge_d program set |
|
65 "merge_eqOut == |
|
66 UNIV guarantees |
|
67 Always {s. length (merge.Out s) = length (merge.iOut s)}" |
|
68 |
|
69 (*spec (12)*) |
|
70 merge_bounded :: ('a,'b) merge_d program set |
|
71 "merge_bounded == |
|
72 UNIV guarantees |
|
73 Always {s. ALL elt : set (merge.iOut s). elt < Nclients}" |
|
74 |
|
75 (*spec (13)*) |
|
76 merge_follows :: ('a,'b) merge_d program set |
|
77 "merge_follows == |
|
78 (INT i : lessThan Nclients. Increasing (sub i o merge.In)) |
|
79 guarantees |
|
80 (INT i : lessThan Nclients. |
|
81 (%s. sublist (merge.Out s) |
|
82 {k. k < size(merge.iOut s) & merge.iOut s! k = i}) |
|
83 Fols (sub i o merge.In))" |
|
84 |
|
85 (*spec: preserves part*) |
|
86 merge_preserves :: ('a,'b) merge_d program set |
|
87 "merge_preserves == preserves merge.In Int preserves merge_d.dummy" |
|
88 |
|
89 (*environmental constraints*) |
|
90 merge_allowed_acts :: ('a,'b) merge_d program set |
|
91 "merge_allowed_acts == |
|
92 {F. AllowedActs F = |
|
93 insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}" |
|
94 |
|
95 merge_spec :: ('a,'b) merge_d program set |
|
96 "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int |
|
97 merge_follows Int merge_allowed_acts Int merge_preserves" |
|
98 |
|
99 (** Distributor specification (the number of outputs is Nclients) ***) |
|
100 |
|
101 (*spec (14)*) |
|
102 distr_follows :: ('a,'b) distr_d program set |
|
103 "distr_follows == |
|
104 Increasing distr.In Int Increasing distr.iIn Int |
|
105 Always {s. ALL elt : set (distr.iIn s). elt < Nclients} |
|
106 guarantees |
|
107 (INT i : lessThan Nclients. |
|
108 (sub i o distr.Out) Fols |
|
109 (%s. sublist (distr.In s) |
|
110 {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))" |
|
111 |
|
112 distr_allowed_acts :: ('a,'b) distr_d program set |
|
113 "distr_allowed_acts == |
|
114 {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}" |
|
115 |
|
116 distr_spec :: ('a,'b) distr_d program set |
|
117 "distr_spec == distr_follows Int distr_allowed_acts" |
|
118 |
|
119 (** Single-client allocator specification (required) ***) |
|
120 |
|
121 (*spec (18)*) |
|
122 alloc_increasing :: 'a allocState_d program set |
|
123 "alloc_increasing == UNIV guarantees Increasing giv" |
|
124 |
|
125 (*spec (19)*) |
|
126 alloc_safety :: 'a allocState_d program set |
|
127 "alloc_safety == |
|
128 Increasing rel |
|
129 guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}" |
|
130 |
|
131 (*spec (20)*) |
|
132 alloc_progress :: 'a allocState_d program set |
|
133 "alloc_progress == |
|
134 Increasing ask Int Increasing rel Int |
|
135 Always {s. ALL elt : set (ask s). elt <= NbT} |
|
136 Int |
|
137 (INT h. {s. h <= giv s & h pfixGe (ask s)} |
|
138 LeadsTo |
|
139 {s. tokens h <= tokens (rel s)}) |
|
140 guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})" |
|
141 |
|
142 (*spec: preserves part*) |
|
143 alloc_preserves :: 'a allocState_d program set |
|
144 "alloc_preserves == preserves rel Int |
|
145 preserves ask Int |
|
146 preserves allocState_d.dummy" |
|
147 |
|
148 |
|
149 (*environmental constraints*) |
|
150 alloc_allowed_acts :: 'a allocState_d program set |
|
151 "alloc_allowed_acts == |
|
152 {F. AllowedActs F = insert Id (UNION (preserves giv) 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 locale Merge = |
|
159 fixes |
|
160 M :: ('a,'b::order) merge_d program |
|
161 assumes |
|
162 Merge_spec "M : merge_spec" |
|
163 |
|
164 locale Distrib = |
|
165 fixes |
|
166 D :: ('a,'b::order) distr_d program |
|
167 assumes |
|
168 Distrib_spec "D : distr_spec" |
|
169 |
|
170 |
|
171 (**** |
|
172 # (** Network specification ***) |
|
173 |
|
174 # (*spec (9.1)*) |
|
175 # network_ask :: 'a systemState program set |
|
176 # "network_ask == INT i : lessThan Nclients. |
|
177 # Increasing (ask o sub i o client) |
|
178 # guarantees[ask] |
|
179 # (ask Fols (ask o sub i o client))" |
|
180 |
|
181 # (*spec (9.2)*) |
|
182 # network_giv :: 'a systemState program set |
|
183 # "network_giv == INT i : lessThan Nclients. |
|
184 # Increasing giv |
|
185 # guarantees[giv o sub i o client] |
|
186 # ((giv o sub i o client) Fols giv )" |
|
187 |
|
188 # (*spec (9.3)*) |
|
189 # network_rel :: 'a systemState program set |
|
190 # "network_rel == INT i : lessThan Nclients. |
|
191 # Increasing (rel o sub i o client) |
|
192 # guarantees[rel] |
|
193 # (rel Fols (rel o sub i o client))" |
|
194 |
|
195 # (*spec: preserves part*) |
|
196 # network_preserves :: 'a systemState program set |
|
197 # "network_preserves == preserves giv Int |
|
198 # (INT i : lessThan Nclients. |
|
199 # preserves (funPair rel ask o sub i o client))" |
|
200 |
|
201 # network_spec :: 'a systemState program set |
|
202 # "network_spec == network_ask Int network_giv Int |
|
203 # network_rel Int network_preserves" |
|
204 |
|
205 |
|
206 # (** State mappings **) |
|
207 # sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState" |
|
208 # "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s |
|
209 # in (| giv = giv s, |
|
210 # ask = ask s, |
|
211 # rel = rel s, |
|
212 # client = cl, |
|
213 # dummy = xtr|)" |
|
214 |
|
215 |
|
216 # sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState" |
|
217 # "sysOfClient == %(cl,al). (| giv = giv al, |
|
218 # ask = ask al, |
|
219 # rel = rel al, |
|
220 # client = cl, |
|
221 # systemState.dummy = allocState_d.dummy al|)" |
|
222 ****) |
|
223 |
|
224 end |
|