theory Ipc_R

lemma possibleSwitchTo_invs'[wp]:
  "\<lbrace>invs' and st_tcb_at' runnable' t
          and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
   possibleSwitchTo t \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def) apply (wp tcbSchedEnqueue_invs' ssa_invs') apply (rule hoare_post_imp[OF _ rescheduleRequired_sa_cnt]) apply (wpsimp wp: ssa_invs' threadGet_wp)+ apply (clarsimp dest!: obj_at_ko_at' simp: tcb_in_cur_domain'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>curDom targetDom action. \<lbrakk>\<not> targetDom \<noteq> curDom; action \<noteq> ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<lbrace>?P'18 curDom targetDom action\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t\<rbrace>
 2. \<And>curDom targetDom action. \<lbrakk>\<not> targetDom \<noteq> curDom; \<not> action \<noteq> ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<lbrace>?R12 curDom targetDom action\<rbrace> setSchedulerAction (SwitchToThread t) \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>curDom targetDom. \<lbrace>?B8 curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (targetDom \<noteq> curDom \<longrightarrow> (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s) \<and> (\<not> targetDom \<noteq> curDom \<longrightarrow> (action \<noteq> ResumeCurrentThread \<longrightarrow> invs' s \<and> st_tcb_at' runnable' t s \<and> ?P'18 curDom targetDom action s) \<and> (\<not> action \<noteq> ResumeCurrentThread \<longrightarrow> ?R12 curDom targetDom action s))\<rbrace>
 4. \<And>curDom. \<lbrace>?B7 curDom\<rbrace> threadGet tcbDomain t \<lbrace>?B8 curDom\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets ksCurDomain \<lbrace>?B7\<rbrace>
 6. \<And>s. (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>curDom targetDom action rv s. \<lbrakk>\<not> targetDom \<noteq> curDom; action \<noteq> ResumeCurrentThread; ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t
 2. \<And>curDom targetDom action. \<lbrakk>\<not> targetDom \<noteq> curDom; \<not> action \<noteq> ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<lbrace>?R12 curDom targetDom action\<rbrace> setSchedulerAction (SwitchToThread t) \<lbrace>\<lambda>_. invs'\<rbrace>
 3. \<And>curDom targetDom. \<lbrace>?B8 curDom targetDom\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (targetDom \<noteq> curDom \<longrightarrow> (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s) \<and> (\<not> targetDom \<noteq> curDom \<longrightarrow> (action \<noteq> ResumeCurrentThread \<longrightarrow> invs' s \<and> st_tcb_at' runnable' t s \<and> True) \<and> (\<not> action \<noteq> ResumeCurrentThread \<longrightarrow> ?R12 curDom targetDom action s))\<rbrace>
 4. \<And>curDom. \<lbrace>?B7 curDom\<rbrace> threadGet tcbDomain t \<lbrace>?B8 curDom\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets ksCurDomain \<lbrace>?B7\<rbrace>
 6. \<And>s. (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; st_tcb_at' runnable' t s; ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>tcb. ko_at' tcb t s \<and> (tcbDomain tcb = ksCurDomain s \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcb_in_cur_domain' t s) proof (prove)
goal:
No subgoals!