# HG changeset patch
# User paulson
# Date 959963524 -7200
# Node ID daeccd9f885f87b8d59e9eb98cc7f967ff7d088b
# Parent  640c4fd8b5b35ba952b8392a53f3b8ef1cc93320
The Allocator Implementation (not yet working)

diff -r 640c4fd8b5b3 -r daeccd9f885f src/HOL/UNITY/AllocImpl.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocImpl.ML	Fri Jun 02 18:32:04 2000 +0200
@@ -0,0 +1,86 @@
+(*  Title:      HOL/UNITY/AllocImpl
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   2000  University of Cambridge
+
+Implementation of a multiple-client allocator from a single-client allocator
+
+add_path "../Induct";
+time_use_thy "AllocImpl";
+*)
+
+AddIs [impOfSubs subset_preserves_o];
+Addsimps [funPair_o_distrib];
+Addsimps [Always_INT_distrib];
+Delsimps [o_apply];
+
+(*Eliminate the "o" operator*)
+val o_simp = simplify (simpset() addsimps [o_def]);
+
+Goalw [merge_spec_def,merge_eqOut_def]
+     "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
+\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";  
+by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+qed "Merge_Always_Out_eq_iOut";
+
+
+Goal "M : merge_spec \
+\ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
+\             guarantees[funPair merge.Out merge.iOut]  \
+\                (bag_of o merge.Out) Fols \
+\                (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
+\                            (lessThan Nclients))";
+by (rtac guaranteesI 1);
+by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")] 
+                  Always_Follows 1);
+by (etac (Merge_Always_Out_eq_iOut RS Always_Compl_Un_eq RS iffD1) 1);
+by (force_tac (claset() addIs [UNIV_AlwaysI], simpset() addsimps [o_apply]) 3);
+by (Asm_full_simp_tac 1); 
+by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [sublist_upt_eq_take]
+                                 addsimps [bag_of_sublist]) 1); 
+by (rtac Follows_trans 1); 
+by (rtac Follows_setsum 2);
+by (asm_full_simp_tac (simpset() addsimps []) 3);
+by (Clarify_tac 2); 
+by (asm_full_simp_tac (simpset() addsimps [o_assoc RS sym]) 2); 
+by (rtac (impOfSubs (mono_bag_of RS mono_Follows_o)) 2);
+
+(*Now need to invoke the merge_follows guarantee*)
+ 
+by (asm_full_simp_tac (simpset() addsimps [merge_spec_def,merge_follows_def]) 2); 
+
+
+by (res_inst_tac [("f", "%s. bag_of (sublist (merge.Out s) {..length(merge.iOut s)(})")] 
+                  Always_Follows 1);
+
+setsum (%i. if i < length l then {# nth l i #} else {#}) {..length (iOut s)(}
+
+             : (%s. bag_of
+                     (sublist (merge.Out s) {..length (iOut s)(})) Fols
+               (%s. setsum (%i. (bag_of o sub i o merge.In) s)
+                     {..Nclients(})
+
+
+	  (%s. sublist (merge.Out s) 
+                       {k. k < size(merge.iOut s) & nth(merge.iOut s)k = i})
+	  Fols (sub i o merge.In))"
+
+
+by Auto_tac;
+by (dtac guaranteesD 1);
+by Auto_tac;
+by (rtac guaranteesI 1);
+
+merge_eqOut
+
+Always_Int_eq
+
+
+by (simp_tac (simpset() addsimps [o_def]) 1);
+by (subgoal_tac
+    "ALL s. merge.Out s = sublist (merge.Out s) {..length(merge.iOut s)(}" 1);
+by (etac ssubst 1);
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist]) 1);
+by (stac bag_of_sublist 1);
+
diff -r 640c4fd8b5b3 -r daeccd9f885f src/HOL/UNITY/AllocImpl.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/AllocImpl.thy	Fri Jun 02 18:32:04 2000 +0200
@@ -0,0 +1,213 @@
+(*  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
+
+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)}
+		 LeadsTo
+	         {s. tokens h <= tokens (rel s)})
+         guarantees[giv]
+	     (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+
+  (*spec: preserves part*)
+    alloc_preserves :: 'a allocState_u program set
+    "alloc_preserves == preserves (funPair rel
+				   (funPair ask allocState_u.extra))"
+  
+  alloc_spec :: 'a allocState_u program set
+    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+                   alloc_preserves"
+
+(****
+    (** 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_u => 'a systemState"
+	"sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+			   in (| giv = giv s,
+				 ask = ask s,
+				 rel = rel s,
+				 client   = cl,
+				 extra    = xtr|)"
+
+
+      sysOfClient :: "(nat => merge) * 'a allocState_u => 'a systemState"
+	"sysOfClient == %(cl,al). (| giv = giv al,
+				     ask = ask al,
+				     rel = rel al,
+				     client   = cl,
+				     systemState.extra = allocState_u.extra al|)"
+****)
+
+consts 
+    Alloc  :: 'a allocState_u program
+    Merge  :: ('a,'b) merge_u program
+(*    
+    Network :: 'a systemState program
+    System  :: 'a systemState program
+  *)
+  
+rules
+    Alloc   "Alloc   : alloc_spec"
+    Merge  "Merge  : merge_spec"
+(**    Network "Network : network_spec"**)
+
+
+
+(**
+defs
+    System_def
+      "System == rename sysOfAlloc Alloc Join Network Join
+                 (rename sysOfMerge
+		  (plam x: lessThan Nclients. rename merge_map Merge))"
+**)
+
+
+end