src/HOL/TLA/Memory/Memory.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 26937 57e7d045774a
child 41589 bbd861837ebc
permissions -rw-r--r--
more antiquotations;
     1 (*
     2     File:        Memory.thy
     3     ID:          $Id$
     4     Author:      Stephan Merz
     5     Copyright:   1997 University of Munich
     6 *)
     7 
     8 header {* RPC-Memory example: Memory specification *}
     9 
    10 theory Memory
    11 imports MemoryParameters ProcedureInterface
    12 begin
    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 defs
    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 
   136 lemmas RM_action_defs =
   137   MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
   138   GoodRead_def BadRead_def ReadInner_def Read_def
   139   GoodWrite_def BadWrite_def WriteInner_def Write_def
   140   MemReturn_def RNext_def
   141 
   142 lemmas UM_action_defs = RM_action_defs MemFail_def UNext_def
   143 
   144 lemmas RM_temp_defs = RPSpec_def MSpec_def IRSpec_def
   145 lemmas UM_temp_defs = UPSpec_def MSpec_def IUSpec_def
   146 
   147 
   148 (* The reliable memory is an implementation of the unreliable one *)
   149 lemma ReliableImplementsUnReliable: "|- IRSpec ch mm rs --> IUSpec ch mm rs"
   150   by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)
   151 
   152 (* The memory spec implies the memory invariant *)
   153 lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
   154   by (tactic {* auto_inv_tac
   155     (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
   156 
   157 (* The invariant is trivial for non-locations *)
   158 lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
   159   by (auto simp: MemInv_def intro!: necT [temp_use])
   160 
   161 lemma MemoryInvariantAll:
   162     "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
   163   apply clarify
   164   apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
   165   done
   166 
   167 (* The memory engages in an action for process p only if there is an
   168    unanswered call from p.
   169    We need this only for the reliable memory.
   170 *)
   171 
   172 lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
   173   by (auto simp: Return_def RM_action_defs)
   174 
   175 (* Enabledness conditions *)
   176 
   177 lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
   178   by (force simp: MemReturn_def angle_def)
   179 
   180 lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   181       |- Calling ch p & (rs!p ~= #NotAResult)
   182          --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   183   apply (tactic
   184     {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
   185   apply (tactic
   186     {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def},
   187       @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   188   done
   189 
   190 lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   191       |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
   192   apply (case_tac "l : MemLoc")
   193   apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
   194     intro!: exI elim!: base_enabled [temp_use])+
   195   done
   196 
   197 lemma WriteInner_enabled: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
   198       |- Calling ch p & (arg<ch!p> = #(write l v))
   199          --> Enabled (WriteInner ch mm rs p l v)"
   200   apply (case_tac "l:MemLoc & v:MemVal")
   201   apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
   202     intro!: exI elim!: base_enabled [temp_use])+
   203   done
   204 
   205 lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
   206   by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)
   207 
   208 lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
   209   by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
   210 
   211 lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p
   212          --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)"
   213   by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
   214 
   215 lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
   216          & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l))
   217          --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   218   by (force simp: RNext_def angle_def elim!: enabled_mono2
   219     dest: ReadResult [temp_use] WriteResult [temp_use])
   220 
   221 
   222 (* Combine previous lemmas: the memory can make a visible step if there is an
   223    outstanding call for which no result has been produced.
   224 *)
   225 lemma RNext_enabled: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==>
   226       |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)
   227          --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   228   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   229   apply (case_tac "arg (ch w p)")
   230    apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def},
   231      temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
   232    apply (force dest: base_pair [temp_use])
   233   apply (erule contrapos_np)
   234   apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def},
   235     temp_rewrite @{thm enabled_ex}])
   236     [@{thm WriteInner_enabled}, exI] [] 1 *})
   237   done
   238 
   239 end