src/HOL/TLA/Memory/Memory.thy
author wenzelm
Fri Oct 05 23:58:52 2001 +0200 (2001-10-05)
changeset 11703 6e5de8d4290a
parent 9517 f58863b1406a
child 17309 c43ed29bd197
permissions -rw-r--r--
tuned;
wenzelm@3807
     1
(*
wenzelm@3807
     2
    File:        Memory.thy
wenzelm@3807
     3
    Author:      Stephan Merz
wenzelm@3807
     4
    Copyright:   1997 University of Munich
wenzelm@3807
     5
wenzelm@3807
     6
    Theory Name: Memory
wenzelm@3807
     7
    Logic Image: TLA
wenzelm@3807
     8
wenzelm@3807
     9
    RPC-Memory example: Memory specification
wenzelm@3807
    10
*)
wenzelm@3807
    11
wenzelm@3807
    12
Memory = MemoryParameters + ProcedureInterface +
wenzelm@3807
    13
wenzelm@3807
    14
types
wenzelm@6255
    15
  memChType  = "(memOp, Vals) channel"
wenzelm@3807
    16
  memType = "(Locs => Vals) stfun"      (* intention: MemLocs => MemVals *)
wenzelm@3807
    17
  resType = "(PrIds => Vals) stfun"
wenzelm@3807
    18
wenzelm@3807
    19
consts
wenzelm@3807
    20
  (* state predicates *)
wenzelm@3807
    21
  MInit      :: "memType => Locs => stpred"
wenzelm@3807
    22
  PInit      :: "resType => PrIds => stpred"
wenzelm@3807
    23
  (* auxiliary predicates: is there a pending read/write request for
wenzelm@3807
    24
     some process id and location/value? *)
wenzelm@3807
    25
  RdRequest  :: "memChType => PrIds => Locs => stpred"
wenzelm@3807
    26
  WrRequest  :: "memChType => PrIds => Locs => Vals => stpred"
wenzelm@3807
    27
wenzelm@3807
    28
  (* actions *)
wenzelm@3807
    29
  GoodRead   :: "memType => resType => PrIds => Locs => action"
wenzelm@3807
    30
  BadRead    :: "memType => resType => PrIds => Locs => action"
wenzelm@3807
    31
  ReadInner  :: "memChType => memType => resType => PrIds => Locs => action"
wenzelm@3807
    32
  Read       :: "memChType => memType => resType => PrIds => action"
wenzelm@3807
    33
  GoodWrite  :: "memType => resType => PrIds => Locs => Vals => action"
wenzelm@3807
    34
  BadWrite   :: "memType => resType => PrIds => Locs => Vals => action"
wenzelm@3807
    35
  WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action"
wenzelm@3807
    36
  Write      :: "memChType => memType => resType => PrIds => Locs => action"
wenzelm@3807
    37
  MemReturn  :: "memChType => resType => PrIds => action"
wenzelm@3807
    38
  MemFail    :: "memChType => resType => PrIds => action"
wenzelm@3807
    39
  RNext      :: "memChType => memType => resType => PrIds => action"
wenzelm@3807
    40
  UNext      :: "memChType => memType => resType => PrIds => action"
wenzelm@3807
    41
wenzelm@3807
    42
  (* temporal formulas *)
wenzelm@3807
    43
  RPSpec     :: "memChType => memType => resType => PrIds => temporal"
wenzelm@3807
    44
  UPSpec     :: "memChType => memType => resType => PrIds => temporal"
wenzelm@3807
    45
  MSpec      :: "memChType => memType => resType => Locs => temporal"
wenzelm@3807
    46
  IRSpec     :: "memChType => memType => resType => temporal"
wenzelm@3807
    47
  IUSpec     :: "memChType => memType => resType => temporal"
wenzelm@3807
    48
wenzelm@3807
    49
  RSpec      :: "memChType => resType => temporal"
wenzelm@3807
    50
  USpec      :: "memChType => temporal"
wenzelm@3807
    51
wenzelm@3807
    52
  (* memory invariant: in the paper, the invariant is hidden in the definition of
wenzelm@3807
    53
     the predicate S used in the implementation proof, but it is easier to verify 
wenzelm@3807
    54
     at this level. *)
wenzelm@3807
    55
  MemInv    :: "memType => Locs => stpred"
wenzelm@3807
    56
wenzelm@3807
    57
rules
wenzelm@6255
    58
  MInit_def         "MInit mm l == PRED mm!l = #InitVal"
wenzelm@6255
    59
  PInit_def         "PInit rs p == PRED rs!p = #NotAResult"
wenzelm@3807
    60
wenzelm@6255
    61
  RdRequest_def     "RdRequest ch p l == PRED
wenzelm@6255
    62
                         Calling ch p & (arg<ch!p> = #(read l))"
wenzelm@6255
    63
  WrRequest_def     "WrRequest ch p l v == PRED
wenzelm@6255
    64
                         Calling ch p & (arg<ch!p> = #(write l v))"
wenzelm@3807
    65
  (* a read that doesn't raise BadArg *)
wenzelm@6255
    66
  GoodRead_def      "GoodRead mm rs p l == ACT
wenzelm@6255
    67
                        #l : #MemLoc & ((rs!p)$ = $(mm!l))"
wenzelm@3807
    68
  (* a read that raises BadArg *)
wenzelm@6255
    69
  BadRead_def       "BadRead mm rs p l == ACT
wenzelm@6255
    70
                        #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
wenzelm@3807
    71
  (* the read action with l visible *)
wenzelm@6255
    72
  ReadInner_def     "ReadInner ch mm rs p l == ACT
wenzelm@3807
    73
                         $(RdRequest ch p l)
wenzelm@6255
    74
                         & (GoodRead mm rs p l  |  BadRead mm rs p l)
wenzelm@6255
    75
                         & unchanged (rtrner ch ! p)"
wenzelm@3807
    76
  (* the read action with l quantified *)
wenzelm@9517
    77
  Read_def          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
wenzelm@3807
    78
wenzelm@3807
    79
  (* similar definitions for the write action *)
wenzelm@6255
    80
  GoodWrite_def     "GoodWrite mm rs p l v == ACT
wenzelm@6255
    81
                        #l : #MemLoc & #v : #MemVal
wenzelm@6255
    82
                        & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
wenzelm@6255
    83
  BadWrite_def      "BadWrite mm rs p l v == ACT
wenzelm@6255
    84
                        ~ (#l : #MemLoc & #v : #MemVal)
wenzelm@6255
    85
                        & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
wenzelm@6255
    86
  WriteInner_def    "WriteInner ch mm rs p l v == ACT
wenzelm@3807
    87
                        $(WrRequest ch p l v)
wenzelm@6255
    88
                        & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
wenzelm@6255
    89
                        & unchanged (rtrner ch ! p)"
wenzelm@9517
    90
  Write_def         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
wenzelm@3807
    91
wenzelm@3807
    92
  (* the return action *)
wenzelm@6255
    93
  MemReturn_def     "MemReturn ch rs p == ACT
wenzelm@6255
    94
                       (   ($(rs!p) ~= #NotAResult)
wenzelm@6255
    95
                        & ((rs!p)$ = #NotAResult)
wenzelm@6255
    96
                        & Return ch p (rs!p))"
wenzelm@6255
    97
wenzelm@3807
    98
  (* the failure action of the unreliable memory *)
wenzelm@6255
    99
  MemFail_def       "MemFail ch rs p == ACT
wenzelm@3807
   100
                        $(Calling ch p)
wenzelm@6255
   101
                        & ((rs!p)$ = #MemFailure)
wenzelm@6255
   102
                        & unchanged (rtrner ch ! p)"
wenzelm@6255
   103
  (* next-state relations for reliable / unreliable memory *)
wenzelm@6255
   104
  RNext_def         "RNext ch mm rs p == ACT 
wenzelm@6255
   105
                       (  Read ch mm rs p
wenzelm@9517
   106
                        | (EX l. Write ch mm rs p l)
wenzelm@6255
   107
                        | MemReturn ch rs p)"
wenzelm@6255
   108
  UNext_def         "UNext ch mm rs p == ACT
wenzelm@6255
   109
                        (RNext ch mm rs p | MemFail ch rs p)"
wenzelm@3807
   110
wenzelm@6255
   111
  RPSpec_def        "RPSpec ch mm rs p == TEMP
wenzelm@6255
   112
                        Init(PInit rs p)
wenzelm@6255
   113
                        & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
wenzelm@6255
   114
                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
wenzelm@6255
   115
                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
wenzelm@6255
   116
  UPSpec_def        "UPSpec ch mm rs p == TEMP
wenzelm@6255
   117
                        Init(PInit rs p)
wenzelm@6255
   118
                        & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
wenzelm@6255
   119
                        & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
wenzelm@6255
   120
                        & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
wenzelm@6255
   121
  MSpec_def         "MSpec ch mm rs l == TEMP
wenzelm@6255
   122
                        Init(MInit mm l)
wenzelm@9517
   123
                        & [][ EX p. Write ch mm rs p l ]_(mm!l)"
wenzelm@6255
   124
  IRSpec_def        "IRSpec ch mm rs == TEMP
wenzelm@9517
   125
                        (ALL p. RPSpec ch mm rs p)
wenzelm@9517
   126
                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
wenzelm@6255
   127
  IUSpec_def        "IUSpec ch mm rs == TEMP
wenzelm@9517
   128
                        (ALL p. UPSpec ch mm rs p)
wenzelm@9517
   129
                        & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
wenzelm@3807
   130
wenzelm@6255
   131
  RSpec_def         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
wenzelm@6255
   132
  USpec_def         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
wenzelm@3807
   133
wenzelm@6255
   134
  MemInv_def        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
wenzelm@3807
   135
end