1(* Title: HOL/TLA/Memory/RPC.thy 2 Author: Stephan Merz, University of Munich 3*) 4 5section \<open>RPC-Memory example: RPC specification\<close> 6 7theory RPC 8imports RPCParameters ProcedureInterface Memory 9begin 10 11type_synonym rpcSndChType = "(rpcOp,Vals) channel" 12type_synonym rpcRcvChType = "memChType" 13type_synonym rpcStType = "(PrIds \<Rightarrow> rpcState) stfun" 14 15 16(* state predicates *) 17 18definition 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 *) 23 24definition 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)" 32 33definition 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))" 39 40definition 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)" 46 47definition 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)" 54 55definition 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 62 63(* temporal *) 64 65definition 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)" 70 71definition RPCISpec :: "rpcSndChType \<Rightarrow> rpcRcvChType \<Rightarrow> rpcStType \<Rightarrow> temporal" 72 where "RPCISpec send rcv rst == TEMP (\<forall>p. RPCIPSpec send rcv rst p)" 73 74 75lemmas RPC_action_defs = 76 RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def 77 78lemmas 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 85lemma RPCidle: "\<turnstile> \<not>$(Calling send p) \<longrightarrow> \<not>RPCNext send rcv rst p" 86 by (auto simp: AReturn_def RPC_action_defs) 87 88lemma RPCbusy: "\<turnstile> $(Calling rcv p) \<and> $(rst!p) = #rpcB \<longrightarrow> \<not>RPCNext send rcv rst p" 89 by (auto simp: RPC_action_defs) 90 91(* RPC failure actions are visible. *) 92lemma RPCFail_vis: "\<turnstile> RPCFail send rcv rst p \<longrightarrow> 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 96lemma RPCFail_Next_enabled: "\<turnstile> Enabled (RPCFail send rcv rst p) \<longrightarrow> 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 *) 101lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow> 102 \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)" 103 by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCFail_def}, 104 @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] 105 [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) 106 107lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow> 108 \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB 109 \<longrightarrow> Enabled (RPCReply send rcv rst p)" 110 by (tactic \<open>action_simp_tac (\<^context> addsimps [@{thm RPCReply_def}, 111 @{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] 112 [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>) 113 114end 115