src/HOL/TLA/Memory/MemoryImplementation.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 9517 f58863b1406a
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        MemoryImplementation.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: MemoryImplementation
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: Memory implementation
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@6255
    12
MemoryImplementation = Memory + RPC + MemClerk + Datatype +
wenzelm@6255
    13
wenzelm@6255
    14
datatype  histState  =  histA | histB
wenzelm@3807
    15
wenzelm@3807
    16
types
wenzelm@3807
    17
  histType  = "(PrIds => histState) stfun"     (* the type of the history variable *)
wenzelm@3807
    18
wenzelm@3807
    19
consts
wenzelm@3807
    20
  (* the specification *)
wenzelm@3807
    21
     (* channel (external) *)
wenzelm@3807
    22
  memCh         :: "memChType"
wenzelm@3807
    23
     (* internal variables *)
wenzelm@6255
    24
  mm            :: "memType"
wenzelm@3807
    25
  
wenzelm@3807
    26
  (* the state variables of the implementation *)
wenzelm@3807
    27
     (* channels *)
wenzelm@3807
    28
  (* same interface channel memCh *)
wenzelm@3807
    29
  crCh          :: "rpcSndChType"
wenzelm@3807
    30
  rmCh          :: "rpcRcvChType"
wenzelm@3807
    31
     (* internal variables *)
wenzelm@6255
    32
  (* identity refinement mapping for mm -- simply reused *)
wenzelm@3807
    33
  rst           :: "rpcStType"
wenzelm@3807
    34
  cst           :: "mClkStType"
wenzelm@3807
    35
  ires          :: "resType"
wenzelm@3807
    36
(* the history variable : not defined as a constant
wenzelm@3807
    37
  rmhist        :: "histType"
wenzelm@3807
    38
*)
wenzelm@3807
    39
wenzelm@6255
    40
constdefs
wenzelm@6255
    41
  (* auxiliary predicates *)
wenzelm@6255
    42
  MVOKBARF      :: "Vals => bool"
wenzelm@6255
    43
     "MVOKBARF v == (v : MemVal) | (v = OK) | (v = BadArg) | (v = RPCFailure)"
wenzelm@6255
    44
  MVOKBA        :: "Vals => bool"
wenzelm@6255
    45
     "MVOKBA v   == (v : MemVal) | (v = OK) | (v = BadArg)"
wenzelm@6255
    46
  MVNROKBA      :: "Vals => bool"
wenzelm@6255
    47
     "MVNROKBA v == (v : MemVal) | (v = NotAResult) | (v = OK) | (v = BadArg)"
wenzelm@6255
    48
wenzelm@6255
    49
  (* tuples of state functions changed by the various components *)
wenzelm@6255
    50
  e             :: "PrIds => (bit * memOp) stfun"
wenzelm@6255
    51
     "e p == PRED (caller memCh!p)"
wenzelm@6255
    52
  c             :: "PrIds => (mClkState * (bit * Vals) * (bit * rpcOp)) stfun"
wenzelm@6255
    53
     "c p == PRED (cst!p, rtrner memCh!p, caller crCh!p)"
wenzelm@6255
    54
  r             :: "PrIds => (rpcState * (bit * Vals) * (bit * memOp)) stfun"
wenzelm@6255
    55
     "r p == PRED (rst!p, rtrner crCh!p, caller rmCh!p)"
wenzelm@6255
    56
  m             :: "PrIds => ((bit * Vals) * Vals) stfun"
wenzelm@6255
    57
     "m p == PRED (rtrner rmCh!p, ires!p)"
wenzelm@6255
    58
wenzelm@3807
    59
  (* the environment action *)
wenzelm@3807
    60
  ENext         :: "PrIds => action"
wenzelm@6255
    61
     "ENext p == ACT (? l. #l : #MemLoc & Call memCh p #(read l))"
wenzelm@6255
    62
wenzelm@3807
    63
wenzelm@3807
    64
  (* specification of the history variable *)
wenzelm@3807
    65
  HInit         :: "histType => PrIds => stpred"
wenzelm@6255
    66
     "HInit rmhist p == PRED rmhist!p = #histA"
wenzelm@6255
    67
wenzelm@3807
    68
  HNext         :: "histType => PrIds => action"
wenzelm@6255
    69
     "HNext rmhist p == ACT (rmhist!p)$ =
wenzelm@6255
    70
                     (if (MemReturn rmCh ires p | RPCFail crCh rmCh rst p)
wenzelm@6255
    71
                      then #histB
wenzelm@6255
    72
                      else if (MClkReply memCh crCh cst p)
wenzelm@6255
    73
                           then #histA
wenzelm@6255
    74
                           else $(rmhist!p))"
wenzelm@6255
    75
wenzelm@3807
    76
  HistP         :: "histType => PrIds => temporal"
wenzelm@6255
    77
     "HistP rmhist p == TEMP Init HInit rmhist p
wenzelm@6255
    78
                           & [][HNext rmhist p]_(c p,r p,m p, rmhist!p)"
wenzelm@6255
    79
wenzelm@3807
    80
  Hist          :: "histType => temporal"
wenzelm@6255
    81
      "Hist rmhist == TEMP (!p. HistP rmhist p)"
wenzelm@3807
    82
wenzelm@3807
    83
  (* the implementation *)
wenzelm@6255
    84
  IPImp          :: "PrIds => temporal"
wenzelm@6255
    85
     "IPImp p == TEMP (  Init ~Calling memCh p & [][ENext p]_(e p)
wenzelm@6255
    86
	               & MClkIPSpec memCh crCh cst p
wenzelm@6255
    87
  	               & RPCIPSpec crCh rmCh rst p
wenzelm@6255
    88
	               & RPSpec rmCh mm ires p
wenzelm@6255
    89
		       & (! l. #l : #MemLoc --> MSpec rmCh mm ires l))"
wenzelm@6255
    90
wenzelm@3807
    91
  ImpInit        :: "PrIds => stpred"
wenzelm@6255
    92
      "ImpInit p == PRED (  ~Calling memCh p
wenzelm@6255
    93
                          & MClkInit crCh cst p
wenzelm@6255
    94
	                  & RPCInit rmCh rst p
wenzelm@6255
    95
	                  & PInit ires p)"
wenzelm@6255
    96
wenzelm@3807
    97
  ImpNext        :: "PrIds => action"
wenzelm@6255
    98
      "ImpNext p == ACT  [ENext p]_(e p) 
wenzelm@6255
    99
                       & [MClkNext memCh crCh cst p]_(c p)
wenzelm@6255
   100
                       & [RPCNext crCh rmCh rst p]_(r p) 
wenzelm@6255
   101
                       & [RNext rmCh mm ires p]_(m p)"
wenzelm@6255
   102
wenzelm@3807
   103
  ImpLive        :: "PrIds => temporal"
wenzelm@6255
   104
      "ImpLive p == TEMP  WF(MClkFwd memCh crCh cst p)_(c p) 
wenzelm@6255
   105
			& SF(MClkReply memCh crCh cst p)_(c p)
wenzelm@6255
   106
			& WF(RPCNext crCh rmCh rst p)_(r p) 
wenzelm@6255
   107
			& WF(RNext rmCh mm ires p)_(m p)
wenzelm@6255
   108
			& WF(MemReturn rmCh ires p)_(m p)"
wenzelm@6255
   109
wenzelm@3807
   110
  Implementation :: "temporal"
wenzelm@6255
   111
      "Implementation == TEMP ( (!p. Init (~Calling memCh p) & [][ENext p]_(e p))
wenzelm@6255
   112
                               & MClkISpec memCh crCh cst
wenzelm@6255
   113
                               & RPCISpec crCh rmCh rst
wenzelm@6255
   114
                               & IRSpec rmCh mm ires)"
wenzelm@3807
   115
wenzelm@3807
   116
  (* the predicate S describes the states of the implementation.
wenzelm@6255
   117
     slight simplification: two "histState" parameters instead of a
wenzelm@6255
   118
     (one- or two-element) set.
wenzelm@6255
   119
     NB: The second conjunct of the definition in the paper is taken care of by
wenzelm@6255
   120
     the type definitions. The last conjunct is asserted separately as the memory
wenzelm@6255
   121
     invariant MemInv, proved in Memory.ML. *)
wenzelm@6255
   122
  S :: "histType => bool => bool => bool => mClkState => rpcState => histState => histState => PrIds => stpred"
wenzelm@6255
   123
      "S rmhist ecalling ccalling rcalling cs rs hs1 hs2 p == PRED
wenzelm@6255
   124
                Calling memCh p = #ecalling
wenzelm@6255
   125
              & Calling crCh p  = #ccalling
wenzelm@6255
   126
              & (#ccalling --> arg<crCh!p> = MClkRelayArg<arg<memCh!p>>)
wenzelm@6255
   127
              & (~ #ccalling & cst!p = #clkB --> MVOKBARF<res<crCh!p>>)
wenzelm@6255
   128
              & Calling rmCh p  = #rcalling
wenzelm@6255
   129
              & (#rcalling --> arg<rmCh!p> = RPCRelayArg<arg<crCh!p>>)
wenzelm@6255
   130
              & (~ #rcalling --> ires!p = #NotAResult)
wenzelm@6255
   131
              & (~ #rcalling & rst!p = #rpcB --> MVOKBA<res<rmCh!p>>)
wenzelm@6255
   132
              & cst!p = #cs
wenzelm@6255
   133
              & rst!p = #rs
wenzelm@6255
   134
              & (rmhist!p = #hs1 | rmhist!p = #hs2)
wenzelm@6255
   135
              & MVNROKBA<ires!p>"
wenzelm@3807
   136
wenzelm@3807
   137
  (* predicates S1 -- S6 define special instances of S *)
wenzelm@3807
   138
  S1            :: "histType => PrIds => stpred"
wenzelm@6255
   139
      "S1 rmhist p == S rmhist False False False clkA rpcA histA histA p"
wenzelm@3807
   140
  S2            :: "histType => PrIds => stpred"
wenzelm@6255
   141
      "S2 rmhist p == S rmhist True False False clkA rpcA histA histA p"
wenzelm@3807
   142
  S3            :: "histType => PrIds => stpred"
wenzelm@6255
   143
      "S3 rmhist p == S rmhist True True False clkB rpcA histA histB p"
wenzelm@3807
   144
  S4            :: "histType => PrIds => stpred"
wenzelm@6255
   145
      "S4 rmhist p == S rmhist True True True clkB rpcB histA histB p"
wenzelm@3807
   146
  S5            :: "histType => PrIds => stpred"
wenzelm@6255
   147
      "S5 rmhist p == S rmhist True True False clkB rpcB histB histB p"
wenzelm@3807
   148
  S6            :: "histType => PrIds => stpred"
wenzelm@6255
   149
      "S6 rmhist p == S rmhist True False False clkB rpcA histB histB p"
wenzelm@3807
   150
wenzelm@6255
   151
  (* The invariant asserts that the system is always in one of S1 - S6, for every p *)
wenzelm@6255
   152
  ImpInv         :: "histType => PrIds => stpred"
wenzelm@6255
   153
      "ImpInv rmhist p == PRED (  S1 rmhist p | S2 rmhist p | S3 rmhist p
wenzelm@6255
   154
				| S4 rmhist p | S5 rmhist p | S6 rmhist p)"
wenzelm@6255
   155
wenzelm@6255
   156
  resbar        :: "histType => resType"        (* refinement mapping *)
wenzelm@6255
   157
      "resbar rmhist s p == 
wenzelm@6255
   158
                  (if (S1 rmhist p s | S2 rmhist p s)
wenzelm@6255
   159
                   then ires s p
wenzelm@6255
   160
                   else if S3 rmhist p s
wenzelm@6255
   161
                   then if rmhist s p = histA 
wenzelm@6255
   162
                        then ires s p else MemFailure
wenzelm@6255
   163
                   else if S4 rmhist p s
wenzelm@6255
   164
                   then if (rmhist s p = histB & ires s p = NotAResult)
wenzelm@6255
   165
                        then MemFailure else ires s p
wenzelm@6255
   166
                   else if S5 rmhist p s
wenzelm@6255
   167
                   then res (rmCh s p)
wenzelm@6255
   168
                   else if S6 rmhist p s
wenzelm@6255
   169
                   then if res (crCh s p) = RPCFailure
wenzelm@6255
   170
                        then MemFailure else res (crCh s p)
wenzelm@6255
   171
                   else NotAResult)" (* dummy value *)
wenzelm@3807
   172
wenzelm@3807
   173
rules
wenzelm@3807
   174
  (* the "base" variables: everything except resbar and hist (for any index) *)
wenzelm@6255
   175
  MI_base       "basevars (caller memCh!p,
wenzelm@6255
   176
			   (rtrner memCh!p, caller crCh!p, cst!p),
wenzelm@6255
   177
			   (rtrner crCh!p, caller rmCh!p, rst!p),
wenzelm@6255
   178
			   (mm!l, rtrner rmCh!p, ires!p))"
wenzelm@3807
   179
wenzelm@3807
   180
end
wenzelm@3807
   181