Repair schedule_bcorres.

This was broken a long while back because arch_switch_to_idle_thread
might sometimes be skipped in the implementation if the idle thread
was previously scheduled. Putting the same behaviour in the most
abstract (unit) specification is pretty easy, and it's not clear why
it wasn't done earlier.

proof/drefine/Ipc_DR.thy

@@ -2687,7 +2687,7 @@ lemma send_sync_ipc_corres:
       apply (rule corres_split[OF corres_dummy_set_sync_ep set_thread_state_block_on_send_corres])
        apply wp
      apply simp
-    apply (wp|clarsimp simp: split del:if_splits)+
+    apply (wp TrueI |clarsimp simp: split del:if_splits)+
 (* SendEP *)
    apply (subst ep_waiting_set_recv_lift)
     apply (simp add:valid_state_def)
@@ -2698,7 +2698,7 @@ lemma send_sync_ipc_corres:
       apply (rule corres_split[OF corres_dummy_set_sync_ep set_thread_state_block_on_send_corres])
        apply wp
      apply simp
-    apply (wp|clarsimp simp: split del:if_splits)+
+    apply (wp TrueI|clarsimp simp: split del:if_splits)+
 (* RecvEP *)
   apply (subst ep_waiting_set_recv_lift,simp add:valid_state_def)
   apply simp

proof/invariant-abstract/BCorres2_AI.thy

@@ -448,113 +448,99 @@ lemma truncate_state_updates[simp]:
   "truncate_state (ready_queues_update g s) = truncate_state s"
   by (rule trans_state_update'')+
 
-(* the old schedule unit def no longer is a refinement of the det_ext def.
+lemma get_before_assert_opt:
-
+  "do s \<leftarrow> assert_opt x; s' \<leftarrow> get; f s s' od
-   if sched_act = resume_cur_thread and cur_thread = idle_thread,
+    = do s' \<leftarrow> get; s \<leftarrow> assert_opt x; f s s' od"
-     then there should be a path through schedule_unit which corresponds to a return().
+  apply (cases x, simp_all add: assert_opt_def)
-   This used to be via switch_to_idle_thread, but now switch_to_idle_thread updates
+  apply (simp add: ext exec_get)
-     arm_globals_frame, so is no longer a return in this case. *)
+  done
-
+
-(*The only nontrivial bcorres result. Since we don't have
+lemma s_bcorres_get_left:
-  a proper calculus we just unfold everything. The refinement
+  "(s_bcorres_underlying t (get >>= f) g s)
-  is made guard-less by asserting that we only switch to
+    = (s_bcorres_underlying t (f s) g s)"
-  runnable threads inside of the deterministic scheduler
+  by (simp add: s_bcorres_underlying_def exec_get)
-  (guaranteed by valid_sched) *)
+
-(*
+lemma get_outside_alternative:
-lemma schedule_bcorres[wp]: "bcorres (schedule :: (unit,det_ext) s_monad) schedule"
+  "alternative (get >>= f) g
-
+    = do s \<leftarrow> get; alternative (f s) g od"
-  apply (simp add: schedule_def)
+  by (simp add: alternative_def exec_get fun_eq_iff)
-  apply (clarsimp simp add: schedule_def gets_def bind_def get_def
+
-                            return_def s_bcorres_underlying_def
+(* FIXME: is this acceptable arch split? *)
-                            allActiveTCBs_def bcorres_underlying_def
+context Arch begin
-                            select_def getActiveTCB_def
+crunch (bcorres)bcorres[wp]: switch_to_thread,switch_to_idle_thread truncate_state
-                            get_thread_state_def thread_get_def
+end
-                            gets_the_def assert_opt_def fail_def
+lemmas switch_to_thread_bcorres
-                            )
+    = Arch.switch_to_thread_bcorres Arch.switch_to_idle_thread_bcorres
-  apply (case_tac "get_tcb (cur_thread s) s",simp_all)
+
-  apply (case_tac "scheduler_action bb",simp_all add: in_monad)
+lemmas schedule_unfold_all = schedule_def allActiveTCBs_def
-  apply (case_tac "runnable (tcb_state aa)")
+                        get_thread_state_def thread_get_def getActiveTCB_def
-    apply (rule alternative_first)
+
-    apply (clarsimp)
+lemma guarded_switch_bcorres: "s_bcorres (guarded_switch_to t) schedule s"
-    apply (rule_tac x="cur_thread s" in exI)
+  using switch_to_thread_bcorres(1)[where param_a=t]
-    apply clarsimp
+  apply (clarsimp simp: schedule_unfold_all s_bcorres_underlying_def
-    apply (rule alternative_first)
+                        in_monad in_select
-    apply clarsimp+
+            split del: if_split)
-   apply (rule alternative_second)
+  apply (drule guarded_sub_switch)
-   apply (simp add: switch_to_idle_thread_def bind_def
+  apply (rule_tac x=t in exI, clarsimp split del: if_split)
-                    gets_def get_def return_def arch_switch_to_idle_thread_def
+  apply (drule_tac s=s in drop_sbcorres_underlying)
-                    in_monad)
+  apply (clarsimp simp: s_bcorres_underlying_def)
-   apply (case_tac "runnable (tcb_state aa)")
+  apply (auto intro!: alternative_second)
-    apply clarsimp
+  done
-    apply (drule tcb_sched_action_extended.ex_st set_scheduler_action_extended.ex_st)+
+
-    apply clarsimp
+lemma choose_thread_bcorres: "s_bcorres choose_thread schedule s"
-    apply (drule bcorres_underlying_dest[OF guarded_switch_to_bcorres])
+  using switch_to_thread_bcorres(2)
-    apply (drule guarded_sub_switch,clarsimp)
+  apply (simp add: choose_thread_def gets_def s_bcorres_get_left
-    apply (rule alternative_first)
+                   guarded_switch_bcorres)
-    apply clarsimp
+  apply (clarsimp simp: schedule_def s_bcorres_underlying_def)
-    apply (rule_tac x=word in exI)
+  apply (drule_tac s=s in drop_sbcorres_underlying)
-    apply (intro conjI impI)
+  apply (clarsimp simp: s_bcorres_underlying_def)
-      apply (rule alternative_second)
+  apply (auto intro!: alternative_second simp: exec_gets)
-
+  done
-      apply simp
+
-     apply (rule_tac x=y in exI)
+lemma tcb_sched_action_bcorres:
-     apply clarsimp
+  "bcorres (tcb_sched_action a b) (return ())"
-    apply simp
+  by (clarsimp simp: bcorres_underlying_def s_bcorres_underlying_def return_def
-   apply clarsimp
+              dest!: tcb_sched_action_extended.ex_st)
-   apply (drule set_scheduler_action_extended.ex_st)+
+
-   apply clarsimp
+lemma schedule_bcorres[wp]: "bcorres (schedule :: (unit,det_ext) s_monad) schedule"
-   apply (drule bcorres_underlying_dest[OF guarded_switch_to_bcorres])
+  apply (clarsimp simp: bcorres_underlying_def)
-   apply (drule guarded_sub_switch,clarsimp)
+  apply (simp add: schedule_det_ext_ext_def s_bcorres_get_left
-   apply (rule alternative_first)
+                   gets_def get_thread_state_def thread_get_def gets_the_def
-   apply clarsimp
+                   bind_assoc get_before_assert_opt)
-   apply (rule_tac x=word in exI)
+  apply (simp add: assert_opt_def)
-   apply clarsimp
+  apply (split option.split, simp, intro conjI impI)
-  apply clarsimp
+   apply (simp add: s_bcorres_underlying_def fail_def)
-  apply (case_tac "runnable (tcb_state aa)")
+  apply clarsimp
-   apply clarsimp
+  apply (split scheduler_action.split, intro conjI impI)
-   apply (subgoal_tac "\<exists>e. s''a = trans_state (\<lambda>_. e) s''")
+    (* resume current *)
-    prefer 2
+    apply (clarsimp simp: s_bcorres_underlying_def schedule_def allActiveTCBs_def
-    apply (erule impCE)
+                          in_monad in_select getActiveTCB_def)
-     apply (rule_tac x="exst s''" in exI)
+    apply (erule disjE)
-     apply simp
+     apply fastforce
-    apply (erule next_domain_extended.ex_st)
+    apply (simp add: switch_to_idle_thread_def in_monad in_select
-   apply (drule tcb_sched_action_extended.ex_st set_scheduler_action_extended.ex_st)+
+                     ex_bool_eq)
-   apply clarsimp
+   (* switch to *)
-   apply (drule choose_switch_or_idle)
+   apply clarsimp
-   apply (elim exE disjE)
+   apply (rule s_bcorres_underlying_split[where g'="\<lambda>_. return ()",
-    apply (drule bcorres_underlying_dest[OF guarded_switch_to_bcorres])
+                OF _ guarded_switch_bcorres, simplified]
-    apply (drule guarded_sub_switch,clarsimp)
+      s_bcorres_underlying_split[where f'="return ()", simplified])+
-    apply (rule alternative_first)
+    apply (simp add: s_bcorres_underlying_def set_scheduler_action_def
-    apply simp
+                     simpler_modify_def return_def)
-    apply (rule_tac x=word in exI)
+   apply (clarsimp simp: when_def return_s_bcorres_underlying
-    apply clarsimp
+                         tcb_sched_action_bcorres drop_sbcorres_underlying)
-    apply (rule alternative_second)
+
-    apply clarsimp
+  (* choose *)
-   apply (drule bcorres_underlying_dest[OF switch_to_idle_thread_bcorres])
+  apply simp
-   apply simp
+  apply (rule s_bcorres_underlying_split[where g'="\<lambda>_. return ()",
-   apply (rule alternative_second)
+                OF _ choose_thread_bcorres, simplified]
-   apply simp
+     s_bcorres_underlying_split[where f'="return ()", simplified]
-  apply clarsimp
+    | subst bind_assoc[symmetric])+
-  apply (drule set_scheduler_action_extended.ex_st)+
+    apply (simp add: s_bcorres_underlying_def set_scheduler_action_def
-  apply (subgoal_tac "\<exists>e. s''a = trans_state (\<lambda>_. e) s")
+                     simpler_modify_def return_def)
-   prefer 2
+   apply (simp add: s_bcorres_underlying_def when_def exec_gets
-   apply (erule impCE)
+                    next_domain_def Let_def simpler_modify_def return_def)
-    apply (rule_tac x="exst s" in exI)
+  apply (clarsimp simp: when_def return_s_bcorres_underlying
-    apply simp
+                        tcb_sched_action_bcorres drop_sbcorres_underlying)
-   apply (erule next_domain_extended.ex_st)
-  apply clarsimp
-  apply (drule choose_switch_or_idle)
-  apply (elim exE disjE)
-   apply (drule bcorres_underlying_dest[OF guarded_switch_to_bcorres])
-   apply (drule guarded_sub_switch,clarsimp)
-   apply (rule alternative_first)
-   apply clarsimp
-   apply (rule_tac x="word" in exI)
-   apply clarsimp
-  apply (rule alternative_second)
-  apply (drule bcorres_underlying_dest[OF switch_to_idle_thread_bcorres])
-  apply simp
   done
-*)
 
 end

proof/invariant-abstract/EmptyFail_AI.thy

@@ -421,9 +421,7 @@ context EmptyFail_AI_schedule_unit begin
 lemma schedule_empty_fail[wp]:
   "empty_fail (schedule :: (unit,unit) s_monad)"
   apply (simp add: schedule_def)
-  apply wp
+  apply (wp disjI2)
-  apply (rule disjI2)
-   apply wp
   done
 
 end

proof/invariant-abstract/Schedule_AI.thy

@@ -198,11 +198,15 @@ lemma (in Schedule_AI_U) schedule_ct_activateable[wp]:
   proof -
   have P: "\<And>t s. ct_in_state activatable (cur_thread_update (\<lambda>_. t) s) = st_tcb_at activatable t s"
     by (fastforce simp: ct_in_state_def pred_tcb_at_def intro: obj_at_pspaceI)
+  have Q: "\<And>s. invs s \<longrightarrow> idle_thread s = cur_thread s \<longrightarrow> ct_in_state activatable s"
+    apply (clarsimp simp: ct_in_state_def dest!: invs_valid_idle)
+    apply (clarsimp simp: valid_idle_def pred_tcb_def2)
+    done
   show ?thesis
     apply (simp add: Schedule_A.schedule_def allActiveTCBs_def)
     apply (wp alternative_wp
               select_ext_weak_wp select_wp stt_activatable stit_activatable
-               | simp add: P)+
+               | simp add: P Q)+
     apply (clarsimp simp: getActiveTCB_def ct_in_state_def)
     apply (rule conjI)
      apply clarsimp

spec/abstract/Schedule_A.thy

@@ -124,19 +124,27 @@ text {*
   The scheduler is heavily underspecified.
   It is allowed to pick any active thread or the idle thread.
   If the thread the scheduler picked is the current thread, it
-  may omit the call to @{const switch_to_thread}.
+  may omit the call to @{const switch_to_thread}. Likewise it
+  may omit the call to @{const switch_to_idle_thread} if the
+  idle thread is the current thread.
 *}
 definition schedule_unit :: "(unit,unit) s_monad" where
-"schedule_unit \<equiv> do
+"schedule_unit \<equiv> (do
    cur \<leftarrow> gets cur_thread;
    threads \<leftarrow> allActiveTCBs;
    thread \<leftarrow> select threads;
-     if thread = cur then
+   (if thread = cur then
-     return () OR switch_to_thread thread
+     return () \<sqinter> switch_to_thread thread
    else
-     switch_to_thread thread
+     switch_to_thread thread)
- od OR
+ od) \<sqinter>
- switch_to_idle_thread"
+ (do
+   cur \<leftarrow> gets cur_thread;
+   idl \<leftarrow> gets idle_thread;
+   if idl = cur then
+     return () \<sqinter> switch_to_idle_thread
+   else switch_to_idle_thread
+  od)"
 
 instance ..
 end