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