src/HOL/TLA/Memory/Memory.thy
author wenzelm
Sun Mar 20 23:07:06 2011 +0100 (2011-03-20)
changeset 42018 878f33040280
parent 41589 bbd861837ebc
child 42769 053b4b487085
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/TLA/Memory/Memory.thy
     2     Author:     Stephan Merz, University of Munich
     3 *)
     4 
     5 header {* RPC-Memory example: Memory specification *}
     6 
     7 theory Memory
     8 imports MemoryParameters ProcedureInterface
     9 begin
    10 
    11 type_synonym memChType = "(memOp, Vals) channel"
    12 type_synonym memType = "(Locs => Vals) stfun"  (* intention: MemLocs => MemVals *)
    13 type_synonym resType = "(PrIds => Vals) stfun"
    14 
    15 consts
    16   (* state predicates *)
    17   MInit      :: "memType => Locs => stpred"
    18   PInit      :: "resType => PrIds => stpred"
    19   (* auxiliary predicates: is there a pending read/write request for
    20      some process id and location/value? *)
    21   RdRequest  :: "memChType => PrIds => Locs => stpred"
    22   WrRequest  :: "memChType => PrIds => Locs => Vals => stpred"
    23 
    24   (* actions *)
    25   GoodRead   :: "memType => resType => PrIds => Locs => action"
    26   BadRead    :: "memType => resType => PrIds => Locs => action"
    27   ReadInner  :: "memChType => memType => resType => PrIds => Locs => action"
    28   Read       :: "memChType => memType => resType => PrIds => action"
    29   GoodWrite  :: "memType => resType => PrIds => Locs => Vals => action"
    30   BadWrite   :: "memType => resType => PrIds => Locs => Vals => action"
    31   WriteInner :: "memChType => memType => resType => PrIds => Locs => Vals => action"
    32   Write      :: "memChType => memType => resType => PrIds => Locs => action"
    33   MemReturn  :: "memChType => resType => PrIds => action"
    34   MemFail    :: "memChType => resType => PrIds => action"
    35   RNext      :: "memChType => memType => resType => PrIds => action"
    36   UNext      :: "memChType => memType => resType => PrIds => action"
    37 
    38   (* temporal formulas *)
    39   RPSpec     :: "memChType => memType => resType => PrIds => temporal"
    40   UPSpec     :: "memChType => memType => resType => PrIds => temporal"
    41   MSpec      :: "memChType => memType => resType => Locs => temporal"
    42   IRSpec     :: "memChType => memType => resType => temporal"
    43   IUSpec     :: "memChType => memType => resType => temporal"
    44 
    45   RSpec      :: "memChType => resType => temporal"
    46   USpec      :: "memChType => temporal"
    47 
    48   (* memory invariant: in the paper, the invariant is hidden in the definition of
    49      the predicate S used in the implementation proof, but it is easier to verify
    50      at this level. *)
    51   MemInv    :: "memType => Locs => stpred"
    52 
    53 defs
    54   MInit_def:         "MInit mm l == PRED mm!l = #InitVal"
    55   PInit_def:         "PInit rs p == PRED rs!p = #NotAResult"
    56 
    57   RdRequest_def:     "RdRequest ch p l == PRED
    58                          Calling ch p & (arg<ch!p> = #(read l))"
    59   WrRequest_def:     "WrRequest ch p l v == PRED
    60                          Calling ch p & (arg<ch!p> = #(write l v))"
    61   (* a read that doesn't raise BadArg *)
    62   GoodRead_def:      "GoodRead mm rs p l == ACT
    63                         #l : #MemLoc & ((rs!p)$ = $(mm!l))"
    64   (* a read that raises BadArg *)
    65   BadRead_def:       "BadRead mm rs p l == ACT
    66                         #l ~: #MemLoc & ((rs!p)$ = #BadArg)"
    67   (* the read action with l visible *)
    68   ReadInner_def:     "ReadInner ch mm rs p l == ACT
    69                          $(RdRequest ch p l)
    70                          & (GoodRead mm rs p l  |  BadRead mm rs p l)
    71                          & unchanged (rtrner ch ! p)"
    72   (* the read action with l quantified *)
    73   Read_def:          "Read ch mm rs p == ACT (EX l. ReadInner ch mm rs p l)"
    74 
    75   (* similar definitions for the write action *)
    76   GoodWrite_def:     "GoodWrite mm rs p l v == ACT
    77                         #l : #MemLoc & #v : #MemVal
    78                         & ((mm!l)$ = #v) & ((rs!p)$ = #OK)"
    79   BadWrite_def:      "BadWrite mm rs p l v == ACT
    80                         ~ (#l : #MemLoc & #v : #MemVal)
    81                         & ((rs!p)$ = #BadArg) & unchanged (mm!l)"
    82   WriteInner_def:    "WriteInner ch mm rs p l v == ACT
    83                         $(WrRequest ch p l v)
    84                         & (GoodWrite mm rs p l v  |  BadWrite mm rs p l v)
    85                         & unchanged (rtrner ch ! p)"
    86   Write_def:         "Write ch mm rs p l == ACT (EX v. WriteInner ch mm rs p l v)"
    87 
    88   (* the return action *)
    89   MemReturn_def:     "MemReturn ch rs p == ACT
    90                        (   ($(rs!p) ~= #NotAResult)
    91                         & ((rs!p)$ = #NotAResult)
    92                         & Return ch p (rs!p))"
    93 
    94   (* the failure action of the unreliable memory *)
    95   MemFail_def:       "MemFail ch rs p == ACT
    96                         $(Calling ch p)
    97                         & ((rs!p)$ = #MemFailure)
    98                         & unchanged (rtrner ch ! p)"
    99   (* next-state relations for reliable / unreliable memory *)
   100   RNext_def:         "RNext ch mm rs p == ACT
   101                        (  Read ch mm rs p
   102                         | (EX l. Write ch mm rs p l)
   103                         | MemReturn ch rs p)"
   104   UNext_def:         "UNext ch mm rs p == ACT
   105                         (RNext ch mm rs p | MemFail ch rs p)"
   106 
   107   RPSpec_def:        "RPSpec ch mm rs p == TEMP
   108                         Init(PInit rs p)
   109                         & [][ RNext ch mm rs p ]_(rtrner ch ! p, rs!p)
   110                         & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
   111                         & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
   112   UPSpec_def:        "UPSpec ch mm rs p == TEMP
   113                         Init(PInit rs p)
   114                         & [][ UNext ch mm rs p ]_(rtrner ch ! p, rs!p)
   115                         & WF(RNext ch mm rs p)_(rtrner ch ! p, rs!p)
   116                         & WF(MemReturn ch rs p)_(rtrner ch ! p, rs!p)"
   117   MSpec_def:         "MSpec ch mm rs l == TEMP
   118                         Init(MInit mm l)
   119                         & [][ EX p. Write ch mm rs p l ]_(mm!l)"
   120   IRSpec_def:        "IRSpec ch mm rs == TEMP
   121                         (ALL p. RPSpec ch mm rs p)
   122                         & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
   123   IUSpec_def:        "IUSpec ch mm rs == TEMP
   124                         (ALL p. UPSpec ch mm rs p)
   125                         & (ALL l. #l : #MemLoc --> MSpec ch mm rs l)"
   126 
   127   RSpec_def:         "RSpec ch rs == TEMP (EEX mm. IRSpec ch mm rs)"
   128   USpec_def:         "USpec ch == TEMP (EEX mm rs. IUSpec ch mm rs)"
   129 
   130   MemInv_def:        "MemInv mm l == PRED  #l : #MemLoc --> mm!l : #MemVal"
   131 
   132 lemmas RM_action_defs =
   133   MInit_def PInit_def RdRequest_def WrRequest_def MemInv_def
   134   GoodRead_def BadRead_def ReadInner_def Read_def
   135   GoodWrite_def BadWrite_def WriteInner_def Write_def
   136   MemReturn_def RNext_def
   137 
   138 lemmas UM_action_defs = RM_action_defs MemFail_def UNext_def
   139 
   140 lemmas RM_temp_defs = RPSpec_def MSpec_def IRSpec_def
   141 lemmas UM_temp_defs = UPSpec_def MSpec_def IUSpec_def
   142 
   143 
   144 (* The reliable memory is an implementation of the unreliable one *)
   145 lemma ReliableImplementsUnReliable: "|- IRSpec ch mm rs --> IUSpec ch mm rs"
   146   by (force simp: UNext_def UPSpec_def IUSpec_def RM_temp_defs elim!: STL4E [temp_use] squareE)
   147 
   148 (* The memory spec implies the memory invariant *)
   149 lemma MemoryInvariant: "|- MSpec ch mm rs l --> [](MemInv mm l)"
   150   by (tactic {* auto_inv_tac
   151     (@{simpset} addsimps (@{thms RM_temp_defs} @ @{thms RM_action_defs})) 1 *})
   152 
   153 (* The invariant is trivial for non-locations *)
   154 lemma NonMemLocInvariant: "|- #l ~: #MemLoc --> [](MemInv mm l)"
   155   by (auto simp: MemInv_def intro!: necT [temp_use])
   156 
   157 lemma MemoryInvariantAll:
   158     "|- (ALL l. #l : #MemLoc --> MSpec ch mm rs l) --> (ALL l. [](MemInv mm l))"
   159   apply clarify
   160   apply (auto elim!: MemoryInvariant [temp_use] NonMemLocInvariant [temp_use])
   161   done
   162 
   163 (* The memory engages in an action for process p only if there is an
   164    unanswered call from p.
   165    We need this only for the reliable memory.
   166 *)
   167 
   168 lemma Memoryidle: "|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
   169   by (auto simp: Return_def RM_action_defs)
   170 
   171 (* Enabledness conditions *)
   172 
   173 lemma MemReturn_change: "|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
   174   by (force simp: MemReturn_def angle_def)
   175 
   176 lemma MemReturn_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   177       |- Calling ch p & (rs!p ~= #NotAResult)
   178          --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   179   apply (tactic
   180     {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
   181   apply (tactic
   182     {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def},
   183       @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   184   done
   185 
   186 lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   187       |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
   188   apply (case_tac "l : MemLoc")
   189   apply (force simp: ReadInner_def GoodRead_def BadRead_def RdRequest_def
   190     intro!: exI elim!: base_enabled [temp_use])+
   191   done
   192 
   193 lemma WriteInner_enabled: "!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==>
   194       |- Calling ch p & (arg<ch!p> = #(write l v))
   195          --> Enabled (WriteInner ch mm rs p l v)"
   196   apply (case_tac "l:MemLoc & v:MemVal")
   197   apply (force simp: WriteInner_def GoodWrite_def BadWrite_def WrRequest_def
   198     intro!: exI elim!: base_enabled [temp_use])+
   199   done
   200 
   201 lemma ReadResult: "|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
   202   by (force simp: Read_def ReadInner_def GoodRead_def BadRead_def MemInv_def)
   203 
   204 lemma WriteResult: "|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
   205   by (auto simp: Write_def WriteInner_def GoodWrite_def BadWrite_def)
   206 
   207 lemma ReturnNotReadWrite: "|- (ALL l. $MemInv mm l) & MemReturn ch rs p
   208          --> ~ Read ch mm rs p & (ALL l. ~ Write ch mm rs p l)"
   209   by (auto simp: MemReturn_def dest!: WriteResult [temp_use] ReadResult [temp_use])
   210 
   211 lemma RWRNext_enabled: "|- (rs!p = #NotAResult) & (!l. MemInv mm l)
   212          & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l))
   213          --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   214   by (force simp: RNext_def angle_def elim!: enabled_mono2
   215     dest: ReadResult [temp_use] WriteResult [temp_use])
   216 
   217 
   218 (* Combine previous lemmas: the memory can make a visible step if there is an
   219    outstanding call for which no result has been produced.
   220 *)
   221 lemma RNext_enabled: "!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==>
   222       |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l)
   223          --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   224   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   225   apply (case_tac "arg (ch w p)")
   226    apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def},
   227      temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
   228    apply (force dest: base_pair [temp_use])
   229   apply (erule contrapos_np)
   230   apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def},
   231     temp_rewrite @{thm enabled_ex}])
   232     [@{thm WriteInner_enabled}, exI] [] 1 *})
   233   done
   234 
   235 end