41589
|
1 |
(* Title: HOL/TLA/Memory/RPC.thy
|
|
2 |
Author: Stephan Merz, University of Munich
|
21624
|
3 |
*)
|
3807
|
4 |
|
60592
|
5 |
section \<open>RPC-Memory example: RPC specification\<close>
|
3807
|
6 |
|
17309
|
7 |
theory RPC
|
|
8 |
imports RPCParameters ProcedureInterface Memory
|
|
9 |
begin
|
3807
|
10 |
|
42018
|
11 |
type_synonym rpcSndChType = "(rpcOp,Vals) channel"
|
|
12 |
type_synonym rpcRcvChType = "memChType"
|
60588
|
13 |
type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun"
|
3807
|
14 |
|
62145
|
15 |
|
|
16 |
(* state predicates *)
|
3807
|
17 |
|
62145
|
18 |
definition RPCInit :: "rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> stpred"
|
|
19 |
where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) \<and> \<not>Calling rcv p)"
|
|
20 |
|
|
21 |
|
|
22 |
(* actions *)
|
3807
|
23 |
|
62145
|
24 |
definition RPCFwd :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
|
|
25 |
where "RPCFwd send rcv rst p == ACT
|
|
26 |
$(Calling send p)
|
|
27 |
\<and> $(rst!p) = # rpcA
|
|
28 |
\<and> IsLegalRcvArg<arg<$(send!p)>>
|
|
29 |
\<and> Call rcv p RPCRelayArg<arg<send!p>>
|
|
30 |
\<and> (rst!p)$ = # rpcB
|
|
31 |
\<and> unchanged (rtrner send!p)"
|
3807
|
32 |
|
62145
|
33 |
definition RPCReject :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
|
|
34 |
where "RPCReject send rcv rst p == ACT
|
|
35 |
$(rst!p) = # rpcA
|
|
36 |
\<and> \<not>IsLegalRcvArg<arg<$(send!p)>>
|
|
37 |
\<and> Return send p #BadCall
|
|
38 |
\<and> unchanged ((rst!p), (caller rcv!p))"
|
3807
|
39 |
|
62145
|
40 |
definition RPCFail :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
|
|
41 |
where "RPCFail send rcv rst p == ACT
|
|
42 |
\<not>$(Calling rcv p)
|
|
43 |
\<and> Return send p #RPCFailure
|
|
44 |
\<and> (rst!p)$ = #rpcA
|
|
45 |
\<and> unchanged (caller rcv!p)"
|
3807
|
46 |
|
62145
|
47 |
definition RPCReply :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
|
|
48 |
where "RPCReply send rcv rst p == ACT
|
|
49 |
\<not>$(Calling rcv p)
|
|
50 |
\<and> $(rst!p) = #rpcB
|
|
51 |
\<and> Return send p res<rcv!p>
|
|
52 |
\<and> (rst!p)$ = #rpcA
|
|
53 |
\<and> unchanged (caller rcv!p)"
|
3807
|
54 |
|
62145
|
55 |
definition RPCNext :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> action"
|
|
56 |
where "RPCNext send rcv rst p == ACT
|
|
57 |
( RPCFwd send rcv rst p
|
|
58 |
\<or> RPCReject send rcv rst p
|
|
59 |
\<or> RPCFail send rcv rst p
|
|
60 |
\<or> RPCReply send rcv rst p)"
|
|
61 |
|
3807
|
62 |
|
62145
|
63 |
(* temporal *)
|
3807
|
64 |
|
62145
|
65 |
definition RPCIPSpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> PrIds \<Rightarrow> temporal"
|
|
66 |
where "RPCIPSpec send rcv rst p == TEMP
|
|
67 |
Init RPCInit rcv rst p
|
|
68 |
\<and> \<box>[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
|
|
69 |
\<and> WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"
|
3807
|
70 |
|
62145
|
71 |
definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal"
|
|
72 |
where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)"
|
17309
|
73 |
|
21624
|
74 |
|
|
75 |
lemmas RPC_action_defs =
|
|
76 |
RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def
|
|
77 |
|
|
78 |
lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def
|
|
79 |
|
|
80 |
|
|
81 |
(* The RPC component engages in an action for process p only if there is an outstanding,
|
|
82 |
unanswered call for that process.
|
|
83 |
*)
|
|
84 |
|
60588
|
85 |
lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p"
|
62146
|
86 |
by (auto simp: AReturn_def RPC_action_defs)
|
21624
|
87 |
|
60591
|
88 |
lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p"
|
21624
|
89 |
by (auto simp: RPC_action_defs)
|
|
90 |
|
|
91 |
(* RPC failure actions are visible. *)
|
60588
|
92 |
lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow>
|
21624
|
93 |
<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
|
|
94 |
by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)
|
|
95 |
|
60588
|
96 |
lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow>
|
21624
|
97 |
Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
|
|
98 |
by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])
|
|
99 |
|
|
100 |
(* Enabledness of some actions *)
|
60588
|
101 |
lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
|
60591
|
102 |
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
|
60592
|
103 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
|
62146
|
104 |
@{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
|
60592
|
105 |
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
|
21624
|
106 |
|
60588
|
107 |
lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>
|
60591
|
108 |
\<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB
|
60588
|
109 |
\<longrightarrow> Enabled (RPCReply send rcv rst p)"
|
60592
|
110 |
by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
|
62146
|
111 |
@{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
|
60592
|
112 |
[@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
|
3807
|
113 |
|
|
114 |
end
|