theory IpcCancel_R

lemma rescheduleRequired_unlive:
  "\<lbrace>\<lambda>s. ko_wp_at' (Not \<circ> live') p s \<and> ksSchedulerAction s \<noteq> SwitchToThread p\<rbrace>
      rescheduleRequired
   \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | simp | wpc)+ apply (simp add: tcbSchedEnqueue_def unless_def
                    threadSet_def setQueue_def threadGet_def) apply (wp setObject_ko_wp_at getObject_tcb_wp
            | simp add: objBits_simps' bitmap_fun_defs split del: if_split)+ apply (clarsimp simp: o_def) apply (drule obj_at_ko_at') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ko_wp_at' (Not \<circ> live') p s \<and> sch_act_not p s\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ko_wp_at' (Not \<circ> live') p s \<and> sch_act_not p s\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R16 (SwitchToThread x3) x3\<rbrace> tcbSchedEnqueue x3 \<lbrace>\<lambda>y. ko_wp_at' (\<lambda>a. \<not> live' a) p\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (action = ChooseNewThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R16 action x s)\<rbrace>
 3. \<And>s. ko_wp_at' (Not \<circ> live') p s \<and> sch_act_not p s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R16 (SwitchToThread x3) x3\<rbrace> do queued <- liftM tcbQueued (getObject x3);
when (\<not> queued) (do tdom <- liftM tcbDomain (getObject x3);
prio <- liftM tcbPriority (getObject x3);
queue <- getQueue tdom prio;
y <- modify (\<lambda>ks. ks\<lparr>ksReadyQueues := (ksReadyQueues ks)((tdom, prio) := x3 # queue)\<rparr>);
y <- when (null queue) (addToBitmap tdom prio);
tcb <- getObject x3;
setObject x3 (tcbQueued_update (\<lambda>_. True) tcb)
od)
od \<lbrace>\<lambda>y. ko_wp_at' (\<lambda>a. \<not> live' a) p\<rbrace>
 2. \<lbrace>?Q\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (action = ChooseNewThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R16 action x s)\<rbrace>
 3. \<And>s. ko_wp_at' (Not \<circ> live') p s \<and> sch_act_not p s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ko_wp_at' (Not \<circ> live') p s \<and> sch_act_not p s \<Longrightarrow> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (ksSchedulerAction s = ChooseNewThread \<longrightarrow> ko_wp_at' (\<lambda>a. \<not> live' a) p s) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> tcb_at' x s \<longrightarrow> (\<exists>t. ko_at' t x s \<and> (if \<not> tcbQueued t then \<lambda>s. tcb_at' x s \<longrightarrow> (\<exists>t. ko_at' t x s \<and> ((\<lambda>xa s. tcb_at' x s \<longrightarrow> (\<exists>t. ko_at' t x s \<and> ((\<lambda>xaa s. (if null (ksReadyQueues s (xa, xaa)) then \<lambda>a. tcb_at' x (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa), ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>))((xa, invertL1Index (prioToL1Index xaa)) := ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>) (xa, invertL1Index (prioToL1Index xaa)) || 2 ^ unat (xaa && mask wordRadix))\<rparr>) \<longrightarrow> (\<exists>t. ko_at' t x (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa), ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>))((xa, invertL1Index (prioToL1Index xaa)) := ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>) (xa, invertL1Index (prioToL1Index xaa)) || 2 ^ unat (xaa && mask wordRadix))\<rparr>) \<and> ko_wp_at' (if x = p then K (\<not> live' (injectKO (tcbQueued_update (\<lambda>_. True) t))) else (\<lambda>a. \<not> live' a)) p (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa), ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>))((xa, invertL1Index (prioToL1Index xaa)) := ksReadyQueuesL2Bitmap (a\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap a)(xa := ksReadyQueuesL1Bitmap a xa || 2 ^ prioToL1Index xaa)\<rparr>) (xa, invertL1Index (prioToL1Index xaa)) || 2 ^ unat (xaa && mask wordRadix))\<rparr>)) else (\<lambda>s. tcb_at' x s \<longrightarrow> (\<exists>t. ko_at' t x s \<and> (tcb_at' x s \<longrightarrow> ko_wp_at' (if x = p then K (\<not> live' (injectKO (tcbQueued_update (\<lambda>_. True) t))) else (\<lambda>a. \<not> live' a)) p s)))) (s\<lparr>ksReadyQueues := (ksReadyQueues s)((xa, xaa) := x # ksReadyQueues s (xa, xaa))\<rparr>)) \<circ> tcbPriority) t s)) \<circ> tcbDomain) t s) else ko_wp_at' (\<lambda>a. \<not> live' a) p) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ko_wp_at' (\<lambda>x. \<not> live' x) p s; x \<noteq> p; ksSchedulerAction s = SwitchToThread x; tcb_at' x s\<rbrakk> \<Longrightarrow> \<exists>t. (\<not> tcbQueued t \<longrightarrow> ko_at' t x s \<and> (\<exists>t. ko_at' t x s)) \<and> (tcbQueued t \<longrightarrow> ko_at' t x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>ko_wp_at' (\<lambda>x. \<not> live' x) p s; x \<noteq> p; ksSchedulerAction s = SwitchToThread x; \<exists>ko. ko_at' ko x s \<and> True\<rbrakk> \<Longrightarrow> \<exists>t. (\<not> tcbQueued t \<longrightarrow> ko_at' t x s \<and> (\<exists>t. ko_at' t x s)) \<and> (tcbQueued t \<longrightarrow> ko_at' t x s) proof (prove)
goal:
No subgoals!