theory Scheduler_IF

lemma schedule_no_domain_switch:
  "\<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace>
   schedule
   \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>" unfolding schedule_def supply ethread_get_wp[wp del] apply (wpsimp wp: hoare_drop_imps simp: if_apply_def2
         | simp add: schedule_choose_new_thread_def
         | wpc
         | rule hoare_pre_cont[where f=next_domain] )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace> schedule \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
ct_runnable <- return $ runnable ct_st;
action <- gets scheduler_action;
case action of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (ct_runnable \<or> ct = id);
return ()
od | switch_thread candidate \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if ct_runnable \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do when ct_runnable (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od
od \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace> proof (prove)
goal:
No subgoals!