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