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