3807
|
1 |
(*
|
|
2 |
File: Memory.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
|
6 |
RPC-Memory example: Memory specification (ML file)
|
|
7 |
*)
|
|
8 |
|
|
9 |
val RM_action_defs =
|
|
10 |
(map (fn t => t RS inteq_reflection)
|
|
11 |
[MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def])
|
|
12 |
@ [GoodRead_def, BadRead_def, ReadInner_def, Read_def,
|
|
13 |
GoodWrite_def, BadWrite_def, WriteInner_def, Write_def,
|
|
14 |
MemReturn_def, RNext_def];
|
|
15 |
|
|
16 |
val UM_action_defs = RM_action_defs @ [MemFail_def, UNext_def];
|
|
17 |
|
|
18 |
val RM_temp_defs = [RPSpec_def, MSpec_def, IRSpec_def];
|
|
19 |
val UM_temp_defs = [UPSpec_def, MSpec_def, IUSpec_def];
|
|
20 |
|
|
21 |
(* Make sure the simpset accepts non-boolean simplifications *)
|
4089
|
22 |
simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift);
|
3807
|
23 |
|
4828
|
24 |
(* -------------------- Proofs ---------------------------------------------- *)
|
3807
|
25 |
|
|
26 |
(* The reliable memory is an implementation of the unreliable one *)
|
|
27 |
qed_goal "ReliableImplementsUnReliable" Memory.thy
|
|
28 |
"IRSpec ch mm rs .-> IUSpec ch mm rs"
|
4828
|
29 |
(fn _ => [auto_tac (temp_css addsimps2 ([square_def,UNext_def] @
|
|
30 |
RM_temp_defs @ UM_temp_defs) addSEs2 [STL4E])]);
|
3807
|
31 |
|
|
32 |
(* The memory spec implies the memory invariant *)
|
|
33 |
qed_goal "MemoryInvariant" Memory.thy
|
|
34 |
"(MSpec ch mm rs l) .-> []($(MemInv mm l))"
|
4828
|
35 |
(fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @
|
|
36 |
MP_simps @ RM_action_defs) 1 ]);
|
3807
|
37 |
|
|
38 |
(* The invariant is trivial for non-locations *)
|
|
39 |
qed_goal "NonMemLocInvariant" Memory.thy
|
|
40 |
".~ #(MemLoc l) .-> []($MemInv mm l)"
|
4828
|
41 |
(K [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT RS tempD]) ]);
|
3807
|
42 |
|
|
43 |
qed_goal "MemoryInvariantAll" Memory.thy
|
|
44 |
"((RALL l. #(MemLoc l) .-> MSpec ch mm rs l)) .-> (RALL l. []($MemInv mm l))"
|
4828
|
45 |
(K [step_tac temp_cs 1,
|
|
46 |
case_tac "MemLoc l" 1,
|
|
47 |
auto_tac (temp_css addSEs2 (map temp_mp [MemoryInvariant,
|
|
48 |
NonMemLocInvariant]))]);
|
3807
|
49 |
|
4828
|
50 |
(* The memory engages in an action for process p only if there is an
|
|
51 |
unanswered call from p.
|
3807
|
52 |
We need this only for the reliable memory.
|
|
53 |
*)
|
|
54 |
|
|
55 |
qed_goal "Memoryidle" Memory.thy
|
|
56 |
".~ $(Calling ch p) .-> .~ RNext ch mm rs p"
|
4828
|
57 |
(K [ auto_tac (action_css addsimps2 (RM_action_defs @ [Return_def])) ]);
|
3807
|
58 |
|
|
59 |
bind_thm("MemoryidleI", action_mp Memoryidle);
|
|
60 |
bind_thm("MemoryidleE", action_impE Memoryidle);
|
|
61 |
|
|
62 |
|
|
63 |
(* Enabledness conditions *)
|
|
64 |
|
|
65 |
qed_goal "MemReturn_change" Memory.thy
|
|
66 |
"MemReturn ch rs p .-> <MemReturn ch rs p>_<rtrner ch @ p, rs@p>"
|
|
67 |
(fn _ => [ auto_tac (action_css addsimps2 [MemReturn_def,angle_def]) ]);
|
|
68 |
|
|
69 |
qed_goal "MemReturn_enabled" Memory.thy
|
|
70 |
"!!p. base_var <rtrner ch @ p, rs@p> ==> \
|
|
71 |
\ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \
|
|
72 |
\ .-> $(Enabled (<MemReturn ch rs p>_<rtrner ch @ p, rs@p>))"
|
4828
|
73 |
(K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1,
|
|
74 |
action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def])
|
3807
|
75 |
[] [base_enabled,Pair_inject] 1
|
|
76 |
]);
|
|
77 |
|
|
78 |
qed_goal "ReadInner_enabled" Memory.thy
|
|
79 |
"!!p. base_var <rtrner ch @ p, rs@p> ==> \
|
|
80 |
\ $(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))) \
|
|
81 |
\ .-> $(Enabled (ReadInner ch mm rs p l))"
|
|
82 |
(fn _ => [Action_simp_tac 1,
|
4828
|
83 |
(* unlift before applying case_tac: case_split_thm expects boolean conclusion *)
|
3807
|
84 |
case_tac "MemLoc l" 1,
|
|
85 |
ALLGOALS
|
|
86 |
(action_simp_tac
|
4089
|
87 |
(simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,
|
3807
|
88 |
RdRequest_def])
|
|
89 |
[] [base_enabled,Pair_inject])
|
|
90 |
]);
|
|
91 |
|
|
92 |
qed_goal "WriteInner_enabled" Memory.thy
|
|
93 |
"!!p. base_var <rtrner ch @ p, mm@l, rs@p> ==> \
|
|
94 |
\ $(Calling ch p) .& (arg[$(ch@p)] .= #(Inr (write,l,v))) \
|
|
95 |
\ .-> $(Enabled (WriteInner ch mm rs p l v))"
|
|
96 |
(fn _ => [Action_simp_tac 1,
|
|
97 |
case_tac "MemLoc l & MemVal v" 1,
|
4828
|
98 |
ALLGOALS (action_simp_tac
|
|
99 |
(simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
|
4743
|
100 |
WrRequest_def] delsimps [disj_not1])
|
3807
|
101 |
[] [base_enabled,Pair_inject])
|
|
102 |
]);
|
|
103 |
|
|
104 |
qed_goal "ReadResult" Memory.thy
|
|
105 |
"(Read ch mm rs p) .& (RALL l. $(MemInv mm l)) .-> (rs@p)$ .~= #NotAResult"
|
|
106 |
(fn _ => [action_simp_tac
|
4089
|
107 |
(simpset() addsimps (MP_simps
|
3807
|
108 |
@ [Read_def,ReadInner_def,GoodRead_def,
|
|
109 |
BadRead_def,MemInv_def]))
|
|
110 |
[] [] 1,
|
|
111 |
auto_tac (action_css addsimps2 MP_simps) ]);
|
|
112 |
|
|
113 |
qed_goal "WriteResult" Memory.thy
|
|
114 |
"(Write ch mm rs p l) .-> (rs@p)$ .~= #NotAResult"
|
4089
|
115 |
(fn _ => [auto_tac (claset(),
|
|
116 |
simpset() addsimps (MP_simps @
|
4828
|
117 |
[Write_def,WriteInner_def,GoodWrite_def,BadWrite_def]))
|
3807
|
118 |
]);
|
|
119 |
|
|
120 |
qed_goal "ReturnNotReadWrite" Memory.thy
|
|
121 |
"(RALL l. $MemInv mm l) .& (MemReturn ch rs p) \
|
|
122 |
\ .-> .~(Read ch mm rs p) .& (RALL l. .~(Write ch mm rs p l))"
|
|
123 |
(fn _ => [auto_tac
|
|
124 |
(action_css addsimps2 [MemReturn_def]
|
4828
|
125 |
addSEs2 [action_impE WriteResult,action_conjimpE ReadResult])
|
3807
|
126 |
]);
|
|
127 |
|
|
128 |
qed_goal "RWRNext_enabled" Memory.thy
|
|
129 |
"($(rs@p) .= #NotAResult) .& (RALL l. $(MemInv mm l)) \
|
|
130 |
\ .& $(Enabled (Read ch mm rs p .| (REX l. Write ch mm rs p l))) \
|
|
131 |
\ .-> $(Enabled (<RNext ch mm rs p>_<rtrner ch @ p, rs@p>))"
|
|
132 |
(fn _ => [auto_tac
|
|
133 |
(action_css addsimps2 [RNext_def,angle_def]
|
|
134 |
addSEs2 [enabled_mono2]
|
4828
|
135 |
addEs2[action_conjimpE ReadResult,action_impE WriteResult])
|
3807
|
136 |
]);
|
|
137 |
|
|
138 |
|
|
139 |
(* Combine previous lemmas: the memory can make a visible step if there is an
|
|
140 |
outstanding call for which no result has been produced.
|
|
141 |
*)
|
|
142 |
qed_goal "RNext_enabled" Memory.thy
|
4828
|
143 |
"!!p. (ALL l. base_var <rtrner ch @ p, mm@l, rs@p>) ==> \
|
|
144 |
\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \
|
|
145 |
\ .-> $(Enabled (<RNext ch mm rs p>_<rtrner ch @ p, rs@p>))" (K [
|
|
146 |
auto_tac (action_css addsimps2 [enabled_disj]
|
3807
|
147 |
addSIs2 [action_mp RWRNext_enabled]),
|
|
148 |
res_inst_tac [("s","arg(ch s p)")] sumE 1,
|
4828
|
149 |
action_simp_tac (simpset()addsimps[Read_def,enabled_ex,base_pair])
|
|
150 |
[action_mp ReadInner_enabled,exI] [] 1,
|
|
151 |
split_all_tac 1, rename_tac "a b" 1, Rd.induct_tac "a" 1,
|
3807
|
152 |
(* introduce a trivial subgoal to solve flex-flex constraint?! *)
|
4828
|
153 |
subgoal_tac "b = snd(a,b)" 1,
|
|
154 |
TRYALL Simp_tac, (* solves "read" case *)
|
3807
|
155 |
etac swap 1,
|
4828
|
156 |
action_simp_tac (simpset()addsimps[Write_def,enabled_ex,base_pair])
|
3807
|
157 |
[action_mp WriteInner_enabled,exI] [] 1,
|
4828
|
158 |
split_all_tac 1, rename_tac "a aa b" 1, Wr.induct_tac "a" 1,
|
|
159 |
subgoal_tac "(aa = fst(snd(a,aa,b))) & (b = snd(snd(a,aa,b)))" 1,
|
3807
|
160 |
ALLGOALS Simp_tac ]);
|