# Theory Alloc

Up to index of Isabelle/HOL/UNITY

theory Alloc
imports AllocBase PPROD
uses [Alloc.ML]
begin

    (*  Title:      HOL/UNITY/Alloc
        ID:         $Id: Alloc.thy,v 1.4 2005/09/07 19:00:30 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1998  University of Cambridge

    Specification of Chandy and Charpentier's Allocator
    *)

    theory Alloc
    imports AllocBase PPROD
    begin

    (** State definitions.  OUTPUT variables are locals **)

    record clientState =
      giv :: "nat list"   (*client's INPUT history:  tokens GRANTED*)
      ask :: "nat list"   (*client's OUTPUT history: tokens REQUESTED*)
      rel :: "nat list"   (*client's OUTPUT history: tokens RELEASED*)

    record 'a clientState_d =
      clientState +
      dummy :: 'a       (*dummy field for new variables*)

    constdefs
      (*DUPLICATED FROM Client.thy, but with "tok" removed*)
      (*Maybe want a special theory section to declare such maps*)
      non_dummy :: "'a clientState_d => clientState"
        "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"

      (*Renaming map to put a Client into the standard form*)
      client_map :: "'a clientState_d => clientState*'a"
        "client_map == funPair non_dummy dummy"

    record allocState =
      allocGiv :: "nat => nat list"   (*OUTPUT history: source of "giv" for i*)
      allocAsk :: "nat => nat list"   (*INPUT: allocator's copy of "ask" for i*)
      allocRel :: "nat => nat list"   (*INPUT: allocator's copy of "rel" for i*)

    record 'a allocState_d =
      allocState +
      dummy    :: 'a                (*dummy field for new variables*)

    record 'a systemState =
      allocState +
      client :: "nat => clientState"  (*states of all clients*)
      dummy  :: 'a                    (*dummy field for new variables*)

    constdefs

    (** Resource allocation system specification **)

      (*spec (1)*)
      system_safety :: "'a systemState program set"
        "system_safety ==
         Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
         <= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"

      (*spec (2)*)
      system_progress :: "'a systemState program set"
        "system_progress == INT i : lessThan Nclients.
                            INT h.
                              {s. h <= (ask o sub i o client)s} LeadsTo
                              {s. h pfixLe (giv o sub i o client) s}"

      system_spec :: "'a systemState program set"
        "system_spec == system_safety Int system_progress"

    (** Client specification (required) ***)

      (*spec (3)*)
      client_increasing :: "'a clientState_d program set"
        "client_increasing ==
             UNIV guarantees  Increasing ask Int Increasing rel"

      (*spec (4)*)
      client_bounded :: "'a clientState_d program set"
        "client_bounded ==
             UNIV guarantees  Always {s. ALL elt : set (ask s). elt <= NbT}"

      (*spec (5)*)
      client_progress :: "'a clientState_d program set"
        "client_progress ==
             Increasing giv  guarantees
             (INT h. {s. h <= giv s & h pfixGe ask s}
                     LeadsTo {s. tokens h <= (tokens o rel) s})"

      (*spec: preserves part*)
      client_preserves :: "'a clientState_d program set"
        "client_preserves == preserves giv Int preserves clientState_d.dummy"

      (*environmental constraints*)
      client_allowed_acts :: "'a clientState_d program set"
        "client_allowed_acts ==
           {F. AllowedActs F =
                insert Id (UNION (preserves (funPair rel ask)) Acts)}"

      client_spec :: "'a clientState_d program set"
        "client_spec == client_increasing Int client_bounded Int client_progress
                        Int client_allowed_acts Int client_preserves"

    (** Allocator specification (required) ***)

      (*spec (6)*)
      alloc_increasing :: "'a allocState_d program set"
        "alloc_increasing ==
             UNIV  guarantees
             (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"

      (*spec (7)*)
      alloc_safety :: "'a allocState_d program set"
        "alloc_safety ==
             (INT i : lessThan Nclients. Increasing (sub i o allocRel))
             guarantees
             Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
             <= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"

      (*spec (8)*)
      alloc_progress :: "'a allocState_d program set"
        "alloc_progress ==
             (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
                                         Increasing (sub i o allocRel))
             Int
             Always {s. ALL i<Nclients.
                         ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
             Int
             (INT i : lessThan Nclients.
              INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
                     LeadsTo
                     {s. tokens h <= (tokens o sub i o allocRel)s})
             guarantees
                 (INT i : lessThan Nclients.
                  INT h. {s. h <= (sub i o allocAsk) s}
                         LeadsTo
                         {s. h pfixLe (sub i o allocGiv) s})"

      (*NOTE: to follow the original paper, the formula above should have had
            INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
                   LeadsTo
                   {s. tokens h i <= (tokens o sub i o allocRel)s})
        thus h should have been a function variable.  However, only h i is ever
        looked at.*)

      (*spec: preserves part*)
      alloc_preserves :: "'a allocState_d program set"
        "alloc_preserves == preserves allocRel Int preserves allocAsk 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 allocGiv) 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"

    (** 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
                            ((sub i o allocAsk) Fols (ask o sub i o client))"

      (*spec (9.2)*)
      network_giv :: "'a systemState program set"
        "network_giv == INT i : lessThan Nclients.
                            Increasing (sub i o allocGiv)
                            guarantees
                            ((giv o sub i o client) Fols (sub i o allocGiv))"

      (*spec (9.3)*)
      network_rel :: "'a systemState program set"
        "network_rel == INT i : lessThan Nclients.
                            Increasing (rel o sub i o client)
                            guarantees
                            ((sub i o allocRel) Fols (rel o sub i o client))"

      (*spec: preserves part*)
      network_preserves :: "'a systemState program set"
        "network_preserves ==
           preserves allocGiv  Int
           (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
                                       preserves (ask o sub i o client))"

      (*environmental constraints*)
      network_allowed_acts :: "'a systemState program set"
        "network_allowed_acts ==
           {F. AllowedActs F =
               insert Id
                (UNION (preserves allocRel Int
                        (INT i: lessThan Nclients. preserves(giv o sub i o client)))
                      Acts)}"

      network_spec :: "'a systemState program set"
        "network_spec == network_ask Int network_giv Int
                         network_rel Int network_allowed_acts Int
                         network_preserves"

    (** State mappings **)
      sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
        "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
                           in (| allocGiv = allocGiv s,
                                 allocAsk = allocAsk s,
                                 allocRel = allocRel s,
                                 client   = cl,
                                 dummy    = xtr|)"

      sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
        "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
                                     allocAsk = allocAsk al,
                                     allocRel = allocRel al,
                                     client   = cl,
                                     systemState.dummy = allocState_d.dummy al|)"

    consts
        Alloc   :: "'a allocState_d program"
        Client  :: "'a clientState_d program"
        Network :: "'a systemState program"
        System  :: "'a systemState program"

    axioms
        Alloc:   "Alloc   : alloc_spec"
        Client:  "Client  : client_spec"
        Network: "Network : network_spec"

    defs
        System_def:
          "System == rename sysOfAlloc Alloc Join Network Join
                     (rename sysOfClient
                      (plam x: lessThan Nclients. rename client_map Client))"

    (**
    locale System =
      fixes
        Alloc   :: 'a allocState_d program
        Client  :: 'a clientState_d program
        Network :: 'a systemState program
        System  :: 'a systemState program

      assumes
        Alloc   "Alloc   : alloc_spec"
        Client  "Client  : client_spec"
        Network "Network : network_spec"

      defines
        System_def
          "System == rename sysOfAlloc Alloc
                     Join
                     Network
                     Join
                     (rename sysOfClient
                      (plam x: lessThan Nclients. rename client_map Client))"
    **)

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem inj_sysOfAlloc:

      inj sysOfAlloc

theorem inv_sysOfAlloc_eq:

      inv sysOfAlloc s =
      (| allocGiv = allocGiv s, allocAsk = allocAsk s, allocRel = allocRel s,
         allocState_d.dummy = (client s, systemState.dummy s) |)

theorem surj_sysOfAlloc:

      surj sysOfAlloc

theorem bij_sysOfAlloc:

      bij sysOfAlloc

theorem inj_sysOfClient:

      inj sysOfClient

theorem inv_sysOfClient_eq:

      inv sysOfClient s =
      (client s,
       (| allocGiv = allocGiv s, allocAsk = allocAsk s, allocRel = allocRel s,
          allocState_d.dummy = systemState.dummy s |))

theorem surj_sysOfClient:

      surj sysOfClient

theorem bij_sysOfClient:

      bij sysOfClient

theorem inj_client_map:

      inj client_map

theorem inv_client_map_eq:

      inv client_map s =
      (%(x, y). (| giv = giv x, ask = ask x, rel = rel x, clientState_d.dummy = y |))
       s

theorem surj_client_map:

      surj client_map

theorem bij_client_map:

      bij client_map

theorem fst_o_client_map:

      fst o client_map = non_dummy

theorem snd_o_client_map:

      snd o client_map = clientState_d.dummy

theorem client_o_sysOfAlloc:

      client o sysOfAlloc = fst o allocState_d.dummy

theorem allocGiv_o_sysOfAlloc_eq:

      allocGiv o sysOfAlloc = allocGiv

theorem allocAsk_o_sysOfAlloc_eq:

      allocAsk o sysOfAlloc = allocAsk

theorem allocRel_o_sysOfAlloc_eq:

      allocRel o sysOfAlloc = allocRel

theorem client_o_sysOfClient:

      client o sysOfClient = fst

theorem allocGiv_o_sysOfClient_eq:

      allocGiv o sysOfClient = allocGiv o snd

theorem allocAsk_o_sysOfClient_eq:

      allocAsk o sysOfClient = allocAsk o snd

theorem allocRel_o_sysOfClient_eq:

      allocRel o sysOfClient = allocRel o snd

theorem allocGiv_o_inv_sysOfAlloc_eq:

      allocGiv o inv sysOfAlloc = allocGiv

theorem allocAsk_o_inv_sysOfAlloc_eq:

      allocAsk o inv sysOfAlloc = allocAsk

theorem allocRel_o_inv_sysOfAlloc_eq:

      allocRel o inv sysOfAlloc = allocRel

theorem rel_inv_client_map_drop_map:

      rel o inv client_map o drop_map i o inv sysOfClient = rel o sub i o client

theorem ask_inv_client_map_drop_map:

      ask o inv client_map o drop_map i o inv sysOfClient = ask o sub i o client

theorem Network_component_System:

      Network Join
      (rename sysOfClient (plam x:{..<Nclients}. rename client_map Client) Join
       rename sysOfAlloc Alloc) =
      System

theorem Client_component_System:

      rename sysOfClient (plam x:{..<Nclients}. rename client_map Client) Join
      (Network Join rename sysOfAlloc Alloc) =
      System

theorem Alloc_component_System:

      rename sysOfAlloc Alloc Join
      (rename sysOfClient (plam x:{..<Nclients}. rename client_map Client) Join
       Network) =
      System

theorem Client_Allowed:

      Allowed Client = preserves rel ∩ preserves ask

theorem Network_Allowed:

      Allowed Network =
      preserves allocRel ∩ (INT i<Nclients. preserves (giv o sub i o client))

theorem Alloc_Allowed:

      Allowed Alloc = preserves allocGiv

theorem OK_lift_rename_Client:

      OK I (%i. lift i (rename client_map Client))