3807
|
1 |
(*
|
|
2 |
File: Memory.ML
|
|
3 |
Author: Stephan Merz
|
|
4 |
Copyright: 1997 University of Munich
|
|
5 |
|
6255
|
6 |
RPC-Memory example: Memory specification (theorems and proofs)
|
3807
|
7 |
*)
|
|
8 |
|
|
9 |
val RM_action_defs =
|
6255
|
10 |
[MInit_def, PInit_def, RdRequest_def, WrRequest_def, MemInv_def,
|
|
11 |
GoodRead_def, BadRead_def, ReadInner_def, Read_def,
|
|
12 |
GoodWrite_def, BadWrite_def, WriteInner_def, Write_def,
|
|
13 |
MemReturn_def, RNext_def];
|
3807
|
14 |
|
|
15 |
val UM_action_defs = RM_action_defs @ [MemFail_def, UNext_def];
|
|
16 |
|
|
17 |
val RM_temp_defs = [RPSpec_def, MSpec_def, IRSpec_def];
|
|
18 |
val UM_temp_defs = [UPSpec_def, MSpec_def, IUSpec_def];
|
|
19 |
|
6255
|
20 |
val mem_css = (claset(), simpset());
|
3807
|
21 |
|
4828
|
22 |
(* -------------------- Proofs ---------------------------------------------- *)
|
3807
|
23 |
|
|
24 |
(* The reliable memory is an implementation of the unreliable one *)
|
|
25 |
qed_goal "ReliableImplementsUnReliable" Memory.thy
|
6255
|
26 |
"|- IRSpec ch mm rs --> IUSpec ch mm rs"
|
|
27 |
(K [force_tac (temp_css addsimps2 ([UNext_def,UPSpec_def,IUSpec_def] @ RM_temp_defs)
|
|
28 |
addSEs2 [STL4E,squareE]) 1]);
|
3807
|
29 |
|
|
30 |
(* The memory spec implies the memory invariant *)
|
|
31 |
qed_goal "MemoryInvariant" Memory.thy
|
6255
|
32 |
"|- MSpec ch mm rs l --> [](MemInv mm l)"
|
|
33 |
(fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @ RM_action_defs) 1 ]);
|
3807
|
34 |
|
|
35 |
(* The invariant is trivial for non-locations *)
|
|
36 |
qed_goal "NonMemLocInvariant" Memory.thy
|
6255
|
37 |
"|- #l ~: #MemLoc --> [](MemInv mm l)"
|
|
38 |
(K [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT]) ]);
|
3807
|
39 |
|
|
40 |
qed_goal "MemoryInvariantAll" Memory.thy
|
6255
|
41 |
"|- (!l. #l : #MemLoc --> MSpec ch mm rs l) --> (!l. [](MemInv mm l))"
|
4828
|
42 |
(K [step_tac temp_cs 1,
|
6255
|
43 |
case_tac "l : MemLoc" 1,
|
|
44 |
auto_tac (temp_css addSEs2 [MemoryInvariant,NonMemLocInvariant]) ]);
|
3807
|
45 |
|
4828
|
46 |
(* The memory engages in an action for process p only if there is an
|
|
47 |
unanswered call from p.
|
3807
|
48 |
We need this only for the reliable memory.
|
|
49 |
*)
|
|
50 |
|
|
51 |
qed_goal "Memoryidle" Memory.thy
|
6255
|
52 |
"|- ~$(Calling ch p) --> ~ RNext ch mm rs p"
|
|
53 |
(K [ auto_tac (mem_css addsimps2 (Return_def::RM_action_defs)) ]);
|
3807
|
54 |
|
|
55 |
(* Enabledness conditions *)
|
|
56 |
|
|
57 |
qed_goal "MemReturn_change" Memory.thy
|
6255
|
58 |
"|- MemReturn ch rs p --> <MemReturn ch rs p>_(rtrner ch ! p, rs!p)"
|
|
59 |
(K [ force_tac (mem_css addsimps2 [MemReturn_def,angle_def]) 1]);
|
3807
|
60 |
|
|
61 |
qed_goal "MemReturn_enabled" Memory.thy
|
6255
|
62 |
"!!p. basevars (rtrner ch ! p, rs!p) ==> \
|
|
63 |
\ |- Calling ch p & (rs!p ~= #NotAResult) \
|
|
64 |
\ --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
|
4828
|
65 |
(K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1,
|
|
66 |
action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def])
|
3807
|
67 |
[] [base_enabled,Pair_inject] 1
|
|
68 |
]);
|
|
69 |
|
|
70 |
qed_goal "ReadInner_enabled" Memory.thy
|
6255
|
71 |
"!!p. basevars (rtrner ch ! p, rs!p) ==> \
|
|
72 |
\ |- Calling ch p & (arg<ch!p> = #(read l)) --> Enabled (ReadInner ch mm rs p l)"
|
|
73 |
(fn _ => [case_tac "l : MemLoc" 1,
|
3807
|
74 |
ALLGOALS
|
|
75 |
(action_simp_tac
|
4089
|
76 |
(simpset() addsimps [ReadInner_def,GoodRead_def,BadRead_def,
|
3807
|
77 |
RdRequest_def])
|
|
78 |
[] [base_enabled,Pair_inject])
|
|
79 |
]);
|
|
80 |
|
|
81 |
qed_goal "WriteInner_enabled" Memory.thy
|
6255
|
82 |
"!!p. basevars (mm!l, rtrner ch ! p, rs!p) ==> \
|
|
83 |
\ |- Calling ch p & (arg<ch!p> = #(write l v)) \
|
|
84 |
\ --> Enabled (WriteInner ch mm rs p l v)"
|
|
85 |
(fn _ => [case_tac "l:MemLoc & v:MemVal" 1,
|
4828
|
86 |
ALLGOALS (action_simp_tac
|
|
87 |
(simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def,
|
4743
|
88 |
WrRequest_def] delsimps [disj_not1])
|
3807
|
89 |
[] [base_enabled,Pair_inject])
|
|
90 |
]);
|
|
91 |
|
|
92 |
qed_goal "ReadResult" Memory.thy
|
6255
|
93 |
"|- Read ch mm rs p & (!l. $(MemInv mm l)) --> (rs!p)` ~= #NotAResult"
|
|
94 |
(fn _ => [force_tac (mem_css addsimps2
|
|
95 |
[Read_def,ReadInner_def,GoodRead_def,BadRead_def,MemInv_def]) 1]);
|
3807
|
96 |
|
|
97 |
qed_goal "WriteResult" Memory.thy
|
6255
|
98 |
"|- Write ch mm rs p l --> (rs!p)` ~= #NotAResult"
|
|
99 |
(fn _ => [auto_tac (mem_css addsimps2 ([Write_def,WriteInner_def,GoodWrite_def,BadWrite_def]))
|
3807
|
100 |
]);
|
|
101 |
|
|
102 |
qed_goal "ReturnNotReadWrite" Memory.thy
|
6255
|
103 |
"|- (!l. $MemInv mm l) & MemReturn ch rs p \
|
|
104 |
\ --> ~ Read ch mm rs p & (!l. ~ Write ch mm rs p l)"
|
3807
|
105 |
(fn _ => [auto_tac
|
6255
|
106 |
(mem_css addsimps2 [MemReturn_def] addSDs2 [WriteResult, ReadResult])
|
3807
|
107 |
]);
|
|
108 |
|
|
109 |
qed_goal "RWRNext_enabled" Memory.thy
|
6255
|
110 |
"|- (rs!p = #NotAResult) & (!l. MemInv mm l) \
|
|
111 |
\ & Enabled (Read ch mm rs p | (? l. Write ch mm rs p l)) \
|
|
112 |
\ --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
|
|
113 |
(K [force_tac (mem_css addsimps2 [RNext_def,angle_def]
|
5525
|
114 |
addSEs2 [enabled_mono2]
|
6255
|
115 |
addDs2 [ReadResult, WriteResult]) 1]);
|
3807
|
116 |
|
|
117 |
|
|
118 |
(* Combine previous lemmas: the memory can make a visible step if there is an
|
|
119 |
outstanding call for which no result has been produced.
|
|
120 |
*)
|
|
121 |
qed_goal "RNext_enabled" Memory.thy
|
6255
|
122 |
"!!p. !l. basevars (mm!l, rtrner ch!p, rs!p) ==> \
|
|
123 |
\ |- (rs!p = #NotAResult) & Calling ch p & (!l. MemInv mm l) \
|
|
124 |
\ --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))" (K [
|
|
125 |
auto_tac (mem_css addsimps2 [enabled_disj]
|
|
126 |
addSIs2 [RWRNext_enabled]),
|
|
127 |
exhaust_tac "arg(ch w p)" 1,
|
|
128 |
action_simp_tac (simpset()addsimps[Read_def,enabled_ex])
|
|
129 |
[ReadInner_enabled,exI] [] 1,
|
|
130 |
force_tac (mem_css addDs2 [base_pair]) 1,
|
3807
|
131 |
etac swap 1,
|
6255
|
132 |
action_simp_tac (simpset() addsimps [Write_def,enabled_ex])
|
|
133 |
[WriteInner_enabled,exI] [] 1]);
|
|
134 |
|