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 |
|
6827
|
13 |
Alloc = Follows + Extend + 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 |
|
|
35 |
record clientState =
|
|
36 |
giv :: nat list (*client's INPUT history: tokens GRANTED*)
|
|
37 |
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
|
|
38 |
rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
|
|
39 |
|
|
40 |
record allocState =
|
|
41 |
allocGiv :: nat => nat list (*allocator's local copy of "giv" for i*)
|
|
42 |
allocAsk :: nat => nat list (*allocator's local copy of "ask" for i*)
|
|
43 |
allocRel :: nat => nat list (*allocator's local copy of "rel" for i*)
|
|
44 |
|
|
45 |
record systemState = allocState +
|
|
46 |
client :: nat => clientState (*states of all clients*)
|
|
47 |
|
|
48 |
|
|
49 |
constdefs
|
|
50 |
|
|
51 |
(** Resource allocation system specification **)
|
|
52 |
|
|
53 |
(*spec (1)*)
|
|
54 |
system_safety :: systemState program set
|
|
55 |
"system_safety ==
|
|
56 |
Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients
|
|
57 |
<= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"
|
|
58 |
|
|
59 |
(*spec (2)*)
|
|
60 |
system_progress :: systemState program set
|
|
61 |
"system_progress == INT i : lessThan Nclients.
|
|
62 |
INT h.
|
|
63 |
{s. h <= (ask o sub i o client)s} LeadsTo
|
6827
|
64 |
{s. h pfixLe (giv o sub i o client) s}"
|
|
65 |
|
|
66 |
system_spec :: systemState program set
|
|
67 |
"system_spec == system_safety Int system_progress"
|
6815
|
68 |
|
|
69 |
(** Client specification (required) ***)
|
|
70 |
|
7347
|
71 |
(*spec (3) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
|
6815
|
72 |
client_increasing :: clientState program set
|
|
73 |
"client_increasing ==
|
7361
|
74 |
UNIV guarantees Increasing ask Int Increasing rel"
|
6815
|
75 |
|
|
76 |
(*spec (4)*)
|
|
77 |
client_bounded :: clientState program set
|
|
78 |
"client_bounded ==
|
7361
|
79 |
UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
|
6815
|
80 |
|
|
81 |
(*spec (5)*)
|
|
82 |
client_progress :: clientState program set
|
|
83 |
"client_progress ==
|
|
84 |
Increasing giv
|
7361
|
85 |
guarantees
|
6827
|
86 |
(INT h. {s. h <= giv s & h pfixGe ask s}
|
6815
|
87 |
LeadsTo
|
|
88 |
{s. tokens h <= (tokens o rel) s})"
|
|
89 |
|
6827
|
90 |
client_spec :: clientState program set
|
|
91 |
"client_spec == client_increasing Int client_bounded Int client_progress"
|
|
92 |
|
6815
|
93 |
(** Allocator specification (required) ***)
|
|
94 |
|
7347
|
95 |
(*spec (6) PROBABLY REQUIRES A LOCALTO PRECONDITION*)
|
6815
|
96 |
alloc_increasing :: allocState program set
|
|
97 |
"alloc_increasing ==
|
|
98 |
UNIV
|
7361
|
99 |
guarantees
|
6815
|
100 |
(INT i : lessThan Nclients. Increasing (sub i o allocAsk))"
|
|
101 |
|
|
102 |
(*spec (7)*)
|
|
103 |
alloc_safety :: allocState program set
|
|
104 |
"alloc_safety ==
|
|
105 |
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
|
7361
|
106 |
guarantees
|
6815
|
107 |
Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
|
|
108 |
<= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
|
|
109 |
|
|
110 |
(*spec (8)*)
|
|
111 |
alloc_progress :: allocState program set
|
|
112 |
"alloc_progress ==
|
|
113 |
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
|
|
114 |
Increasing (sub i o allocRel))
|
|
115 |
Int
|
|
116 |
Always {s. ALL i : lessThan Nclients.
|
|
117 |
ALL k : lessThan (length (allocAsk s i)).
|
|
118 |
allocAsk s i ! k <= NbT}
|
|
119 |
Int
|
|
120 |
(INT i : lessThan Nclients.
|
6827
|
121 |
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
|
6815
|
122 |
LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
|
7361
|
123 |
guarantees
|
6815
|
124 |
(INT i : lessThan Nclients.
|
|
125 |
INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
|
6827
|
126 |
{s. h pfixLe (sub i o allocGiv) s})"
|
|
127 |
|
|
128 |
alloc_spec :: allocState program set
|
|
129 |
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress"
|
6815
|
130 |
|
|
131 |
(** Network specification ***)
|
|
132 |
|
|
133 |
(*spec (9.1)*)
|
|
134 |
network_ask :: systemState program set
|
|
135 |
"network_ask == INT i : lessThan Nclients.
|
6827
|
136 |
Increasing (ask o sub i o client)
|
7361
|
137 |
guarantees
|
6815
|
138 |
((sub i o allocAsk) Fols (ask o sub i o client))"
|
|
139 |
|
|
140 |
(*spec (9.2)*)
|
|
141 |
network_giv :: systemState program set
|
|
142 |
"network_giv == INT i : lessThan Nclients.
|
6827
|
143 |
Increasing (sub i o allocGiv)
|
7361
|
144 |
guarantees
|
6815
|
145 |
((giv o sub i o client) Fols (sub i o allocGiv))"
|
|
146 |
|
|
147 |
(*spec (9.3)*)
|
|
148 |
network_rel :: systemState program set
|
|
149 |
"network_rel == INT i : lessThan Nclients.
|
6827
|
150 |
Increasing (rel o sub i o client)
|
7361
|
151 |
guarantees
|
6815
|
152 |
((sub i o allocRel) Fols (rel o sub i o client))"
|
|
153 |
|
6827
|
154 |
network_spec :: systemState program set
|
|
155 |
"network_spec == network_ask Int network_giv Int network_rel"
|
|
156 |
|
|
157 |
|
|
158 |
(** State mappings **)
|
|
159 |
sysOfAlloc :: "(allocState * (nat => clientState)) => systemState"
|
|
160 |
"sysOfAlloc == %(s,y). (| allocGiv = allocGiv s,
|
|
161 |
allocAsk = allocAsk s,
|
|
162 |
allocRel = allocRel s,
|
|
163 |
client = y |)"
|
6841
|
164 |
(*** "sysOfAlloc == %(s,y). s(|client := y|)" TYPE DOESN'T CHANGE***)
|
|
165 |
|
6827
|
166 |
|
|
167 |
sysOfClient :: "((nat => clientState) * allocState ) => systemState"
|
|
168 |
"sysOfClient == %(x,y). sysOfAlloc(y,x)"
|
|
169 |
|
|
170 |
|
|
171 |
locale System =
|
|
172 |
fixes
|
|
173 |
Alloc :: allocState program
|
|
174 |
Client :: clientState program
|
|
175 |
Network :: systemState program
|
|
176 |
System :: systemState program
|
|
177 |
|
|
178 |
assumes
|
|
179 |
Alloc "Alloc : alloc_spec"
|
|
180 |
Client "Client : client_spec"
|
|
181 |
Network "Network : network_spec"
|
|
182 |
|
|
183 |
defines
|
|
184 |
System_def
|
|
185 |
"System == (extend sysOfAlloc Alloc)
|
|
186 |
Join
|
6841
|
187 |
(extend sysOfClient (plam x: lessThan Nclients. Client))
|
6827
|
188 |
Join
|
|
189 |
Network"
|
6815
|
190 |
end
|