SELFOUR-707: schedule highest priority thread on setPriority

proof/crefine/ARM/Tcb_C.thy

@@ -430,42 +430,30 @@ lemma setPriority_ccorres:
               (simp add: typ_heap_simps')+, simp_all?)[1]
         apply (rule ball_tcb_cte_casesI, simp+)
        apply (simp add: ctcb_relation_def cast_simps)
-       apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down)
       apply (ctac(no_vcg) add: isRunnable_ccorres)
-       apply (rule ccorres_split_nothrow_novcg_dc)
        apply (simp add: when_def to_bool_def del: Collect_const)
        apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem)
         apply (ctac add: tcbSchedEnqueue_ccorres)
-          apply (rule ccorres_return_Skip)
-         apply (rule ccorres_pre_getCurThread)
-         apply (simp add: when_def to_bool_def)
-         apply (rule_tac R="\<lambda>s. rvb = ksCurThread s"
-                    in ccorres_cond2)
-           apply (clarsimp simp: rf_sr_ksCurThread)
           apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def])
-         apply (rule ccorres_return_Skip')
-        apply simp
-        apply (wp hoare_drop_imps weak_sch_act_wf_lift_linear)
-       apply (simp add: guard_is_UNIV_def)
-      apply simp
          apply wp
-     apply simp
+        apply vcg
-     apply (rule_tac Q="\<lambda>rv s. valid_queues s \<and> valid_objs' s \<and> tcb_at' t s
+       apply (rule ccorres_return_Skip')
-                  \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
+      apply (wp isRunnable_wp)
-      apply (clarsimp simp: st_tcb_at'_def o_def valid_objs'_maxDomain
+     apply clarsimp
-                            valid_objs'_maxPriority
-                     split: if_splits)
      apply (wp hoare_drop_imps threadSet_valid_queues threadSet_valid_objs'
                weak_sch_act_wf_lift_linear threadSet_pred_tcb_at_state)
        apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits)
-     apply (wp threadSet_tcbDomain_triv)
+      apply (wpsimp wp: threadSet_tcbDomain_triv)
-     apply simp
+     apply (wp threadSet_valid_objs')
-    apply (simp add: guard_is_UNIV_def)+
+    apply (simp add: guard_is_UNIV_def)
-   apply (simp add: inQ_def pred_conj_def conj_comms)
+   apply (rule hoare_strengthen_post[where Q="\<lambda>rv s.
-   apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues)
+            obj_at' (\<lambda>_. True) t s \<and>
-    apply (rule hoare_strengthen_post,
+            Invariants_H.valid_queues s \<and>
-          rule tcbSchedDequeue_nonq[where t'=t])
+            valid_objs' s \<and>
-   apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
+            weak_sch_act_wf (ksSchedulerAction s) s \<and>
+            (\<forall>d p. \<not> t \<in> set (ksReadyQueues s (d, p)))"])
+    apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues tcbSchedDequeue_nonq)
+   apply (clarsimp simp: valid_tcb'_tcbPriority_update)
   apply (fastforce simp: invs'_def valid_state'_def
                          valid_objs'_maxDomain valid_objs'_maxPriority)
   done

proof/crefine/ARM_HYP/Tcb_C.thy

@@ -430,42 +430,30 @@ lemma setPriority_ccorres:
               (simp add: typ_heap_simps')+, simp_all?)[1]
         apply (rule ball_tcb_cte_casesI, simp+)
        apply (simp add: ctcb_relation_def cast_simps)
-       apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down)
       apply (ctac(no_vcg) add: isRunnable_ccorres)
-       apply (rule ccorres_split_nothrow_novcg_dc)
        apply (simp add: when_def to_bool_def del: Collect_const)
        apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem)
         apply (ctac add: tcbSchedEnqueue_ccorres)
-          apply (rule ccorres_return_Skip)
-         apply (rule ccorres_pre_getCurThread)
-         apply (simp add: when_def to_bool_def)
-         apply (rule_tac R="\<lambda>s. rvb = ksCurThread s"
-                    in ccorres_cond2)
-           apply (clarsimp simp: rf_sr_ksCurThread)
           apply (ctac add: rescheduleRequired_ccorres[unfolded dc_def])
-         apply (rule ccorres_return_Skip')
-        apply simp
-        apply (wp hoare_drop_imps weak_sch_act_wf_lift_linear)
-       apply (simp add: guard_is_UNIV_def)
-      apply simp
          apply wp
-     apply simp
+        apply vcg
-     apply (rule_tac Q="\<lambda>rv s. valid_queues s \<and> valid_objs' s \<and> tcb_at' t s
+       apply (rule ccorres_return_Skip')
-                  \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp)
+      apply (wp isRunnable_wp)
-      apply (clarsimp simp: st_tcb_at'_def o_def valid_objs'_maxDomain
+     apply clarsimp
-                            valid_objs'_maxPriority
-                     split: if_splits)
      apply (wp hoare_drop_imps threadSet_valid_queues threadSet_valid_objs'
                weak_sch_act_wf_lift_linear threadSet_pred_tcb_at_state)
        apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits)
-     apply (wp threadSet_tcbDomain_triv)
+      apply (wpsimp wp: threadSet_tcbDomain_triv)
-     apply simp
+     apply (wp threadSet_valid_objs')
-    apply (simp add: guard_is_UNIV_def)+
+    apply (simp add: guard_is_UNIV_def)
-   apply (simp add: inQ_def pred_conj_def conj_comms)
+   apply (rule hoare_strengthen_post[where Q="\<lambda>rv s.
-   apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues)
+            obj_at' (\<lambda>_. True) t s \<and>
-    apply (rule hoare_strengthen_post,
+            Invariants_H.valid_queues s \<and>
-          rule tcbSchedDequeue_nonq[where t'=t])
+            valid_objs' s \<and>
-   apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def)
+            weak_sch_act_wf (ksSchedulerAction s) s \<and>
+            (\<forall>d p. \<not> t \<in> set (ksReadyQueues s (d, p)))"])
+    apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues tcbSchedDequeue_nonq)
+   apply (clarsimp simp: valid_tcb'_tcbPriority_update)
   apply (fastforce simp: invs'_def valid_state'_def
                          valid_objs'_maxDomain valid_objs'_maxPriority)
   done

proof/refine/ARM/Tcb_R.thy

@@ -644,8 +644,9 @@ lemma sp_corres2:
     apply (rule corres_split [OF _ tcbSchedDequeue_corres])
       apply (rule corres_split [OF _ ethread_set_corres], simp_all)[1]
          apply (rule corres_split [OF _ gts_isRunnable_corres])
-           apply (rule corres_split [OF _ corres_when[OF _ tcbSchedEnqueue_corres]])
+           apply (erule corres_when)
-              apply (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_corres])
+           apply (rule corres_split [OF _ tcbSchedEnqueue_corres])
+             apply (rule rescheduleRequired_corres)
             apply (wp hoare_vcg_imp_lift hoare_vcg_if_lift hoare_vcg_all_lift hoare_vcg_disj_lift
                       gts_wp isRunnable_wp threadSet_pred_tcb_no_state threadSet_valid_queues_no_state
                       threadSet_valid_queues'_no_state threadSet_valid_objs_tcbPriority_update threadSet_weak_sch_act_wf
@@ -791,29 +792,16 @@ lemma tcbPriority_Queued_caps_safe:
 
 lemma setP_invs':
   "\<lbrace>invs' and tcb_at' t and K (p \<le> maxPriority)\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace>"
-proof -
-  have enq: "\<And>s'. t \<noteq> ksCurThread s' \<Longrightarrow>
-            \<lbrace>(op = s') and invs' and st_tcb_at' runnable' t\<rbrace>
-             tcbSchedEnqueue t \<lbrace>\<lambda>_. invs'\<rbrace>"
-    by (wp, clarsimp)
-  show ?thesis
   including no_pre
   apply (rule hoare_gen_asm)
   apply (simp add: setPriority_def)
   apply (wp rescheduleRequired_all_invs_but_ct_not_inQ)
-     apply (wps tcbSchedEnqueue_ct')
-     apply (case_tac "t \<noteq> ksCurThread prev_s")
-      apply (clarsimp, erule enq)
-     apply (clarsimp simp add: invs'_def valid_state'_def)
      apply (wp valid_irq_node_lift, clarsimp+)
-         apply (erule(1) st_tcb_ex_cap'')
-         apply (case_tac st, clarsimp+)[1]
-        apply (clarsimp)+
     apply (rule_tac Q="\<lambda>r s. (r \<longrightarrow> st_tcb_at' runnable' t s) \<and> invs' s"
-             in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def)
+             in hoare_post_imp)
-    apply (wp)
+     apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'')
-   apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp,
+     apply (case_tac st; clarsimp)
-          clarsimp simp: pred_tcb_at'_def comp_def)
+    apply (wp, simp)
    apply (wp threadSet_invs_trivial,
           simp_all add: inQ_def cong: conj_cong)
   apply (rule_tac Q="\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t
@@ -823,7 +811,6 @@ proof -
   apply (wp tcbSchedDequeue_not_queued)+
     apply (clarsimp)+
   done
-qed
 
 crunch typ_at'[wp]: setPriority, setMCPriority "\<lambda>s. P (typ_at' T p s)"
   (ignore: getObject simp: crunch_simps)

proof/refine/ARM_HYP/Tcb_R.thy

@@ -636,8 +636,9 @@ lemma sp_corres2:
     apply (rule corres_split [OF _ tcbSchedDequeue_corres])
       apply (rule corres_split [OF _ ethread_set_corres], simp_all)[1]
          apply (rule corres_split [OF _ gts_isRunnable_corres])
-           apply (rule corres_split [OF _ corres_when[OF _ tcbSchedEnqueue_corres]])
+           apply (erule corres_when)
-              apply (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_corres])
+           apply (rule corres_split [OF _ tcbSchedEnqueue_corres])
+             apply (rule rescheduleRequired_corres)
             apply (wp hoare_vcg_imp_lift hoare_vcg_if_lift hoare_vcg_all_lift hoare_vcg_disj_lift
                       gts_wp isRunnable_wp threadSet_pred_tcb_no_state threadSet_valid_queues_no_state
                       threadSet_valid_queues'_no_state threadSet_valid_objs_tcbPriority_update threadSet_weak_sch_act_wf
@@ -784,29 +785,16 @@ lemma tcbPriority_Queued_caps_safe:
 
 lemma setP_invs':
   "\<lbrace>invs' and tcb_at' t and K (p \<le> maxPriority)\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace>"
-proof -
-  have enq: "\<And>s'. t \<noteq> ksCurThread s' \<Longrightarrow>
-            \<lbrace>(op = s') and invs' and st_tcb_at' runnable' t\<rbrace>
-             tcbSchedEnqueue t \<lbrace>\<lambda>_. invs'\<rbrace>"
-    by (wp, clarsimp)
-  show ?thesis
   including no_pre
   apply (rule hoare_gen_asm)
   apply (simp add: setPriority_def)
   apply (wp rescheduleRequired_all_invs_but_ct_not_inQ)
-     apply (wps tcbSchedEnqueue_ct')
-     apply (case_tac "t \<noteq> ksCurThread prev_s")
-      apply (clarsimp, erule enq)
-     apply (clarsimp simp add: invs'_def valid_state'_def)
      apply (wp valid_irq_node_lift, clarsimp+)
-         apply (erule(1) st_tcb_ex_cap'')
-         apply (case_tac st, clarsimp+)[1]
-        apply (clarsimp)+
     apply (rule_tac Q="\<lambda>r s. (r \<longrightarrow> st_tcb_at' runnable' t s) \<and> invs' s"
-             in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def)
+             in hoare_post_imp)
-    apply (wp)
+     apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'')
-   apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp,
+     apply (case_tac st; clarsimp)
-          clarsimp simp: pred_tcb_at'_def comp_def)
+    apply (wp, simp)
    apply (wp threadSet_invs_trivial,
           simp_all add: inQ_def cong: conj_cong)
   apply (rule_tac Q="\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t
@@ -816,7 +804,6 @@ proof -
   apply (wp tcbSchedDequeue_not_queued)+
     apply (clarsimp)+
   done
-qed
 
 crunch typ_at'[wp]: setPriority, setMCPriority "\<lambda>s. P (typ_at' T p s)"
   (ignore: getObject simp: crunch_simps)

proof/refine/X64/Tcb_R.thy

@@ -647,8 +647,9 @@ lemma sp_corres2:
     apply (rule corres_split [OF _ tcbSchedDequeue_corres])
       apply (rule corres_split [OF _ ethread_set_corres], simp_all)[1]
          apply (rule corres_split [OF _ gts_isRunnable_corres])
-           apply (rule corres_split [OF _ corres_when[OF _ tcbSchedEnqueue_corres]])
+           apply (erule corres_when)
-              apply (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_corres])
+           apply (rule corres_split [OF _ tcbSchedEnqueue_corres])
+             apply (rule rescheduleRequired_corres)
             apply (wp hoare_vcg_imp_lift hoare_vcg_if_lift hoare_vcg_all_lift hoare_vcg_disj_lift
                       gts_wp isRunnable_wp threadSet_pred_tcb_no_state threadSet_valid_queues_no_state
                       threadSet_valid_queues'_no_state threadSet_valid_objs_tcbPriority_update threadSet_weak_sch_act_wf
@@ -794,29 +795,16 @@ lemma tcbPriority_Queued_caps_safe:
 
 lemma setP_invs':
   "\<lbrace>invs' and tcb_at' t and K (p \<le> maxPriority)\<rbrace> setPriority t p \<lbrace>\<lambda>rv. invs'\<rbrace>"
-proof -
-  have enq: "\<And>s'. t \<noteq> ksCurThread s' \<Longrightarrow>
-            \<lbrace>(op = s') and invs' and st_tcb_at' runnable' t\<rbrace>
-             tcbSchedEnqueue t \<lbrace>\<lambda>_. invs'\<rbrace>"
-    by (wp, clarsimp)
-  show ?thesis
   including no_pre
   apply (rule hoare_gen_asm)
   apply (simp add: setPriority_def)
   apply (wp rescheduleRequired_all_invs_but_ct_not_inQ)
-     apply (wps tcbSchedEnqueue_ct')
-     apply (case_tac "t \<noteq> ksCurThread prev_s")
-      apply (clarsimp, erule enq)
-     apply (clarsimp simp add: invs'_def valid_state'_def)
      apply (wp valid_irq_node_lift, clarsimp+)
-         apply (erule(1) st_tcb_ex_cap'')
-         apply (case_tac st, clarsimp+)[1]
-        apply (clarsimp)+
     apply (rule_tac Q="\<lambda>r s. (r \<longrightarrow> st_tcb_at' runnable' t s) \<and> invs' s"
-             in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def)
+             in hoare_post_imp)
-    apply (wp)
+     apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'')
-   apply (rule_tac Q="\<lambda>_. invs'" in hoare_post_imp,
+     apply (case_tac st; clarsimp)
-          clarsimp simp: pred_tcb_at'_def comp_def)
+    apply (wp, simp)
    apply (wp threadSet_invs_trivial,
           simp_all add: inQ_def cong: conj_cong)
   apply (rule_tac Q="\<lambda>_. invs' and obj_at' (Not \<circ> tcbQueued) t
@@ -826,7 +814,6 @@ proof -
   apply (wp tcbSchedDequeue_not_queued)+
     apply (clarsimp)+
   done
-qed
 
 crunch typ_at'[wp]: setPriority, setMCPriority "\<lambda>s. P (typ_at' T p s)"
   (ignore: getObject simp: crunch_simps)

spec/abstract/KHeap_A.thy

@@ -127,9 +127,10 @@ definition
      tcb_sched_action tcb_sched_dequeue tptr;
      thread_set_priority tptr prio;
      ts \<leftarrow> get_thread_state tptr;
-     when (runnable ts) $ tcb_sched_action tcb_sched_enqueue tptr;
+     when (runnable ts) $ do
-     cur \<leftarrow> gets cur_thread;
+       tcb_sched_action tcb_sched_enqueue tptr;
-     when (tptr = cur) reschedule_required
+       reschedule_required
+     od
    od"
 
 definition

spec/haskell/src/SEL4/Kernel/Thread.lhs

@@ -466,16 +466,14 @@ Then, the new priority can be set.
 
 >         threadSet (\t -> t { tcbPriority = prio }) tptr
 
-If the thread is runnable, it is enqueued at the new priority.
+If the thread is runnable, it is enqueued at the new priority. Furthermore,
+since the thread may now be the highest priority thread, we run the scheduler
+to choose a new thread.
 
 >         runnable <- isRunnable tptr
->         when runnable $ tcbSchedEnqueue tptr
+>         when runnable $ do
-
+>             tcbSchedEnqueue tptr
-Finally, if the thread is the current one, we run the scheduler to choose a new thread.
+>             rescheduleRequired
-
->         curThread <- getCurThread
->         when (tptr == curThread) $ rescheduleRequired
-
 
 \subsubsection{Switching to Woken Threads}