1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory StartThreads_SI 12imports 13 InitTCB_SI 14begin 15 16lemma is_waiting_thread_is_tcb [simp]: 17 "\<lbrakk>cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk> 18 \<Longrightarrow> is_tcb obj" 19 by (clarsimp simp: is_waiting_thread_def) 20 21lemma is_waiting_thread_at_tcb_at [simp]: 22 "is_waiting_thread_at obj_id spec \<Longrightarrow> tcb_at obj_id spec" 23 by (clarsimp simp: object_at_def is_waiting_thread_def) 24 25lemma is_waiting_thread_at_real_object_at [simp]: 26 "\<lbrakk>well_formed spec; is_waiting_thread_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 27 by (metis is_waiting_thread_at_tcb_at real_object_not_irq_node(2)) 28 29lemma is_waiting_thread_tcb_at [simp]: 30 "(tcb_at obj_id spec \<and> object_at is_waiting_thread obj_id spec) = object_at is_waiting_thread obj_id spec" 31 by fastforce 32 33lemma is_waiting_thread_opt_cap_tcb_pending_op_slot [simp]: 34 "\<lbrakk>cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk> 35 \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap" 36 by (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def) 37 38 39lemma is_waiting_thread_opt_cap_tcb_replycap_slot [simp]: 40 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk> 41 \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)" 42 apply (frule well_formed_tcb_pending_op_replycap [where obj_id=obj_id], simp add: object_at_def) 43 apply (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def) 44 done 45 46lemma is_waiting_thread_opt_cap_tcb_boundntfn_slot[simp]: 47 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_waiting_thread obj\<rbrakk> 48 \<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap" 49 apply (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def) 50 apply (frule well_formed_tcb_boundntfn_cap [where obj_id=obj_id], simp add: object_at_def) 51 by (clarsimp simp: is_waiting_thread_def opt_cap_def slots_of_def opt_object_def) 52 53lemma cap_transform_RestartCap [simp]: 54 "cap_transform t RestartCap = RestartCap" 55 by (clarsimp simp: cap_transform_def cap_type_def update_cap_object_def) 56 57lemma cap_type_MasterReplyCap [simp]: 58 "cap_type (MasterReplyCap obj_id) = None" 59 by (simp add: cap_type_def) 60 61lemma cap_transform_MasterReplyCap: 62 "\<lbrakk>t obj_id = Some k_obj_id\<rbrakk> 63 \<Longrightarrow> cap_transform t (MasterReplyCap obj_id) = MasterReplyCap k_obj_id" 64 apply (frule cap_transform_update_cap_object [where cap="MasterReplyCap obj_id"], simp+) 65 apply (clarsimp simp: cap_transform_def cap_object_def update_cap_object_def) 66 done 67 68 69 70lemma start_thread_sep: 71 "\<lbrace>\<guillemotleft>tcb_half_initialised spec t obj_id \<and>* 72 si_cap_at t dup_caps spec False obj_id \<and>* 73 si_objects \<and>* R\<guillemotright> and 74 K(well_formed spec \<and> obj_id \<in> {obj_id. is_waiting_thread_at obj_id spec})\<rbrace> 75 start_thread spec dup_caps obj_id 76 \<lbrace>\<lambda>_.\<guillemotleft>object_initialised spec t obj_id \<and>* 77 si_cap_at t dup_caps spec False obj_id \<and>* 78 si_objects \<and>* R\<guillemotright>\<rbrace>" 79 apply (rule hoare_gen_asm) 80 apply (clarsimp simp: start_thread_def object_initialised_def tcb_half_initialised_def object_initialised_general_def 81 si_cap_at_def si_objects_def sep_conj_exists) 82 apply (rule hoare_vcg_ex_lift | rule hoare_grab_asm | simp)+ 83 apply (subst tcb_half_decomp, (simp add: object_at_def)+)+ 84 apply (subst tcb_decomp, (simp add: object_at_def)+)+ 85 apply (wp add: hoare_drop_imps 86 sep_wp: seL4_TCB_Resume_wp 87 [where root_tcb = root_tcb 88 and cnode_cap = si_cspace_cap 89 and root_size = si_cnode_size 90 and tcb_cap = "TcbCap (the (t obj_id))"] | 91 simp add: guard_equal_si_cspace_cap' cap_object_simps is_tcb_default_cap)+ 92 apply (subst offset_slot_si_cnode_size', assumption)+ 93 apply (clarsimp simp: cap_transform_MasterReplyCap) 94 by sep_solve 95 96 97lemma tcb_half_id: 98 "\<lbrakk>well_formed spec; is_tcb object; \<not> is_waiting_thread object; 99 cdl_objects spec obj_id = Some object\<rbrakk> 100 \<Longrightarrow> tcb_half spec object = object" 101 apply (frule well_formed_tcb_pending_op_cap [where obj_id=obj_id], simp add: object_at_def) 102 apply (frule well_formed_tcb_replycap_cap [where obj_id=obj_id], simp add: object_at_def) 103 apply (frule well_formed_tcb_pending_op_replycap [where obj_id=obj_id], simp add: object_at_def) 104 apply (frule well_formed_tcb_boundntfn_cap [where obj_id=obj_id], simp add: object_at_def) 105 apply (fastforce simp: tcb_half_def is_waiting_thread_def is_tcb_def 106 opt_cap_def slots_of_def opt_object_def object_slots_def update_slots_def 107 cdl_tcb.splits 108 split: cdl_object.splits) 109 done 110 111lemma tcb_half_initialised_object_initialised: 112 "\<lbrakk>well_formed spec; tcb_at obj_id spec; \<not> object_at is_waiting_thread obj_id spec\<rbrakk> 113 \<Longrightarrow> tcb_half_initialised spec t obj_id = object_initialised spec t obj_id" 114 by (clarsimp simp: tcb_half_initialised_def object_initialised_def object_initialised_general_def 115 object_at_def tcb_half_id) 116 117lemma tcb_half_initialised_object_initialised': 118 "well_formed spec 119 \<Longrightarrow> (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec. 120 tcb_half_initialised spec t obj_id) 121 = (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec. 122 object_initialised spec t obj_id)" 123 apply(rule sep.prod.cong, simp) 124 apply (rule tcb_half_initialised_object_initialised, simp+) 125 done 126 127lemma start_threads_sep: 128 "\<lbrace>\<guillemotleft>tcbs_half_initialised spec t {obj_id. tcb_at obj_id spec} \<and>* 129 si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>* 130 si_objects \<and>* R\<guillemotright> and 131 K(well_formed spec \<and> set obj_ids = dom (cdl_objects spec) \<and> distinct obj_ids)\<rbrace> 132 start_threads spec dup_caps obj_ids 133 \<lbrace>\<lambda>_.\<guillemotleft>objects_initialised spec t {obj_id. tcb_at obj_id spec} \<and>* 134 si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>* 135 si_objects \<and>* R\<guillemotright>\<rbrace>" 136 apply (rule hoare_gen_asm) 137 apply (clarsimp simp: start_threads_def tcbs_half_initialised_def objects_initialised_def) 138 139 (* The threads that don't need to be started can be ignored. *) 140 apply (subst sep_map_set_conj_restrict 141 [where P="tcb_half_initialised spec t" 142 and t="\<lambda>obj_id. object_at is_waiting_thread obj_id spec"], simp+) 143 apply (subst sep_map_set_conj_restrict 144 [where P="object_initialised spec t" 145 and t="\<lambda>obj_id. object_at is_waiting_thread obj_id spec"], simp+) 146 apply (subst tcb_half_initialised_object_initialised', assumption) 147 148 (* Now apply the mapM_x rule to reason about a single thread. *) 149 apply (clarsimp simp: sep_conj_ac) 150 apply (rule mapM_x_set_sep' [where 151 P="\<lambda>obj_id. tcb_half_initialised spec t obj_id" and 152 Q="\<lambda>obj_id. object_initialised spec t obj_id" and 153 I="si_caps_at t dup_caps spec False {obj_id. cnode_or_tcb_at obj_id spec} \<and>* 154 si_objects" and 155 xs="[obj_id \<leftarrow> obj_ids. is_waiting_thread_at obj_id spec]" and 156 X="{obj_id. object_at is_waiting_thread obj_id spec}" and 157 R="R \<and>* (\<And>*obj_id | tcb_at obj_id spec \<and> \<not> object_at is_waiting_thread obj_id spec. 158 object_initialised spec t obj_id)" 159 , simplified sep_conj_ac], simp+) 160 161 (* Now select only a single one of the "si_cap_at t dup_caps spec" predicates. *) 162 apply (clarsimp simp: si_caps_at_def, rename_tac obj_id) 163 apply (rule hoare_chain) 164 apply (rule_tac x = obj_id 165 and xs = "{obj_id. cnode_or_tcb_at obj_id spec}" 166 and P = "tcb_half_initialised spec t obj_id \<and>* si_objects" 167 and Q = "object_initialised spec t obj_id \<and>* si_objects" 168 and I = "si_cap_at t dup_caps spec False" 169 and R=R 170 in sep_set_conj_map_singleton_wp [simplified], simp_all add: object_at_real_object_at) 171 172 (* Then apply the start_thread_sep rule and we are done. *) 173 apply (wp sep_wp: start_thread_sep [where t=t], (simp|sep_solve)+) 174 done 175 176end 177