diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index 9c9dd67b70..8fb94b9f6c 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -3114,7 +3114,8 @@ lemma tcbReleaseRemove_tcbSchedNext_tcbSchedPrev_None: tcbReleaseRemove t \\_. obj_at' (\tcb. tcbSchedNext tcb = None \ tcbSchedPrev tcb = None) t\" apply (clarsimp simp: tcbReleaseRemove_def) - apply (wpsimp wp: tcbQueueRemove_tcbSchedNext_tcbSchedPrev_None inReleaseQueue_wp) + apply (wpsimp wp: tcbQueueRemove_tcbSchedNext_tcbSchedPrev_None inReleaseQueue_wp + hoare_vcg_ex_lift threadSet_sched_pointers) apply (clarsimp simp: valid_sched_pointers_def) apply (drule_tac x=t in spec) apply (fastforce simp: ksReleaseQueue_asrt_def opt_pred_def obj_at'_def opt_map_def) diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index 3d679ec8b7..8023742bf6 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -3225,7 +3225,7 @@ lemma tcbSchedEnqueue_unlive_other: tcbSchedEnqueue t \\_. ko_wp_at' (Not \ live') p\" apply (simp add: tcbSchedEnqueue_def tcbQueuePrepend_def) - apply (wpsimp wp: threadGet_wp threadSet_unlive_other) + apply (wpsimp wp: threadGet_wp threadSet_unlive_other hoare_vcg_imp_lift') apply (normalise_obj_at', rename_tac tcb) apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index edb542ddcf..3171d51eb1 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -3597,9 +3597,10 @@ lemma tcbReleaseEnqueue_corres: apply (corres corres: setReprogramTimer_corres) \ \prepend t\ + apply (simp add: bind_assoc) apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre) - apply (wpsimp simp: tcbQueuePrepend_def wp: hoare_vcg_if_lift2) + apply (wpsimp simp: tcbQueuePrepend_def wp: hoare_vcg_imp_lift' hoare_vcg_if_lift2) apply (clarsimp simp: ex_abs_def) apply (frule state_relation_release_queue_relation) apply (clarsimp simp: release_queue_relation_def list_queue_relation_def) @@ -3615,37 +3616,25 @@ lemma tcbReleaseEnqueue_corres: \ \ready_queues_relation\ apply (drule set_release_queue_new_state) - apply (wpsimp wp: threadSet_ready_queues_relation simp: tcbQueuePrepend_def) - apply (clarsimp simp: ready_queues_relation_def release_queue_relation_def) - apply (force dest!: hd_in_set ready_or_release'D1 simp: tcbQueueEmpty_def) + apply (wpsimp wp: tcbQueuePrepend_list_queue_relation_other threadSet_sched_pointers + hoare_vcg_all_lift threadSet_inQ + simp: ready_queues_relation_def ready_queue_relation_def Let_def + | wps)+ + apply (rule_tac x="release_queue s" in exI) + subgoal + by (auto dest!: ready_or_release_disjoint simp: release_queue_relation_def not_queued_def) \ \release_queue_relation\ apply (drule set_release_queue_new_state) - apply (clarsimp simp: tcbQueuePrepend_def) - apply (wpsimp wp: threadSet_wp simp: setReleaseQueue_def) - apply (drule valid_sched_pointersD[where t=t]) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (case_tac "release_queue s = []"; clarsimp simp: tcbQueueEmpty_def) - apply (clarsimp simp: list_queue_relation_def heap_path.simps queue_end_valid_def obj_at'_def - opt_pred_def prev_queue_head_def release_queue_relation_def opt_map_def - split: if_splits) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def split: if_splits) - apply (frule heap_path_head, fastforce) - apply (drule heap_ls_prepend[where new=t]) - apply (clarsimp simp: not_in_release_q_def) - apply assumption - apply (drule obj_at'_prop)+ - apply clarsimp - apply (prop_tac "t \ hd (release_queue s)") - apply (clarsimp dest!: hd_in_set simp: not_in_release_q_def) - apply (rule conjI) - apply (subst opt_map_upd_triv) - apply (clarsimp simp: opt_map_def split: if_splits) - apply clarsimp - subgoal - by (force simp: queue_end_valid_def prev_queue_head_def opt_pred_def opt_map_def - split: if_splits option.splits) + apply (clarsimp simp: release_queue_relation_def) + apply (intro hoare_vcg_conj_lift_pre_fix) + apply ((wpsimp wp: tcbQueuePrepend_list_queue_relation threadSet_sched_pointers | wps)+)[1] + apply (frule (1) valid_sched_pointersD[where t=t]; + clarsimp simp: not_in_release_q_2_def in_opt_pred opt_map_red obj_at'_def) + apply (rule hoare_allI, rename_tac t') + apply (case_tac "t' = t"; clarsimp) + apply (wpsimp wp: threadSet_wp hoare_vcg_all_lift) + apply (wpsimp wp: threadSet_opt_pred_other) apply (simp add: bind_assoc) apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ assert_sp, rotated]; wpsimp?) @@ -3663,7 +3652,7 @@ lemma tcbReleaseEnqueue_corres: \ \append t\ apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre) - apply (wpsimp simp: tcbQueueAppend_def wp: hoare_vcg_if_lift2) + apply (wpsimp simp: tcbQueueAppend_def wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift') apply (clarsimp simp: ex_abs_def) apply (frule state_relation_release_queue_relation) apply (fastforce intro!: tcb_at_cross dest!: last_in_set @@ -3677,35 +3666,23 @@ lemma tcbReleaseEnqueue_corres: \ \ready_queues_relation\ apply (drule set_release_queue_new_state) - apply (wpsimp wp: threadSet_ready_queues_relation threadSet_tcbInReleaseQueue - simp: tcbQueueAppend_def setReleaseQueue_def tcbQueueEmpty_def - simp_del: comp_apply) - subgoal - by (force dest!: tcbQueueEnd_ksReleaseQueue last_in_set ready_or_release'D1 - simp: release_queue_relation_def tcbQueueEmpty_def) + apply (wpsimp wp: tcbQueueAppend_list_queue_relation_other threadSet_sched_pointers + hoare_vcg_all_lift threadSet_inQ + simp: ready_queues_relation_def ready_queue_relation_def Let_def + | wps)+ + apply (rule_tac x="release_queue s" in exI) + subgoal by (auto dest!: ready_or_release_disjoint simp: release_queue_relation_def not_queued_def) - \ \release_queue_relation\ apply (drule set_release_queue_new_state) - apply (clarsimp simp: tcbQueueAppend_def) - apply (wpsimp wp: threadSet_wp simp: setReleaseQueue_def) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def tcbQueueEmpty_def - queue_end_valid_def) - apply (drule valid_sched_pointersD[where t=t]) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (prop_tac "t \ last (release_queue s)") - apply (force dest!: last_in_set simp: not_in_release_q_def) - apply (drule (1) heap_ls_append[where new=t]) - apply (clarsimp simp: not_in_release_q_def) - apply clarsimp - apply (drule obj_at'_prop)+ - apply (rule conjI) - apply (clarsimp simp: opt_map_def) - apply (rule conjI) - apply (rule prev_queue_head_heap_upd) - apply (clarsimp simp: prev_queue_head_def opt_map_def split: if_splits) - apply (clarsimp dest!: hd_in_set simp: opt_map_def opt_pred_def split: option.splits) - apply (clarsimp simp: opt_map_def opt_pred_def split: if_splits option.splits) + apply (clarsimp simp: release_queue_relation_def) + apply (intro hoare_vcg_conj_lift_pre_fix) + apply ((wpsimp wp: tcbQueueAppend_list_queue_relation threadSet_sched_pointers | wps)+)[1] + apply (frule (1) valid_sched_pointersD[where t=t]; + clarsimp simp: not_in_release_q_2_def in_opt_pred opt_map_red obj_at'_def) + apply (rule hoare_allI, rename_tac t') + apply (case_tac "t' = t"; clarsimp) + apply (wpsimp wp: threadSet_wp hoare_vcg_all_lift) + apply (wpsimp wp: threadSet_opt_pred_other) \ \insert t into the middle of the release queue\ apply (rule corres_split_forwards' @@ -3772,63 +3749,39 @@ lemma tcbReleaseEnqueue_corres: (solves \frule set_release_queue_projs_inv, wpsimp simp: swp_def\)?) \ \ready_queues_relation\ - apply (drule set_release_queue_new_state) - apply (wpsimp wp: threadSet_ready_queues_relation getTCB_wp simp: tcbQueueInsert_def) + apply (drule set_release_queue_new_state) + apply (wpsimp wp: tcbQueueInsert_list_queue_relation_other threadSet_sched_pointers + hoare_vcg_all_lift threadSet_inQ + simp: ready_queues_relation_def ready_queue_relation_def Let_def + | wps)+ + apply (rename_tac s' tcb' d p) apply (intro conjI) - apply (erule in_ready_q_tcbQueued_eq[THEN arg_cong_Not, THEN iffD1]) - apply (erule ready_or_released_in_release_queue) - subgoal by (force dest!: set_mono_suffix hd_in_set simp: in_release_q_def) - apply (cut_tac ls="release_queue s" and p="hd sfx" in list_queue_relation_neighbour_in_set) - apply (force simp: release_queue_relation_def) - apply fastforce + apply (clarsimp simp: not_queued_def) + apply (rule_tac x="release_queue s" in exI) + apply (intro conjI) + apply (rule_tac x="ksReleaseQueue s'" in exI) + subgoal by (auto simp: release_queue_relation_def) subgoal by (force dest!: set_mono_suffix hd_in_set) - apply (erule in_ready_q_tcbQueued_eq[THEN arg_cong_Not, THEN iffD1]) - apply (erule ready_or_released_in_release_queue) - apply (clarsimp simp: in_release_q_def opt_map_def obj_at'_def) + subgoal by (auto dest!: ready_or_release_disjoint) - \ \release_queue_relation\ + \ \release_queue_relation\ apply (drule set_release_queue_new_state) - apply (frule valid_release_q_distinct) - apply (frule (3) nonempty_proper_suffix_split_distinct) - apply clarsimp - apply (rename_tac xs ys) - apply (clarsimp simp: tcbQueueInsert_def bind_assoc) - \ \forwards step in order to name beforePtr below\ - apply (rule bind_wp[OF _ stateAssert_sp]) - apply (rule bind_wp[OF _ get_tcb_sp'], rename_tac after_tcb) - apply (rule bind_wp[OF _ assert_sp]) - apply (rule hoare_ex_pre_conj[simplified conj_commute], rename_tac beforePtr) - apply (wpsimp wp: threadSet_wp getTCB_wp) - apply normalise_obj_at' - apply (drule obj_at'_prop)+ - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def) - apply (frule (2) heap_path_sym_heap_non_nil_lookup_prev) - apply (prop_tac "hd sfx \ t", fastforce simp: in_queue_2_def) - apply (prop_tac "beforePtr \ t", clarsimp simp: opt_map_def in_queue_2_def) - apply (cut_tac xs=xs and ys="hd sfx # ys" and new=t in list_insert_before_distinct) - subgoal by fastforce - apply fastforce - apply (drule heap_ls_list_insert_before[where new=t]) - apply (clarsimp simp: in_queue_2_def) + apply (clarsimp simp: release_queue_relation_def) + apply (intro hoare_vcg_conj_lift_pre_fix) + apply (clarsimp simp: suffix_def) + apply (subst list_insert_before_distinct) + apply (clarsimp simp: valid_release_q_def) apply fastforce - apply fastforce - apply (prop_tac "beforePtr = last xs", clarsimp simp: opt_map_def) - apply clarsimp - apply (rule conjI) - apply (subst opt_map_upd_triv) - apply (clarsimp simp: opt_map_red) - apply fastforce - apply (rule conjI) - apply (clarsimp simp: queue_end_valid_def) - apply (rule conjI) - apply (case_tac "hd xs = last xs") - apply (clarsimp simp: prev_queue_head_def opt_map_def) - apply (intro prev_queue_head_heap_upd) - apply force - apply force - apply force - apply (force dest!: heap_ls_distinct hd_in_set) - apply (clarsimp simp: opt_pred_def opt_map_def split: if_splits option.splits) + apply ((wpsimp wp: tcbQueueInsert_list_queue_relation threadSet_sched_pointers | wps)+)[1] + apply (frule (1) valid_sched_pointersD[where t=t]; + clarsimp simp: not_in_release_q_2_def in_opt_pred opt_map_red obj_at'_def) + apply (clarsimp simp: not_in_release_q_def) + apply (frule_tac before="hd sfx" in set_list_insert_before[where new=t]) + apply (force dest!: set_mono_suffix hd_in_set) + apply (rule hoare_allI, rename_tac t') + apply (case_tac "t' = t") + apply (wpsimp wp: threadSet_wp hoare_vcg_all_lift hoare_drop_imps) + apply (wpsimp wp: threadSet_opt_pred_other) done lemma postpone_corres: @@ -4722,13 +4675,9 @@ lemma tcbReleaseEnqueue_if_live_then_nonz_cap'[wp]: apply (clarsimp simp: ksReleaseQueue_asrt_def) apply (frule (3) obj_at'_tcbQueueHead_ksReleaseQueue) apply (frule (3) obj_at'_tcbQueueEnd_ksReleaseQueue) - apply (intro conjI impI allI; clarsimp simp: tcbQueueEmpty_def) - apply (fastforce elim!: if_live_then_nonz_capE' - dest: heap_path_head intro: aligned'_distinct'_ko_wp_at'I - simp: opt_pred_def opt_map_def obj_at'_def) - apply (fastforce elim!: if_live_then_nonz_capE' intro: aligned'_distinct'_ko_wp_at'I - simp: queue_end_valid_def opt_pred_def opt_map_def obj_at'_def) - done + by (fastforce elim!: if_live_then_nonz_capE' + dest: heap_path_head intro: aligned'_distinct'_ko_wp_at'I + simp: tcbQueueEmpty_def opt_pred_def opt_map_def obj_at'_def)+ crunch tcbReleaseEnqueue for valid_bitmaps[wp]: valid_bitmaps diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy index 8e3da19b1b..241a7c677b 100644 --- a/proof/refine/RISCV64/SchedContextInv_R.thy +++ b/proof/refine/RISCV64/SchedContextInv_R.thy @@ -1216,17 +1216,16 @@ lemma tcbSchedDequeue_valid_refills'[wp]: crunch tcbSchedDequeue, tcbReleaseRemove for ksCurSc[wp]: "\s. P (ksCurSc s)" - (wp: crunch_wps threadSet_wp getTCB_wp - simp: setQueue_def valid_refills'_def bitmap_fun_defs crunch_simps) + (wp: simp: crunch_simps) + +crunch setReleaseQueue + for valid_refills'[wp]: "valid_refills' scPtr" + (simp: valid_refills'_def) lemma tcbReleaseRemove_valid_refills'[wp]: "tcbReleaseRemove tcbPtr \valid_refills' scPtr\" - apply (clarsimp simp: tcbReleaseRemove_def tcbQueueRemove_def) - apply (wpsimp wp: threadSet_wp threadGet_wp getTCB_wp inReleaseQueue_wp - simp: bitmap_fun_defs setReleaseQueue_def setReprogramTimer_def - | intro conjI impI)+ - by (fastforce simp: obj_at_simps valid_refills'_def opt_map_def opt_pred_def - split: option.splits)+ + unfolding tcbReleaseRemove_def tcbQueueRemove_def + by (wpsimp wp: hoare_vcg_all_lift hoare_drop_imps) crunch commitTime, refillNew, refillUpdate for ksCurSc[wp]: "\s. P (ksCurSc s)" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index b009440d57..348ecd6a12 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -178,7 +178,6 @@ lemma tcbSchedAppend_corres: (sym_heap_sched_pointers and valid_sched_pointers and valid_tcbs') (tcb_sched_action tcb_sched_append tcb_ptr) (tcbSchedAppend tcbPtr)" supply if_split[split del] - heap_path_append[simp del] fun_upd_apply[simp del] distinct_append[simp del] apply (rule_tac Q'="st_tcb_at' runnable' tcbPtr" in corres_cross_add_guard) apply (fastforce intro!: st_tcb_at_runnable_cross simp: vs_all_heap_simps obj_at_def is_tcb_def) apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard) @@ -235,15 +234,20 @@ lemma tcbSchedAppend_corres: apply (wpsimp wp: hoare_vcg_if_lift hoare_vcg_ex_lift) apply (corres corres: addToBitmap_if_null_noop_corres) + apply (rule_tac F="tdom = domain \ prio = priority" in corres_req) + apply (fastforce dest: pspace_relation_tcb_domain_priority state_relation_pspace_relation + simp: obj_at_def obj_at'_def) + apply clarsimp + apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre simp: set_tcb_queue_def) - apply (wpsimp simp: tcbQueueAppend_def wp: hoare_vcg_if_lift2 | drule Some_to_the)+ + apply (wpsimp simp: tcbQueueAppend_def wp: hoare_vcg_imp_lift' hoare_vcg_if_lift2) apply (clarsimp simp: ex_abs_def split: if_splits) apply (frule state_relation_ready_queues_relation) apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) - apply (auto dest!: obj_at'_tcbQueueEnd_ksReadyQueues simp: obj_at'_def)[1] + subgoal by (auto dest!: obj_at'_tcbQueueEnd_ksReadyQueues simp: obj_at'_def) apply (rename_tac s rv t) apply (clarsimp simp: state_relation_def) @@ -251,134 +255,60 @@ lemma tcbSchedAppend_corres: (solves \frule singleton_eqD, frule set_tcb_queue_projs_inv, wpsimp simp: swp_def\)?) apply (find_goal \match conclusion in "\_\ _ \\_. release_queue_relation t\" for t \ \-\\) - apply (wpsimp wp: threadSet_release_queue_relation simp: tcbQueueAppend_def) - apply normalise_obj_at' - apply (rename_tac s' tcb) - apply (prop_tac "release_queue_relation t s'") - apply (force dest!: set_tcb_queue_projs_inv simp: release_queue_relation_def) - apply simp - apply (rule impI) - apply (erule ready_or_release'D2) - apply (rule inQ_implies_tcbQueueds_of) - apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) - apply (cut_tac d="tcbDomain tcb" and p="tcbPriority tcb" in tcbQueueEnd_ksReadyQueues) - apply fast - apply fast - apply force + apply (frule_tac d=domain and p=priority in ready_or_release_disjoint) + apply (drule set_tcb_queue_projs_inv) + apply (wpsimp wp: tcbQueueAppend_list_queue_relation_other hoare_vcg_ex_lift + threadSet_sched_pointers + simp: release_queue_relation_def + | wps)+ + apply (rule_tac x="ready_queues s (tcbDomain tcba) (tcbPriority tcb)" in exI) + apply (auto simp: ready_queues_relation_def ready_queue_relation_def Let_def)[1] \ \ready_queues_relation\ apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) apply (intro hoare_allI) apply (drule singleton_eqD) apply (drule set_tcb_queue_new_state) - apply (wpsimp wp: threadSet_wp simp: setQueue_def tcbQueueAppend_def) - apply normalise_obj_at' - apply (clarsimp simp: obj_at_def) - apply (rename_tac s' tcb' tcb) - apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) - apply (force simp: obj_at_def) - apply (force simp: obj_at'_def) - apply (clarsimp split: if_splits) - apply (cut_tac ts="ready_queues s d p" in list_queue_relation_nil) - apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - in obj_at'_tcbQueueEnd_ksReadyQueues) - apply fast - apply fast - apply fastforce - apply fastforce - apply (cut_tac xs="ready_queues s d p" in heap_path_head') - apply (force dest!: spec simp: list_queue_relation_def) - apply (clarsimp simp: list_queue_relation_def) + apply (intro hoare_vcg_conj_lift_pre_fix) - apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") - apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" - in ready_queues_disjoint) - apply force + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxDomain < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueueAppend_def) + apply (frule valid_tcbs'_maxDomain[where t=tcbPtr]) + apply fastforce + subgoal by (force simp: obj_at'_def tcbQueueEmpty_def split: if_split) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxPriority < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueueAppend_def) + apply (frule valid_tcbs'_maxPriority[where t=tcbPtr]) apply fastforce + subgoal by (force simp: obj_at'_def tcbQueueEmpty_def split: if_split) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. list_queue_relation _ _ _ _ \" \ \-\\) + apply (clarsimp simp: obj_at_def) + apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") + apply (wpsimp wp: tcbQueueAppend_list_queue_relation_other setQueue_ksReadyQueues_other + threadSet_sched_pointers hoare_vcg_ex_lift + | wps)+ + apply (intro conjI) + subgoal by fastforce + apply (rule_tac x="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in exI) + apply (auto dest!: in_correct_ready_qD simp: ready_queues_disjoint + split: if_splits)[1] apply fastforce - apply (prop_tac "tcbPtr \ set (ready_queues s d p)") - apply (force simp: in_correct_ready_qD) - apply (intro conjI impI; clarsimp) + apply ((wpsimp wp: tcbQueueAppend_list_queue_relation threadSet_sched_pointers | wps)+)[1] + apply (fastforce dest!: valid_sched_pointersD[where t=tcbPtr] + simp: in_opt_pred opt_map_red obj_at'_def) - \ \the ready queue was originally empty\ - apply (rule heap_path_heap_upd_not_in) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply fastforce - apply (clarsimp simp: queue_end_valid_def fun_upd_apply split: if_splits) - apply (rule prev_queue_head_heap_upd) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (case_tac "ready_queues s d p"; - clarsimp simp: fun_upd_apply tcbQueueEmpty_def split: if_splits) - apply (clarsimp simp: inQ_def in_opt_pred fun_upd_apply obj_at'_def split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - - \ \the ready queue was not originally empty\ - apply (drule obj_at'_prop)+ - apply clarsimp - apply (prop_tac "the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))) - \ set (ready_queues s d p)") - apply (erule orthD2) - apply (drule_tac x="tcb_domain tcb" in spec) - apply (drule_tac x="tcb_priority tcb" in spec) - apply clarsimp - apply (drule_tac x="the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))" - in spec) - subgoal by (auto simp: in_opt_pred opt_map_red) - apply (intro conjI impI allI) - apply (intro heap_path_heap_upd_not_in) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply simp - apply fastforce - apply (clarsimp simp: queue_end_valid_def fun_upd_apply split: if_splits) - apply (intro prev_queue_head_heap_upd) - apply (force simp: fun_upd_apply split: if_splits) - apply (case_tac "ready_queues s d p"; - clarsimp simp: fun_upd_apply tcbQueueEmpty_def split: if_splits) - apply (clarsimp simp: fun_upd_apply inQ_def split: if_splits) - apply (case_tac "ready_queues s d p"; force simp: tcbQueueEmpty_def) - apply (case_tac "t = tcbPtr") - apply (clarsimp simp: inQ_def fun_upd_apply split: if_splits) - apply (case_tac "t = the (tcbQueueEnd (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))") - apply (clarsimp simp: inQ_def opt_pred_def fun_upd_apply) - apply (clarsimp simp: inQ_def in_opt_pred opt_map_def fun_upd_apply) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - - \ \d = tcb_domain tcb \ p = tcb_priority tcb\ - apply clarsimp - apply (drule_tac x="tcb_domain tcb" in spec) - apply (drule_tac x="tcb_priority tcb" in spec) - apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - in tcbQueueHead_iff_tcbQueueEnd) - apply (force simp: list_queue_relation_def) - apply (frule valid_tcbs'_maxDomain[where t=tcbPtr], fastforce) - apply (frule valid_tcbs'_maxPriority[where t=tcbPtr], fastforce) - apply (drule valid_sched_pointersD[where t=tcbPtr]) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (intro conjI; clarsimp) - - \ \the ready queue was originally empty\ - apply (force simp: inQ_def in_opt_pred fun_upd_apply opt_map_def obj_at'_def - queue_end_valid_def prev_queue_head_def - split: if_splits option.splits) - - \ \the ready queue was not originally empty\ - apply normalise_obj_at' - apply (drule obj_at'_prop)+ - apply clarsimp - apply (drule (2) heap_ls_append[where new=tcbPtr]) - apply (rule conjI) - apply (clarsimp simp: fun_upd_apply queue_end_valid_def opt_map_def split: if_splits) - apply (rule conjI) - apply (clarsimp simp: fun_upd_apply queue_end_valid_def) - apply (rule conjI) - apply (subst opt_map_upd_triv) - apply (clarsimp simp: opt_map_def fun_upd_apply queue_end_valid_def split: if_splits) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply split: if_splits) - by (clarsimp simp: inQ_def in_opt_pred fun_upd_apply queue_end_valid_def split: if_splits) + apply (rule hoare_allI, rename_tac t') + apply (case_tac "d \ domain \ p \ priority") + apply (wpsimp wp: tcbQueued_update_inQ_other hoare_vcg_disj_lift + simp: opt_pred_disj[simplified pred_disj_def, symmetric] simp_del: disj_not1) + apply (clarsimp simp: opt_map_def opt_pred_def obj_at'_def split: option.splits if_splits) + apply (case_tac "t' = tcbPtr") + apply (wpsimp wp: tcbQueued_True_makes_inQ) + apply (clarsimp simp: opt_pred_def opt_map_def obj_at'_def) + apply (wpsimp wp: threadSet_opt_pred_other) + done lemma tcbQueueAppend_valid_objs'[wp]: "\\s. valid_objs' s \ tcb_at' tcbPtr s \ (\end. tcbQueueEnd queue = Some end \ tcb_at' end s)\ @@ -432,16 +362,21 @@ lemma tcbSchedAppend_iflive'[wp]: tcbSchedAppend tcbPtr \\_. if_live_then_nonz_cap'\" unfolding tcbSchedAppend_def - apply (wpsimp wp: tcbQueueAppend_if_live_then_nonz_cap' threadGet_wp simp: bitmap_fun_defs) + apply (wpsimp wp: tcbQueueAppend_if_live_then_nonz_cap' threadGet_wp + threadSet_sched_pointers hoare_vcg_all_lift hoare_vcg_imp_lift' + simp: bitmap_fun_defs) apply (frule_tac p=tcbPtr in if_live_then_nonz_capE') apply (fastforce simp: ko_wp_at'_def st_tcb_at'_def obj_at'_def runnable_eq_active') - apply (clarsimp simp: tcbQueueEmpty_def) - apply (erule if_live_then_nonz_capE') apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) - apply (drule_tac x="tcbDomain tcb" in spec) - apply (drule_tac x="tcbPriority tcb" in spec) - apply (fastforce dest!: obj_at'_tcbQueueEnd_ksReadyQueues - simp: ko_wp_at'_def inQ_def obj_at'_def tcbQueueEmpty_def) + apply (intro conjI impI allI) + apply (erule if_live_then_nonz_capE') + apply (drule_tac x="tcbDomain tcb" in spec) + apply (drule_tac x="tcbPriority tcb" in spec) + apply clarsimp + apply (frule (3) obj_at'_tcbQueueEnd_ksReadyQueues) + apply (frule tcbQueueHead_iff_tcbQueueEnd) + apply (clarsimp simp: ko_wp_at'_def inQ_def obj_at'_def tcbQueueEmpty_def) + apply fastforce done lemma tcbSchedDequeue_iflive'[wp]: @@ -449,7 +384,7 @@ lemma tcbSchedDequeue_iflive'[wp]: tcbSchedDequeue tcbPtr \\_. if_live_then_nonz_cap'\" apply (simp add: tcbSchedDequeue_def) - apply (wpsimp wp: tcbQueueRemove_if_live_then_nonz_cap' threadGet_wp) + apply (wpsimp wp: tcbQueueRemove_if_live_then_nonz_cap' threadGet_wp threadSet_valid_objs') apply (fastforce elim: if_live_then_nonz_capE' simp: obj_at'_def ko_wp_at'_def) done @@ -543,7 +478,7 @@ lemma tcbSchedAppend_valid_bitmapQ[wp]: unfolding tcbSchedAppend_def apply (wpsimp simp: tcbQueueAppend_def wp: setQueue_valid_bitmapQ' addToBitmap_valid_bitmapQ_except addToBitmap_bitmapQ - threadGet_wp hoare_vcg_if_lift2) + threadGet_wp hoare_vcg_if_lift2 threadSet_bitmapQ) apply (clarsimp simp: ksReadyQueues_asrt_def split: if_splits) apply normalise_obj_at' apply (force dest: tcbQueueHead_iff_tcbQueueEnd @@ -588,11 +523,7 @@ lemma tcbSchedDequeue_vms'[wp]: lemma tcbSchedDequeue_valid_mdb'[wp]: "\valid_mdb' and valid_objs'\ tcbSchedDequeue tcbPtr \\_. valid_mdb'\" unfolding tcbSchedDequeue_def - apply (wpsimp simp: bitmap_fun_defs setQueue_def wp: threadSet_mdb' tcbQueueRemove_valid_mdb') - apply (rule_tac Q'="\_. tcb_at' tcbPtr" in hoare_post_imp) - apply (fastforce simp: tcb_cte_cases_def cteSizeBits_def) - apply (wpsimp wp: threadGet_wp)+ - done + by (wpsimp simp: bitmap_fun_defs setQueue_def wp: tcbQueueRemove_valid_mdb' threadGet_wp) lemma tcbSchedDequeue_invs'[wp]: "tcbSchedDequeue t \invs'\" @@ -840,8 +771,7 @@ lemma tcbSchedDequeue_not_tcbQueued: "\\\ tcbSchedDequeue t \\_. obj_at' (\tcb. \ tcbQueued tcb) t\" unfolding tcbSchedDequeue_def apply (wpsimp wp: hoare_vcg_if_lift2 threadGet_wp) - apply (clarsimp simp: obj_at'_def) - done + by (clarsimp simp: obj_at'_def) lemma asUser_tcbState_inv[wp]: "asUser t m \obj_at' (P \ tcbState) t\" @@ -2995,7 +2925,7 @@ lemma tcbReleaseRemove_corres: \ \setting the release queue\ apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre) - apply (wpsimp wp: tcbQueueRemove_no_fail) + apply (wpsimp wp: tcbQueueRemove_no_fail hoare_vcg_ex_lift threadSet_sched_pointers) apply (fastforce dest: state_relation_release_queue_relation simp: ex_abs_def release_queue_relation_def list_queue_relation_def) apply (clarsimp simp: state_relation_def) @@ -3004,122 +2934,26 @@ lemma tcbReleaseRemove_corres: apply (intro hoare_vcg_conj_lift_pre_fix; (solves \wpsimp simp: swp_def\)?) apply (find_goal \match conclusion in "\_\ _ \\_. ready_queues_relation t\" for t \ \-\\) - apply (simp add: tcbQueueRemove_def) - apply (wpsimp wp: threadSet_ready_queues_relation getTCB_wp) - apply (frule (2) ready_or_release_cross) - apply normalise_obj_at' - apply (drule obj_at'_prop)+ - apply (rename_tac s') - apply (cut_tac p=tcbPtr and ls="release_queue s" in list_queue_relation_neighbour_in_set) - apply (fastforce dest!: spec simp: release_queue_relation_def) - apply fastforce - apply fastforce - apply (clarsimp simp: ready_queues_relation_def Let_def) - apply (frule ready_or_release'D1[where tcbPtr=tcbPtr]) - apply (clarsimp simp: release_queue_relation_def) - apply (fastforce elim!: ready_or_release'D1 simp: release_queue_relation_def opt_map_def) + apply (wpsimp wp: tcbQueueRemove_list_queue_relation_other threadSet_sched_pointers + hoare_vcg_all_lift threadSet_inQ + simp: ready_queues_relation_def ready_queue_relation_def Let_def + | wps)+ + apply (rule_tac x="release_queue s" in exI) + apply (auto dest: ready_or_release_disjoint simp: release_queue_relation_def Let_def)[1] + apply (clarsimp simp: release_queue_relation_def) apply (frule singleton_eqD) apply (drule set_release_queue_new_state) - apply (wpsimp wp: threadSet_wp getTCB_wp simp: tcbQueueRemove_def setReleaseQueue_def) - apply (rename_tac s' tcb) - apply (frule set_list_mem_nonempty) - apply (cut_tac xs="release_queue s" in heap_path_head') - apply (force simp: release_queue_relation_def list_queue_relation_def) - apply (cut_tac xs="release_queue s" in heap_ls_distinct) - apply (force simp: release_queue_relation_def list_queue_relation_def) - apply (intro conjI; clarsimp simp: queue_end_valid_def) - - \ \the release queue is the singleton consisting of tcb_ptr\ - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def tcb_queue_remove_def) - apply (intro conjI) - apply (simp add: fun_upd_apply queue_end_valid_def heap_ls_unique heap_path_last_end) - apply (clarsimp simp: queue_end_valid_def heap_ls_unique heap_path_last_end) - apply (simp add: fun_upd_apply prev_queue_head_def) - apply (case_tac "release_queue s"; - clarsimp simp: opt_pred_def fun_upd_apply queue_end_valid_def split: if_splits) - - apply (rule conjI) - - \ \tcbPtr is the head of the ready queue\ - apply (intro impI allI) - apply (frule in_queue_not_head_or_not_tail_length_gt_1) - apply fastforce - apply (force simp: release_queue_relation_def list_queue_relation_def) - apply (frule list_not_head) - apply (frule length_tail_nonempty) - apply (drule obj_at'_prop)+ - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def tcb_queue_remove_def) - apply (frule (2) heap_ls_next_of_hd) - apply (intro conjI) - apply (fastforce dest: heap_ls_remove_head_not_singleton - simp: opt_map_red opt_map_upd_triv fun_upd_apply) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply last_tl) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply split: if_splits) - apply (case_tac "release_queue s"; - auto simp: opt_pred_def opt_map_def fun_upd_apply split: if_splits)[1] + apply (intro hoare_vcg_conj_lift_pre_fix) + apply ((wpsimp wp: tcbQueueRemove_list_queue_relation threadSet_sched_pointers | wps)+)[1] - apply clarsimp - apply (rule conjI) - apply (intro impI allI) - - \ \tcbPtr is the end of the ready queue\ - apply (frule set_list_mem_nonempty) - apply (frule_tac q="ksReleaseQueue s'" in in_queue_not_head_or_not_tail_length_gt_1) - apply (force simp: list_queue_relation_def) - apply (force simp: release_queue_relation_def) - apply (frule list_not_last) - apply (frule length_gt_1_imp_butlast_nonempty) - apply (drule obj_at'_prop)+ - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def queue_end_valid_def - tcb_queue_remove_def) - apply (frule (3) heap_ls_prev_of_last) - apply (rename_tac beforePtr) - apply (intro conjI impI; clarsimp?) - apply (drule (1) heap_ls_remove_last_not_singleton) - apply (force elim!: rsubst3[where P=heap_ls] simp: opt_map_def fun_upd_apply split: if_splits) - apply (clarsimp simp: opt_map_def fun_upd_apply) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply opt_map_def split: if_splits) - apply (case_tac "t = last (release_queue s)") - apply (force dest!: distinct_in_butlast_not_last simp: fun_upd_apply) - apply (case_tac "t = beforePtr") - apply (drule_tac x="last (butlast (release_queue s))" in spec) - apply (clarsimp dest!: in_set_butlastD last_in_set simp: opt_pred_def opt_map_def fun_upd_apply) - apply (fastforce intro: not_last_in_set_butlast dest!: in_set_butlastD - simp: inQ_def opt_pred_def opt_map_def fun_upd_apply) - - \ \tcbPtr is in the middle of the ready queue\ - apply (intro conjI impI allI) - apply (frule set_list_mem_nonempty) - apply (frule split_list) - apply clarsimp - apply (rename_tac afterPtr beforePtr xs ys) - apply (clarsimp simp: release_queue_relation_def list_queue_relation_def) - apply (prop_tac "xs \ [] \ ys \ []", force simp: queue_end_valid_def) - apply clarsimp - apply (frule (3) ptr_in_middle_prev_next) - apply (drule obj_at'_prop)+ - apply clarsimp - apply (prop_tac "tcbPtr \ beforePtr", clarsimp simp: opt_map_red) - apply (prop_tac "tcbPtr \ afterPtr", fastforce dest: hd_in_set simp: opt_map_red) - apply (prop_tac "beforePtr \ afterPtr") - apply (force dest: hd_in_set last_in_set simp: not_emptyI opt_map_red) - apply (clarsimp simp: tcb_queue_remove_def list_remove_middle_distinct split: if_splits) - apply (intro conjI impI allI) - apply (drule (2) heap_ls_remove_middle) - apply (fastforce elim!: rsubst3[where P=heap_ls] - simp: opt_map_def fun_upd_apply split: if_splits) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply) - apply (case_tac xs; force simp: prev_queue_head_def opt_map_def fun_upd_apply split: if_splits) - apply (case_tac "t = tcbPtr") - apply (clarsimp simp: fun_upd_apply) - apply (case_tac "t = beforePtr") - subgoal - by (auto dest!: last_in_set simp: opt_pred_def opt_map_def fun_upd_apply split: option.splits) - apply (case_tac "t = afterPtr") - subgoal - by (auto dest!: hd_in_set simp: opt_pred_def opt_map_def fun_upd_apply split: option.splits) - by (auto simp: in_opt_pred opt_map_red fun_upd_apply split: option.splits) + apply (rule hoare_allI, rename_tac t') + apply (subst set_tcb_queue_remove) + apply clarsimp + apply (case_tac "t' = tcbPtr") + apply (wpsimp wp: threadSet_wp) + apply (wpsimp wp: threadSet_opt_pred_other) + done lemma tcbInReleaseQueue_update_valid_tcbs'[wp]: "threadSet (tcbInReleaseQueue_update f) tcbPtr \valid_tcbs'\" @@ -3135,7 +2969,7 @@ lemma tcbQueueRemove_valid_tcbs'[wp]: crunch tcbReleaseDequeue for valid_tcbs'[wp]: valid_tcbs' and valid_sched_pointers[wp]: valid_sched_pointers - (wp: crunch_wps) + (wp: crunch_wps simp: crunch_simps) crunch tcb_release_remove for ready_qs_distinct[wp]: ready_qs_distinct diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 0ee8aeb789..0ce6a77bec 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -372,7 +372,7 @@ crunch removeFromBitmap lemma tcbSchedDequeue_isSchedulable_bool[wp]: "tcbSchedDequeue tcbPtr \\s. P (isSchedulable_bool tcbPtr' s)\" unfolding tcbSchedDequeue_def tcbQueueRemove_def setQueue_def - by (wpsimp wp: threadSet_isSchedulable_bool_fields_inv getTCB_wp threadGet_wp) + by (wpsimp wp: threadSet_isSchedulable_bool_fields_inv getTCB_wp threadGet_wp hoare_drop_imps) lemma setDomain_corres: "corres dc diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 807829012c..8b59b359f6 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -2364,15 +2364,387 @@ lemma in_correct_ready_qD: \ tcb_domain tcb = d \ tcb_priority tcb = p " by (fastforce simp: in_correct_ready_q_def vs_all_heap_simps) -lemma ready_or_release'D1: - "\ready_or_release' s'; (tcbInReleaseQueue |< tcbs_of' s') tcbPtr\ - \ \ (tcbQueued |< tcbs_of' s') tcbPtr" - by (clarsimp simp: ready_or_release'_def opt_pred_def opt_map_def split: option.splits) +lemma threadSet_heap_ls_other: + "\\s. heap_ls (tcbSchedNexts_of s) st ls \ t \ set ls\ + threadSet F t + \\_ s. heap_ls (tcbSchedNexts_of s) st ls\" + apply (wpsimp wp: threadSet_wp) + by (fastforce dest: heap_path_heap_upd_not_in) + +lemma heap_path_not_Nil: + "heap_ls hp (Some st) ls \ ls \ []" + by fastforce + +lemma threadSet_prev_queue_head_other: + "\\s. prev_queue_head q (tcbSchedPrevs_of s) + \ (\ls. heap_ls (tcbSchedNexts_of s) (tcbQueueHead q) ls \ t \ set ls)\ + threadSet F t + \\_ s. prev_queue_head q (tcbSchedPrevs_of s)\" + apply (wpsimp wp: threadSet_wp) + apply (frule heap_path_head') + apply (fastforce simp: prev_queue_head_def dest: heap_path_not_Nil hd_in_set) + done + +lemma list_queue_relation_neighbour_in_set: + "\list_queue_relation ls q hp hp'; sym_heap hp hp'; p \ set ls\ + \ \nbr. (hp p = Some nbr \ nbr \ set ls) \ (hp' p = Some nbr \ nbr \ set ls)" + apply (rule heap_ls_neighbour_in_set) + apply (fastforce simp: list_queue_relation_def) + apply fastforce + apply (clarsimp simp: list_queue_relation_def prev_queue_head_def) + apply fastforce + done + +lemma tcbQueueRemove_list_queue_relation_other: + "\\s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ (\ls'. list_queue_relation ls' queue' (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ tcbPtr \ set ls' \ set ls \ set ls' = {})\ + tcbQueueRemove queue' tcbPtr + \\_ s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + unfolding tcbQueueRemove_def list_queue_relation_def + apply (wpsimp wp: threadSet_prev_queue_head_other threadSet_heap_ls_other getTCB_wp + hoare_vcg_ex_lift) + by (fastforce dest: list_queue_relation_neighbour_in_set[where p=tcbPtr, rotated 2] + simp: list_queue_relation_def opt_map_def obj_at'_def) + +lemma tcbQueuePrepend_list_queue_relation_other: + "\\s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ (\ls'. list_queue_relation ls' queue' (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ tcbPtr \ set ls \ set ls \ set ls' = {})\ + tcbQueuePrepend queue' tcbPtr + \\_ s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + unfolding tcbQueuePrepend_def list_queue_relation_def + apply (wpsimp wp: threadSet_prev_queue_head_other threadSet_heap_ls_other hoare_vcg_ex_lift) + by (fastforce dest: list_queue_relation_nil[THEN arg_cong_Not, THEN iffD2, rotated] heap_path_head + simp: list_queue_relation_def) + +lemma tcbQueueAppend_list_queue_relation_other: + "\\s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ (\ls'. list_queue_relation ls' queue' (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ tcbPtr \ set ls \ set ls \ set ls' = {})\ + tcbQueueAppend queue' tcbPtr + \\_ s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + unfolding tcbQueueAppend_def list_queue_relation_def + apply (wpsimp wp: threadSet_prev_queue_head_other threadSet_heap_ls_other hoare_vcg_ex_lift) + by (fastforce dest: list_queue_relation_nil[THEN arg_cong_Not, THEN iffD2, rotated] heap_path_head + simp: list_queue_relation_def queue_end_valid_def) + +lemma tcbQueueInsert_list_queue_relation_other: + "\\s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ tcbPtr \ set ls + \ (\ls' queue'. list_queue_relation ls' queue' (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ afterPtr \ set ls' \ set ls \ set ls' = {})\ + tcbQueueInsert tcbPtr afterPtr + \\_ s. list_queue_relation ls queue (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + unfolding tcbQueueInsert_def list_queue_relation_def + apply (wpsimp wp: threadSet_prev_queue_head_other threadSet_heap_ls_other getTCB_wp + hoare_vcg_ex_lift) + by (force dest!: heap_ls_neighbour_in_set[where p=afterPtr] intro!: exI[where x=ls] + simp: prev_queue_head_def opt_map_def obj_at'_def) + +lemma tcbQueued_update_tcbInReleaseQueue[wp]: + "threadSet (tcbQueued_update f) tcbPtr \\s. P (tcbInReleaseQueue |< tcbs_of' s)\" + by (wpsimp wp: threadSet_tcbInReleaseQueue) + +lemma threadSet_tcbPriority: + "(\tcb. tcbPriority (F tcb) = tcbPriority tcb) \ + threadSet F t \\s. P ((\tcb. Q (tcbPriority tcb)) |< tcbs_of' s)\" + apply (wpsimp wp: threadSet_wp) + by (fastforce elim: rsubst[where P=P] simp: opt_pred_def opt_map_def obj_at'_def) + +lemma threadSet_tcbDomain: + "(\tcb. tcbDomain (F tcb) = tcbDomain tcb) \ + threadSet F t \\s. P ((\tcb. Q (tcbDomain tcb)) |< tcbs_of' s)\" + apply (wpsimp wp: threadSet_wp) + by (fastforce elim: rsubst[where P=P] simp: opt_pred_def opt_map_def obj_at'_def) + +lemma ready_or_release_disjoint: + "ready_or_release s \ set (ready_queues s d p) \ set (release_queue s) = {}" + by (fastforce simp: ready_or_release_def in_ready_q_def not_in_release_q_def) + +lemma setQueue_ksReadyQueues_other: + "\\s. P (ksReadyQueues s (d, p)) \ (domain \ d \ priority \ p)\ + setQueue domain priority ts + \\_ s. P (ksReadyQueues s (d, p))\" + by (wpsimp simp: setQueue_def) + +lemma tcbQueued_update_inQ_other: + "\\s. P (inQ d p |< tcbs_of' s) + \ ((\tcb. tcbDomain tcb \ d \ tcbPriority tcb \ p) |< tcbs_of' s) tcbPtr\ + threadSet (tcbQueued_update f) tcbPtr + \\_ s. P (inQ d p |< tcbs_of' s)\" + apply (wpsimp wp: threadSet_wp) + by (fastforce elim: rsubst[where P=P] simp: inQ_def opt_pred_def opt_map_def obj_at'_def) + +lemma threadSet_inQ: + "\\tcb. tcbPriority (F tcb) = tcbPriority tcb; \tcb. tcbDomain (F tcb) = tcbDomain tcb; + \tcb. tcbQueued (F tcb) = tcbQueued tcb\ + \ threadSet F tcbPtr \\s. P (inQ d p |< tcbs_of' s)\" + apply (wpsimp wp: threadSet_wp) + by (fastforce elim: rsubst[where P=P] simp: inQ_def opt_pred_def opt_map_def obj_at'_def) + +crunch tcbQueueRemove, tcbQueuePrepend, tcbQueueAppend, tcbQueueInsert + for ksReleaseQueue[wp]: "\s. P (ksReleaseQueue s)" + and ksReadyQueues[wp]: "\s. P (ksReadyQueues s)" + and tcbInReleaseQueue_opt_pred[wp]: "\s. P (tcbInReleaseQueue |< tcbs_of' s)" + and tcbQueued_opt_pred[wp]: "\s. P (tcbQueued |< tcbs_of' s)" + and tcbPriority_opt_pred[wp]: "\s. P ((\tcb. Q (tcbPriority tcb)) |< tcbs_of' s)" + and tcbDomain_opt_pred[wp]: "\s. P ((\tcb. Q (tcbDomain tcb)) |< tcbs_of' s)" + and inQ_opt_pred[wp]: "\s. P (inQ d p |< tcbs_of' s)" + (wp: crunch_wps threadSet_tcbPriority threadSet_tcbDomain threadSet_inQ + threadSet_tcbInReleaseQueue threadSet_tcbQueued + ignore: threadSet) + +lemma set_butlast: + "distinct list \ set (butlast list) = (set list) - {last list}" + by (induct list, simp+, fastforce) + +\ \ + A direct analogue of tcbQueueRemove, used in tcb_sched_dequeue' below, so that within the proof of + tcbQueueRemove_corres, we may reason in terms of the list operations used within this function + rather than @{term filter}.\ +definition tcb_queue_remove :: "'a \ 'a list \ 'a list" where + "tcb_queue_remove a ls \ + if ls = [a] + then [] + else if a = hd ls + then tl ls + else if a = last ls + then butlast ls + else list_remove ls a" + +lemma set_tcb_queue_remove: + "distinct ls \ set (tcb_queue_remove t ls) = set ls - {t}" + by (auto dest: set_remove1_eq[where x=t] + simp: tcb_queue_remove_def set_butlast list_remove_removed) + +lemma tcb_queue_remove_middle: + "distinct (xs @ tcbPtr # ys) \ tcb_queue_remove tcbPtr (xs @ tcbPtr # ys) = xs @ ys" + by (cases xs; fastforce simp: tcb_queue_remove_def list_remove_none) + +lemma in_queue_not_head_or_not_tail_length_gt_1: + "\tcbPtr \ set ls; tcbQueueHead q \ Some tcbPtr \ tcbQueueEnd q \ Some tcbPtr; + list_queue_relation ls q nexts prevs\ + \ Suc 0 < length ls" + by (cases ls; fastforce simp: list_queue_relation_def queue_end_valid_def) + +lemma tcbQueueRemove_list_queue_relation: + "\\s. list_queue_relation ls q (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ tcbPtr \ set ls\ + tcbQueueRemove q tcbPtr + \\q' s. list_queue_relation (tcb_queue_remove tcbPtr ls) q' (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + supply heap_path_append[simp del] distinct_append[simp del] + apply (clarsimp simp: tcbQueueRemove_def) + apply (wpsimp wp: threadSet_wp getTCB_wp) + apply (intro conjI impI allI) + \ \ls is a singleton list containing tcbPtr\ + apply (clarsimp simp: list_queue_relation_def queue_end_valid_def prev_queue_head_def + tcb_queue_remove_def heap_ls_unique heap_path_last_end) + apply (frule heap_ls_distinct) + apply (cases ls; clarsimp) + \ \tcbPtr is the head of ls\ + apply (clarsimp simp: list_queue_relation_def) + apply (frule heap_path_head') + apply (frule set_list_mem_nonempty) + apply (frule in_queue_not_head_or_not_tail_length_gt_1) + apply fastforce + apply (force dest!: spec simp: list_queue_relation_def) + apply (intro conjI) + apply (frule list_not_head) + apply (clarsimp simp: tcb_queue_remove_def) + apply (frule length_tail_nonempty) + apply (frule (2) heap_ls_next_of_hd) + apply (drule (1) heap_ls_remove_head_not_singleton) + apply (clarsimp simp: opt_map_red opt_map_upd_triv obj_at'_def) + apply (cases ls; clarsimp simp: queue_end_valid_def tcb_queue_remove_def) + apply (clarsimp simp: prev_queue_head_def tcb_queue_remove_def opt_map_def obj_at'_def) + \ \tcbPtr is the last element of ls\ + apply (clarsimp simp: list_queue_relation_def) + apply (intro conjI) + apply (frule in_queue_not_head_or_not_tail_length_gt_1) + apply fast + apply (force dest!: spec simp: list_queue_relation_def) + apply (clarsimp simp: queue_end_valid_def) + apply (frule list_not_last) + apply (clarsimp simp: tcb_queue_remove_def) + apply (frule length_gt_1_imp_butlast_nonempty) + apply (frule (3) heap_ls_prev_of_last) + apply (intro conjI impI; clarsimp?) + apply (cases ls; clarsimp) + apply (drule (1) heap_ls_remove_last_not_singleton) + apply (force elim!: rsubst3[where P=heap_ls] simp: opt_map_def obj_at'_def) + apply (clarsimp simp: queue_end_valid_def tcb_queue_remove_def) + apply (frule heap_ls_prev_of_last) + apply (cases ls; clarsimp) + apply (fastforce intro: butlast_nonempty_length) + apply fastforce + apply (cases ls; force simp: opt_map_def obj_at'_def) + apply (clarsimp simp: prev_queue_head_def opt_map_def obj_at'_def) + \ \tcbPtr is in the middle of ls\ + apply (clarsimp simp: list_queue_relation_def) + apply (frule heap_ls_distinct) + apply (frule split_list) + apply (elim exE) + apply (rename_tac xs ys) + apply (prop_tac "xs \ [] \ ys \ []", fastforce simp: queue_end_valid_def) + apply clarsimp + apply (frule (2) ptr_in_middle_prev_next[where ptr=tcbPtr]) + apply fastforce + apply (frule tcb_queue_remove_middle) + apply clarsimp + apply (intro conjI) + apply (drule (2) heap_ls_remove_middle) + apply (fastforce elim!: rsubst3[where P=heap_ls] simp: opt_map_def obj_at'_def) + apply (simp add: queue_end_valid_def) + apply (subst opt_map_upd_triv) + apply (clarsimp simp: prev_queue_head_def tcb_queue_remove_def opt_map_def obj_at'_def) + apply (intro prev_queue_head_heap_upd) + apply assumption + apply (frule heap_path_head') + apply (prop_tac "the (tcbQueueHead q) \ set xs") + apply (fastforce simp: hd_append) + apply (fastforce simp: hd_append distinct_append opt_map_def obj_at'_def) + apply fastforce + done + +lemma tcbQueuePrepend_list_queue_relation: + "\\s. list_queue_relation ls q (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ tcbPtr \ set ls \ (tcbSchedNexts_of s) tcbPtr = None \ (tcbSchedPrevs_of s) tcbPtr = None\ + tcbQueuePrepend q tcbPtr + \\q' s. list_queue_relation (tcbPtr # ls) q' (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + supply if_split[split del] + apply (clarsimp simp: tcbQueuePrepend_def tcbQueueEmpty_def) + apply (wpsimp wp: threadSet_wp getTCB_wp) + apply (intro conjI impI allI) + \ \ls was originally empty\ + apply (clarsimp simp: list_queue_relation_def queue_end_valid_def prev_queue_head_def) + \ \ls was not originally empty\ + apply (clarsimp simp: list_queue_relation_def) + apply (frule heap_path_not_Nil) + apply (frule (1) heap_path_head) + apply (drule (2) heap_ls_prepend[where new=tcbPtr]) + apply (rule conjI) + apply (fastforce elim: rsubst3[where P=heap_ls] + simp: opt_map_upd_triv opt_map_def obj_at'_def split: if_splits) + apply (clarsimp simp: queue_end_valid_def prev_queue_head_def opt_map_def obj_at'_def + split: if_splits) + done + +(* FIXME RT: move *) +lemma heap_upd_cong: + "\hp = hp'; p = p'\ \ hp(p := val) = hp' (p' := val)" + by fastforce + +lemma tcbQueueAppend_list_queue_relation: + "\\s. list_queue_relation ls q (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ tcbPtr \ set ls + \ (tcbSchedNexts_of s) tcbPtr = None \ (tcbSchedPrevs_of s) tcbPtr = None\ + tcbQueueAppend q tcbPtr + \\q' s. list_queue_relation (ls @ [tcbPtr]) q' (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + supply heap_path_append[simp del] if_split[split del] + apply (clarsimp simp: tcbQueueAppend_def tcbQueueEmpty_def) + apply (wpsimp wp: threadSet_wp getTCB_wp) + apply (intro conjI impI allI) + \ \ls was originally empty\ + apply (clarsimp simp: list_queue_relation_def queue_end_valid_def prev_queue_head_def) + \ \ls was not originally empty\ + apply (clarsimp simp: list_queue_relation_def) + apply (frule heap_path_not_Nil) + apply (frule (1) heap_path_head) + apply (drule (2) heap_ls_append[where new=tcbPtr]) + apply (rule conjI) + apply (erule rsubst3[where P=heap_ls]) + apply (subst opt_map_upd_triv) + apply (fastforce simp: opt_map_def obj_at'_def) + apply (clarsimp simp: queue_end_valid_def) + apply (subst fun_upd_swap) + apply fastforce + apply (simp add: opt_map_upd_triv_None opt_map_upd_triv obj_at'_def) + apply simp + apply simp + apply (force simp: queue_end_valid_def prev_queue_head_def opt_map_def obj_at'_def split: if_splits) + done + +lemma tcbQueueInsert_list_queue_relation: + "\\s. list_queue_relation (xs @ ys) q (tcbSchedNexts_of s) (tcbSchedPrevs_of s) + \ sym_heap_sched_pointers s + \ tcbPtr \ set (xs @ ys) \ xs \ [] \ ys \ [] \ afterPtr = hd ys + \ (tcbSchedNexts_of s) tcbPtr = None \ (tcbSchedPrevs_of s) tcbPtr = None\ + tcbQueueInsert tcbPtr afterPtr + \\_ s. list_queue_relation (xs @ tcbPtr # ys) q (tcbSchedNexts_of s) (tcbSchedPrevs_of s)\" + supply heap_path_append[simp del] + apply (clarsimp simp: tcbQueueInsert_def bind_assoc) + apply (rule bind_wp[OF _ get_tcb_sp'], rename_tac after_tcb) + apply (rule bind_wp[OF _ assert_sp]) + apply (rule hoare_ex_pre_conj[simplified conj_commute], rename_tac beforePtr) + apply (wpsimp wp: threadSet_wp getTCB_wp) + apply (clarsimp simp: list_queue_relation_def) + apply normalise_obj_at' + apply (frule heap_ls_distinct) + apply (frule heap_path_head') + apply (frule nonempty_proper_suffix_split_distinct[where queue="xs @ ys" and sfx=ys]) + apply fastforce + apply (clarsimp simp: suffix_def) + apply simp + apply (clarsimp, rename_tac xs' ys') + apply (frule (2) heap_path_sym_heap_non_nil_lookup_prev) + apply (prop_tac "hd ys \ tcbPtr", fastforce) + apply (prop_tac "beforePtr \ tcbPtr", clarsimp simp: obj_at'_def opt_map_def in_queue_2_def) + apply (metis Un_iff last_in_set set_append) + apply (cut_tac xs=xs and ys=ys and new=tcbPtr in list_insert_before_distinct) + apply (metis distinct_append) + apply fastforce + apply (drule heap_ls_list_insert_before[where new=tcbPtr]) + apply (metis Un_iff set_append) + apply fastforce + apply fastforce + apply (prop_tac "beforePtr = last xs'", clarsimp simp: obj_at'_def opt_map_def) + apply (rule conjI) + apply (erule rsubst3[where P=heap_ls]) + apply (subst fun_upd_swap) + apply fastforce + apply (rule heap_upd_cong) + apply (subst fun_upd_swap) + apply fastforce + apply (fastforce simp: fun_upd_swap opt_map_red obj_at'_def opt_map_upd_triv) + apply fastforce + apply fastforce + apply fastforce + apply (rule conjI) + apply (cases ys; fastforce simp: append_Cons_eq_iff queue_end_valid_def) + apply (fastforce simp: prev_queue_head_def obj_at'_def opt_map_red split: if_splits) + done + +lemma setQueue_sets_queue[wp]: + "\d p ts P. \ \s. P ts \ setQueue d p ts \\rv s. P (ksReadyQueues s (d, p)) \" + unfolding setQueue_def + by (wp, simp) + +lemma threadSet_opt_pred_other: + "t' \ t \ threadSet F t' \\s. P ((prop |< tcbs_of' s) t)\" + apply (wpsimp wp: threadSet_wp) + by (clarsimp simp: obj_at'_def opt_pred_def) + +lemma tcbQueued_True_makes_inQ: + "\\s. ((\tcb. tcbPriority tcb = priority) |< tcbs_of' s) tcbPtr + \ ((\tcb. tcbDomain tcb = domain) |< tcbs_of' s) tcbPtr\ + threadSet (tcbQueued_update (\_. True)) tcbPtr + \\_ s. (inQ domain priority |< tcbs_of' s) tcbPtr\" + apply (wpsimp wp: threadSet_wp) + by (clarsimp simp: inQ_def opt_pred_def opt_map_def obj_at'_def) -lemma ready_or_release'D2: - "\ready_or_release' s'; (tcbQueued |< tcbs_of' s') tcbPtr\ - \ \ (tcbInReleaseQueue |< tcbs_of' s') tcbPtr" - by (clarsimp simp: ready_or_release'_def opt_pred_def opt_map_def split: option.splits) +lemma tcbQueued_False_makes_not_inQ: + "\\\ + threadSet (tcbQueued_update (\_. False)) tcbPtr + \\_ s. \ (inQ domain priority |< tcbs_of' s) tcbPtr\" + apply (wpsimp wp: threadSet_wp) + by (clarsimp simp: inQ_def opt_pred_def opt_map_def obj_at'_def) lemma tcbSchedEnqueue_corres: "tcb_ptr = tcbPtr \ @@ -2382,7 +2754,6 @@ lemma tcbSchedEnqueue_corres: (sym_heap_sched_pointers and valid_sched_pointers and valid_tcbs') (tcb_sched_action tcb_sched_enqueue tcb_ptr) (tcbSchedEnqueue tcbPtr)" supply if_split[split del] - heap_path_append[simp del] fun_upd_apply[simp del] distinct_append[simp del] apply (rule_tac Q'="st_tcb_at' runnable' tcbPtr" in corres_cross_add_guard) apply (fastforce intro!: st_tcb_at_runnable_cross simp: vs_all_heap_simps obj_at_def is_tcb_def) apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard) @@ -2439,9 +2810,14 @@ lemma tcbSchedEnqueue_corres: apply (wpsimp wp: hoare_vcg_if_lift hoare_vcg_ex_lift) apply (corres corres: addToBitmap_if_null_noop_corres) + apply (rule_tac F="tdom = domain \ prio = priority" in corres_req) + apply (fastforce dest: pspace_relation_tcb_domain_priority state_relation_pspace_relation + simp: obj_at_def obj_at'_def) + apply clarsimp + apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre simp: set_tcb_queue_def) - apply (wpsimp simp: tcbQueuePrepend_def wp: hoare_vcg_if_lift2 | drule Some_to_the)+ + apply (wpsimp simp: tcbQueuePrepend_def wp: hoare_vcg_imp_lift' hoare_vcg_if_lift2) apply (clarsimp simp: ex_abs_def split: if_splits) apply (frule state_relation_ready_queues_relation) apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) @@ -2455,141 +2831,60 @@ lemma tcbSchedEnqueue_corres: (solves \frule singleton_eqD, frule set_tcb_queue_projs_inv, wpsimp simp: swp_def\)?) apply (find_goal \match conclusion in "\_\ _ \\_. release_queue_relation t\" for t \ \-\\) - apply (wpsimp wp: threadSet_release_queue_relation threadSet_tcbInReleaseQueue - simp: tcbQueuePrepend_def) - apply normalise_obj_at' - apply (rename_tac s' tcb) - apply (prop_tac "release_queue_relation t s'") - apply (force dest!: set_tcb_queue_projs_inv simp: release_queue_relation_def) - apply simp - apply (rule impI) - apply (erule ready_or_release'D2) - apply (rule inQ_implies_tcbQueueds_of) - apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) - apply (cut_tac d="tcbDomain tcb" and p="tcbPriority tcb" in tcbQueueHead_ksReadyQueues) - apply fast - apply fast - apply force + apply (frule_tac d=domain and p=priority in ready_or_release_disjoint) + apply (drule set_tcb_queue_projs_inv) + apply (wpsimp wp: tcbQueuePrepend_list_queue_relation_other hoare_vcg_ex_lift + threadSet_sched_pointers + simp: release_queue_relation_def setQueue_def + | wps)+ + apply (rule_tac x="ready_queues s (tcbDomain tcba) (tcbPriority tcb)" in exI) + apply (auto simp: ready_queues_relation_def ready_queue_relation_def Let_def)[1] \ \ready_queues_relation\ apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) apply (intro hoare_allI) apply (drule singleton_eqD) apply (drule set_tcb_queue_new_state) - apply (wpsimp wp: threadSet_wp simp: setQueue_def tcbQueuePrepend_def) - apply normalise_obj_at' - apply (clarsimp simp: obj_at_def) - apply (rename_tac s' tcb' tcb) - apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) - apply (force simp: obj_at_def) - apply (force simp: obj_at'_def) - apply (clarsimp split: if_splits) - apply (cut_tac ts="ready_queues s d p" in list_queue_relation_nil) - apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - in list_queue_relation_nil) - apply (force dest!: spec simp: list_queue_relation_def) - apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" and s'=s' - in obj_at'_tcbQueueEnd_ksReadyQueues) - apply fast - apply auto[1] - apply fastforce - apply fastforce - apply (cut_tac xs="ready_queues s d p" and st="tcbQueueHead (ksReadyQueues s' (d, p))" - in heap_path_head') - apply (auto dest: spec simp: list_queue_relation_def tcbQueueEmpty_def)[1] - apply (cut_tac xs="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - and st="tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))" - in heap_path_head') - apply (auto dest: spec simp: list_queue_relation_def tcbQueueEmpty_def)[1] - apply (clarsimp simp: list_queue_relation_def) + apply (intro hoare_vcg_conj_lift_pre_fix) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxDomain < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueuePrepend_def) + apply (frule valid_tcbs'_maxDomain[where t=tcbPtr]) + apply fastforce + subgoal by (force simp: obj_at'_def tcbQueueEmpty_def split: if_split) - apply (case_tac "\ (d = tcb_domain tcb \ p = tcb_priority tcb)") - apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" - in ready_queues_disjoint) - apply force + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxPriority < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueuePrepend_def) + apply (frule valid_tcbs'_maxPriority[where t=tcbPtr]) apply fastforce + subgoal by (force simp: obj_at'_def tcbQueueEmpty_def split: if_split) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. list_queue_relation _ _ _ _ \" \ \-\\) + apply (clarsimp simp: obj_at_def) + apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") + apply (wpsimp wp: tcbQueuePrepend_list_queue_relation_other setQueue_ksReadyQueues_other + threadSet_sched_pointers hoare_vcg_ex_lift + | wps)+ + apply (intro conjI) + subgoal by fastforce + apply (rule_tac x="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in exI) + apply (auto dest!: in_correct_ready_qD simp: ready_queues_disjoint + split: if_splits)[1] apply fastforce - apply (prop_tac "tcbPtr \ set (ready_queues s d p)") - apply (force simp: in_correct_ready_qD) - apply (intro conjI impI; simp) - - \ \the ready queue was originally empty\ - apply (rule heap_path_heap_upd_not_in) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply fastforce - apply (clarsimp simp: queue_end_valid_def fun_upd_apply split: if_splits) - apply (rule prev_queue_head_heap_upd) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (case_tac "ready_queues s d p"; - clarsimp simp: fun_upd_apply tcbQueueEmpty_def split: if_splits) - apply (clarsimp simp: inQ_def in_opt_pred fun_upd_apply obj_at'_def split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - - \ \the ready queue was not originally empty\ - apply clarsimp - apply (prop_tac "the (tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb))) - \ set (ready_queues s d p)") - apply (erule orthD2) - apply (clarsimp simp: tcbQueueEmpty_def) - apply (intro conjI impI allI) - apply (intro heap_path_heap_upd_not_in) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply simp - apply fastforce - apply (clarsimp simp: queue_end_valid_def fun_upd_apply split: if_splits) - apply (intro prev_queue_head_heap_upd) - apply (force simp: fun_upd_apply split: if_splits) - apply (case_tac "ready_queues s d p"; - force simp: fun_upd_apply tcbQueueEmpty_def split: if_splits) - apply (clarsimp simp: fun_upd_apply inQ_def split: if_splits) - apply (case_tac "ready_queues s d p"; force simp: tcbQueueEmpty_def) - apply (case_tac "t = tcbPtr") - apply (clarsimp simp: inQ_def fun_upd_apply obj_at'_def split: if_splits) - apply (case_tac "t = the (tcbQueueHead (ksReadyQueues s' (tcb_domain tcb, tcb_priority tcb)))") - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def obj_at'_def fun_upd_apply - split: option.splits) - apply metis - apply (clarsimp simp: inQ_def in_opt_pred opt_map_def fun_upd_apply) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - - \ \d = tcb_domain tcb \ p = tcb_priority tcb\ - apply clarsimp - apply (drule_tac x="tcb_domain tcb" in spec) - apply (drule_tac x="tcb_priority tcb" in spec) - apply (cut_tac ts="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - in tcbQueueHead_iff_tcbQueueEnd) - apply (force simp: list_queue_relation_def) - apply (frule valid_tcbs'_maxDomain[where t=tcbPtr], fastforce) - apply (frule valid_tcbs'_maxPriority[where t=tcbPtr], fastforce) - apply (drule valid_sched_pointersD[where t=tcbPtr]) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (clarsimp simp: in_opt_pred opt_map_red obj_at'_def) - apply (intro conjI; clarsimp simp: tcbQueueEmpty_def) - - \ \the ready queue was originally empty\ - apply (force simp: inQ_def in_opt_pred fun_upd_apply queue_end_valid_def prev_queue_head_def - opt_map_red obj_at'_def - split: if_splits) - - \ \the ready queue was not originally empty\ - apply (drule obj_at'_prop)+ - apply clarsimp - apply (drule (2) heap_ls_prepend[where new=tcbPtr]) - apply (rule conjI) - apply (clarsimp simp: fun_upd_apply) - apply (rule conjI) - apply (subst opt_map_upd_triv) - apply (clarsimp simp: opt_map_def obj_at'_def fun_upd_apply split: if_splits) - apply (clarsimp simp: fun_upd_apply split: if_splits) - apply (rule conjI) - apply (clarsimp simp: fun_upd_apply queue_end_valid_def) - apply (rule conjI) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply opt_map_def split: if_splits) - by (auto dest!: hd_in_set simp: inQ_def in_opt_pred opt_map_def fun_upd_apply - split: if_splits option.splits) + apply ((wpsimp wp: tcbQueuePrepend_list_queue_relation threadSet_sched_pointers | wps)+)[1] + apply (fastforce dest!: valid_sched_pointersD[where t=tcbPtr] + simp: in_opt_pred opt_map_red obj_at'_def) + + apply (rule hoare_allI, rename_tac t') + apply (case_tac "d \ domain \ p \ priority") + apply (wpsimp wp: tcbQueued_update_inQ_other hoare_vcg_disj_lift + simp: opt_pred_disj[simplified pred_disj_def, symmetric] simp_del: disj_not1) + apply (clarsimp simp: opt_map_def opt_pred_def obj_at'_def split: option.splits if_splits) + apply (case_tac "t' = tcbPtr") + apply (wpsimp wp: tcbQueued_True_makes_inQ) + apply (clarsimp simp: opt_pred_def opt_map_def obj_at'_def) + apply (wpsimp wp: threadSet_opt_pred_other) + done definition weak_sch_act_wf :: "scheduler_action \ kernel_state \ bool" where "weak_sch_act_wf sa s \ \t. sa = SwitchToThread t \ tcb_at' t s" @@ -3045,20 +3340,6 @@ lemma gets_the_exec: "f s \ None \ (do x \ ge return_def assert_opt_def) done -\ \ - A direct analogue of tcbQueueRemove, used in tcb_sched_dequeue' below, so that within the proof of - tcbQueueRemove_corres, we may reason in terms of the list operations used within this function - rather than @{term filter}.\ -definition tcb_queue_remove :: "'a \ 'a list \ 'a list" where - "tcb_queue_remove a ls \ - if ls = [a] - then [] - else if a = hd ls - then tl ls - else if a = last ls - then butlast ls - else list_remove ls a" - definition tcb_sched_dequeue' :: "obj_ref \ unit det_ext_monad" where "tcb_sched_dequeue' tcb_ptr \ do d \ thread_get tcb_domain tcb_ptr; @@ -3272,7 +3553,7 @@ lemma tcbSchedPrev_update_valid_objs'[wp]: lemma tcbQueuePrepend_valid_objs'[wp]: "\\s. valid_objs' s \ tcb_at' tcbPtr s - \ (\ tcbQueueEmpty queue \ tcb_at' (the (tcbQueueHead queue)) s)\ + \ (\head. tcbQueueHead queue = Some head \ tcb_at' head s)\ tcbQueuePrepend queue tcbPtr \\_. valid_objs'\" unfolding tcbQueuePrepend_def @@ -3287,10 +3568,13 @@ lemma tcbSchedEnqueue_valid_objs'[wp]: tcbSchedEnqueue tcbPtr \\_. valid_objs'\" unfolding tcbSchedEnqueue_def setQueue_def - apply (wpsimp wp: threadSet_valid_objs' threadGet_wp) + apply (wpsimp wp: threadSet_valid_objs' threadGet_wp hoare_vcg_all_lift) apply normalise_obj_at' - apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues - simp: ready_queue_relation_def ksReadyQueues_asrt_def) + apply (rename_tac tcb head) + apply (clarsimp simp: ksReadyQueues_asrt_def ready_queue_relation_def) + apply (drule_tac x="tcbDomain tcb" in spec) + apply (drule_tac x="tcbPriority tcb" in spec) + apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues simp: tcbQueueEmpty_def) done crunch rescheduleRequired, removeFromBitmap, scheduleTCB @@ -3308,7 +3592,7 @@ lemma tcbQueueRemove_valid_objs'[wp]: lemma tcbSchedDequeue_valid_objs'[wp]: "tcbSchedDequeue t \valid_objs'\" unfolding tcbSchedDequeue_def setQueue_def - by (wpsimp wp: threadSet_valid_objs') + by (wpsimp wp: threadSet_valid_objs' threadGet_wp) lemma sts_valid_objs': "\valid_objs' and valid_tcb_state' st and pspace_aligned' and pspace_distinct'\ @@ -3985,11 +4269,6 @@ lemma setQueue_bitmapQ_no_L2_orphans[wp]: unfolding setQueue_def bitmapQ_no_L2_orphans_def null_def by (wp, auto) -lemma setQueue_sets_queue[wp]: - "\d p ts P. \ \s. P ts \ setQueue d p ts \\rv s. P (ksReadyQueues s (d, p)) \" - unfolding setQueue_def - by (wp, simp) - crunch setQueue for ksReleaseQueue[wp]: "\s. P (ksReleaseQueue s)" @@ -4005,17 +4284,11 @@ crunch tcbSchedEnqueue lemma tcbSchedPrev_update_tcbInReleaseQueues[wp]: "threadSet (tcbSchedPrev_update f) tcbPtr \\s. P (tcbInReleaseQueue |< tcbs_of' s)\" - apply (wpsimp wp: threadSet_wp) - apply (fastforce simp: obj_at'_def opt_pred_def opt_map_def - split: option.splits elim!: rsubst[where P=P]) - done + by (wpsimp wp: threadSet_tcbInReleaseQueue) lemma tcbSchedNext_update_tcbInReleaseQueue[wp]: "threadSet (tcbSchedNext_update f) tcbPtr \\s. P (tcbInReleaseQueue |< tcbs_of' s)\" - apply (wpsimp wp: threadSet_wp) - apply (fastforce simp: obj_at'_def opt_pred_def opt_map_def - split: option.splits elim!: rsubst[where P=P]) - done + by (wpsimp wp: threadSet_tcbInReleaseQueue) crunch tcbSchedEnqueue for valid_dom_schedule'_misc[wp]: "\s. P (ksDomScheduleIdx s) (ksDomSchedule s)" @@ -4138,7 +4411,7 @@ lemma tcbQueued_update_valid_tcbs'[wp]: lemma tcbQueuePrepend_valid_tcbs'[wp]: "\\s. valid_tcbs' s \ tcb_at' tcbPtr s - \ (\ tcbQueueEmpty queue \ tcb_at' (the (tcbQueueHead queue)) s)\ + \ (\head. tcbQueueHead queue = Some head \ tcb_at' head s)\ tcbQueuePrepend queue tcbPtr \\_. valid_tcbs'\" unfolding tcbQueuePrepend_def @@ -4149,9 +4422,13 @@ lemma tcbSchedEnqueue_valid_tcbs': tcbSchedEnqueue thread \\_. valid_tcbs'\" apply (clarsimp simp: tcbSchedEnqueue_def setQueue_def bitmap_fun_defs) - apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift' threadGet_wp) - apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues - simp: ready_queue_relation_def ksReadyQueues_asrt_def obj_at'_def) + apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift' threadGet_wp hoare_vcg_all_lift) + apply normalise_obj_at' + apply (rename_tac tcb head) + apply (clarsimp simp: ksReadyQueues_asrt_def ready_queue_relation_def) + apply (drule_tac x="tcbDomain tcb" in spec) + apply (drule_tac x="tcbPriority tcb" in spec) + apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues simp: tcbQueueEmpty_def) done lemma setSchedulerAction_valid_tcbs'[wp]: @@ -4834,12 +5111,10 @@ lemma tcbSchedDequeue_tcbState_obj_at'[wp]: lemma tcbSchedDequeue_pred_tcb_at'[wp]: "tcbSchedDequeue t \\s. Q (pred_tcb_at' proj P t' s)\" - apply (rule_tac P=Q in P_bool_lift) - apply (simp add: tcbSchedDequeue_def tcbQueueRemove_def) - apply (wp threadSet_pred_tcb_no_state getTCB_wp threadGet_wp | clarsimp simp: tcb_to_itcb'_def)+ - apply (simp add: tcbSchedDequeue_def tcbQueueRemove_def) - apply (wp threadSet_pred_tcb_no_state getTCB_wp threadGet_wp | clarsimp simp: tcb_to_itcb'_def)+ - done + by (rule_tac P=Q in P_bool_lift; + simp add: tcbSchedDequeue_def tcbQueueRemove_def, + (wp threadSet_pred_tcb_no_state getTCB_wp threadGet_wp hoare_vcg_all_lift hoare_drop_imps + | clarsimp simp: tcb_to_itcb'_def)+) crunch tcbQueueRemove for pred_tcb_at'[wp]: "\s. P' (pred_tcb_at' proj P t' s)" @@ -5001,6 +5276,14 @@ lemma tcbSchedPrev_update_ctes_of[wp]: "threadSet (tcbSchedPrev_update f) x \\s. P (ctes_of s)\" by (wpsimp wp: threadSet_ctes_ofT simp: tcbSchedPrev_update_tcb_cte_cases) +lemma tcbQueued_ex_nonz_cap_to'[wp]: + "threadSet (tcbQueued_update f) tptr \ex_nonz_cap_to' p\" + by (wpsimp wp: threadSet_cap_to simp: tcbQueued_update_tcb_cte_cases) + +lemma tcbInReleaseQueue_ex_nonz_cap_to'[wp]: + "threadSet (tcbInReleaseQueue_update f) tptr \ex_nonz_cap_to' p\" + by (wpsimp wp: threadSet_cap_to simp: tcbInReleaseQueue_update_tcb_cte_cases) + lemma tcbSchedNext_ex_nonz_cap_to'[wp]: "threadSet (tcbSchedNext_update f) tptr \ex_nonz_cap_to' p\" by (wpsimp wp: threadSet_cap_to simp: tcbSchedNext_update_tcb_cte_cases) @@ -5053,20 +5336,22 @@ lemma tcbQueueRemove_ex_nonz_cap_to'[wp]: lemma tcbQueuePrepend_if_live_then_nonz_cap': "\\s. if_live_then_nonz_cap' s \ ex_nonz_cap_to' tcbPtr s - \ (\ tcbQueueEmpty q \ ex_nonz_cap_to' (the (tcbQueueHead q)) s)\ + \ (\head. tcbQueueHead q = Some head \ ex_nonz_cap_to' head s)\ tcbQueuePrepend q tcbPtr \\_. if_live_then_nonz_cap'\" - unfolding tcbQueuePrepend_def + unfolding tcbQueuePrepend_def tcbQueueEmpty_def by (wpsimp wp: tcbSchedPrev_update_iflive' tcbSchedNext_update_iflive' hoare_vcg_if_lift2 hoare_vcg_imp_lift') lemma tcbQueueAppend_if_live_then_nonz_cap': "\\s. if_live_then_nonz_cap' s \ ex_nonz_cap_to' tcbPtr s - \ (\ tcbQueueEmpty q \ ex_nonz_cap_to' (the (tcbQueueEnd q)) s)\ + \ (\end. tcbQueueEnd q = Some end \ ex_nonz_cap_to' end s) + \ (\ls. list_queue_relation ls q (tcbSchedNexts_of s) (tcbSchedPrevs_of s))\ tcbQueueAppend q tcbPtr \\_. if_live_then_nonz_cap'\" - unfolding tcbQueueAppend_def - by (wpsimp wp: tcbSchedPrev_update_iflive' tcbSchedNext_update_iflive') + unfolding tcbQueueAppend_def tcbQueueEmpty_def + apply (wpsimp wp: tcbSchedPrev_update_iflive' tcbSchedNext_update_iflive') + by (fastforce dest: tcbQueueHead_iff_tcbQueueEnd) lemma tcbQueueInsert_if_live_then_nonz_cap': "\if_live_then_nonz_cap' and ex_nonz_cap_to' tcbPtr and valid_objs' and sym_heap_sched_pointers\ @@ -5089,7 +5374,8 @@ lemma tcbSchedEnqueue_iflive'[wp]: tcbSchedEnqueue tcbPtr \\_. if_live_then_nonz_cap'\" unfolding tcbSchedEnqueue_def - apply (wpsimp wp: tcbQueuePrepend_if_live_then_nonz_cap' threadGet_wp) + apply (wpsimp wp: tcbQueuePrepend_if_live_then_nonz_cap' threadGet_wp hoare_vcg_imp_lift' + hoare_vcg_all_lift) apply (normalise_obj_at', rename_tac tcb) apply (frule_tac p=tcbPtr in if_live_then_nonz_capE') apply (fastforce simp: ko_wp_at'_def obj_at'_def ) @@ -5098,10 +5384,8 @@ lemma tcbSchedEnqueue_iflive'[wp]: apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) - apply (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues - simp: ko_wp_at'_def inQ_def opt_pred_def opt_map_def obj_at'_def - split: option.splits) - done + by (fastforce dest!: obj_at'_tcbQueueHead_ksReadyQueues + simp: ko_wp_at'_def inQ_def obj_at'_def tcbQueueEmpty_def) crunch scheduleTCB for if_live_then_nonz_cap'[wp]: if_live_then_nonz_cap' @@ -5514,7 +5798,7 @@ lemma tcbSchedEnqueue_valid_bitmapQ[wp]: unfolding tcbSchedEnqueue_def apply (wpsimp simp: tcbQueuePrepend_def wp: setQueue_valid_bitmapQ' addToBitmap_valid_bitmapQ_except addToBitmap_bitmapQ - threadGet_wp) + threadGet_wp threadSet_bitmapQ) apply (fastforce simp: valid_bitmaps_def valid_bitmapQ_def tcbQueueEmpty_def split: if_splits) done @@ -5585,14 +5869,6 @@ lemma tcbSchedAppend_valid_sched_pointers[wp]: split: if_splits option.splits; fastforce) -lemma in_queue_not_head_or_not_tail_length_gt_1: - "\tcbPtr \ set ls; tcbQueueHead q \ Some tcbPtr \ tcbQueueEnd q \ Some tcbPtr; - list_queue_relation ls q nexts prevs\ - \ Suc 0 < length ls" - apply (clarsimp simp: list_queue_relation_def) - apply (cases ls; fastforce simp: queue_end_valid_def) - done - lemma monadic_rewrite_threadSet_same: "monadic_rewrite F E (obj_at' (\tcb :: tcb. f tcb = tcb) tcbPtr) (threadSet f tcbPtr) (return ())" @@ -5609,16 +5885,6 @@ lemma monadic_rewrite_threadSet_same: apply (clarsimp simp: obj_at'_def) done -lemma list_queue_relation_neighbour_in_set: - "\list_queue_relation ls q hp hp'; sym_heap hp hp'; p \ set ls\ - \ \nbr. (hp p = Some nbr \ nbr \ set ls) \ (hp' p = Some nbr \ nbr \ set ls)" - apply (rule heap_ls_neighbour_in_set) - apply (fastforce simp: list_queue_relation_def) - apply fastforce - apply (clarsimp simp: list_queue_relation_def prev_queue_head_def) - apply fastforce - done - lemma tcbSchedDequeue_valid_sched_pointers[wp]: "\valid_sched_pointers and sym_heap_sched_pointers\ tcbSchedDequeue tcbPtr @@ -5644,21 +5910,22 @@ lemma tcbSchedDequeue_valid_sched_pointers[wp]: apply (simp add: fun_upd_def opt_pred_def) \ \tcbPtr is the head of the ready queue\ subgoal - by (auto dest!: heap_ls_last_None - simp: valid_sched_pointers_def fun_upd_apply prev_queue_head_def - inQ_def opt_pred_def opt_map_def obj_at'_def - split: if_splits option.splits) + by (clarsimp simp: valid_sched_pointers_def fun_upd_apply prev_queue_head_def + inQ_def opt_pred_def opt_map_def obj_at'_def + split: if_splits option.splits; + auto) \ \tcbPtr is the end of the ready queue\ + apply (frule heap_ls_last_None) + apply (fastforce simp: fun_upd_apply opt_map_def obj_at'_def) subgoal - by (auto dest!: heap_ls_last_None - simp: valid_sched_pointers_def queue_end_valid_def inQ_def opt_pred_def - opt_map_def fun_upd_apply obj_at'_def - split: if_splits option.splits) + by (clarsimp simp: valid_sched_pointers_def inQ_def opt_pred_def + opt_map_def fun_upd_apply obj_at'_def queue_end_valid_def + split: if_splits option.splits; + auto) \ \tcbPtr is in the middle of the ready queue\ - apply (intro conjI impI allI) - by (clarsimp simp: valid_sched_pointers_def inQ_def opt_pred_def opt_map_def fun_upd_apply obj_at'_def - split: if_splits option.splits; - auto) + by (auto simp: valid_sched_pointers_def inQ_def opt_pred_def opt_map_def fun_upd_apply + obj_at'_def + split: if_splits option.splits) lemma tcbQueueRemove_sym_heap_sched_pointers: "\\s. sym_heap_sched_pointers s @@ -5791,41 +6058,39 @@ lemma tcbSchedEnqueue_sym_heap_sched_pointers[wp]: tcbSchedEnqueue tcbPtr \\_. sym_heap_sched_pointers\" unfolding tcbSchedEnqueue_def - apply (wpsimp wp: tcbQueuePrepend_sym_heap_sched_pointers threadGet_wp - simp: addToBitmap_def bitmap_fun_defs) + apply (wpsimp wp: tcbQueuePrepend_sym_heap_sched_pointers threadGet_wp threadSet_sched_pointers + simp: addToBitmap_def bitmap_fun_defs | wps)+ apply (normalise_obj_at', rename_tac tcb) apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) - apply (fastforce dest!: spec[where x=tcbPtr] inQ_implies_tcbQueueds_of - simp: valid_sched_pointers_def opt_pred_def opt_map_def obj_at'_def) - done + by (fastforce dest!: spec[where x=tcbPtr] inQ_implies_tcbQueueds_of + simp: valid_sched_pointers_def opt_pred_def opt_map_def obj_at'_def) lemma tcbSchedAppend_sym_heap_sched_pointers[wp]: "\sym_heap_sched_pointers and valid_sched_pointers\ tcbSchedAppend tcbPtr \\_. sym_heap_sched_pointers\" unfolding tcbSchedAppend_def - apply (wpsimp wp: tcbQueueAppend_sym_heap_sched_pointers threadGet_wp + apply (wpsimp wp: tcbQueueAppend_sym_heap_sched_pointers threadGet_wp threadSet_sched_pointers simp: addToBitmap_def bitmap_fun_defs) apply (normalise_obj_at', rename_tac tcb) apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) apply (drule_tac x="tcbDomain tcb" in spec) apply (drule_tac x="tcbPriority tcb" in spec) - apply (fastforce dest!: spec[where x=tcbPtr] inQ_implies_tcbQueueds_of - simp: valid_sched_pointers_def opt_pred_def opt_map_def obj_at'_def) - done + by (fastforce dest!: spec[where x=tcbPtr] inQ_implies_tcbQueueds_of + simp: valid_sched_pointers_def opt_pred_def opt_map_def obj_at'_def) lemma tcbSchedDequeue_sym_heap_sched_pointers[wp]: "\sym_heap_sched_pointers and valid_sched_pointers\ tcbSchedDequeue tcbPtr \\_. sym_heap_sched_pointers\" unfolding tcbSchedDequeue_def - apply (wpsimp wp: tcbQueueRemove_sym_heap_sched_pointers hoare_vcg_if_lift2 threadGet_wp - simp: bitmap_fun_defs) - apply (fastforce simp: ready_queue_relation_def ksReadyQueues_asrt_def inQ_def opt_pred_def - opt_map_def obj_at'_def) - done + apply (wpsimp wp: tcbQueueRemove_sym_heap_sched_pointers threadGet_wp threadSet_sched_pointers + simp: bitmap_fun_defs + | wps)+ + by (fastforce simp: ready_queue_relation_def ksReadyQueues_asrt_def inQ_def opt_pred_def + opt_map_def obj_at'_def) crunch setThreadState for valid_sched_pointers[wp]: valid_sched_pointers @@ -6110,6 +6375,7 @@ crunch setReleaseQueue, tcbQueueRemove, setReprogramTimer crunch tcbReleaseRemove for valid_objs'[wp]: valid_objs' + (simp: crunch_simps) crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue for pred_tcb_at'[wp]: "\s. P' (pred_tcb_at' P obj t s)" @@ -6153,25 +6419,17 @@ lemma tcbReleaseRemove_if_live_then_nonz_cap'[wp]: "\if_live_then_nonz_cap' and valid_objs' and sym_heap_sched_pointers\ tcbReleaseRemove tcbPtr \\_. if_live_then_nonz_cap'\" - apply (clarsimp simp: tcbReleaseRemove_def setReleaseQueue_def) - apply (wpsimp wp: tcbQueueRemove_if_live_then_nonz_cap' inReleaseQueue_wp) - apply (fastforce elim: if_live_then_nonz_capE' - simp: obj_at'_def ko_wp_at'_def) - done + unfolding tcbReleaseRemove_def setReleaseQueue_def + apply (wpsimp wp: tcbQueueRemove_if_live_then_nonz_cap' inReleaseQueue_wp threadSet_valid_objs') + by (fastforce elim: if_live_then_nonz_capE' simp: obj_at'_def ko_wp_at'_def) lemma tcbSchedPrev_update_tcbQueueds_of[wp]: "threadSet (tcbSchedPrev_update f) tcbPtr \\s. P (tcbQueued |< tcbs_of' s)\" - apply (wpsimp wp: threadSet_wp) - apply (erule rsubst[where P=P]) - apply (fastforce simp: opt_pred_def obj_at'_def opt_map_def split: option.splits) - done + by (wpsimp wp: threadSet_tcbQueued) lemma tcbSchedNext_update_tcbQueueds_of[wp]: "threadSet (tcbSchedNext_update f) tcbPtr \\s. P (tcbQueued |< tcbs_of' s)\" - apply (wpsimp wp: threadSet_wp) - apply (erule rsubst[where P=P]) - apply (fastforce simp: opt_pred_def obj_at'_def opt_map_def split: option.splits) - done + by (wpsimp wp: threadSet_tcbQueued) lemma setReprogramTimer_ready_or_release'[wp]: "setReprogramTimer reprogramTimer \ready_or_release'\" @@ -6208,9 +6466,6 @@ crunch removeFromBitmap crunch removeFromBitmap for release_queue_relation[wp]: "release_queue_relation s" and ready_queues_relation[wp]: "ready_queues_relation s" - and list_queue_relation[wp]: - "\s'. list_queue_relation ts (P (ksReadyQueues s')) - (tcbSchedNexts_of s') (tcbSchedPrevs_of s')" (simp: bitmap_fun_defs release_queue_relation_def ready_queues_relation_def) lemma ready_or_release'_inQ: @@ -6225,8 +6480,7 @@ lemma tcbSchedDequeue_corres: and pspace_aligned and pspace_distinct) (sym_heap_sched_pointers and valid_objs') (tcb_sched_action tcb_sched_dequeue tcb_ptr) (tcbSchedDequeue tcbPtr)" - supply heap_path_append[simp del] fun_upd_apply[simp del] distinct_append[simp del] - list_remove_append[simp del] + supply if_split[split del] apply (rule_tac Q'="tcb_at' tcbPtr" in corres_cross_add_guard) apply (fastforce intro!: tcb_at_cross simp: vs_all_heap_simps obj_at_def is_tcb_def) apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard) @@ -6236,7 +6490,7 @@ lemma tcbSchedDequeue_corres: apply (rule monadic_rewrite_corres_l[where P=P and Q=P for P, simplified]) apply (rule monadic_rewrite_guard_imp[OF tcb_sched_dequeue_monadic_rewrite]) apply (clarsimp simp: ready_qs_distinct_def) - apply (clarsimp simp: tcb_sched_dequeue'_def get_tcb_queue_def tcbSchedDequeue_def getQueue_def + apply (clarsimp simp: tcb_sched_dequeue'_def get_tcb_queue_def tcbSchedDequeue_def getQueue_def unless_def when_def) apply (rule corres_symb_exec_l[OF _ _ thread_get_sp]; wpsimp?) apply (rename_tac dom) @@ -6251,235 +6505,93 @@ lemma tcbSchedDequeue_corres: apply (rule corres_if_strong'; fastforce?) apply (intro iffI) apply (frule state_relation_ready_queues_relation) - apply (fastforce dest: in_ready_q_tcbQueued_eq[THEN iffD1] - simp: obj_at'_def obj_at_def in_ready_q_def opt_pred_def opt_map_def) + apply (fastforce dest!: in_ready_q_tcbQueued_eq[THEN iffD1] + simp: obj_at'_def obj_at_def in_ready_q_def opt_pred_def opt_map_def) apply (frule state_relation_ready_queues_relation) apply (frule in_ready_q_tcbQueued_eq[THEN iffD2, where t1=tcb_ptr]) apply (fastforce simp: obj_at'_def opt_pred_def opt_map_def) apply (fastforce simp: in_correct_ready_q_def vs_all_heap_simps obj_at_def in_ready_q_def) apply (rule corres_symb_exec_r[OF _ threadGet_sp]; wpsimp?) + apply (rename_tac dom') apply (rule corres_symb_exec_r[OF _ threadGet_sp]; wpsimp?) - apply (rule corres_symb_exec_r[OF _ gets_sp]; wpsimp?) + apply (rename_tac prio') + + apply (rule_tac F="dom' = dom \ prio' = prio" in corres_req) + apply (fastforce dest: pspace_relation_tcb_domain_priority state_relation_pspace_relation + simp: obj_at_def obj_at'_def) + apply clarsimp apply (rule corres_from_valid_det) apply (fastforce intro: det_wp_modify det_wp_pre simp: set_tcb_queue_def) - apply (wpsimp wp: tcbQueueRemove_no_fail) + apply ((wpsimp wp: tcbQueueRemove_no_fail hoare_vcg_ex_lift + threadSet_sched_pointers threadSet_valid_objs' + | wps)+)[1] apply (fastforce dest: state_relation_ready_queues_relation - simp: ex_abs_def ready_queues_relation_def ready_queue_relation_def Let_def - inQ_def opt_pred_def opt_map_def obj_at'_def) + simp: ex_abs_def ready_queues_relation_def ready_queue_relation_def Let_def) apply (clarsimp simp: state_relation_def) apply (intro hoare_vcg_conj_lift_pre_fix; (solves \frule singleton_eqD, frule set_tcb_queue_projs_inv, wpsimp simp: swp_def\)?) apply (find_goal \match conclusion in "\_\ _ \\_. release_queue_relation t\" for t \ \-\\) - apply (simp add: tcbQueueRemove_def) - apply (wpsimp wp: threadSet_release_queue_relation threadSet_tcbInReleaseQueue - getTCB_wp hoare_vcg_imp_lift') - apply normalise_obj_at' - apply (drule obj_at'_prop)+ - apply (rename_tac s' tcb) - apply (cut_tac p=tcbPtr and ls="ready_queues s dom prio" in list_queue_relation_neighbour_in_set) - apply (fastforce dest!: spec simp: ready_queues_relation_def ready_queue_relation_def Let_def) - apply fastforce - apply fastforce - apply (prop_tac "release_queue_relation t s'") - apply (force dest!: set_tcb_queue_projs_inv simp: release_queue_relation_def) - apply (drule_tac domain=dom and prio=prio in ready_or_release'_inQ) - apply (force simp: opt_map_def ready_queues_relation_def ready_queue_relation_def Let_def - split: option.splits) + apply (frule_tac d=dom and p=prio in ready_or_release_disjoint) + apply (drule set_tcb_queue_projs_inv) + apply (wpsimp wp: tcbQueueRemove_list_queue_relation_other hoare_vcg_ex_lift + threadSet_sched_pointers + simp: release_queue_relation_def + | wps)+ + apply (rule_tac x="ready_queues s (tcbDomain tcba) (tcbPriority tcb)" in exI) + apply (auto simp: ready_queues_relation_def ready_queue_relation_def Let_def)[1] \ \ready_queues_relation\ apply (clarsimp simp: ready_queues_relation_def ready_queue_relation_def Let_def) apply (intro hoare_allI) apply (drule singleton_eqD) apply (drule set_tcb_queue_new_state) - apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueueRemove_def split_del: if_split) - apply normalise_obj_at' - apply (drule tcb_at_ko_at)+ - apply clarsimp - apply (rename_tac s' tcb' tcb) - apply (clarsimp simp: obj_at_def) - apply (frule_tac t=tcbPtr in pspace_relation_tcb_domain_priority) - apply (fastforce simp: obj_at_def) - apply (fastforce simp: obj_at'_def) - - apply (case_tac "d \ tcb_domain tcb \ p \ tcb_priority tcb") - apply clarsimp - apply (cut_tac p=tcbPtr and ls="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" - in list_queue_relation_neighbour_in_set) - apply (fastforce dest!: spec) - apply fastforce - apply fastforce - apply (cut_tac xs="ready_queues s d p" in heap_path_head') - apply (force dest!: spec simp: ready_queues_relation_def Let_def list_queue_relation_def) - apply (cut_tac d=d and d'="tcb_domain tcb" and p=p and p'="tcb_priority tcb" - in ready_queues_disjoint) - apply fastforce - apply fastforce - apply fastforce - apply (cut_tac ts="ready_queues s d p" in list_queue_relation_nil) - apply fast - apply (clarsimp simp: tcbQueueEmpty_def) - apply (prop_tac "Some tcbPtr \ tcbQueueHead (ksReadyQueues s' (d, p))") - apply (metis hd_in_set not_emptyI option.sel option.simps(2)) - apply (prop_tac "tcbPtr \ set (ready_queues s d p)") - apply blast - apply (clarsimp simp: list_queue_relation_def) - apply (intro conjI; clarsimp) - - \ \the ready queue is the singleton consisting of tcbPtr\ - apply (intro conjI) - apply (force intro!: heap_path_heap_upd_not_in simp: fun_upd_apply) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply) - apply (force simp: prev_queue_head_heap_upd fun_upd_apply) - apply (clarsimp simp: inQ_def in_opt_pred fun_upd_apply) - apply (clarsimp simp: fun_upd_apply) - apply (clarsimp simp: fun_upd_apply) - - apply (intro conjI; clarsimp) - - \ \tcbPtr is the head of the ready queue\ + apply (intro hoare_vcg_conj_lift_pre_fix) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxDomain < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueueRemove_def) + apply (force simp: obj_at_def tcbQueueEmpty_def split: if_split) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. maxPriority < d \ _\" for d \ \-\\) + apply (wpsimp wp: threadSet_wp getTCB_wp simp: setQueue_def tcbQueueRemove_def) + apply (force simp: obj_at_def tcbQueueEmpty_def split: if_split) + + apply (find_goal \match conclusion in "\_\ _ \\_ s. list_queue_relation _ _ _ _ \" \ \-\\) + apply (case_tac "d \ dom \ p \ prio") + apply (clarsimp simp: obj_at_def obj_at'_def) + apply (wpsimp wp: tcbQueueRemove_list_queue_relation_other setQueue_ksReadyQueues_other + threadSet_sched_pointers hoare_vcg_ex_lift + | wps)+ + apply (frule (2) pspace_relation_tcb_domain_priority[where t=tcbPtr]) apply (intro conjI) - apply (intro heap_path_heap_upd_not_in) - apply (force simp: fun_upd_apply) - apply (force simp: not_emptyI opt_map_red obj_at'_def) - apply assumption - apply (clarsimp simp: queue_end_valid_def fun_upd_apply) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply) - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply obj_at'_def - split: option.splits) - apply (clarsimp simp: fun_upd_apply) - apply (clarsimp simp: fun_upd_apply) - apply (intro conjI; clarsimp) - - \ \tcbPtr is the end of the ready queue\ - apply (intro conjI) - apply (intro heap_path_heap_upd_not_in) - apply (simp add: fun_upd_apply) - apply (force simp: not_emptyI opt_map_red obj_at'_def) - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply split: option.splits) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply) - apply (force simp: prev_queue_head_def fun_upd_apply opt_map_red opt_map_upd_triv obj_at'_def) - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply obj_at'_def - split: option.splits) - apply (clarsimp simp: fun_upd_apply) - apply (clarsimp simp: fun_upd_apply) - - \ \tcbPtr is in the middle of the ready queue\ - apply (intro conjI) - apply (intro heap_path_heap_upd_not_in) - apply (simp add: fun_upd_apply) - apply (force simp: not_emptyI opt_map_red obj_at'_def) - apply (force simp: not_emptyI opt_map_red obj_at'_def) - apply fastforce - apply (clarsimp simp: opt_map_red opt_map_upd_triv obj_at'_def) - apply (intro prev_queue_head_heap_upd) - apply (force dest!: spec) - apply (metis hd_in_set not_emptyI option.sel option.simps(2)) + apply fastforce + apply (rule_tac x="ready_queues s (tcb_domain tcb) (tcb_priority tcb)" in exI) + apply (auto simp: ready_queues_disjoint split: if_splits)[1] apply fastforce - subgoal - by (clarsimp simp: inQ_def opt_map_def opt_pred_def fun_upd_apply obj_at'_def - split: if_splits option.splits) - - \ \d = tcb_domain tcb \ p = tcb_priority tcb\ - apply clarsimp - apply (drule_tac x="tcb_domain tcb" in spec) - apply (drule_tac x="tcb_priority tcb" in spec) - apply (clarsimp simp: list_queue_relation_def) - apply (frule heap_path_head') - apply (frule heap_ls_distinct) - apply (intro conjI; clarsimp simp: tcbQueueEmpty_def) - - \ \the ready queue is the singleton consisting of tcbPtr\ - apply (intro conjI) - apply (simp add: fun_upd_apply tcb_queue_remove_def queue_end_valid_def heap_ls_unique - heap_path_last_end) - apply (simp add: fun_upd_apply tcb_queue_remove_def queue_end_valid_def heap_ls_unique - heap_path_last_end) - apply (simp add: fun_upd_apply prev_queue_head_def) - apply (case_tac "ready_queues s (tcb_domain tcb) (tcb_priority tcb)"; - clarsimp simp: tcb_queue_remove_def inQ_def opt_pred_def fun_upd_apply) - apply (intro conjI; clarsimp) - - \ \tcbPtr is the head of the ready queue\ - apply (frule set_list_mem_nonempty) - apply (frule in_queue_not_head_or_not_tail_length_gt_1) - apply fastforce - apply (fastforce simp: list_queue_relation_def) - apply (frule list_not_head) - apply (clarsimp simp: tcb_queue_remove_def) - apply (frule length_tail_nonempty) - apply (frule (2) heap_ls_next_of_hd) - apply (intro conjI) - apply (drule (1) heap_ls_remove_head_not_singleton) - apply (clarsimp simp: opt_map_red opt_map_upd_triv fun_upd_apply obj_at'_def) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply last_tl) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply obj_at'_def) - apply (case_tac "ready_queues s (tcb_domain tcb) (tcb_priority tcb)"; - clarsimp simp: inQ_def opt_pred_def opt_map_def obj_at'_def fun_upd_apply - split: option.splits) - apply (intro conjI; clarsimp) - - \ \tcbPtr is the end of the ready queue\ - apply (frule set_list_mem_nonempty) - apply (frule in_queue_not_head_or_not_tail_length_gt_1) - apply fast - apply (force dest!: spec simp: list_queue_relation_def) - apply (clarsimp simp: queue_end_valid_def) - apply (frule list_not_last) - apply (clarsimp simp: tcb_queue_remove_def) - apply (frule length_gt_1_imp_butlast_nonempty) - apply (frule (3) heap_ls_prev_of_last) - apply (intro conjI impI; clarsimp?) - apply (drule (1) heap_ls_remove_last_not_singleton) - apply (drule obj_at'_prop)+ - apply (force elim!: rsubst3[where P=heap_ls] simp: opt_map_def fun_upd_apply) - apply (clarsimp simp: opt_map_def fun_upd_apply obj_at'_def) - apply (clarsimp simp: prev_queue_head_def fun_upd_apply obj_at'_def opt_map_def) - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply obj_at'_def - split: option.splits) - apply (meson distinct_in_butlast_not_last in_set_butlastD last_in_set not_last_in_set_butlast) - - \ \tcbPtr is in the middle of the ready queue\ - apply (frule set_list_mem_nonempty) - apply (frule split_list) - apply clarsimp - apply (rename_tac xs ys) - apply (prop_tac "xs \ [] \ ys \ []", fastforce simp: queue_end_valid_def) + apply ((wpsimp wp: tcbQueueRemove_list_queue_relation threadSet_sched_pointers | wps)+)[1] + + apply (rule hoare_allI, rename_tac t') + apply (case_tac "d \ dom \ p \ prio") + apply (wpsimp wp: tcbQueued_update_inQ_other hoare_vcg_disj_lift hoare_drop_imp + simp: opt_pred_disj[simplified pred_disj_def, symmetric] + simp_del: disj_not1 fun_upd_apply) + apply (clarsimp simp: opt_map_def opt_pred_def obj_at'_def split: if_splits) apply clarsimp - apply (frule (2) ptr_in_middle_prev_next) - apply fastforce - apply (clarsimp simp: tcb_queue_remove_def) - apply (prop_tac "tcbPtr \ last xs") - apply (clarsimp simp: distinct_append) - apply (prop_tac "tcbPtr \ hd ys") - apply (fastforce dest: hd_in_set simp: distinct_append) - apply (prop_tac "last xs \ hd ys") - apply (metis distinct_decompose2 hd_Cons_tl last_in_set) - apply (prop_tac "list_remove (xs @ tcbPtr # ys) tcbPtr = xs @ ys") - apply (simp add: list_remove_middle_distinct del: list_remove_append) - apply (drule obj_at'_prop)+ - apply clarsimp - apply (intro conjI impI allI; (solves \clarsimp simp: distinct_append\)?) - apply (fastforce elim!: rsubst3[where P=heap_ls] - dest!: heap_ls_remove_middle hd_in_set last_in_set - simp: distinct_append not_emptyI opt_map_def fun_upd_apply) - apply (clarsimp simp: queue_end_valid_def fun_upd_apply) - apply (case_tac xs; - fastforce simp: prev_queue_head_def opt_map_def fun_upd_apply distinct_append) - apply (clarsimp simp: inQ_def opt_pred_def opt_map_def fun_upd_apply distinct_append - split: option.splits) + apply (subst set_tcb_queue_remove) + apply (clarsimp simp: ready_qs_distinct_def) + apply (case_tac "t' = tcbPtr") + apply (wpsimp wp: tcbQueued_False_makes_not_inQ) + apply (wpsimp wp: threadSet_opt_pred_other) done lemma tcbReleaseRemove_sym_heap_sched_pointers[wp]: "tcbReleaseRemove tcbPtr \sym_heap_sched_pointers\" - apply (clarsimp simp: tcbReleaseRemove_def setReleaseQueue_def) - apply (wpsimp wp: tcbQueueRemove_sym_heap_sched_pointers inReleaseQueue_wp) - apply (fastforce simp: ksReleaseQueue_asrt_def opt_pred_def obj_at'_def opt_map_red) - done - -crunch tcbReleaseRemove - for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers + unfolding tcbReleaseRemove_def + apply (wpsimp wp: tcbQueueRemove_sym_heap_sched_pointers inReleaseQueue_wp + threadSet_sched_pointers + | wps)+ + by (fastforce simp: ksReleaseQueue_asrt_def opt_pred_def obj_at'_def opt_map_red) crunch setReprogramTimer for sch_act_wf[wp]: "\s. sch_act_wf (ksSchedulerAction s) s" @@ -6500,6 +6612,11 @@ lemma tcbSchedPrev_update_valid_mdb'[wp]: apply (fastforce simp: obj_at'_def valid_tcb'_def tcb_cte_cases_def cteSizeBits_def) done +lemma tcbInReleaseQueue_update_valid_mdb'[wp]: + "\valid_mdb' and tcb_at' tcbPtr\ threadSet (tcbInReleaseQueue_update f) tcbPtr \\_. valid_mdb'\" + apply (wpsimp wp: threadSet_mdb') + by (fastforce simp: obj_at'_def tcb_cte_cases_def cteSizeBits_def) + lemma tcbQueueRemove_valid_mdb': "\\s. valid_mdb' s \ valid_objs' s\ tcbQueueRemove q tcbPtr \\_. valid_mdb'\" unfolding tcbQueueRemove_def @@ -6512,17 +6629,21 @@ crunch setReleaseQueue for valid_mdb'[wp]: valid_mdb' (simp: valid_mdb'_def) +lemma tcbInReleaseQueue_update_valid_objs'[wp]: + "threadSet (tcbInReleaseQueue_update f) tcbPtr \valid_objs'\" + by (wpsimp wp: threadSet_valid_objs') + +lemma tcbQueued_update_valid_objs'[wp]: + "threadSet (tcbQueued_update f) tcbPtr \valid_objs'\" + by (wpsimp wp: threadSet_valid_objs') + lemma tcbReleaseRemove_valid_mdb'[wp]: "\valid_mdb' and valid_objs' and sym_heap_sched_pointers\ tcbReleaseRemove tcbPtr \\_. valid_mdb'\" unfolding tcbReleaseRemove_def - apply (wpsimp simp: setReleaseQueue_def wp: threadSet_mdb' tcbQueueRemove_valid_mdb') - apply (rule_tac Q'="\_. tcb_at' tcbPtr" in hoare_post_imp) - apply (fastforce simp: tcb_cte_cases_def cteSizeBits_def) - apply (wpsimp wp: inReleaseQueue_wp)+ - apply (fastforce simp: ksReleaseQueue_asrt_def obj_at'_def opt_map_def) - done + apply (wpsimp simp: setReleaseQueue_def wp: tcbQueueRemove_valid_mdb' inReleaseQueue_wp) + by (fastforce simp: ksReleaseQueue_asrt_def obj_at'_def opt_map_def) crunch setReprogramTimer for obj_at'[wp]: "\s. Q (obj_at' P ptr s)" diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index 93a4392bf3..8c9b0a660c 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread.lhs @@ -854,5 +854,3 @@ Kernel init will created a initial thread whose tcbPriority is max priority. > new_queue <- tcbQueueRemove releaseQueue tcbPtr > setReleaseQueue new_queue > threadSet (\t -> t { tcbInReleaseQueue = False }) tcbPtr - -%