From 3e3baf7b49ef8ad9feb06dbc0e1cbcb60452ff80 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Sun, 17 Jul 2016 15:20:02 +1000 Subject: [PATCH] arch_split: invariants: split DetSchedAux_AI [VER-602] --- .../ARM/ArchDetSchedAux_AI.thy | 134 ++++++++++++++ proof/invariant-abstract/DetSchedAux_AI.thy | 164 +++++++----------- .../DetSchedSchedule_AI.thy | 2 +- 3 files changed, 194 insertions(+), 106 deletions(-) create mode 100644 proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy diff --git a/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy new file mode 100644 index 000000000..ac4ade8e8 --- /dev/null +++ b/proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy @@ -0,0 +1,134 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +theory ArchDetSchedAux_AI +imports "../DetSchedAux_AI" +begin + +context Arch begin global_naming ARM + +named_theorems DetSchedAux_AI_assms + +crunch exst[wp]: init_arch_objects "\s. P (exst s)" (wp: crunch_wps) +crunch ct[wp]: init_arch_objects "\s. P (cur_thread s)" (wp: crunch_wps) +crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp') +crunch valid_etcbs[wp, DetSchedAux_AI_assms]: init_arch_objects valid_etcbs (wp: valid_etcbs_lift) + +lemma delete_objects_etcb_at[wp, DetSchedAux_AI_assms]: + "\\s::det_ext state. etcb_at P t s\ delete_objects a b \\r s. etcb_at P t s\" + apply (simp add: delete_objects_def) + apply (wp) + apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+ + done + +lemma invoke_untyped_etcb_at [DetSchedAux_AI_assms]: + "\(\s :: det_ext state. etcb_at P t s) and valid_etcbs\ invoke_untyped ui \\r s. st_tcb_at (Not o inactive) t s \ etcb_at P t s\ " + apply (cases ui) + apply (simp add: mapM_x_def[symmetric]) + apply wp + apply (wp retype_region_etcb_at mapM_x_wp' create_cap_no_pred_tcb_at + hoare_convert_imp typ_at_pred_tcb_at_lift ) + apply simp + done + +crunch valid_blocked[wp, DetSchedAux_AI_assms]: init_arch_objects valid_blocked + (wp: valid_blocked_lift set_cap_typ_at) + +crunch ct[wp, DetSchedAux_AI_assms]: invoke_untyped "\s. P (cur_thread s)" + (wp: crunch_wps dxo_wp_weak simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym + ignore: freeMemory ignore: retype_region_ext) + +crunch ready_queues[wp, DetSchedAux_AI_assms]: + invoke_untyped "\s :: det_ext state. P (ready_queues s)" + (wp: crunch_wps + simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym + ignore: freeMemory) + +crunch scheduler_action[wp, DetSchedAux_AI_assms]: + invoke_untyped "\s :: det_ext state. P (scheduler_action s)" + (wp: crunch_wps + simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym + ignore: freeMemory) + +crunch cur_domain[wp, DetSchedAux_AI_assms]: invoke_untyped "\s :: det_ext state. P (cur_domain s)" + (wp: crunch_wps + simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym + ignore: freeMemory) + +crunch idle_thread[wp, DetSchedAux_AI_assms]: invoke_untyped "\s. P (idle_thread s)" + (wp: crunch_wps dxo_wp_weak + simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym + ignore: freeMemory retype_region_ext) + +lemma perform_asid_control_etcb_at:"\(\s. etcb_at P t s) and valid_etcbs\ + perform_asid_control_invocation aci + \\r s. st_tcb_at (Not \ inactive) t s \ etcb_at P t s\" + apply (simp add: perform_asid_control_invocation_def) + apply (rule hoare_pre) + apply ( wp | wpc | simp)+ + apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1] + apply (rule hoare_drop_imps) + apply (wp retype_region_etcb_at) + apply simp + done + +crunch ct[wp]: perform_asid_control_invocation "\s. P (cur_thread s)" + +crunch idle_thread[wp]: perform_asid_control_invocation "\s. P (idle_thread s)" + +crunch valid_etcbs[wp]: perform_asid_control_invocation valid_etcbs (wp: static_imp_wp) + +crunch valid_blocked[wp]: perform_asid_control_invocation valid_blocked (wp: static_imp_wp) + +crunch schedact[wp]: perform_asid_control_invocation "\s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) + +crunch rqueues[wp]: perform_asid_control_invocation "\s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) + +crunch cur_domain[wp]: perform_asid_control_invocation "\s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) + +lemma perform_asid_control_invocation_valid_sched: + "\ct_active and invs and valid_aci aci and valid_sched and valid_idle\ + perform_asid_control_invocation aci + \\_. valid_sched\" + apply (rule hoare_pre) + apply (rule_tac I="invs and ct_active and valid_aci aci" in valid_sched_tcb_state_preservation) + apply (wp perform_asid_control_invocation_st_tcb_at) + apply simp + apply (wp perform_asid_control_etcb_at) + apply (rule hoare_strengthen_post, rule aci_invs) + apply (simp add: invs_def valid_state_def) + apply (rule hoare_lift_Pf[where f="\s. scheduler_action s"]) + apply (rule hoare_lift_Pf[where f="\s. cur_domain s"]) + apply (rule hoare_lift_Pf[where f="\s. idle_thread s"]) + apply wp + apply simp + done + +crunch valid_queues[wp]: init_arch_objects valid_queues (wp: valid_queues_lift) + +crunch valid_sched_action[wp]: init_arch_objects valid_sched_action (wp: valid_sched_action_lift) + +crunch valid_sched[wp]: init_arch_objects valid_sched (wp: valid_sched_lift) + +end + +global_interpretation DetSchedAux_AI_det_ext?: DetSchedAux_AI_det_ext + proof goal_cases + interpret Arch . + case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?) + qed + +global_interpretation DetSchedAux_AI?: DetSchedAux_AI + proof goal_cases + interpret Arch . + case 1 show ?case by (unfold_locales; (fact DetSchedAux_AI_assms)?) + qed + +end diff --git a/proof/invariant-abstract/DetSchedAux_AI.thy b/proof/invariant-abstract/DetSchedAux_AI.thy index 546353cf3..45631a5e5 100644 --- a/proof/invariant-abstract/DetSchedAux_AI.thy +++ b/proof/invariant-abstract/DetSchedAux_AI.thy @@ -12,6 +12,11 @@ theory DetSchedAux_AI imports DetSchedInvs_AI begin +context begin interpretation Arch . +requalify_facts + invoke_untyped_st_tcb_at +end + crunch_ignore (del: cap_swap_ext cap_move_ext cap_insert_ext empty_slot_ext create_cap_ext tcb_sched_action reschedule_required set_thread_state_ext switch_if_required_to @@ -19,16 +24,11 @@ crunch_ignore (del: crunch_ignore (add: do_extended_op) - crunch ekheap[wp]: update_cdt_list "\s. P (ekheap s)" crunch rqueues[wp]: update_cdt_list "\s. P (ready_queues s)" crunch schedact[wp]: update_cdt_list "\s. P (scheduler_action s)" crunch cur_domain[wp]: update_cdt_list "\s. P (cur_domain s)" -context begin interpretation Arch . (*FIXME: arch_split*) -crunch exst[wp]: init_arch_objects "\s. P (exst s)" (wp: crunch_wps) -end - crunch ekheap[wp]: create_cap, cap_insert "\s :: det_ext state. P (ekheap s)" (wp: crunch_wps) crunch rqueues[wp]: create_cap, cap_insert "\s :: det_ext state. P (ready_queues s)" (wp: crunch_wps) @@ -37,23 +37,13 @@ crunch schedact[wp]: create_cap, cap_insert "\s :: det_ext state. P (sch crunch cur_domain[wp]: create_cap, cap_insert "\s :: det_ext state. P (cur_domain s)" (wp: crunch_wps) -context begin interpretation Arch . (*FIXME: arch_split*) -crunch ct[wp]: init_arch_objects "\s. P (cur_thread s)" (wp: crunch_wps) -end - lemma create_cap_ct[wp]: "\\s. P (cur_thread s)\ create_cap a b c d \\r s. P (cur_thread s)\" apply (simp add: create_cap_def) apply (rule hoare_pre) apply (wp dxo_wp_weak | wpc | simp)+ done - - -context begin interpretation Arch . (*FIXME: arch_split*) -crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at Q t" (wp: mapM_x_wp') - -crunch valid_etcbs[wp]: create_cap,cap_insert,init_arch_objects,set_cap valid_etcbs (wp: valid_etcbs_lift set_cap_typ_at) -end +crunch valid_etcbs[wp]: create_cap,cap_insert,set_cap valid_etcbs (wp: valid_etcbs_lift set_cap_typ_at) lemma valid_etcb_fold_update: "valid_etcbs_2 ekh kh \ type \ apiobject_type.Untyped \ valid_etcbs_2 (foldr (\p ekh. ekh(p := default_ext type cdom)) @@ -191,11 +181,31 @@ lemma cap_insert_no_pred_tcb_at: "\\s. \ pred_tcb_at proj P done -lemma delete_objects_etcb_at[wp]: "\\s. etcb_at P t s\ delete_objects a b \\r s. etcb_at P t s\" - apply (simp add: delete_objects_def) - apply (wp) - apply (simp add: detype_def detype_ext_def wrap_ext_det_ext_ext_def etcb_at_def|wp)+ - done +locale DetSchedAux_AI = + fixes state_ext_t :: "'state_ext::state_ext itself" + assumes invoke_untyped_ct[wp]: + "\P i. \\s::'state_ext state. P (cur_thread s)\ invoke_untyped i \\_ s. P (cur_thread s)\" + assumes invoke_untyped_idle_thread[wp]: + "\P i. \\s::'state_ext state. P (idle_thread s)\ invoke_untyped i \\_ s. P (idle_thread s)\" + +locale DetSchedAux_AI_det_ext = DetSchedAux_AI "TYPE(det_ext)" + + assumes delete_objects_etcb_at[wp]: + "\P t a b. \\s::det_ext state. etcb_at P t s\ delete_objects a b \\r s. etcb_at P t s\" + assumes invoke_untyped_etcb_at: + "\P t ui. + \(\s :: det_ext state. etcb_at P t s) and valid_etcbs\ + invoke_untyped ui + \\r s. st_tcb_at (Not o inactive) t s \ etcb_at P t s\ " + assumes init_arch_objects_valid_etcbs[wp]: + "\t r n sz refs. \valid_etcbs\ init_arch_objects t r n sz refs \\_. valid_etcbs\" + assumes init_arch_objects_valid_blocked[wp]: + "\t r n sz refs. \valid_blocked\ init_arch_objects t r n sz refs \\_. valid_blocked\" + assumes invoke_untyped_cur_domain[wp]: + "\P i. \\s. P (cur_domain s)\ invoke_untyped i \\_ s. P (cur_domain s)\" + assumes invoke_untyped_ready_queues[wp]: + "\P i. \\s. P (ready_queues s)\ invoke_untyped i \\_ s. P (ready_queues s)\" + assumes invoke_untyped_scheduler_action[wp]: + "\P i. \\s. P (scheduler_action s)\ invoke_untyped i \\_ s. P (scheduler_action s)\" lemma delete_objects_valid_etcbs[wp]: "\valid_etcbs\ delete_objects a b \\_. valid_etcbs\" apply (simp add: delete_objects_def) @@ -207,16 +217,8 @@ lemma delete_objects_valid_etcbs[wp]: "\valid_etcbs\ delete_obje apply (simp add: valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def) done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma invoke_untyped_etcb_at: "\(\s :: det_ext state. etcb_at P t s) and valid_etcbs\ invoke_untyped ui \\r s. st_tcb_at (Not o inactive) t s \ etcb_at P t s\ " - apply (cases ui) - apply (simp add: mapM_x_def[symmetric]) - apply wp - apply (wp retype_region_etcb_at mapM_x_wp' create_cap_no_pred_tcb_at - hoare_convert_imp typ_at_pred_tcb_at_lift ) - apply simp - done -end + +context DetSchedAux_AI_det_ext begin lemma invoke_untyped_valid_etcbs[wp]: "\valid_etcbs\ invoke_untyped ui \\_.valid_etcbs\" apply (cases ui) @@ -225,11 +227,12 @@ lemma invoke_untyped_valid_etcbs[wp]: "\valid_etcbs\ invoke_unty apply simp done -context begin interpretation Arch . (*FIXME: arch_split*) -crunch valid_blocked[wp]: create_cap,cap_insert,init_arch_objects,set_cap valid_blocked - (wp: valid_blocked_lift set_cap_typ_at) end + +crunch valid_blocked[wp]: create_cap,cap_insert,set_cap valid_blocked + (wp: valid_blocked_lift set_cap_typ_at) + lemma valid_blocked_fold_update: "valid_blocked_2 queues kh sa ct \ type \ apiobject_type.Untyped \ valid_blocked_2 queues (foldr (\p kh. kh(p \ default_object type o_bits)) @@ -263,6 +266,8 @@ lemma delete_objects_valid_blocked[wp]: "\valid_blocked\ delete_ apply (simp add: valid_blocked_def st_tcb_at_kh_def obj_at_kh_def obj_at_def is_etcb_at_def) done +context DetSchedAux_AI_det_ext begin + lemma invoke_untyped_valid_blocked[wp]: "\valid_blocked\ invoke_untyped ui \\_.valid_blocked\" apply (cases ui) apply (simp add: mapM_x_def[symmetric]) @@ -270,6 +275,8 @@ lemma invoke_untyped_valid_blocked[wp]: "\valid_blocked\ invoke_ apply simp done +end + (*Leverages the fact that retype only clears out inactive tcbs under the invariants*) lemma valid_sched_tcb_state_preservation: @@ -365,18 +372,6 @@ lemma valid_sched_tcb_state_preservation: lemmas mapM_x_defsym = mapM_x_def[symmetric] -crunch ct[wp]: invoke_untyped "\s. P (cur_thread s)" (wp: crunch_wps dxo_wp_weak simp: crunch_simps do_machine_op_def detype_def mapM_x_defsym ignore: freeMemory ignore: retype_region_ext) - -crunch ready_queues[wp]: invoke_untyped "\s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory) - -crunch scheduler_action[wp]: invoke_untyped "\s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory) - -crunch cur_domain[wp]: invoke_untyped "\s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory) - -context begin interpretation Arch . (*FIXME: arch_split*) -crunch idle_thread[wp]: invoke_untyped "\s. P (idle_thread s)" (wp: crunch_wps dxo_wp_weak simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def mapM_x_defsym ignore: freeMemory retype_region_ext) -end - lemma valid_idle_etcb_lift: assumes "\P t. \\s. etcb_at P t s\ f \\r s. etcb_at P t s\" shows "\valid_idle_etcb\ f \\r. valid_idle_etcb\" @@ -385,81 +380,40 @@ lemma valid_idle_etcb_lift: done +context DetSchedAux_AI_det_ext begin + lemma invoke_untyped_valid_sched: "\invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle \ invoke_untyped ui \ \_ . valid_sched \" apply (rule hoare_pre) apply (rule_tac I="invs and valid_untyped_inv ui and ct_active" in valid_sched_tcb_state_preservation) - apply (wp invoke_untyped_st_tcb_at) - apply simp - apply (wp invoke_untyped_etcb_at) + apply (wp invoke_untyped_st_tcb_at) + apply simp + apply (wp invoke_untyped_etcb_at) apply (rule hoare_strengthen_post) - apply (wp invoke_untyp_invs, simp add: invs_def valid_state_def) - apply (rule_tac f="\s. P (scheduler_action s)" in hoare_lift_Pf) - apply (rule_tac f="\s. x (ready_queues s)" in hoare_lift_Pf) - apply wp + apply (wp invoke_untyp_invs, simp add: invs_def valid_state_def) + apply (rule_tac f="\s. P (scheduler_action s)" in hoare_lift_Pf) + apply (rule_tac f="\s. x (ready_queues s)" in hoare_lift_Pf) + apply wp apply simp done +end + + lemma hoare_imp_lift_something: "\\\s. \ P s \ f \\r s. \ P s\;\Q\ f \\_.Q\\ \ \\s. P s \ Q s\ f \\r s. P s \ Q s\" apply (clarsimp simp add: valid_def) apply force done -context Arch begin global_naming ARM (*FIXME: arch_split*) +crunch valid_queues[wp]: create_cap,cap_insert valid_queues + (wp: valid_queues_lift) -lemma perform_asid_control_etcb_at:"\(\s. etcb_at P t s) and valid_etcbs\ - perform_asid_control_invocation aci - \\r s. st_tcb_at (Not \ inactive) t s \ etcb_at P t s\" - apply (simp add: perform_asid_control_invocation_def) - apply (rule hoare_pre) - apply ( wp | wpc | simp)+ - apply (wp hoare_imp_lift_something typ_at_pred_tcb_at_lift)[1] - apply (rule hoare_drop_imps) - apply (wp retype_region_etcb_at) - apply simp - done +crunch valid_sched_action[wp]: create_cap,cap_insert valid_sched_action + (wp: valid_sched_action_lift) -crunch ct[wp]: perform_asid_control_invocation "\s. P (cur_thread s)" - -crunch idle_thread[wp]: perform_asid_control_invocation "\s. P (idle_thread s)" - -crunch valid_etcbs[wp]: perform_asid_control_invocation valid_etcbs (wp: static_imp_wp) - -crunch valid_blocked[wp]: perform_asid_control_invocation valid_blocked (wp: static_imp_wp) - -crunch schedact[wp]: perform_asid_control_invocation "\s :: det_ext state. P (scheduler_action s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) - -crunch rqueues[wp]: perform_asid_control_invocation "\s :: det_ext state. P (ready_queues s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) - -crunch cur_domain[wp]: perform_asid_control_invocation "\s :: det_ext state. P (cur_domain s)" (wp: crunch_wps simp: detype_def detype_ext_def wrap_ext_det_ext_ext_def cap_insert_ext_def ignore: freeMemory) - -lemma perform_asid_control_invocation_valid_sched: "\ct_active and invs and - valid_aci aci and valid_sched and valid_idle\ -perform_asid_control_invocation aci \\_. valid_sched\" - apply (rule hoare_pre) - apply (rule_tac I="invs and ct_active and valid_aci aci" in valid_sched_tcb_state_preservation) - apply (wp perform_asid_control_invocation_st_tcb_at) - apply simp - apply (wp perform_asid_control_etcb_at) - apply (rule hoare_strengthen_post, rule aci_invs) - apply (simp add: invs_def valid_state_def) - apply (rule hoare_lift_Pf[where f="\s. scheduler_action s"]) - apply (rule hoare_lift_Pf[where f="\s. cur_domain s"]) - apply (rule hoare_lift_Pf[where f="\s. idle_thread s"]) - apply wp - apply simp - done - -end - -crunch valid_queues[wp]: create_cap,cap_insert,init_arch_objects valid_queues (wp: valid_queues_lift) - -crunch valid_sched_action[wp]: create_cap,cap_insert,init_arch_objects valid_sched_action (wp: valid_sched_action_lift) - -context begin interpretation Arch . (*FIXME: arch_split*) -crunch valid_sched[wp]: create_cap,cap_insert,init_arch_objects valid_sched (wp: valid_sched_lift) -end +crunch valid_sched[wp]: create_cap,cap_insert valid_sched + (wp: valid_sched_lift) end diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 08511974f..19837111f 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -9,7 +9,7 @@ *) theory DetSchedSchedule_AI -imports DetSchedAux_AI +imports "$L4V_ARCH/ArchDetSchedAux_AI" begin lemma ethread_get_wp[wp]: "\\s. etcb_at (\t. P (f t) s) ptr s\ ethread_get f ptr \P\"