author | paulson |
Wed, 15 Dec 1999 10:45:37 +0100 | |
changeset 8065 | 658e0d4e4ed9 |
parent 8055 | bb15396278fb |
child 8069 | 19b9f92ca503 |
permissions | -rw-r--r-- |
6815 | 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 |
|
7537 | 7 |
|
8 |
CONSIDER CHANGING "sum" to work on type "int", not "nat" |
|
9 |
--then can use subtraction in spec (1), |
|
10 |
--but need invariants that values are non-negative |
|
6815 | 11 |
*) |
12 |
||
8041 | 13 |
Alloc = Follows + PPROD + |
6815 | 14 |
|
15 |
(*Duplicated from HOL/ex/NatSum.thy. |
|
16 |
Maybe type should be [nat=>int, nat] => int**) |
|
17 |
consts sum :: [nat=>nat, nat] => nat |
|
18 |
primrec |
|
19 |
"sum f 0 = 0" |
|
20 |
"sum f (Suc n) = f(n) + sum f n" |
|
21 |
||
22 |
||
23 |
(*This function merely sums the elements of a list*) |
|
24 |
consts tokens :: nat list => nat |
|
25 |
primrec |
|
26 |
"tokens [] = 0" |
|
27 |
"tokens (x#xs) = x + tokens xs" |
|
28 |
||
29 |
||
30 |
consts |
|
31 |
NbT :: nat (*Number of tokens in system*) |
|
32 |
Nclients :: nat (*Number of clients*) |
|
33 |
||
34 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
35 |
(** State definitions. OUTPUT variables are locals **) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
36 |
|
6815 | 37 |
record clientState = |
38 |
giv :: nat list (*client's INPUT history: tokens GRANTED*) |
|
39 |
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*) |
|
40 |
rel :: nat list (*client's OUTPUT history: tokens RELEASED*) |
|
41 |
||
42 |
record allocState = |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
43 |
allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
44 |
allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*) |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
45 |
allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*) |
6815 | 46 |
|
47 |
record systemState = allocState + |
|
48 |
client :: nat => clientState (*states of all clients*) |
|
49 |
||
50 |
||
51 |
constdefs |
|
52 |
||
53 |
(** Resource allocation system specification **) |
|
54 |
||
55 |
(*spec (1)*) |
|
56 |
system_safety :: systemState program set |
|
57 |
"system_safety == |
|
58 |
Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients |
|
59 |
<= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}" |
|
60 |
||
61 |
(*spec (2)*) |
|
62 |
system_progress :: systemState program set |
|
63 |
"system_progress == INT i : lessThan Nclients. |
|
64 |
INT h. |
|
65 |
{s. h <= (ask o sub i o client)s} LeadsTo |
|
6827 | 66 |
{s. h pfixLe (giv o sub i o client) s}" |
67 |
||
68 |
system_spec :: systemState program set |
|
69 |
"system_spec == system_safety Int system_progress" |
|
6815 | 70 |
|
71 |
(** Client specification (required) ***) |
|
72 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
73 |
(*spec (3)*) |
6815 | 74 |
client_increasing :: clientState program set |
75 |
"client_increasing == |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
76 |
UNIV guarantees[funPair rel ask] |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
77 |
Increasing ask Int Increasing rel" |
6815 | 78 |
|
79 |
(*spec (4)*) |
|
80 |
client_bounded :: clientState program set |
|
81 |
"client_bounded == |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
82 |
UNIV guarantees[ask] |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
83 |
Always {s. ALL elt : set (ask s). elt <= NbT}" |
6815 | 84 |
|
85 |
(*spec (5)*) |
|
86 |
client_progress :: clientState program set |
|
87 |
"client_progress == |
|
88 |
Increasing giv |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
89 |
guarantees[funPair rel ask] |
6827 | 90 |
(INT h. {s. h <= giv s & h pfixGe ask s} |
8041 | 91 |
LeadsTo[givenBy (funPair rel ask)] |
6815 | 92 |
{s. tokens h <= (tokens o rel) s})" |
93 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
94 |
(*spec: preserves part*) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
95 |
client_preserves :: clientState program set |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
96 |
"client_preserves == preserves giv" |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
97 |
|
6827 | 98 |
client_spec :: clientState program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
99 |
"client_spec == client_increasing Int client_bounded Int client_progress |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
100 |
Int client_preserves" |
6827 | 101 |
|
6815 | 102 |
(** Allocator specification (required) ***) |
103 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
104 |
(*spec (6)*) |
6815 | 105 |
alloc_increasing :: allocState program set |
106 |
"alloc_increasing == |
|
107 |
UNIV |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
108 |
guarantees[allocGiv] |
7540 | 109 |
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))" |
6815 | 110 |
|
111 |
(*spec (7)*) |
|
112 |
alloc_safety :: allocState program set |
|
113 |
"alloc_safety == |
|
114 |
(INT i : lessThan Nclients. Increasing (sub i o allocRel)) |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
115 |
guarantees[allocGiv] |
6815 | 116 |
Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients |
117 |
<= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}" |
|
118 |
||
119 |
(*spec (8)*) |
|
120 |
alloc_progress :: allocState program set |
|
121 |
"alloc_progress == |
|
122 |
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int |
|
123 |
Increasing (sub i o allocRel)) |
|
124 |
Int |
|
125 |
Always {s. ALL i : lessThan Nclients. |
|
126 |
ALL k : lessThan (length (allocAsk s i)). |
|
127 |
allocAsk s i ! k <= NbT} |
|
128 |
Int |
|
129 |
(INT i : lessThan Nclients. |
|
6827 | 130 |
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} |
6815 | 131 |
LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
132 |
guarantees[allocGiv] |
6815 | 133 |
(INT i : lessThan Nclients. |
134 |
INT h. {s. h <= (sub i o allocAsk) s} LeadsTo |
|
6827 | 135 |
{s. h pfixLe (sub i o allocGiv) s})" |
136 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
137 |
(*spec: preserves part*) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
138 |
alloc_preserves :: allocState program set |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
139 |
"alloc_preserves == preserves (funPair allocRel allocAsk)" |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
140 |
|
6827 | 141 |
alloc_spec :: allocState program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
142 |
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
143 |
alloc_preserves" |
6815 | 144 |
|
145 |
(** Network specification ***) |
|
146 |
||
147 |
(*spec (9.1)*) |
|
148 |
network_ask :: systemState program set |
|
149 |
"network_ask == INT i : lessThan Nclients. |
|
6827 | 150 |
Increasing (ask o sub i o client) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
151 |
guarantees[allocAsk] |
6815 | 152 |
((sub i o allocAsk) Fols (ask o sub i o client))" |
153 |
||
154 |
(*spec (9.2)*) |
|
155 |
network_giv :: systemState program set |
|
156 |
"network_giv == INT i : lessThan Nclients. |
|
6827 | 157 |
Increasing (sub i o allocGiv) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
158 |
guarantees[giv o sub i o client] |
6815 | 159 |
((giv o sub i o client) Fols (sub i o allocGiv))" |
160 |
||
161 |
(*spec (9.3)*) |
|
162 |
network_rel :: systemState program set |
|
163 |
"network_rel == INT i : lessThan Nclients. |
|
6827 | 164 |
Increasing (rel o sub i o client) |
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
8041
diff
changeset
|
165 |
guarantees[allocRel] |
6815 | 166 |
((sub i o allocRel) Fols (rel o sub i o client))" |
167 |
||
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
168 |
(*spec: preserves part*) |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
169 |
network_preserves :: systemState program set |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
170 |
"network_preserves == preserves allocGiv |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
171 |
Int |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
172 |
(INT i : lessThan Nclients. |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
173 |
preserves (funPair rel ask o sub i o client))" |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
174 |
|
6827 | 175 |
network_spec :: systemState program set |
8065
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
176 |
"network_spec == network_ask Int network_giv Int |
658e0d4e4ed9
first working version to Alloc/System_Client_Progress;
paulson
parents:
8055
diff
changeset
|
177 |
network_rel Int network_preserves" |
6827 | 178 |
|
179 |
||
180 |
(** State mappings **) |
|
181 |
sysOfAlloc :: "(allocState * (nat => clientState)) => systemState" |
|
182 |
"sysOfAlloc == %(s,y). (| allocGiv = allocGiv s, |
|
183 |
allocAsk = allocAsk s, |
|
184 |
allocRel = allocRel s, |
|
185 |
client = y |)" |
|
186 |
||
187 |
sysOfClient :: "((nat => clientState) * allocState ) => systemState" |
|
188 |
"sysOfClient == %(x,y). sysOfAlloc(y,x)" |
|
189 |
||
190 |
||
191 |
locale System = |
|
192 |
fixes |
|
193 |
Alloc :: allocState program |
|
194 |
Client :: clientState program |
|
195 |
Network :: systemState program |
|
196 |
System :: systemState program |
|
197 |
||
198 |
assumes |
|
199 |
Alloc "Alloc : alloc_spec" |
|
200 |
Client "Client : client_spec" |
|
201 |
Network "Network : network_spec" |
|
202 |
||
203 |
defines |
|
204 |
System_def |
|
205 |
"System == (extend sysOfAlloc Alloc) |
|
206 |
Join |
|
6841 | 207 |
(extend sysOfClient (plam x: lessThan Nclients. Client)) |
6827 | 208 |
Join |
209 |
Network" |
|
6815 | 210 |
end |