added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.
(* Title: HOL/UNITY/AllocImpl
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Implementation of a multiple-client allocator from a single-client allocator
*)
AllocImpl = AllocBase + Follows + PPROD +
(** State definitions. OUTPUT variables are locals **)
(*Type variable 'b is the type of items being merged*)
record 'b merge =
In :: nat => 'b list (*merge's INPUT histories: streams to merge*)
Out :: 'b list (*merge's OUTPUT history: merged items*)
iOut :: nat list (*merge's OUTPUT history: origins of merged items*)
record ('a,'b) merge_d =
'b merge +
dummy :: 'a (*dummy field for new variables*)
constdefs
non_dummy :: ('a,'b) merge_d => 'b merge
"non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
record 'b distr =
In :: 'b list (*items to distribute*)
iIn :: nat list (*destinations of items to distribute*)
Out :: nat => 'b list (*distributed items*)
record ('a,'b) distr_d =
'b distr +
dummy :: 'a (*dummy field for new variables*)
record allocState =
giv :: nat list (*OUTPUT history: source of tokens*)
ask :: nat list (*INPUT: tokens requested from allocator*)
rel :: nat list (*INPUT: tokens released to allocator*)
record 'a allocState_d =
allocState +
dummy :: 'a (*dummy field for new variables*)
record 'a systemState =
allocState +
mergeRel :: nat merge
mergeAsk :: nat merge
distr :: nat distr
dummy :: 'a (*dummy field for new variables*)
constdefs
(** Merge specification (the number of inputs is Nclients) ***)
(*spec (10)*)
merge_increasing :: ('a,'b) merge_d program set
"merge_increasing ==
UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
(*spec (11)*)
merge_eqOut :: ('a,'b) merge_d program set
"merge_eqOut ==
UNIV guarantees
Always {s. length (merge.Out s) = length (merge.iOut s)}"
(*spec (12)*)
merge_bounded :: ('a,'b) merge_d program set
"merge_bounded ==
UNIV guarantees
Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
(*spec (13)*)
merge_follows :: ('a,'b) merge_d program set
"merge_follows ==
(INT i : lessThan Nclients. Increasing (sub i o merge.In))
guarantees
(INT i : lessThan Nclients.
(%s. sublist (merge.Out s)
{k. k < size(merge.iOut s) & merge.iOut s! k = i})
Fols (sub i o merge.In))"
(*spec: preserves part*)
merge_preserves :: ('a,'b) merge_d program set
"merge_preserves == preserves merge.In Int preserves merge_d.dummy"
(*environmental constraints*)
merge_allowed_acts :: ('a,'b) merge_d program set
"merge_allowed_acts ==
{F. AllowedActs F =
insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
merge_spec :: ('a,'b) merge_d program set
"merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
merge_follows Int merge_allowed_acts Int merge_preserves"
(** Distributor specification (the number of outputs is Nclients) ***)
(*spec (14)*)
distr_follows :: ('a,'b) distr_d program set
"distr_follows ==
Increasing distr.In Int Increasing distr.iIn Int
Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
guarantees
(INT i : lessThan Nclients.
(sub i o distr.Out) Fols
(%s. sublist (distr.In s)
{k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
distr_allowed_acts :: ('a,'b) distr_d program set
"distr_allowed_acts ==
{D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
distr_spec :: ('a,'b) distr_d program set
"distr_spec == distr_follows Int distr_allowed_acts"
(** Single-client allocator specification (required) ***)
(*spec (18)*)
alloc_increasing :: 'a allocState_d program set
"alloc_increasing == UNIV guarantees Increasing giv"
(*spec (19)*)
alloc_safety :: 'a allocState_d program set
"alloc_safety ==
Increasing rel
guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
(*spec (20)*)
alloc_progress :: 'a allocState_d program set
"alloc_progress ==
Increasing ask Int Increasing rel Int
Always {s. ALL elt : set (ask s). elt <= NbT}
Int
(INT h. {s. h <= giv s & h pfixGe (ask s)}
LeadsTo
{s. tokens h <= tokens (rel s)})
guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
(*spec: preserves part*)
alloc_preserves :: 'a allocState_d program set
"alloc_preserves == preserves rel Int
preserves ask Int
preserves allocState_d.dummy"
(*environmental constraints*)
alloc_allowed_acts :: 'a allocState_d program set
"alloc_allowed_acts ==
{F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_allowed_acts Int alloc_preserves"
locale Merge =
fixes
M :: ('a,'b::order) merge_d program
assumes
Merge_spec "M : merge_spec"
locale Distrib =
fixes
D :: ('a,'b::order) distr_d program
assumes
Distrib_spec "D : distr_spec"
(****
# (** Network specification ***)
# (*spec (9.1)*)
# network_ask :: 'a systemState program set
# "network_ask == INT i : lessThan Nclients.
# Increasing (ask o sub i o client)
# guarantees[ask]
# (ask Fols (ask o sub i o client))"
# (*spec (9.2)*)
# network_giv :: 'a systemState program set
# "network_giv == INT i : lessThan Nclients.
# Increasing giv
# guarantees[giv o sub i o client]
# ((giv o sub i o client) Fols giv )"
# (*spec (9.3)*)
# network_rel :: 'a systemState program set
# "network_rel == INT i : lessThan Nclients.
# Increasing (rel o sub i o client)
# guarantees[rel]
# (rel Fols (rel o sub i o client))"
# (*spec: preserves part*)
# network_preserves :: 'a systemState program set
# "network_preserves == preserves giv Int
# (INT i : lessThan Nclients.
# preserves (funPair rel ask o sub i o client))"
# network_spec :: 'a systemState program set
# "network_spec == network_ask Int network_giv Int
# network_rel Int network_preserves"
# (** State mappings **)
# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
# in (| giv = giv s,
# ask = ask s,
# rel = rel s,
# client = cl,
# dummy = xtr|)"
# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
# "sysOfClient == %(cl,al). (| giv = giv al,
# ask = ask al,
# rel = rel al,
# client = cl,
# systemState.dummy = allocState_d.dummy al|)"
****)
end