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