theory IpcCancel_R

lemma suspend_unqueued:
  "\<lbrace>\<top>\<rbrace> suspend t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace>" apply (simp add: suspend_def unless_def tcbSchedDequeue_def) apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift) apply (simp add: threadGet_def| wp getObject_tcb_wp)+ apply (rule hoare_strengthen_post, rule hoare_post_taut) apply (fastforce simp: obj_at'_def projectKOs) apply (rule hoare_post_taut) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> ThreadDecls_H.suspend t \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do y <- cancelIPC t;
state <- getThreadState t;
y <- if state = Structures_H.thread_state.Running then updateRestartPC t else return ();
y <- setThreadState Structures_H.thread_state.Inactive t;
queued <- threadGet tcbQueued t;
when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od)
od \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) t\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>y state ya yb queued tdom. queued \<Longrightarrow> \<lbrace>?P26 y state ya yb queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. \<not> null (filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tdom, rv))) \<or> obj_at' (\<lambda>obj. if t = t then (Not \<circ> tcbQueued) (tcbQueued_update (\<lambda>_. False) obj) else (Not \<circ> tcbQueued) obj) t s\<rbrace>
 2. \<And>y state ya yb queued tdom. queued \<Longrightarrow> \<lbrace>?P'26 y state ya yb queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. \<not> \<not> null (filter (\<lambda>x. x \<noteq> t) (ksReadyQueues s (tdom, rv))) \<or> obj_at' (\<lambda>obj. if t = t then (Not \<circ> tcbQueued) (tcbQueued_update (\<lambda>_. False) obj) else (Not \<circ> tcbQueued) obj) t s\<rbrace>
 3. \<And>y state ya yb queued. queued \<Longrightarrow> \<lbrace>?Q6 y state ya yb queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom s. ?P26 y state ya yb queued tdom s \<and> ?P'26 y state ya yb queued tdom s\<rbrace>
 4. \<And>y state ya yb. \<lbrace>?B4 y state ya yb\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q6 y state ya yb queued else obj_at' (Not \<circ> tcbQueued) t\<rbrace>
 5. \<And>y state ya. \<lbrace>?B3 y state ya\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>?B4 y state ya\<rbrace>
 6. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B3 y state\<rbrace>
 7. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>?B2 y\<rbrace>
 8. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 9. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B3 () state ()\<rbrace> setThreadState Structures_H.thread_state.Inactive t \<lbrace>\<lambda>x xa. tcb_at' t xa \<longrightarrow> (\<exists>ta. (tcbQueued ta \<longrightarrow> ko_at' ta t xa \<and> (\<exists>ta. ko_at' ta t xa)) \<and> (\<not> tcbQueued ta \<longrightarrow> ko_at' ta t xa \<and> obj_at' (\<lambda>a. \<not> tcbQueued a) t xa))\<rbrace>
 2. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B3 y state\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state rv s. True \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. (tcbQueued ta \<longrightarrow> ko_at' ta t s \<and> (\<exists>ta. ko_at' ta t s)) \<and> (\<not> tcbQueued ta \<longrightarrow> ko_at' ta t s \<and> obj_at' (\<lambda>a. \<not> tcbQueued a) t s))
 2. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B3 y state\<rbrace>
 3. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Structures_H.thread_state.Running then updateRestartPC t else return () \<lbrace>?B3 y state\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>?B2 y\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B1 y\<rbrace> getThreadState t \<lbrace>?B2 y\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancelIPC t \<lbrace>?B1\<rbrace>
 3. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!