<commit_before>(*  Title:      HOL/UNITY/AllocImpl
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Implementation of a multiple-client allocator from a single-client allocator

add_path "../Induct";
with_path "../Induct" time_use_thy "AllocImpl";
*)

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_u =
  'b merge +
  extra :: 'a       (*dummy field for new variables*)

constdefs
  non_extra :: ('a,'b) merge_u => 'b merge
    "non_extra 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_u =
  'b distr +
  extra :: '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_u =
  allocState +
  extra    :: 'a                (*dummy field for new variables*)

record 'a systemState =
  allocState +
  mergeRel :: nat merge
  mergeAsk :: nat merge
  distr    :: nat distr
  extra    :: 'a                  (*dummy field for new variables*)


constdefs

(** Merge specification (NbT is the number of inputs) ***)

  (*spec (10)*)
  merge_increasing :: ('a,'b) merge_u program set
    "merge_increasing ==
         UNIV guarantees[funPair merge.Out merge.iOut]
         (Increasing merge.Out) Int (Increasing merge.iOut)"

  (*spec (11)*)
  merge_eqOut :: ('a,'b) merge_u program set
    "merge_eqOut ==
         UNIV guarantees[funPair merge.Out merge.iOut]
         Always {s. length (merge.Out s) = length (merge.iOut s)}"

  (*spec (12)*)
  merge_bounded :: ('a,'b) merge_u program set
    "merge_bounded ==
         UNIV guarantees[merge.iOut]
         Always {s. ALL elt : set (merge.iOut s). elt <= NbT}"

  (*spec (13)*)
  merge_follows :: ('a,'b) merge_u program set
    "merge_follows ==
	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
	 guarantees[funPair merge.Out merge.iOut]
	 (INT i : lessThan Nclients. 
	  (%s. sublist (merge.Out s) 
                       {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
	  Fols (sub i o merge.In))"

(*
	  (%s. map fst (filter (%p. snd p = i)
			(zip (merge.Out s) (merge.iOut s))))
	  Fols (sub i o merge.In)
*)

  (*spec: preserves part*)
    merge_preserves :: ('a,'b) merge_u program set
    "merge_preserves == preserves (funPair merge.In merge_u.extra)"

  merge_spec :: ('a,'b) merge_u program set
    "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                   merge_follows Int merge_preserves"

(** Single-client allocator specification (required) ***)

  (*spec (18)*)
  alloc_increasing :: 'a allocState_u program set
    "alloc_increasing == UNIV guarantees[giv] Increasing giv"

  (*spec (19)*)
  alloc_safety :: 'a allocState_u program set
    "alloc_safety ==
	 Increasing rel
         guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"

  (*spec (20)*)
  alloc_progress :: 'a allocState_u 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)}<commit_msg>fixed the merge spec (NbT -> Nclients) and added the distributor spec<commit_after>(*  Title:      HOL/UNITY/AllocImpl
    ID:         $Id$
    Author:     <NAME>, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Implementation of a multiple-client allocator from a single-client allocator

add_path "../Induct";
with_path "../Induct" time_use_thy "AllocImpl";
*)

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_u =
  'b merge +
  extra :: 'a       (*dummy field for new variables*)

constdefs
  non_extra :: ('a,'b) merge_u => 'b merge
    "non_extra 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_u =
  'b distr +
  extra :: '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_u =
  allocState +
  extra    :: 'a                (*dummy field for new variables*)

record 'a systemState =
  allocState +
  mergeRel :: nat merge
  mergeAsk :: nat merge
  distr    :: nat distr
  extra    :: 'a                  (*dummy field for new variables*)


constdefs

(** Merge specification (the number of inputs is Nclients) ***)

  (*spec (10)*)
  merge_increasing :: ('a,'b) merge_u program set
    "merge_increasing ==
         UNIV guarantees[funPair merge.Out merge.iOut]
         (Increasing merge.Out) Int (Increasing merge.iOut)"

  (*spec (11)*)
  merge_eqOut :: ('a,'b) merge_u program set
    "merge_eqOut ==
         UNIV guarantees[funPair merge.Out merge.iOut]
         Always {s. length (merge.Out s) = length (merge.iOut s)}"

  (*spec (12)*)
  merge_bounded :: ('a,'b) merge_u program set
    "merge_bounded ==
         UNIV guarantees[merge.iOut]
         Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"

  (*spec (13)*)
  merge_follows :: ('a,'b) merge_u program set
    "merge_follows ==
	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
	 guarantees[funPair merge.Out merge.iOut]
	 (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_u program set
    "merge_preserves == preserves (funPair merge.In merge_u.extra)"

  merge_spec :: ('a,'b) merge_u program set
    "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                   merge_follows Int merge_preserves"

(** Distributor specification (the number of outputs is Nclients) ***)

  (*spec (14)*)
  distr_follows :: ('a,'b) distr_u program set
    "distr_follows ==
	 Increasing distr.In Int Increasing distr.iIn Int
	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
	 guarantees[distr.Out]
	 (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}))"


(** Single-client allocator specification (required) ***)

  (*spec (18)*)
  alloc_increasing :: 'a allocState_u program set
    "alloc_increasing == UNIV guarantees[giv] Increasing giv"

  (*spec (19)*)
  alloc_safety :: 'a allocState_u program set
    "alloc_safety ==
	 Increasing rel
         guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"

  (*spec (20)*)
  alloc_progress :: 'a allocState_u 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)}
{'fraction_non_alphanumeric': 0.1285678517776665, 'fraction_numerical': 0.004757135703555333, 'mean_word_length': 2.824317855433222, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 12, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6931077', 'n_tokens_mistral': 2736, 'n_tokens_neox': 2562, 'n_words': 893}