theory Schedule_R

lemma schedule_ct_activatable'[wp]:
  "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" supply ssa_wp[wp del] apply (simp add: schedule_def) apply (rule_tac hoare_seq_ext, rename_tac t) apply (wp, wpc)
      \<comment> \<open>action = ResumeCurrentThread\<close> apply (wp)[1]
     \<comment> \<open>action = ChooseNewThread\<close> apply wpsimp
    \<comment> \<open>action = SwitchToThread\<close> apply (wpsimp wp: ssa_invs' setSchedulerAction_direct ssa_ct
           | wp hoare_drop_imp[where f="isHighestPrio d p" for d p]
           | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def]
           | strengthen invs'_invs_no_cicd
           | wp hoare_vcg_imp_lift)+ apply (fastforce dest: invs_sch_act_wf' elim: pred_tcb'_weakenE
                   simp: sch_act_wf obj_at'_activatable_st_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrace>?B t\<rbrace> do action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable t;
when curRunnable $ tcbSchedEnqueue t;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable t;
when wasRunnable (tcbSchedEnqueue t);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority t;
fastfail <- scheduleSwitchThreadFastfail t idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 2. \<lbrace>invs'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>t action. action = ResumeCurrentThread \<Longrightarrow> \<lbrace>?R14 t action\<rbrace> return () \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 2. \<And>t action. action = ChooseNewThread \<Longrightarrow> \<lbrace>?R15 t action\<rbrace> do curRunnable <- isRunnable t;
when curRunnable $ tcbSchedEnqueue t;
scheduleChooseNewThread
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 3. \<And>t action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R16 t action x3\<rbrace> do wasRunnable <- isRunnable t;
when wasRunnable (tcbSchedEnqueue t);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority t;
fastfail <- scheduleSwitchThreadFastfail t idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 4. \<And>t. \<lbrace>?B t\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ?R14 t action s) \<and> (action = ChooseNewThread \<longrightarrow> ?R15 t action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R16 t action x s)\<rbrace>
 5. \<lbrace>invs'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>t action. action = ChooseNewThread \<Longrightarrow> \<lbrace>?R15 t action\<rbrace> do curRunnable <- isRunnable t;
when curRunnable $ tcbSchedEnqueue t;
scheduleChooseNewThread
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 2. \<And>t action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R16 t action x3\<rbrace> do wasRunnable <- isRunnable t;
when wasRunnable (tcbSchedEnqueue t);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority t;
fastfail <- scheduleSwitchThreadFastfail t idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 3. \<And>t. \<lbrace>?B t\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (action = ChooseNewThread \<longrightarrow> ?R15 t action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R16 t action x s)\<rbrace>
 4. \<lbrace>invs'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>t action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R16 t action x3\<rbrace> do wasRunnable <- isRunnable t;
when wasRunnable (tcbSchedEnqueue t);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority t;
fastfail <- scheduleSwitchThreadFastfail t idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>
 2. \<And>t. \<lbrace>?B t\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (action = ChooseNewThread \<longrightarrow> (if st_tcb_at' runnable' t s then \<lambda>s. (invs' and st_tcb_at' runnable' t and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)) s \<and> ksSchedulerAction s = ChooseNewThread else (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread)) s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R16 t action x s)\<rbrace>
 3. \<lbrace>invs'\<rbrace> getCurThread \<lbrace>?B\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s \<and> st_tcb_at' activatable' x s)) \<and> (\<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s \<and> obj_at' (activatable' \<circ> tcbState) x s)) proof (prove)
goal:
No subgoals!