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