From 995b88cefa4ce403669ab245eb7a91936092f942 Mon Sep 17 00:00:00 2001 From: Michael Sproul Date: Mon, 15 Jan 2018 17:31:54 +1100 Subject: [PATCH] SELFOUR-707: schedule highest priority thread on setPriority --- proof/crefine/ARM/Tcb_C.thy | 56 ++++++++++--------------- proof/crefine/ARM_HYP/Tcb_C.thy | 56 ++++++++++--------------- proof/refine/ARM/Tcb_R.thy | 39 ++++++----------- proof/refine/ARM_HYP/Tcb_R.thy | 39 ++++++----------- proof/refine/X64/Tcb_R.thy | 39 ++++++----------- spec/abstract/KHeap_A.thy | 7 ++-- spec/haskell/src/SEL4/Kernel/Thread.lhs | 14 +++---- 7 files changed, 93 insertions(+), 157 deletions(-) diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index eaa1b904b..3b8bd1085 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -430,44 +430,32 @@ 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=\], 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="\s. rvb = ksCurThread s" - in ccorres_cond2) - apply (clarsimp simp: rf_sr_ksCurThread) + apply (simp add: when_def to_bool_def del: Collect_const) + apply (rule ccorres_cond2[where R=\], simp add: Collect_const_mem) + apply (ctac add: tcbSchedEnqueue_ccorres) 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 (rule_tac Q="\rv s. valid_queues s \ valid_objs' s \ tcb_at' t s - \ weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) - apply (clarsimp simp: st_tcb_at'_def o_def valid_objs'_maxDomain - valid_objs'_maxPriority - split: if_splits) + apply wp + apply vcg + apply (rule ccorres_return_Skip') + apply (wp isRunnable_wp) + apply clarsimp 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 simp - apply (simp add: guard_is_UNIV_def)+ - apply (simp add: inQ_def pred_conj_def conj_comms) - apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) - apply (rule hoare_strengthen_post, - rule tcbSchedDequeue_nonq[where t'=t]) - apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) - apply (fastforce simp: invs'_def valid_state'_def - valid_objs'_maxDomain valid_objs'_maxPriority) + apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits) + apply (wpsimp wp: threadSet_tcbDomain_triv) + apply (wp threadSet_valid_objs') + apply (simp add: guard_is_UNIV_def) + apply (rule hoare_strengthen_post[where Q="\rv s. + obj_at' (\_. True) t s \ + Invariants_H.valid_queues s \ + valid_objs' s \ + weak_sch_act_wf (ksSchedulerAction s) s \ + (\d p. \ t \ 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 lemma setMCPriority_ccorres: diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index d71177f51..1ebb07dbe 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -430,44 +430,32 @@ 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=\], 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="\s. rvb = ksCurThread s" - in ccorres_cond2) - apply (clarsimp simp: rf_sr_ksCurThread) + apply (simp add: when_def to_bool_def del: Collect_const) + apply (rule ccorres_cond2[where R=\], simp add: Collect_const_mem) + apply (ctac add: tcbSchedEnqueue_ccorres) 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 (rule_tac Q="\rv s. valid_queues s \ valid_objs' s \ tcb_at' t s - \ weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) - apply (clarsimp simp: st_tcb_at'_def o_def valid_objs'_maxDomain - valid_objs'_maxPriority - split: if_splits) + apply wp + apply vcg + apply (rule ccorres_return_Skip') + apply (wp isRunnable_wp) + apply clarsimp 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 simp - apply (simp add: guard_is_UNIV_def)+ - apply (simp add: inQ_def pred_conj_def conj_comms) - apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) - apply (rule hoare_strengthen_post, - rule tcbSchedDequeue_nonq[where t'=t]) - apply (clarsimp simp: valid_tcb'_def tcb_cte_cases_def) - apply (fastforce simp: invs'_def valid_state'_def - valid_objs'_maxDomain valid_objs'_maxPriority) + apply (clarsimp simp: st_tcb_at'_def o_def split: if_splits) + apply (wpsimp wp: threadSet_tcbDomain_triv) + apply (wp threadSet_valid_objs') + apply (simp add: guard_is_UNIV_def) + apply (rule hoare_strengthen_post[where Q="\rv s. + obj_at' (\_. True) t s \ + Invariants_H.valid_queues s \ + valid_objs' s \ + weak_sch_act_wf (ksSchedulerAction s) s \ + (\d p. \ t \ 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 lemma setMCPriority_ccorres: diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 58b563744..12af21e44 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -644,14 +644,15 @@ 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 (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_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 - tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] - tcbSchedDequeue_valid_queues - tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ + apply (erule corres_when) + 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 + tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] + tcbSchedDequeue_valid_queues + tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ apply (force simp: valid_etcbs_def tcb_at_st_tcb_at[symmetric] state_relation_def dest: pspace_relation_tcb_at) apply (force simp: state_relation_def elim: valid_objs'_maxDomain valid_objs'_maxPriority) @@ -791,29 +792,16 @@ lemma tcbPriority_Queued_caps_safe: lemma setP_invs': "\invs' and tcb_at' t and K (p \ maxPriority)\ setPriority t p \\rv. invs'\" -proof - - have enq: "\s'. t \ ksCurThread s' \ - \(op = s') and invs' and st_tcb_at' runnable' t\ - tcbSchedEnqueue t \\_. invs'\" - 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 \ 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="\r s. (r \ st_tcb_at' runnable' t s) \ invs' s" - in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def) - apply (wp) - apply (rule_tac Q="\_. invs'" in hoare_post_imp, - clarsimp simp: pred_tcb_at'_def comp_def) + in hoare_post_imp) + apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'') + apply (case_tac st; clarsimp) + apply (wp, simp) apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) apply (rule_tac Q="\_. invs' and obj_at' (Not \ tcbQueued) t @@ -823,7 +811,6 @@ proof - apply (wp tcbSchedDequeue_not_queued)+ apply (clarsimp)+ done -qed crunch typ_at'[wp]: setPriority, setMCPriority "\s. P (typ_at' T p s)" (ignore: getObject simp: crunch_simps) diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 3bcaf5963..75111aca8 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -636,14 +636,15 @@ 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 (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_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 - tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] - tcbSchedDequeue_valid_queues - tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ + apply (erule corres_when) + 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 + tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] + tcbSchedDequeue_valid_queues + tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ apply (force simp: valid_etcbs_def tcb_at_st_tcb_at[symmetric] state_relation_def dest: pspace_relation_tcb_at) apply (force simp: state_relation_def elim: valid_objs'_maxDomain valid_objs'_maxPriority) @@ -784,29 +785,16 @@ lemma tcbPriority_Queued_caps_safe: lemma setP_invs': "\invs' and tcb_at' t and K (p \ maxPriority)\ setPriority t p \\rv. invs'\" -proof - - have enq: "\s'. t \ ksCurThread s' \ - \(op = s') and invs' and st_tcb_at' runnable' t\ - tcbSchedEnqueue t \\_. invs'\" - 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 \ 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="\r s. (r \ st_tcb_at' runnable' t s) \ invs' s" - in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def) - apply (wp) - apply (rule_tac Q="\_. invs'" in hoare_post_imp, - clarsimp simp: pred_tcb_at'_def comp_def) + in hoare_post_imp) + apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'') + apply (case_tac st; clarsimp) + apply (wp, simp) apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) apply (rule_tac Q="\_. invs' and obj_at' (Not \ tcbQueued) t @@ -816,7 +804,6 @@ proof - apply (wp tcbSchedDequeue_not_queued)+ apply (clarsimp)+ done -qed crunch typ_at'[wp]: setPriority, setMCPriority "\s. P (typ_at' T p s)" (ignore: getObject simp: crunch_simps) diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 41c148495..1bb78ecdb 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -647,14 +647,15 @@ 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 (rule corres_split [OF corres_when[OF _ rescheduleRequired_corres] gct_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 - tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] - tcbSchedDequeue_valid_queues - tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ + apply (erule corres_when) + 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 + tcbSchedDequeue_not_in_queue threadSet_ct_in_state'[simplified ct_in_state'_def] + tcbSchedDequeue_valid_queues + tcbSchedDequeue_ct_in_state'[simplified ct_in_state'_def] | simp add: etcb_relation_def)+ apply (force simp: valid_etcbs_def tcb_at_st_tcb_at[symmetric] state_relation_def dest: pspace_relation_tcb_at) apply (force simp: state_relation_def elim: valid_objs'_maxDomain valid_objs'_maxPriority) @@ -794,29 +795,16 @@ lemma tcbPriority_Queued_caps_safe: lemma setP_invs': "\invs' and tcb_at' t and K (p \ maxPriority)\ setPriority t p \\rv. invs'\" -proof - - have enq: "\s'. t \ ksCurThread s' \ - \(op = s') and invs' and st_tcb_at' runnable' t\ - tcbSchedEnqueue t \\_. invs'\" - 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 \ 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="\r s. (r \ st_tcb_at' runnable' t s) \ invs' s" - in hoare_post_imp, clarsimp simp: invs'_def valid_state'_def) - apply (wp) - apply (rule_tac Q="\_. invs'" in hoare_post_imp, - clarsimp simp: pred_tcb_at'_def comp_def) + in hoare_post_imp) + apply (clarsimp simp: invs'_def valid_state'_def invs_valid_objs' elim!: st_tcb_ex_cap'') + apply (case_tac st; clarsimp) + apply (wp, simp) apply (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) apply (rule_tac Q="\_. invs' and obj_at' (Not \ tcbQueued) t @@ -826,7 +814,6 @@ proof - apply (wp tcbSchedDequeue_not_queued)+ apply (clarsimp)+ done -qed crunch typ_at'[wp]: setPriority, setMCPriority "\s. P (typ_at' T p s)" (ignore: getObject simp: crunch_simps) diff --git a/spec/abstract/KHeap_A.thy b/spec/abstract/KHeap_A.thy index a09599ced..b3ef65990 100644 --- a/spec/abstract/KHeap_A.thy +++ b/spec/abstract/KHeap_A.thy @@ -127,9 +127,10 @@ definition tcb_sched_action tcb_sched_dequeue tptr; thread_set_priority tptr prio; ts \ get_thread_state tptr; - when (runnable ts) $ tcb_sched_action tcb_sched_enqueue tptr; - cur \ gets cur_thread; - when (tptr = cur) reschedule_required + when (runnable ts) $ do + tcb_sched_action tcb_sched_enqueue tptr; + reschedule_required + od od" definition diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index 747dd7292..20b62dca6 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/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 - -Finally, if the thread is the current one, we run the scheduler to choose a new thread. - -> curThread <- getCurThread -> when (tptr == curThread) $ rescheduleRequired - +> when runnable $ do +> tcbSchedEnqueue tptr +> rescheduleRequired \subsubsection{Switching to Woken Threads}