theory Schedule_R

lemma schedule_invs':
  "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<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 (wp scheduleChooseNewThread_invs')
    \<comment> \<open>action = SwitchToThread candidate\<close> apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs'
                      chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct
                      switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2
           | wp hoare_disjI2[where R="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"]
           | 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 (frule invs_sch_act_wf') apply (auto simp: invs_sch_act_wf' obj_at'_activatable_st_tcb_at'
                     st_tcb_at'_runnable_is_activatable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<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>rv. invs'\<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>rv. invs'\<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>rv. invs'\<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>rv. invs'\<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>rv. invs'\<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>rv. invs'\<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>rv. invs'\<rbrace>
 3. \<And>t. \<lbrace>?B t\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> invs' 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>rv. invs'\<rbrace>
 2. \<And>t. \<lbrace>?B t\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> invs' 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 x. \<lbrakk>invs' s; ksSchedulerAction s = SwitchToThread x\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x s \<and> tcb_in_cur_domain' x s \<and> st_tcb_at' activatable' x s \<and> tcb_in_cur_domain' x s \<and> tcb_at' x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>invs' s; ksSchedulerAction s = SwitchToThread x; sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' x s \<and> tcb_in_cur_domain' x s \<and> st_tcb_at' activatable' x s \<and> tcb_in_cur_domain' x s \<and> tcb_at' x s proof (prove)
goal:
No subgoals!