1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11theory Schedule_R 12imports VSpace_R 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17declare static_imp_wp[wp_split del] 18 19(* FIXME: move *) 20lemma corres_if_r': 21 "\<lbrakk> G' \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<not>G' \<Longrightarrow> corres_underlying sr nf nf' r P Q' a d \<rbrakk> 22 \<Longrightarrow> corres_underlying sr nf nf' r (P) (if G' then P' else Q') 23 (a) (if G' then c else d)" 24 by (simp) 25 26(* FIXME: move *) 27lemma corres_gets_pre_lhs: 28 "(\<And>x. corres r (P x) P' (g x) g') \<Longrightarrow> 29 corres r (\<lambda>s. P (f s) s) P' (gets f >>= (\<lambda>x. g x)) g'" 30 by (rule corres_underlying_gets_pre_lhs) 31 32(* FIXME: move *) 33lemma corres_if_lhs: 34 assumes "P \<Longrightarrow> corres r A Q f f'" 35 assumes "\<not>P \<Longrightarrow> corres r B Q g f'" 36 shows "corres r (\<lambda>s. (P \<longrightarrow> A s) \<and> (\<not>P \<longrightarrow> B s)) Q (if P then f else g) f'" 37 by (simp add: assms) 38 39(* Levity: added (20090713 10:04:12) *) 40declare sts_rel_idle [simp] 41 42(* FIXME: move to NonDetMonadVCG *) 43lemma return_wp_exs_valid [wp]: "\<lbrace> P x \<rbrace> return x \<exists>\<lbrace> P \<rbrace>" 44 by (simp add: exs_valid_def return_def) 45 46(* FIXME: move to NonDetMonadVCG *) 47lemma get_exs_valid [wp]: "\<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 48 by (simp add: get_def exs_valid_def) 49 50lemma invs_no_cicd'_queues: 51 "invs_no_cicd' s \<Longrightarrow> valid_queues s" 52 unfolding invs_no_cicd'_def 53 by simp 54 55lemma gsa_wf [wp]: "\<lbrace>invs'\<rbrace> getSchedulerAction \<lbrace>sch_act_wf\<rbrace>" 56 by (simp add: getSchedulerAction_def invs'_def valid_state'_def | wp)+ 57 58lemma corres_if2: 59 "\<lbrakk> G = G'; G \<Longrightarrow> corres r P P' a c; \<not> G' \<Longrightarrow> corres r Q Q' b d \<rbrakk> 60 \<Longrightarrow> corres r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)" 61 by simp 62 63lemma findM_awesome': 64 assumes x: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow> 65 corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None) 66 P (P' (x # xs)) 67 ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)" 68 assumes y: "corres r P (P' []) f (return None)" 69 assumes z: "\<And>x xs. suffix (x # xs) xs' \<Longrightarrow> 70 \<lbrace>P' (x # xs)\<rbrace> g x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P' xs s\<rbrace>" 71 assumes p: "suffix xs xs'" 72 shows "corres r P (P' xs) f (findM g xs)" 73proof - 74 have P: "f = do x \<leftarrow> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None; if x \<noteq> None then return (the x) else f od" 75 apply (rule ext) 76 apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) 77 done 78 have Q: "\<lbrace>P\<rbrace> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<top> else P\<rbrace>" 79 by (wp alternative_wp | simp)+ 80 show ?thesis using p 81 apply (induct xs) 82 apply (simp add: y del: dc_simp) 83 apply (simp only: findM.simps) 84 apply (subst P) 85 apply (rule corres_guard_imp) 86 apply (rule corres_split [OF _ x]) 87 apply (rule corres_if2) 88 apply (case_tac ra, clarsimp+)[1] 89 apply (rule corres_trivial, clarsimp) 90 apply (case_tac ra, simp_all)[1] 91 apply (erule(1) meta_mp [OF _ suffix_ConsD]) 92 apply assumption 93 apply (rule Q) 94 apply (rule hoare_post_imp [OF _ z]) 95 apply simp+ 96 done 97qed 98 99lemmas findM_awesome = findM_awesome' [OF _ _ _ suffix_order.order.refl] 100 101lemma corres_rhs_disj_division: 102 "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres r R S x y; Q \<Longrightarrow> corres r T U x y \<rbrakk> 103 \<Longrightarrow> corres r (R and T) (\<lambda>s. (P \<longrightarrow> S s) \<and> (Q \<longrightarrow> U s)) x y" 104 apply (rule corres_guard_imp) 105 apply (erule corres_disj_division) 106 apply simp+ 107 done 108 109lemma findM_alternative_awesome: 110 assumes x: "\<And>x. corres (\<lambda>a b. if b then (\<exists>a'. a = Some a') else a = None) 111 P (P' and (\<lambda>s. x \<in> fn s)) ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)" 112 assumes z: "\<And>x xs. \<lbrace>\<lambda>s. P' s \<and> x \<in> fn s \<and> set xs \<subseteq> fn s\<rbrace> g x \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> P' s \<and> set xs \<subseteq> fn s\<rbrace>" 113 assumes on_none: "corres dc P P' f g'" 114 shows "corres dc P (P' and (\<lambda>s. set xs \<subseteq> fn s)) f (findM g xs >>= (\<lambda>x. when (x = None) g'))" 115proof - 116 have P: "f = do x \<leftarrow> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None; if x \<noteq> None then return (the x) else f od" 117 apply (rule ext) 118 apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) 119 done 120 have Q: "\<lbrace>P\<rbrace> (do x \<leftarrow> f; return (Some x) od) \<sqinter> return None \<lbrace>\<lambda>rv. if rv \<noteq> None then \<top> else P\<rbrace>" 121 by (wp alternative_wp | simp)+ 122 have R: "\<And>P x g xs. (do x \<leftarrow> if P then return (Some x) else findM g xs; 123 when (x = None) g' 124 od) = (if P then return () else (findM g xs >>= (\<lambda>x . when (x = None) g')))" 125 by (simp add: when_def) 126 show ?thesis 127 apply (induct xs) 128 apply (simp add: when_def) 129 apply (fold dc_def, rule on_none) 130 apply (simp only: findM.simps bind_assoc) 131 apply (subst P) 132 apply (rule corres_guard_imp) 133 apply (rule corres_split [OF _ x]) 134 apply (subst R) 135 apply (rule corres_if2) 136 apply (case_tac xa, simp_all)[1] 137 apply (rule corres_trivial, simp) 138 apply assumption 139 apply (rule Q) 140 apply (rule hoare_post_imp [OF _ z]) 141 apply simp+ 142 done 143qed 144 145lemma awesome_case1: 146 assumes x: "corres (=) P P' (return False) (g x)" 147 shows "corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None) 148 P P' ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)" 149proof - 150 have P: "return None = liftM (\<lambda>x. None) (return False)" 151 by (simp add: liftM_def) 152 show ?thesis 153 apply (rule corres_alternate2) 154 apply (subst P, simp only: corres_liftM_simp, simp) 155 apply (subst corres_cong [OF refl refl refl refl]) 156 defer 157 apply (rule x) 158 apply (simp add: return_def) 159 done 160qed 161 162lemma awesome_case2: 163 assumes x: "corres (\<lambda>a b. r a (Some x) \<and> b) P P' f (g x)" 164 shows "corres (\<lambda>a b. if b then (\<exists>a'. a = Some a' \<and> r a' (Some x)) else a = None) 165 P P' ((f >>= (\<lambda>x. return (Some x))) \<sqinter> (return None)) (g x)" 166 apply (rule corres_alternate1) 167 apply (fold liftM_def) 168 apply (simp add: o_def) 169 apply (rule corres_rel_imp [OF x]) 170 apply simp 171 done 172 173lemma bind_select_corres: 174 assumes x: "corres (\<lambda>rvs rv'. \<exists>rv\<in>rvs. r rv rv') P P' m m'" 175 shows "corres r P P' (m >>= select) m'" 176 apply (insert x) 177 apply (clarsimp simp: corres_underlying_def bind_def select_def split_def) 178 done 179 180lemma bind_select_fail_corres: 181 assumes x: "corres (\<lambda>rvs rv'. \<exists>rv\<in>rvs. r rv rv') P P' m m'" 182 shows "corres r P P' (m >>= (\<lambda>x. select x \<sqinter> fail)) m'" 183 apply (insert x) 184 apply (clarsimp simp: corres_underlying_def bind_def 185 select_def fail_def alternative_def split_def) 186 done 187 188(* Levity: added (20090721 10:56:29) *) 189declare objBitsT_koTypeOf [simp] 190 191lemma arch_switch_thread_corres: 192 "corres dc (valid_arch_state and valid_objs and valid_asid_map 193 and valid_vspace_objs and pspace_aligned and pspace_distinct 194 and valid_vs_lookup and valid_global_objs 195 and unique_table_refs o caps_of_state 196 and st_tcb_at runnable t) 197 (valid_arch_state' and valid_pspace' and st_tcb_at' runnable' t) 198 (arch_switch_to_thread t) (Arch.switchToThread t)" 199 apply (simp add: arch_switch_to_thread_def X64_H.switchToThread_def) 200 apply (rule corres_guard_imp) 201 apply (rule set_vm_root_corres[OF refl]) 202 apply (clarsimp simp: st_tcb_at_tcb_at) 203 apply (clarsimp simp: valid_pspace'_def) 204 done 205 206lemma schedule_choose_new_thread_sched_act_rct[wp]: 207 "\<lbrace>\<top>\<rbrace> schedule_choose_new_thread \<lbrace>\<lambda>rs s. scheduler_action s = resume_cur_thread\<rbrace>" 208 unfolding schedule_choose_new_thread_def 209 by wp 210 211lemma tcbSchedAppend_corres: 212 notes trans_state_update'[symmetric, simp del] 213 shows 214 "corres dc (is_etcb_at t) (tcb_at' t and Invariants_H.valid_queues and valid_queues') (tcb_sched_action (tcb_sched_append) t) (tcbSchedAppend t)" 215 apply (simp only: tcbSchedAppend_def tcb_sched_action_def) 216 apply (rule corres_symb_exec_r [OF _ _ threadGet_inv, where Q'="\<lambda>rv. tcb_at' t and Invariants_H.valid_queues and valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"]) 217 defer 218 apply (wp threadGet_obj_at', simp, simp) 219 apply (rule no_fail_pre, wp, simp) 220 apply (case_tac queued) 221 apply (simp add: unless_def when_def) 222 apply (rule corres_no_failI) 223 apply wp+ 224 apply (clarsimp simp: in_monad ethread_get_def gets_the_def bind_assoc 225 assert_opt_def exec_gets is_etcb_at_def get_etcb_def get_tcb_queue_def 226 set_tcb_queue_def simpler_modify_def) 227 228 apply (subgoal_tac "tcb_sched_append t (ready_queues a (tcb_domain y) (tcb_priority y)) 229 = (ready_queues a (tcb_domain y) (tcb_priority y))") 230 apply (simp add: state_relation_def ready_queues_relation_def) 231 apply (clarsimp simp: tcb_sched_append_def state_relation_def 232 valid_queues'_def ready_queues_relation_def 233 ekheap_relation_def etcb_relation_def 234 obj_at'_def inQ_def projectKO_eq project_inject) 235 apply (drule_tac x=t in bspec,clarsimp) 236 apply clarsimp 237 apply (clarsimp simp: unless_def when_def cong: if_cong) 238 apply (rule stronger_corres_guard_imp) 239 apply (rule corres_split[where r'="(=)", OF _ ethreadget_corres]) 240 apply (rule corres_split[where r'="(=)", OF _ ethreadget_corres]) 241 apply (rule corres_split[where r'="(=)"]) 242 apply (rule corres_split_noop_rhs2) 243 apply (rule corres_split_noop_rhs2) 244 apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1] 245 apply (rule addToBitmap_if_null_corres_noop) 246 apply wp+ 247 apply (simp add: tcb_sched_append_def) 248 apply (intro conjI impI) 249 apply (rule corres_guard_imp) 250 apply (rule setQueue_corres) 251 prefer 3 252 apply (rule_tac P=\<top> and Q="K (t \<notin> set queuea)" in corres_assume_pre) 253 apply (wp getQueue_corres getObject_tcb_wp | simp add: etcb_relation_def threadGet_def)+ 254 apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def 255 projectKO_eq project_inject) 256 done 257 258 259crunch valid_pspace'[wp]: tcbSchedEnqueue valid_pspace' 260 (simp: unless_def) 261crunch valid_pspace'[wp]: tcbSchedAppend valid_pspace' 262 (simp: unless_def) 263crunch valid_pspace'[wp]: tcbSchedDequeue valid_pspace' 264 265crunch valid_arch_state'[wp]: tcbSchedEnqueue valid_arch_state' 266 (simp: unless_def) 267crunch valid_arch_state'[wp]: tcbSchedAppend valid_arch_state' 268 (simp: unless_def) 269crunch valid_arch_state'[wp]: tcbSchedDequeue valid_arch_state' 270 271crunch pred_tcb_at'[wp]: tcbSchedAppend, tcbSchedDequeue "pred_tcb_at' proj P t" 272 (wp: threadSet_pred_tcb_no_state simp: unless_def tcb_to_itcb'_def ignore: getObject setObject) 273 274crunch state_refs_of'[wp]: setQueue "\<lambda>s. P (state_refs_of' s)" 275 276lemma removeFromBitmap_valid_queues_no_bitmap[wp]: 277" \<lbrace> valid_queues_no_bitmap \<rbrace> 278 removeFromBitmap d p 279 \<lbrace>\<lambda>_. valid_queues_no_bitmap \<rbrace>" 280 unfolding bitmapQ_defs valid_queues_no_bitmap_def 281 by (wp| clarsimp simp: bitmap_fun_defs comp_def pred_conj_def)+ 282 283lemma removeFromBitmap_valid_queues_no_bitmap_except[wp]: 284" \<lbrace> valid_queues_no_bitmap_except t \<rbrace> 285 removeFromBitmap d p 286 \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>" 287 unfolding bitmapQ_defs valid_queues_no_bitmap_except_def 288 by (wp| clarsimp simp: bitmap_fun_defs)+ 289 290lemma removeFromBitmap_bitmapQ: 291 "\<lbrace> \<lambda>s. True \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_ s. \<not> bitmapQ d p s \<rbrace>" 292 unfolding bitmapQ_defs bitmap_fun_defs 293 apply (wp| clarsimp simp: bitmap_fun_defs)+ 294 apply (subst (asm) complement_nth_w2p, simp_all) 295 apply (fastforce intro!: order_less_le_trans[OF word_unat_mask_lt] simp: word_size wordRadix_def') 296 done 297 298lemma removeFromBitmap_valid_bitmapQ[wp]: 299" \<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and 300 (\<lambda>s. ksReadyQueues s (d,p) = []) \<rbrace> 301 removeFromBitmap d p 302 \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" 303proof - 304 have "\<lbrace> valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and 305 (\<lambda>s. ksReadyQueues s (d,p) = []) \<rbrace> 306 removeFromBitmap d p 307 \<lbrace>\<lambda>_. valid_bitmapQ_except d p and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and 308 (\<lambda>s. \<not> bitmapQ d p s \<and> ksReadyQueues s (d,p) = []) \<rbrace>" 309 by (rule hoare_pre) 310 (wp removeFromBitmap_valid_queues_no_bitmap_except removeFromBitmap_valid_bitmapQ_except 311 removeFromBitmap_bitmapQ, simp) 312 thus ?thesis 313 by - (erule hoare_strengthen_post; fastforce elim: valid_bitmap_valid_bitmapQ_exceptE) 314qed 315 316lemma threadSet_bitmapQ_no_L1_orphans[wp]: 317 "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> threadSet f t \<lbrace>\<lambda>_. bitmapQ_no_L1_orphans \<rbrace>" 318 unfolding bitmapQ_defs threadSet_def 319 by (wp hoare_vcg_all_lift hoare_vcg_imp_lift) simp 320 321lemma threadSet_bitmapQ_no_L2_orphans[wp]: 322 "\<lbrace> bitmapQ_no_L2_orphans \<rbrace> threadSet f t \<lbrace>\<lambda>_. bitmapQ_no_L2_orphans \<rbrace>" 323 unfolding bitmapQ_defs threadSet_def 324 by (wp hoare_vcg_all_lift hoare_vcg_imp_lift) simp 325 326lemma threadSet_valid_bitmapQ[wp]: 327 "\<lbrace> valid_bitmapQ \<rbrace> threadSet f t \<lbrace>\<lambda>_. valid_bitmapQ \<rbrace>" 328 unfolding bitmapQ_defs threadSet_def 329 by (wp hoare_vcg_all_lift hoare_vcg_imp_lift hoare_vcg_conj_lift | wps)+ 330 331lemma setQueue_valid_queues_no_bitmap_except: 332 "\<lbrace> valid_queues_no_bitmap_except t 333 and (\<lambda>s. \<forall>t \<in> set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t s) 334 and K (t \<notin> set ts) 335 and K (distinct ts) and K (d \<le> maxDomain \<and> p \<le> maxPriority)\<rbrace> 336 setQueue d p ts 337 \<lbrace>\<lambda>_. valid_queues_no_bitmap_except t \<rbrace>" 338 unfolding setQueue_def valid_queues_def 339 by (wp, fastforce simp: valid_queues_no_bitmap_except_def) 340 341(* this should be the actual weakest precondition to establish valid_queues 342 under tagging a thread as not queued *) 343lemma threadSet_valid_queues_dequeue_wp: 344 "\<lbrace> valid_queues_no_bitmap_except t and 345 valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and 346 (\<lambda>s. \<forall>d p. t \<notin> set (ksReadyQueues s (d,p))) \<rbrace> 347 threadSet (tcbQueued_update (\<lambda>_. False)) t 348 \<lbrace>\<lambda>rv. valid_queues \<rbrace>" 349 unfolding threadSet_def 350 apply (rule hoare_seq_ext[OF _ getObject_tcb_sp]) 351 apply (rule hoare_pre) 352 apply (simp add: valid_queues_def valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def) 353 apply (wp setObject_queues_unchanged_tcb hoare_Ball_helper hoare_vcg_all_lift 354 setObject_tcb_strongest) 355 apply (clarsimp simp: valid_queues_no_bitmap_except_def obj_at'_def valid_queues_no_bitmap_def) 356 done 357 358(* FIXME move *) 359lemmas obj_at'_conjI = obj_at_conj' 360 361lemma obj_at'_disj: 362 "\<lbrakk> obj_at' (\<lambda>x. P x s) t s \<or> obj_at' (\<lambda>x. Q x s) t s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. P x s \<or> Q x s) t s" 363 by (auto simp: obj_at'_def) 364 365(* FIXME move, also not_obj_at' is too type constrained *) 366lemma obj_at'_imp: 367 "\<lbrakk> obj_at' (\<lambda>(_::'a::pspace_storable). True) t s ; 368 obj_at' (\<lambda>(x::'a). P x s) t s \<longrightarrow> obj_at' (\<lambda>x. Q x s) t s \<rbrakk> 369 \<Longrightarrow> obj_at' (\<lambda>x. P x s \<longrightarrow> Q x s) t s" 370 by (auto simp: obj_at'_def) 371 372lemma setQueue_valid_queues_no_bitmap_except_dequeue_wp: 373 "\<And>d p ts t. 374 \<lbrace> \<lambda>s. valid_queues_no_bitmap_except t s \<and> 375 (\<forall>t' \<in> set ts. obj_at' (inQ d p and runnable' \<circ> tcbState) t' s) \<and> 376 t \<notin> set ts \<and> distinct ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<rbrace> 377 setQueue d p ts 378 \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t \<rbrace>" 379 unfolding setQueue_def valid_queues_no_bitmap_except_def null_def 380 by wp force 381 382definition (* if t is in a queue, it should be tagged with right priority and domain *) 383 "correct_queue t s \<equiv> \<forall>d p. t \<in> set(ksReadyQueues s (d, p)) \<longrightarrow> 384 (obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t s)" 385 386lemma valid_queues_no_bitmap_correct_queueI[intro]: 387 "valid_queues_no_bitmap s \<Longrightarrow> correct_queue t s" 388 unfolding correct_queue_def valid_queues_no_bitmap_def 389 by (fastforce simp: obj_at'_def inQ_def) 390 391 392lemma tcbSchedDequeue_valid_queues_weak: 393 "\<lbrace> valid_queues_no_bitmap_except t and valid_bitmapQ and 394 bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and 395 correct_queue t and 396 obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t \<rbrace> 397 tcbSchedDequeue t 398 \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" 399proof - 400 show ?thesis 401 unfolding tcbSchedDequeue_def null_def valid_queues_def 402 apply wp (* stops on threadSet *) 403 apply (rule hoare_post_eq[OF _ threadSet_valid_queues_dequeue_wp], 404 simp add: valid_queues_def) 405 apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ 406 apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp 407 setQueue_valid_bitmapQ threadGet_const_tcb_at)+ 408 (* wp done *) 409 apply (normalise_obj_at') 410 apply (clarsimp simp: correct_queue_def) 411 apply (normalise_obj_at') 412 apply (fastforce simp add: valid_queues_no_bitmap_except_def valid_queues_no_bitmap_def elim: obj_at'_weaken)+ 413 done 414qed 415 416lemma tcbSchedDequeue_valid_queues: 417 "\<lbrace>Invariants_H.valid_queues 418 and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t 419 and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t\<rbrace> 420 tcbSchedDequeue t 421 \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" 422 apply (rule hoare_pre, rule tcbSchedDequeue_valid_queues_weak) 423 apply (fastforce simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_def inQ_def) 424 done 425 426lemma tcbSchedAppend_valid_queues'[wp]: 427 (* most of this is identical to tcbSchedEnqueue_valid_queues' in TcbAcc_R *) 428 "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_queues'\<rbrace>" 429 apply (simp add: tcbSchedAppend_def) 430 apply (rule hoare_pre) 431 apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t" 432 in hoare_seq_ext) 433 apply (rename_tac queued) 434 apply (case_tac queued; simp_all add: unless_def when_def) 435 apply (wp threadSet_valid_queues' setQueue_valid_queues' | simp)+ 436 apply (subst conj_commute, wp) 437 apply (rule hoare_pre_post, assumption) 438 apply (clarsimp simp: addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def 439 getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def) 440 apply wp 441 apply fastforce 442 apply wp 443 apply (subst conj_commute) 444 apply (clarsimp simp: imp_conj_taut) 445 apply (rule_tac Q="\<lambda>rv. valid_queues' 446 and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t 447 and obj_at' (\<lambda>obj. tcbPriority obj = prio) t 448 and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t 449 and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))" 450 in hoare_post_imp) 451 apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def) 452 apply (wp setQueue_valid_queues' | simp | simp add: setQueue_def)+ 453 apply (wp getObject_tcb_wp | simp add: threadGet_def)+ 454 apply (clarsimp simp: obj_at'_def inQ_def projectKOs valid_queues'_def) 455 apply (wp getObject_tcb_wp | simp add: threadGet_def)+ 456 apply (clarsimp simp: obj_at'_def) 457 done 458 459crunch norq[wp]: threadSet "\<lambda>s. P (ksReadyQueues s)" 460 (simp: updateObject_default_def ignore: setObject getObject) 461 462lemma removeFromBitmap_valid_queues'[wp]: 463 "\<lbrace> valid_queues' \<rbrace> removeFromBitmap d p \<lbrace>\<lambda>_. valid_queues' \<rbrace>" 464 unfolding valid_queues'_def 465 by (wp| simp add: bitmap_fun_defs)+ 466 467lemma threadSet_valid_queues'_dequeue: (* threadSet_valid_queues' is too weak for dequeue *) 468 "\<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> 469 obj_at' (inQ d p) t s \<rbrace> 470 threadSet (tcbQueued_update (\<lambda>_. False)) t 471 \<lbrace>\<lambda>rv. valid_queues' \<rbrace>" 472 unfolding valid_queues'_def 473 apply (rule hoare_pre) 474 apply (wp hoare_vcg_all_lift) 475 apply (simp only: imp_conv_disj not_obj_at') 476 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) 477 apply (simp add: not_obj_at') 478 apply (clarsimp simp: typ_at_tcb') 479 apply normalise_obj_at' 480 apply (fastforce elim: obj_at'_weaken simp: inQ_def) 481 done 482 483lemma setQueue_ksReadyQueues_lift: 484 "\<lbrace> \<lambda>s. P (s\<lparr>ksReadyQueues := (ksReadyQueues s)((d, p) := ts)\<rparr>) ts \<rbrace> 485 setQueue d p ts 486 \<lbrace> \<lambda>_ s. P s (ksReadyQueues s (d,p))\<rbrace>" 487 unfolding setQueue_def 488 by (wp, clarsimp simp: fun_upd_def cong: if_cong) 489 490lemma tcbSchedDequeue_valid_queues'[wp]: 491 "\<lbrace>valid_queues' and tcb_at' t\<rbrace> 492 tcbSchedDequeue t \<lbrace>\<lambda>_. valid_queues'\<rbrace>" 493 unfolding tcbSchedDequeue_def 494 apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t" 495 in hoare_seq_ext) 496 prefer 2 497 apply (wp threadGet_const_tcb_at) 498 apply (fastforce simp: obj_at'_def) 499 apply clarsimp 500 apply (rename_tac queued) 501 apply (case_tac queued, simp_all) 502 apply wp 503 apply (rule_tac d=tdom and p=prio in threadSet_valid_queues'_dequeue) 504 apply (rule hoare_pre_post, assumption) 505 apply (wp | clarsimp simp: bitmap_fun_defs)+ 506 apply (wp hoare_vcg_all_lift setQueue_ksReadyQueues_lift) 507 apply clarsimp 508 apply (wp threadGet_obj_at' threadGet_const_tcb_at)+ 509 apply clarsimp 510 apply (rule context_conjI, clarsimp simp: obj_at'_def) 511 apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def|wp)+ 512 done 513 514crunch tcb_at'[wp]: tcbSchedEnqueue "tcb_at' t" 515 (simp: unless_def) 516crunch tcb_at'[wp]: tcbSchedAppend "tcb_at' t" 517 (simp: unless_def) 518crunch tcb_at'[wp]: tcbSchedDequeue "tcb_at' t" 519 520crunch state_refs_of'[wp]: tcbSchedEnqueue "\<lambda>s. P (state_refs_of' s)" 521 (wp: refl simp: crunch_simps unless_def) 522crunch state_refs_of'[wp]: tcbSchedAppend "\<lambda>s. P (state_refs_of' s)" 523 (wp: refl simp: crunch_simps unless_def) 524crunch state_refs_of'[wp]: tcbSchedDequeue "\<lambda>s. P (state_refs_of' s)" 525 (wp: refl simp: crunch_simps) 526 527crunch cap_to'[wp]: tcbSchedEnqueue "ex_nonz_cap_to' p" 528 (simp: unless_def) 529crunch cap_to'[wp]: tcbSchedAppend "ex_nonz_cap_to' p" 530 (simp: unless_def) 531crunch cap_to'[wp]: tcbSchedDequeue "ex_nonz_cap_to' p" 532 533crunch iflive'[wp]: setQueue if_live_then_nonz_cap' 534 535lemma tcbSchedAppend_iflive'[wp]: 536 "\<lbrace>if_live_then_nonz_cap' and ex_nonz_cap_to' tcb\<rbrace> 537 tcbSchedAppend tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>" 538 apply (simp add: tcbSchedAppend_def unless_def) 539 apply (wp threadSet_iflive' hoare_drop_imps | simp add: crunch_simps)+ 540 done 541 542lemma tcbSchedDequeue_iflive'[wp]: 543 "\<lbrace>if_live_then_nonz_cap'\<rbrace> tcbSchedDequeue tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap'\<rbrace>" 544 apply (simp add: tcbSchedDequeue_def) 545 apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+ 546 apply ((wp | clarsimp simp: bitmap_fun_defs)+)[1] (* deal with removeFromBitmap *) 547 apply (wp threadSet_iflive' hoare_when_weak_wp | simp add: crunch_simps)+ 548 apply (rule_tac Q="\<lambda>rv. \<top>" in hoare_post_imp, fastforce) 549 apply (wp | simp add: crunch_simps)+ 550 done 551 552crunch ifunsafe'[wp]: tcbSchedEnqueue if_unsafe_then_cap' 553 (simp: unless_def) 554crunch ifunsafe'[wp]: tcbSchedAppend if_unsafe_then_cap' 555 (simp: unless_def) 556crunch ifunsafe'[wp]: tcbSchedDequeue if_unsafe_then_cap' 557 558crunch idle'[wp]: tcbSchedEnqueue valid_idle' 559 (simp: crunch_simps unless_def) 560crunch idle'[wp]: tcbSchedAppend valid_idle' 561 (simp: crunch_simps unless_def) 562crunch idle'[wp]: tcbSchedDequeue valid_idle' 563 (simp: crunch_simps) 564 565crunch global_refs'[wp]: tcbSchedEnqueue valid_global_refs' 566 (wp: threadSet_global_refs simp: unless_def ignore: getObject setObject) 567crunch global_refs'[wp]: tcbSchedAppend valid_global_refs' 568 (wp: threadSet_global_refs simp: unless_def) 569crunch global_refs'[wp]: tcbSchedDequeue valid_global_refs' 570 (wp: threadSet_global_refs) 571 572crunch irq_node'[wp]: tcbSchedEnqueue "\<lambda>s. P (irq_node' s)" 573 (simp: unless_def) 574crunch irq_node'[wp]: tcbSchedAppend "\<lambda>s. P (irq_node' s)" 575 (simp: unless_def) 576crunch irq_node'[wp]: tcbSchedDequeue "\<lambda>s. P (irq_node' s)" 577 578crunch typ_at'[wp]: tcbSchedEnqueue "\<lambda>s. P (typ_at' T p s)" 579 (simp: unless_def) 580crunch typ_at'[wp]: tcbSchedAppend "\<lambda>s. P (typ_at' T p s)" 581 (simp: unless_def) 582crunch typ_at'[wp]: tcbSchedDequeue "\<lambda>s. P (typ_at' T p s)" 583 584crunch ctes_of[wp]: tcbSchedEnqueue "\<lambda>s. P (ctes_of s)" 585 (simp: unless_def) 586crunch ctes_of[wp]: tcbSchedAppend "\<lambda>s. P (ctes_of s)" 587 (simp: unless_def) 588crunch ctes_of[wp]: tcbSchedDequeue "\<lambda>s. P (ctes_of s)" 589 590crunch ksInterrupt[wp]: tcbSchedEnqueue "\<lambda>s. P (ksInterruptState s)" 591 (simp: unless_def) 592crunch ksInterrupt[wp]: tcbSchedAppend "\<lambda>s. P (ksInterruptState s)" 593 (simp: unless_def) 594crunch ksInterrupt[wp]: tcbSchedDequeue "\<lambda>s. P (ksInterruptState s)" 595 596crunch irq_states[wp]: tcbSchedEnqueue valid_irq_states' 597 (simp: unless_def) 598crunch irq_states[wp]: tcbSchedAppend valid_irq_states' 599 (simp: unless_def) 600crunch irq_states[wp]: tcbSchedDequeue valid_irq_states' 601 602crunch ct'[wp]: tcbSchedEnqueue "\<lambda>s. P (ksCurThread s)" 603 (simp: unless_def) 604crunch ct'[wp]: tcbSchedAppend "\<lambda>s. P (ksCurThread s)" 605 (simp: unless_def) 606crunch ct'[wp]: tcbSchedDequeue "\<lambda>s. P (ksCurThread s)" 607 608lemma tcbSchedEnqueue_vms'[wp]: 609 "\<lbrace>valid_machine_state'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" 610 apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) 611 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedEnqueue_ksMachine) 612 done 613 614crunch ksCurDomain[wp]: tcbSchedEnqueue "\<lambda>s. P (ksCurDomain s)" 615(simp: unless_def) 616 617lemma tcbSchedEnqueue_tcb_in_cur_domain'[wp]: 618 "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" 619 apply (rule tcb_in_cur_domain'_lift) 620 apply wp 621 apply (clarsimp simp: tcbSchedEnqueue_def) 622 apply (wpsimp simp: unless_def)+ 623 done 624 625lemma ct_idle_or_in_cur_domain'_lift2: 626 "\<lbrakk> \<And>t. \<lbrace>tcb_in_cur_domain' t\<rbrace> f \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>; 627 \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s) \<rbrace>; 628 \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s) \<rbrace>; 629 \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s) \<rbrace> f \<lbrace>\<lambda>_ s. P (ksSchedulerAction s) \<rbrace>\<rbrakk> 630 \<Longrightarrow> \<lbrace> ct_idle_or_in_cur_domain'\<rbrace> f \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain' \<rbrace>" 631 apply (unfold ct_idle_or_in_cur_domain'_def) 632 apply (rule hoare_lift_Pf2[where f=ksCurThread]) 633 apply (rule hoare_lift_Pf2[where f=ksSchedulerAction]) 634 including no_pre 635 apply (wp static_imp_wp hoare_vcg_disj_lift) 636 apply simp+ 637 done 638 639lemma tcbSchedEnqueue_invs'[wp]: 640 "\<lbrace>invs' 641 and st_tcb_at' runnable' t 642 and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> 643 tcbSchedEnqueue t 644 \<lbrace>\<lambda>_. invs'\<rbrace>" 645 apply (simp add: invs'_def valid_state'_def) 646 apply (rule hoare_pre) 647 apply (wp tcbSchedEnqueue_ct_not_inQ valid_irq_node_lift irqs_masked_lift hoare_vcg_disj_lift 648 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 649 untyped_ranges_zero_lift valid_ioports_lift' 650 | simp add: cteCaps_of_def o_def 651 | auto elim!: st_tcb_ex_cap'' valid_objs'_maxDomain valid_objs'_maxPriority split: thread_state.split_asm simp: valid_pspace'_def)+ 652 done 653 654crunch ksMachine[wp]: tcbSchedAppend "\<lambda>s. P (ksMachineState s)" 655 (simp: unless_def) 656 657lemma tcbSchedAppend_vms'[wp]: 658 "\<lbrace>valid_machine_state'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" 659 apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) 660 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedAppend_ksMachine) 661 done 662 663crunch pspace_domain_valid[wp]: tcbSchedAppend "pspace_domain_valid" 664 (simp: unless_def) 665 666crunch ksCurDomain[wp]: tcbSchedAppend "\<lambda>s. P (ksCurDomain s)" 667(simp: unless_def) 668 669crunch ksIdleThread[wp]: tcbSchedAppend "\<lambda>s. P (ksIdleThread s)" 670(simp: unless_def) 671 672crunch ksDomSchedule[wp]: tcbSchedAppend "\<lambda>s. P (ksDomSchedule s)" 673(simp: unless_def) 674 675lemma tcbSchedAppend_tcbDomain[wp]: 676 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> 677 tcbSchedAppend t 678 \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" 679 apply (clarsimp simp: tcbSchedAppend_def) 680 apply (wpsimp simp: unless_def)+ 681 done 682 683lemma tcbSchedAppend_tcbPriority[wp]: 684 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> 685 tcbSchedAppend t 686 \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" 687 apply (clarsimp simp: tcbSchedAppend_def) 688 apply (wpsimp simp: unless_def)+ 689 done 690 691lemma tcbSchedAppend_tcb_in_cur_domain'[wp]: 692 "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" 693 apply (rule tcb_in_cur_domain'_lift) 694 apply wp+ 695 done 696 697crunch ksDomScheduleIdx[wp]: tcbSchedAppend "\<lambda>s. P (ksDomScheduleIdx s)" 698 (simp: unless_def) 699 700crunch gsUntypedZeroRanges[wp]: tcbSchedAppend, tcbSchedDequeue "\<lambda>s. P (gsUntypedZeroRanges s)" 701 (simp: unless_def) 702 703crunches tcbSchedDequeue, tcbSchedAppend 704 for arch'[wp]: "\<lambda>s. P (ksArchState s)" 705 and ioports'[wp]: valid_ioports' 706 (wp: valid_ioports_lift'') 707 708lemma tcbSchedAppend_invs_but_ct_not_inQ': 709 "\<lbrace>invs' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> 710 tcbSchedAppend t \<lbrace>\<lambda>_. all_invs_but_ct_not_inQ'\<rbrace>" 711 apply (simp add: invs'_def valid_state'_def) 712 apply (rule hoare_pre) 713 apply (wp sch_act_wf_lift valid_irq_node_lift irqs_masked_lift 714 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 715 untyped_ranges_zero_lift 716 | simp add: cteCaps_of_def o_def 717 | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+ 718 done 719 720lemma tcbSchedAppend_sch_act_wf[wp]: 721 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> tcbSchedAppend thread 722 \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 723 apply (simp add:tcbSchedAppend_def bitmap_fun_defs) 724 apply (wp hoare_unless_wp setQueue_sch_act threadGet_wp|simp)+ 725 apply (fastforce simp:typ_at'_def obj_at'_def) 726 done 727 728lemma tcbSchedAppend_invs'[wp]: 729 "\<lbrace>invs' 730 and st_tcb_at' runnable' t 731 and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace> 732 tcbSchedAppend t 733 \<lbrace>\<lambda>_. invs'\<rbrace>" 734 apply (simp add: invs'_def valid_state'_def) 735 apply (rule hoare_pre) 736 apply (wp tcbSchedAppend_ct_not_inQ valid_irq_node_lift irqs_masked_lift hoare_vcg_disj_lift 737 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 738 untyped_ranges_zero_lift 739 | simp add: cteCaps_of_def o_def 740 | auto elim!: st_tcb_ex_cap'' valid_objs'_maxDomain valid_objs'_maxPriority split: thread_state.split_asm simp: valid_pspace'_def)+ 741 done 742 743lemma tcbSchedAppend_invs'_weak: 744 "\<lbrace>invs' and st_tcb_at' runnable' t and (\<lambda>s. t \<noteq> ksCurThread s) \<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. invs'\<rbrace>" 745 apply (simp add: invs'_def valid_state'_def) 746 apply (rule hoare_pre) 747 apply (wp tcbSchedAppend_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift 748 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 749 untyped_ranges_zero_lift 750 | simp add: cteCaps_of_def o_def 751 | fastforce elim!: st_tcb_ex_cap'' split: thread_state.split_asm)+ 752 done 753 754lemma tcbSchedEnqueue_invs'_not_ResumeCurrentThread: 755 "\<lbrace>invs' 756 and st_tcb_at' runnable' t 757 and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace> 758 tcbSchedEnqueue t 759 \<lbrace>\<lambda>_. invs'\<rbrace>" 760 by wpsimp 761 762lemma tcbSchedAppend_invs'_not_ResumeCurrentThread: 763 "\<lbrace>invs' 764 and st_tcb_at' runnable' t 765 and (\<lambda>s. ksSchedulerAction s \<noteq> ResumeCurrentThread)\<rbrace> 766 tcbSchedAppend t 767 \<lbrace>\<lambda>_. invs'\<rbrace>" 768 by wpsimp 769 770lemma tcb_at'_has_tcbDomain: 771 "tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbDomain tcb = p) t s" 772 by (clarsimp simp add: obj_at'_def) 773 774lemma tcbSchedEnqueue_in_ksQ: 775 "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedEnqueue t 776 \<lbrace>\<lambda>r s. \<exists>domain priority. t \<in> set (ksReadyQueues s (domain, priority))\<rbrace>" 777 apply (rule_tac Q="\<lambda>s. \<exists>d p. valid_queues' s \<and> 778 obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> 779 obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s" 780 in hoare_pre_imp) 781 apply (clarsimp simp: tcb_at'_has_tcbPriority tcb_at'_has_tcbDomain) 782 apply (rule hoare_vcg_ex_lift)+ 783 apply (simp add: tcbSchedEnqueue_def unless_def) 784 apply wpsimp 785 apply (rule_tac Q="\<lambda>rv s. tdom = d \<and> rv = p \<and> obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s 786 \<and> obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s" 787 in hoare_post_imp, clarsimp) 788 apply (wp, (wp threadGet_const)+) 789 apply (rule_tac Q="\<lambda>rv s. 790 obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s \<and> 791 obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s \<and> 792 obj_at' (\<lambda>tcb. tcbQueued tcb = rv) t s \<and> 793 (rv \<longrightarrow> t \<in> set (ksReadyQueues s (d, p)))" in hoare_post_imp) 794 apply (clarsimp simp: o_def elim!: obj_at'_weakenE) 795 apply (wp threadGet_obj_at' hoare_vcg_imp_lift threadGet_const) 796 apply (clarsimp simp: valid_queues'_def) 797 apply (drule_tac x=d in spec) 798 apply (drule_tac x=p in spec) 799 apply (drule_tac x=t in spec) 800 apply normalise_obj_at' 801 apply (clarsimp simp: inQ_def) 802 done 803 804crunch ksMachine[wp]: tcbSchedDequeue "\<lambda>s. P (ksMachineState s)" 805 (simp: unless_def) 806 807lemma tcbSchedDequeue_vms'[wp]: 808 "\<lbrace>valid_machine_state'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" 809 apply (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) 810 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift tcbSchedDequeue_ksMachine) 811 done 812 813crunch pspace_domain_valid[wp]: tcbSchedDequeue "pspace_domain_valid" 814 815crunch ksCurDomain[wp]: tcbSchedDequeue "\<lambda>s. P (ksCurDomain s)" 816(simp: unless_def) 817 818crunch ksIdleThread[wp]: tcbSchedDequeue "\<lambda>s. P (ksIdleThread s)" 819(simp: unless_def) 820 821crunch ksDomSchedule[wp]: tcbSchedDequeue "\<lambda>s. P (ksDomSchedule s)" 822(simp: unless_def) 823 824crunch ksDomScheduleIdx[wp]: tcbSchedDequeue "\<lambda>s. P (ksDomScheduleIdx s)" 825(simp: unless_def) 826 827lemma tcbSchedDequeue_tcb_in_cur_domain'[wp]: 828 "\<lbrace>tcb_in_cur_domain' t'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" 829 apply (rule tcb_in_cur_domain'_lift) 830 apply wp 831 apply (clarsimp simp: tcbSchedDequeue_def) 832 apply (wp hoare_when_weak_wp | simp)+ 833 done 834 835lemma tcbSchedDequeue_tcbDomain[wp]: 836 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> 837 tcbSchedDequeue t 838 \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" 839 apply (clarsimp simp: tcbSchedDequeue_def) 840 apply (wp hoare_when_weak_wp | simp)+ 841 done 842 843lemma tcbSchedDequeue_tcbPriority[wp]: 844 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> 845 tcbSchedDequeue t 846 \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" 847 apply (clarsimp simp: tcbSchedDequeue_def) 848 apply (wp hoare_when_weak_wp | simp)+ 849 done 850 851lemma tcbSchedDequeue_invs'[wp]: 852 "\<lbrace>invs' and tcb_at' t\<rbrace> 853 tcbSchedDequeue t 854 \<lbrace>\<lambda>_. invs'\<rbrace>" 855 unfolding invs'_def valid_state'_def 856 apply (rule hoare_pre) 857 apply (wp tcbSchedDequeue_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift 858 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 859 tcbSchedDequeue_valid_queues 860 untyped_ranges_zero_lift 861 | simp add: cteCaps_of_def o_def)+ 862 apply (fastforce elim: valid_objs'_maxDomain valid_objs'_maxPriority simp: valid_pspace'_def)+ 863 done 864 865lemma no_fail_isRunnable[wp]: 866 "no_fail (tcb_at' t) (isRunnable t)" 867 apply (simp add: isRunnable_def isBlocked_def) 868 apply (rule no_fail_pre, wp) 869 apply (clarsimp simp: pred_tcb_at'_def) 870 done 871 872lemma corres_when_r: 873 "\<lbrakk> G \<Longrightarrow> corres r P P' f g; 874 \<not> G \<Longrightarrow> corres r Q Q' f (return ()) \<rbrakk> 875 \<Longrightarrow> corres r (P and Q) (\<lambda>s. (G \<longrightarrow> P' s) \<and> (\<not>G \<longrightarrow> Q' s)) f (when G g)" 876 apply (cases G, simp_all add: when_def) 877 apply (rule corres_guard_imp, simp+)+ 878 done 879 880lemma cur_thread_update_corres: 881 "corres dc \<top> \<top> (modify (cur_thread_update (\<lambda>_. t))) (setCurThread t)" 882 apply (unfold setCurThread_def) 883 apply (rule corres_modify) 884 apply (simp add: state_relation_def swp_def) 885 done 886 887lemma arch_switch_thread_tcb_at' [wp]: "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" 888 by (unfold X64_H.switchToThread_def, wp typ_at_lift_tcb') 889 890crunch typ_at'[wp]: "switchToThread" "\<lambda>s. P (typ_at' T p s)" 891 (ignore: ) 892 893lemma Arch_switchToThread_pred_tcb'[wp]: 894 "\<lbrace>\<lambda>s. P (pred_tcb_at' proj P' t' s)\<rbrace> 895 Arch.switchToThread t \<lbrace>\<lambda>rv s. P (pred_tcb_at' proj P' t' s)\<rbrace>" 896proof - 897 have pos: "\<And>P t t'. \<lbrace>pred_tcb_at' proj P t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. pred_tcb_at' proj P t'\<rbrace>" 898 apply (simp add: pred_tcb_at'_def X64_H.switchToThread_def) 899 apply (rule setVMRoot_obj_at) 900 done 901 show ?thesis 902 apply (rule P_bool_lift [OF pos]) 903 by (rule lift_neg_pred_tcb_at' [OF ArchThreadDecls_H_X64_H_switchToThread_typ_at' pos]) 904qed 905 906 907crunch ksQ[wp]: storeWordUser "\<lambda>s. P (ksReadyQueues s p)" 908crunch ksQ[wp]: setVMRoot "\<lambda>s. P (ksReadyQueues s)" 909(wp: crunch_wps simp: crunch_simps) 910crunch ksIdleThread[wp]: storeWordUser "\<lambda>s. P (ksIdleThread s)" 911crunch ksIdleThread[wp]: asUser "\<lambda>s. P (ksIdleThread s)" 912(wp: crunch_wps simp: crunch_simps) 913crunch ksQ[wp]: asUser "\<lambda>s. P (ksReadyQueues s p)" 914(wp: crunch_wps simp: crunch_simps) 915 916lemma arch_switch_thread_ksQ[wp]: 917 "\<lbrace>\<lambda>s. P (ksReadyQueues s p)\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_ s. P (ksReadyQueues s p)\<rbrace>" 918 apply (simp add: X64_H.switchToThread_def) 919 apply (wp) 920 done 921 922crunch valid_queues[wp]: "Arch.switchToThread" "Invariants_H.valid_queues" 923(wp: crunch_wps simp: crunch_simps) 924 925lemma switch_thread_corres: 926 "corres dc (valid_arch_state and valid_objs and valid_asid_map 927 and valid_vspace_objs and pspace_aligned and pspace_distinct 928 and valid_vs_lookup and valid_global_objs 929 and unique_table_refs o caps_of_state 930 and st_tcb_at runnable t and valid_etcbs) 931 (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues 932 and st_tcb_at' runnable' t and cur_tcb') 933 (switch_to_thread t) (switchToThread t)" 934 (is "corres _ ?PA ?PH _ _") 935 936proof - 937 have mainpart: "corres dc (?PA) (?PH) 938 (do y \<leftarrow> arch_switch_to_thread t; 939 y \<leftarrow> (tcb_sched_action tcb_sched_dequeue t); 940 modify (cur_thread_update (\<lambda>_. t)) 941 od) 942 (do y \<leftarrow> Arch.switchToThread t; 943 y \<leftarrow> tcbSchedDequeue t; 944 setCurThread t 945 od)" 946 apply (rule corres_guard_imp) 947 apply (rule corres_split [OF _ arch_switch_thread_corres]) 948 apply (rule corres_split[OF cur_thread_update_corres tcbSchedDequeue_corres]) 949 apply (wp|clarsimp simp: tcb_at_is_etcb_at st_tcb_at_tcb_at)+ 950 done 951 952 show ?thesis 953 apply - 954 apply (simp add: switch_to_thread_def Thread_H.switchToThread_def) 955 apply (rule corres_symb_exec_l [where Q = "\<lambda> s rv. (?PA and (=) rv) s", 956 OF corres_symb_exec_l [OF mainpart]]) 957 apply (auto intro: no_fail_pre [OF no_fail_assert] 958 no_fail_pre [OF no_fail_get] 959 dest: st_tcb_at_tcb_at [THEN get_tcb_at] | 960 simp add: assert_def | wp)+ 961 done 962qed 963 964lemma allActiveTCBs_corres: 965 assumes "\<And>threads. corres r (P threads) P' (m threads) m'" 966 shows "corres r (\<lambda>s. P {x. getActiveTCB x s \<noteq> None} s) P' (do threads \<leftarrow> allActiveTCBs; m threads od) m'" 967 apply (simp add: allActiveTCBs_def) 968 apply (simp add: bind_def get_def) 969 apply (insert assms) 970 apply (simp add: corres_underlying_def) 971 apply force 972 done 973 974lemma typ_at'_typ_at'_mask: "\<And>s. \<lbrakk> typ_at' t (P s) s \<rbrakk> \<Longrightarrow> typ_at' t (P s && ~~mask (objBitsT t)) s" 975 apply (rule split_state_strg [where P = "typ_at' t", THEN mp]) 976 apply (frule typ_at_aligned') 977 apply (clarsimp dest!: is_aligned_neg_mask_eq) 978 done 979 980lemma arch_switch_idle_thread_corres: 981 "corres dc 982 (valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state 983 and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct 984 and valid_vspace_objs and valid_idle) 985 (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle') 986 arch_switch_to_idle_thread Arch.switchToIdleThread" 987 apply (simp add: arch_switch_to_idle_thread_def 988 X64_H.switchToIdleThread_def) 989 apply (corressimp corres: git_corres set_vm_root_corres) 990 apply (clarsimp simp: valid_idle_def valid_idle'_def pred_tcb_at_def obj_at_def is_tcb) 991 done 992 993lemma switch_idle_thread_corres: 994 "corres dc invs invs_no_cicd' switch_to_idle_thread switchToIdleThread" 995 apply (simp add: switch_to_idle_thread_def Thread_H.switchToIdleThread_def) 996 apply (rule corres_guard_imp) 997 apply (rule corres_split [OF _ git_corres]) 998 apply (rule corres_split [OF _ arch_switch_idle_thread_corres]) 999 apply (unfold setCurThread_def) 1000 apply (rule corres_trivial, rule corres_modify) 1001 apply (simp add: state_relation_def cdt_relation_def) 1002 apply (wp+, simp+) 1003 apply (simp add: invs_unique_refs invs_valid_vs_lookup invs_valid_objs invs_valid_asid_map 1004 invs_arch_state invs_valid_global_objs invs_psp_aligned invs_distinct 1005 invs_valid_idle invs_vspace_objs) 1006 apply (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def) 1007 done 1008 1009lemma gq_sp: "\<lbrace>P\<rbrace> getQueue d p \<lbrace>\<lambda>rv. P and (\<lambda>s. ksReadyQueues s (d, p) = rv)\<rbrace>" 1010 by (unfold getQueue_def, rule gets_sp) 1011 1012lemma gq_se: "\<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> True\<rbrace> getQueue d p \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>" 1013 by (simp add: getQueue_def) 1014 1015lemma setQueue_no_change_ct[wp]: 1016 "\<lbrace>ct_in_state' st\<rbrace> setQueue d p q \<lbrace>\<lambda>rv. ct_in_state' st\<rbrace>" 1017 apply (simp add: setQueue_def) 1018 apply wp 1019 apply (simp add: ct_in_state'_def pred_tcb_at'_def) 1020 done 1021 1022lemma sch_act_wf: 1023 "sch_act_wf sa s = ((\<forall>t. sa = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s \<and> 1024 tcb_in_cur_domain' t s) \<and> 1025 (sa = ResumeCurrentThread \<longrightarrow> ct_in_state' activatable' s))" 1026 by (case_tac sa, simp_all add: ) 1027 1028declare gq_wp[wp] 1029declare setQueue_obj_at[wp] 1030 1031lemma ready_tcb': 1032 "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); invs' s \<rbrakk> 1033 \<Longrightarrow> obj_at' (inQ d p) t s" 1034 apply (clarsimp simp: invs'_def valid_state'_def 1035 valid_pspace'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def) 1036 apply (drule_tac x=d in spec) 1037 apply (drule_tac x=p in spec) 1038 apply (clarsimp) 1039 apply (drule(1) bspec) 1040 apply (erule obj_at'_weakenE) 1041 apply (simp) 1042 done 1043 1044lemma ready_tcb_valid_queues: 1045 "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); valid_queues s \<rbrakk> 1046 \<Longrightarrow> obj_at' (inQ d p) t s" 1047 apply (clarsimp simp: invs'_def valid_state'_def 1048 valid_pspace'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def) 1049 apply (drule_tac x=d in spec) 1050 apply (drule_tac x=p in spec) 1051 apply (clarsimp) 1052 apply (drule(1) bspec) 1053 apply (erule obj_at'_weakenE) 1054 apply (simp) 1055 done 1056 1057lemma queued_vs_state[wp]: 1058 "\<lbrace>ct_in_state' st\<rbrace> threadSet (tcbQueued_update x) t \<lbrace>\<lambda>rv. ct_in_state' st\<rbrace>" 1059 apply (rule hoare_vcg_precond_imp) 1060 apply (rule hoare_post_imp[where Q="\<lambda>rv s. \<exists>t. t = ksCurThread s \<and> st_tcb_at' st t s"]) 1061 apply (simp add: ct_in_state'_def) 1062 apply (unfold pred_tcb_at'_def) 1063 apply (wp hoare_ex_wp threadSet_ct) 1064 apply (simp add: ct_in_state'_def pred_tcb_at'_def) 1065 done 1066 1067lemma threadSet_timeslice_invs: 1068 "\<lbrace>invs' and tcb_at' t\<rbrace> threadSet (tcbTimeSlice_update b) t \<lbrace>\<lambda>rv. invs'\<rbrace>" 1069 by (wp threadSet_invs_trivial, simp_all add: inQ_def cong: conj_cong) 1070 1071lemma setCurThread_invs_no_cicd': 1072 "\<lbrace>invs_no_cicd' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and tcb_in_cur_domain' t\<rbrace> 1073 setCurThread t 1074 \<lbrace>\<lambda>rv. invs'\<rbrace>" 1075proof - 1076 have obj_at'_ct: "\<And>f P addr s. 1077 obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s" 1078 by (fastforce intro: obj_at'_pspaceI) 1079 have valid_pspace'_ct: "\<And>s f. 1080 valid_pspace' (ksCurThread_update f s) = valid_pspace' s" 1081 by (rule valid_pspace'_ksPSpace, simp) 1082 have vms'_ct: "\<And>s f. 1083 valid_machine_state' (ksCurThread_update f s) = valid_machine_state' s" 1084 by (simp add: valid_machine_state'_def) 1085 have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)" 1086 apply (simp add: ct_not_inQ_def o_def) 1087 done 1088 have tcb_in_cur_domain_ct: "\<And>s f t. 1089 tcb_in_cur_domain' t (ksCurThread_update f s)= tcb_in_cur_domain' t s" 1090 by (fastforce simp: tcb_in_cur_domain'_def) 1091 show ?thesis 1092 apply (simp add: setCurThread_def) 1093 apply wp 1094 apply (clarsimp simp add: all_invs_but_ct_idle_or_in_cur_domain'_def invs'_def cur_tcb'_def valid_state'_def obj_at'_ct 1095 valid_pspace'_ct vms'_ct Invariants_H.valid_queues_def 1096 sch_act_wf ct_in_state'_def state_refs_of'_def 1097 ps_clear_def valid_irq_node'_def valid_queues'_def ct_not_inQ_ct 1098 tcb_in_cur_domain_ct ct_idle_or_in_cur_domain'_def 1099 bitmapQ_defs valid_queues_no_bitmap_def 1100 cong: option.case_cong) 1101 done 1102qed 1103 1104(* Don't use this rule when considering the idle thread. The invariant ct_idle_or_in_cur_domain' 1105 says that either "tcb_in_cur_domain' t" or "t = ksIdleThread s". 1106 Use setCurThread_invs_idle_thread instead. *) 1107lemma setCurThread_invs: 1108 "\<lbrace>invs' and st_tcb_at' activatable' t and obj_at' (\<lambda>x. \<not> tcbQueued x) t and 1109 tcb_in_cur_domain' t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" 1110 by (rule hoare_pre, rule setCurThread_invs_no_cicd') 1111 (simp add: invs'_to_invs_no_cicd'_def) 1112 1113lemma valid_queues_not_runnable_not_queued: 1114 fixes s 1115 assumes vq: "Invariants_H.valid_queues s" 1116 and vq': "valid_queues' s" 1117 and st: "st_tcb_at' (Not \<circ> runnable') t s" 1118 shows "obj_at' (Not \<circ> tcbQueued) t s" 1119proof (rule ccontr) 1120 assume "\<not> obj_at' (Not \<circ> tcbQueued) t s" 1121 moreover from st have "typ_at' TCBT t s" 1122 by (rule pred_tcb_at' [THEN tcb_at_typ_at' [THEN iffD1]]) 1123 ultimately have "obj_at' tcbQueued t s" 1124 by (clarsimp simp: not_obj_at' comp_def) 1125 1126 moreover 1127 from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbPriority] 1128 obtain p where tp: "obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s" 1129 by clarsimp 1130 1131 moreover 1132 from st [THEN pred_tcb_at', THEN tcb_at'_has_tcbDomain] 1133 obtain d where td: "obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s" 1134 by clarsimp 1135 1136 ultimately 1137 have "t \<in> set (ksReadyQueues s (d, p))" using vq' 1138 unfolding valid_queues'_def 1139 apply - 1140 apply (drule_tac x=d in spec) 1141 apply (drule_tac x=p in spec) 1142 apply (drule_tac x=t in spec) 1143 apply (erule impE) 1144 apply (fastforce simp add: inQ_def obj_at'_def) 1145 apply (assumption) 1146 done 1147 1148 with vq have "st_tcb_at' runnable' t s" 1149 unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def 1150 apply - 1151 apply clarsimp 1152 apply (drule_tac x=d in spec) 1153 apply (drule_tac x=p in spec) 1154 apply (clarsimp simp add: st_tcb_at'_def) 1155 apply (drule(1) bspec) 1156 apply (erule obj_at'_weakenE) 1157 apply (clarsimp) 1158 done 1159 1160 with st show False 1161 apply - 1162 apply (drule(1) pred_tcb_at_conj') 1163 apply (clarsimp) 1164 done 1165qed 1166 1167(* 1168 * The idle thread is not part of any ready queues. 1169 *) 1170lemma idle'_not_tcbQueued': 1171 assumes vq: "Invariants_H.valid_queues s" 1172 and vq': "valid_queues' s" 1173 and idle: "valid_idle' s" 1174 shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s" 1175 proof - 1176 from idle have stidle: "st_tcb_at' (Not \<circ> runnable') (ksIdleThread s) s" 1177 by (clarsimp simp add: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) 1178 1179 with vq vq' show ?thesis 1180 by (rule valid_queues_not_runnable_not_queued) 1181 qed 1182 1183lemma idle'_not_tcbQueued: 1184 assumes "invs' s" 1185 shows "obj_at' (Not \<circ> tcbQueued) (ksIdleThread s) s" 1186 by (insert assms) 1187 (clarsimp simp: invs'_def valid_state'_def 1188 elim!: idle'_not_tcbQueued') 1189 1190lemma setCurThread_invs_no_cicd'_idle_thread: 1191 "\<lbrace>invs_no_cicd' and (\<lambda>s. t = ksIdleThread s) \<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" 1192proof - 1193 have vms'_ct: "\<And>s f. 1194 valid_machine_state' (ksCurThread_update f s) = valid_machine_state' s" 1195 by (simp add: valid_machine_state'_def) 1196 have ct_not_inQ_ct: "\<And>s t . \<lbrakk> ct_not_inQ s; obj_at' (\<lambda>x. \<not> tcbQueued x) t s\<rbrakk> \<Longrightarrow> ct_not_inQ (s\<lparr> ksCurThread := t \<rparr>)" 1197 apply (simp add: ct_not_inQ_def o_def) 1198 done 1199 have idle'_activatable': "\<And> s t. st_tcb_at' idle' t s \<Longrightarrow> st_tcb_at' activatable' t s" 1200 apply (clarsimp simp: st_tcb_at'_def o_def obj_at'_def) 1201 done 1202 show ?thesis 1203 apply (simp add: setCurThread_def) 1204 apply wp 1205 apply (clarsimp simp add: vms'_ct ct_not_inQ_ct idle'_activatable' idle'_not_tcbQueued'[simplified o_def] 1206 invs'_def cur_tcb'_def valid_state'_def valid_idle'_def 1207 sch_act_wf ct_in_state'_def state_refs_of'_def 1208 ps_clear_def valid_irq_node'_def 1209 ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def 1210 valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def valid_queues'_def 1211 all_invs_but_ct_idle_or_in_cur_domain'_def pred_tcb_at'_def 1212 cong: option.case_cong) 1213 apply (clarsimp simp: obj_at'_def projectKOs) 1214 done 1215qed 1216 1217lemma setCurThread_invs_idle_thread: 1218 "\<lbrace>invs' and (\<lambda>s. t = ksIdleThread s) \<rbrace> setCurThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" 1219 by (rule hoare_pre, rule setCurThread_invs_no_cicd'_idle_thread) 1220 (clarsimp simp: invs'_to_invs_no_cicd'_def all_invs_but_ct_idle_or_in_cur_domain'_def) 1221 1222lemma Arch_switchToThread_invs[wp]: 1223 "\<lbrace>invs' and tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs'\<rbrace>" 1224 apply (simp add: X64_H.switchToThread_def) 1225 apply (wp; auto) 1226 done 1227 1228lemma Arch_switchToThread_tcb'[wp]: 1229 "\<lbrace>tcb_at' t\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>" 1230 apply (simp add: X64_H.switchToThread_def) 1231 apply (wp doMachineOp_obj_at hoare_drop_imps)+ 1232 done 1233 1234crunch ksCurDomain[wp]: "Arch.switchToThread" "\<lambda>s. P (ksCurDomain s)" 1235(simp: crunch_simps) 1236 1237lemma Arch_swichToThread_tcbDomain_triv[wp]: 1238 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' \<rbrace>" 1239 apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def) 1240 apply (wp hoare_drop_imp | simp)+ 1241 done 1242 1243lemma Arch_swichToThread_tcbPriority_triv[wp]: 1244 "\<lbrace> obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace> Arch.switchToThread t \<lbrace> \<lambda>_. obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t' \<rbrace>" 1245 apply (clarsimp simp: X64_H.switchToThread_def storeWordUser_def) 1246 apply (wp hoare_drop_imp | simp)+ 1247 done 1248 1249lemma Arch_switchToThread_tcb_in_cur_domain'[wp]: 1250 "\<lbrace>tcb_in_cur_domain' t'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>_. tcb_in_cur_domain' t' \<rbrace>" 1251 apply (rule tcb_in_cur_domain'_lift) 1252 apply wp+ 1253 done 1254 1255lemma tcbSchedDequeue_not_tcbQueued: 1256 "\<lbrace> tcb_at' t \<rbrace> tcbSchedDequeue t \<lbrace> \<lambda>_. obj_at' (\<lambda>x. \<not> tcbQueued x) t \<rbrace>" 1257 apply (simp add: tcbSchedDequeue_def) 1258 apply (wp|clarsimp)+ 1259 apply (rule_tac Q="\<lambda>queued. obj_at' (\<lambda>x. tcbQueued x = queued) t" in hoare_post_imp) 1260 apply (clarsimp simp: obj_at'_def) 1261 apply (wp threadGet_obj_at') 1262 apply (simp) 1263 done 1264 1265lemma asUser_obj_at[wp]: "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> 1266 asUser t' f 1267 \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>" 1268 apply (simp add: asUser_def threadGet_stateAssert_gets_asUser) 1269 apply (wp|wpc)+ 1270 apply (simp add: asUser_fetch_def obj_at'_def) 1271 done 1272 1273lemma Arch_switchToThread_obj_at[wp]: 1274 "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> 1275 Arch.switchToThread t 1276 \<lbrace>\<lambda>rv. obj_at' (P \<circ> tcbState) t\<rbrace>" 1277 apply (simp add: X64_H.switchToThread_def ) 1278 apply (rule setVMRoot_obj_at) 1279 done 1280 1281declare doMachineOp_obj_at[wp] 1282 1283crunch valid_arch_state'[wp]: asUser "valid_arch_state'" 1284(wp: crunch_wps simp: crunch_simps) 1285 1286crunch valid_irq_states'[wp]: asUser "valid_irq_states'" 1287(wp: crunch_wps simp: crunch_simps) 1288 1289crunch valid_machine_state'[wp]: asUser "valid_machine_state'" 1290(wp: crunch_wps simp: crunch_simps) 1291 1292crunch valid_queues'[wp]: asUser "valid_queues'" 1293(wp: crunch_wps simp: crunch_simps) 1294 1295 1296lemma asUser_valid_irq_node'[wp]: 1297 "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> asUser t (setRegister f r) 1298 \<lbrace>\<lambda>_ s. valid_irq_node' (irq_node' s) s\<rbrace>" 1299 apply (rule_tac valid_irq_node_lift) 1300 apply (simp add: asUser_def) 1301 apply (wpsimp wp: crunch_wps)+ 1302 done 1303 1304crunch irq_masked'_helper: asUser "\<lambda>s. P (intStateIRQTable (ksInterruptState s))" 1305(wp: crunch_wps simp: crunch_simps) 1306 1307lemma asUser_irq_masked'[wp]: 1308 "\<lbrace>irqs_masked'\<rbrace> asUser t (setRegister f r) 1309 \<lbrace>\<lambda>_ . irqs_masked'\<rbrace>" 1310 apply (rule irqs_masked_lift) 1311 apply (rule asUser_irq_masked'_helper) 1312 done 1313 1314lemma asUser_ct_not_inQ[wp]: 1315 "\<lbrace>ct_not_inQ\<rbrace> asUser t (setRegister f r) 1316 \<lbrace>\<lambda>_ . ct_not_inQ\<rbrace>" 1317 apply (clarsimp simp: submonad_asUser.fn_is_sm submonad_fn_def) 1318 apply (rule hoare_seq_ext)+ 1319 prefer 4 1320 apply (rule stateAssert_sp) 1321 prefer 3 1322 apply (rule gets_inv) 1323 defer 1324 apply (rule select_f_inv) 1325 apply (case_tac x; simp) 1326 apply (clarsimp simp: projectKOs asUser_replace_def obj_at'_def fun_upd_def 1327 split: option.split kernel_object.split) 1328 apply wp 1329 apply (clarsimp simp: ct_not_inQ_def obj_at'_def projectKOs objBitsKO_def ps_clear_def dom_def) 1330 apply (rule conjI; clarsimp; blast) 1331 done 1332 1333crunch pspace_domain_valid[wp]: asUser "pspace_domain_valid" 1334(wp: crunch_wps simp: crunch_simps) 1335 1336crunch valid_dom_schedule'[wp]: asUser "valid_dom_schedule'" 1337(wp: crunch_wps simp: crunch_simps) 1338 1339crunch gsUntypedZeroRanges[wp]: asUser "\<lambda>s. P (gsUntypedZeroRanges s)" 1340 (wp: crunch_wps simp: unless_def) 1341 1342crunch ctes_of[wp]: asUser "\<lambda>s. P (ctes_of s)" 1343 (wp: crunch_wps simp: unless_def) 1344 1345lemmas asUser_cteCaps_of[wp] = cteCaps_of_ctes_of_lift[OF asUser_ctes_of] 1346 1347lemma asUser_utr[wp]: 1348 "\<lbrace>untyped_ranges_zero'\<rbrace> asUser f t \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace>" 1349 apply (simp add: cteCaps_of_def) 1350 apply (rule hoare_pre, wp untyped_ranges_zero_lift) 1351 apply (simp add: o_def) 1352 done 1353 1354lemma asUser_ioports'[wp]: 1355 "\<lbrace>valid_ioports'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_ioports'\<rbrace>" 1356 apply (simp add: asUser_def split_def) 1357 apply (wpsimp wp: valid_ioports_lift'' select_f_inv threadSet_ctes_of) 1358 done 1359 1360lemma asUser_invs_no_cicd'[wp]: 1361 "\<lbrace>invs_no_cicd'\<rbrace> asUser t (setRegister f r) \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" 1362 apply (simp add: invs_no_cicd'_def) 1363 apply (rule hoare_pre) 1364 apply (wpc | wp asUser_global_refs' asUser_irq_handlers')+ 1365 apply (rule hoare_post_imp[rotated]) 1366 apply (rule hoare_vcg_conj_lift) 1367 apply (rule asUser_valid_dom_schedule') 1368 apply (rule asUser_utr) 1369 apply clarsimp 1370 apply clarsimp 1371 done 1372 1373 1374lemma Arch_switchToThread_invs_no_cicd': 1375 "\<lbrace>invs_no_cicd'\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" 1376 apply (simp add: X64_H.switchToThread_def) 1377 by (wp|rule setVMRoot_invs_no_cicd')+ 1378 1379lemma tcbSchedDequeue_invs_no_cicd'[wp]: 1380 "\<lbrace>invs_no_cicd' and tcb_at' t\<rbrace> 1381 tcbSchedDequeue t 1382 \<lbrace>\<lambda>_. invs_no_cicd'\<rbrace>" 1383 unfolding all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def 1384 apply (wp tcbSchedDequeue_ct_not_inQ sch_act_wf_lift valid_irq_node_lift irqs_masked_lift 1385 valid_irq_handlers_lift' cur_tcb_lift ct_idle_or_in_cur_domain'_lift2 1386 tcbSchedDequeue_valid_queues_weak 1387 untyped_ranges_zero_lift 1388 | simp add: cteCaps_of_def o_def)+ 1389 apply clarsimp 1390 apply (fastforce simp: valid_pspace'_def valid_queues_def 1391 elim: valid_objs'_maxDomain valid_objs'_maxPriority intro: obj_at'_conjI) 1392 done 1393 1394lemma switchToThread_invs_no_cicd': 1395 "\<lbrace>invs_no_cicd' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> ThreadDecls_H.switchToThread t \<lbrace>\<lambda>rv. invs' \<rbrace>" 1396 apply (simp add: Thread_H.switchToThread_def) 1397 apply (wp setCurThread_invs_no_cicd' tcbSchedDequeue_not_tcbQueued 1398 Arch_switchToThread_invs_no_cicd' Arch_switchToThread_pred_tcb') 1399 apply (auto elim!: pred_tcb'_weakenE) 1400 done 1401 1402lemma switchToThread_invs[wp]: 1403 "\<lbrace>invs' and st_tcb_at' runnable' t and tcb_in_cur_domain' t \<rbrace> switchToThread t \<lbrace>\<lambda>rv. invs' \<rbrace>" 1404 apply (simp add: Thread_H.switchToThread_def ) 1405 apply (wp threadSet_timeslice_invs setCurThread_invs 1406 Arch_switchToThread_invs dmo_invs' 1407 doMachineOp_obj_at tcbSchedDequeue_not_tcbQueued) 1408 by (auto elim!: pred_tcb'_weakenE) 1409 1410lemma setCurThread_ct_in_state: 1411 "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" 1412proof - 1413 have obj_at'_ct: "\<And>P addr f s. 1414 obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s" 1415 by (fastforce intro: obj_at'_pspaceI) 1416 show ?thesis 1417 apply (simp add: setCurThread_def) 1418 apply wp 1419 apply (simp add: ct_in_state'_def pred_tcb_at'_def obj_at'_ct o_def) 1420 done 1421qed 1422 1423lemma switchToThread_ct_in_state[wp]: 1424 "\<lbrace>obj_at' (P \<circ> tcbState) t\<rbrace> switchToThread t \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" 1425proof - 1426 have P: "\<And>f x. tcbState (tcbTimeSlice_update f x) = tcbState x" 1427 by (case_tac x, simp) 1428 show ?thesis 1429 apply (simp add: Thread_H.switchToThread_def tcbSchedEnqueue_def unless_def) 1430 apply (wp setCurThread_ct_in_state Arch_switchToThread_obj_at 1431 | simp add: P o_def cong: if_cong)+ 1432 done 1433qed 1434 1435lemma setCurThread_obj_at[wp]: 1436 "\<lbrace>obj_at' P addr\<rbrace> setCurThread t \<lbrace>\<lambda>rv. obj_at' P addr\<rbrace>" 1437 apply (simp add: setCurThread_def) 1438 apply wp 1439 apply (fastforce intro: obj_at'_pspaceI) 1440 done 1441 1442lemma switchToThread_tcb'[wp]: 1443 "\<lbrace>tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>" 1444 apply (simp add: Thread_H.switchToThread_def when_def) 1445 apply wp 1446 done 1447 1448crunch cap_to'[wp]: setQueue "ex_nonz_cap_to' p" 1449 1450lemma dmo_cap_to'[wp]: 1451 "\<lbrace>ex_nonz_cap_to' p\<rbrace> 1452 doMachineOp m 1453 \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" 1454 by (wp ex_nonz_cap_to_pres') 1455 1456lemma sct_cap_to'[wp]: 1457 "\<lbrace>ex_nonz_cap_to' p\<rbrace> setCurThread t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" 1458 apply (simp add: setCurThread_def) 1459 apply (wp ex_nonz_cap_to_pres') 1460 apply (clarsimp elim!: cte_wp_at'_pspaceI)+ 1461 done 1462 1463 1464crunch cap_to'[wp]: "Arch.switchToThread" "ex_nonz_cap_to' p" 1465 (simp: crunch_simps) 1466 1467crunch cap_to'[wp]: switchToThread "ex_nonz_cap_to' p" 1468 (simp: crunch_simps) 1469 1470lemma no_longer_inQ[simp]: 1471 "\<not> inQ d p (tcbQueued_update (\<lambda>x. False) tcb)" 1472 by (simp add: inQ_def) 1473 1474lemma rq_distinct: 1475 "invs' s \<Longrightarrow> distinct (ksReadyQueues s (d, p))" 1476 by (clarsimp simp: invs'_def valid_state'_def Invariants_H.valid_queues_def 1477 valid_queues_no_bitmap_def) 1478 1479lemma iflive_inQ_nonz_cap_strg: 1480 "if_live_then_nonz_cap' s \<and> obj_at' (inQ d prio) t s 1481 \<longrightarrow> ex_nonz_cap_to' t s" 1482 by (clarsimp simp: obj_at'_real_def projectKOs inQ_def 1483 elim!: if_live_then_nonz_capE' ko_wp_at'_weakenE) 1484 1485lemmas iflive_inQ_nonz_cap[elim] 1486 = mp [OF iflive_inQ_nonz_cap_strg, OF conjI[rotated]] 1487 1488crunch ksRQ[wp]: threadSet "\<lambda>s. P (ksReadyQueues s)" 1489 (ignore: setObject getObject 1490 wp: updateObject_default_inv) 1491 1492declare Cons_eq_tails[simp] 1493 1494lemma invs_ksReadyQueues_update_triv: 1495 assumes a: "\<forall>d p. set (f (ksReadyQueues s) (d,p)) = set (ksReadyQueues s (d,p))" 1496 assumes b: "\<forall>d p. distinct (f (ksReadyQueues s) (d,p)) = distinct (ksReadyQueues s (d,p))" 1497 assumes c: "\<forall>d p. (d > maxDomain \<or> p > maxPriority \<longrightarrow> 1498 (f (ksReadyQueues s) (d,p) = [])) = (d > maxDomain \<or> p > maxPriority \<longrightarrow> 1499 (ksReadyQueues s (d,p) = []))" 1500 shows "invs' (ksReadyQueues_update f s) = invs' s" 1501 1502proof - 1503 have orphans: 1504 "bitmapQ_no_L1_orphans (ksReadyQueues_update f s) = bitmapQ_no_L1_orphans s" 1505 "bitmapQ_no_L2_orphans (ksReadyQueues_update f s) = bitmapQ_no_L2_orphans s" 1506 using a b c unfolding bitmapQ_no_L2_orphans_def bitmapQ_no_L1_orphans_def by auto 1507 1508 have bitmapQ: 1509 "valid_bitmapQ (ksReadyQueues_update f s) = valid_bitmapQ s" 1510 using a b c 1511 unfolding valid_bitmapQ_def 1512 by (simp add: orphans bitmapQ_def set_empty[symmetric] del: set_empty) 1513 1514 show ?thesis 1515 unfolding invs'_def valid_state'_def ct_not_inQ_def valid_irq_node'_def cur_tcb'_def 1516 Invariants_H.valid_queues_def valid_queues'_def valid_queues_no_bitmap_def 1517 ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def 1518 using a b c 1519 by (clarsimp simp: cur_tcb'_def orphans bitmapQ) 1520qed 1521 1522lemma tcbSchedDequeue_ksReadyQueues_eq: 1523 "\<lbrace>\<lambda>s. obj_at' (inQ d p) t s \<and> filter ((\<noteq>) t) (ksReadyQueues s (d, p)) = ts\<rbrace> 1524 tcbSchedDequeue t 1525 \<lbrace>\<lambda>rv s. ksReadyQueues s (d, p) = ts\<rbrace>" 1526 apply (simp add: tcbSchedDequeue_def threadGet_def liftM_def) 1527 apply (wp getObject_tcb_wp|clarsimp)+ 1528 apply (clarsimp simp: obj_at'_def projectKOs inQ_def split del: if_split) 1529 apply (simp add: eq_commute) 1530 apply (rule_tac x=obj in exI, clarsimp)+ 1531 done 1532 1533lemma hd_ksReadyQueues_runnable: 1534 "\<lbrakk>invs' s; ksReadyQueues s (d, p) = a # as\<rbrakk> 1535 \<Longrightarrow> st_tcb_at' runnable' a s" 1536 apply(simp add: invs'_def valid_state'_def, rule valid_queues_running, clarsimp) 1537 apply(rule suffix_Cons_mem) 1538 apply(simp add: suffix_def) 1539 apply(rule exI) 1540 apply(rule eq_Nil_appendI) 1541 by auto 1542 1543lemma chooseThread_invs_fragment: "\<lbrace>invs' and (\<lambda>s. ksCurDomain s = d)\<rbrace> 1544 do x \<leftarrow> getQueue d r; 1545 (case x of [] \<Rightarrow> return False 1546 | thread # x \<Rightarrow> do y \<leftarrow> ThreadDecls_H.switchToThread thread; return True od) 1547 od 1548 \<lbrace>\<lambda>_. invs'\<rbrace>" 1549 apply (rule seq_ext) 1550 apply (rule gq_sp) 1551 apply (case_tac x) 1552 apply (simp) 1553 apply (wp) 1554 apply (clarsimp) 1555 apply (simp) 1556 apply (wp) 1557 apply (clarsimp simp: invs'_def valid_state'_def , rule conjI) 1558 apply (rule valid_queues_running) 1559 apply (rule suffix_Cons_mem) 1560 apply (simp add: suffix_def) 1561 apply (rule exI) 1562 apply (rule eq_Nil_appendI) 1563 apply simp+ 1564 apply (clarsimp simp add: tcb_in_cur_domain'_def valid_queues_def valid_queues_no_bitmap_def) 1565 apply (drule_tac x="ksCurDomain s" in spec) 1566 apply (drule_tac x=r in spec) 1567 apply (fastforce simp: obj_at'_def inQ_def) 1568 done 1569 1570crunch ksCurDomain[wp]: "ThreadDecls_H.switchToThread" "\<lambda>s. P (ksCurDomain s)" 1571 1572lemma chooseThread_ksCurDomain_fragment: 1573 "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> 1574 do x \<leftarrow> getQueue d r; 1575 (case x of [] \<Rightarrow> return False 1576 | thread # x \<Rightarrow> do y \<leftarrow> ThreadDecls_H.switchToThread thread; return True od) 1577 od 1578 \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>" 1579 apply (wp | wpc | clarsimp)+ 1580 done 1581 1582(* FIXME move *) 1583lemma obj_tcb_at': 1584 "obj_at' (\<lambda>tcb::tcb. P tcb) t s \<Longrightarrow> tcb_at' t s" 1585 by (clarsimp simp: obj_at'_def) 1586 1587lemma valid_queues_queued_runnable: 1588 fixes s 1589 assumes vq: "Invariants_H.valid_queues s" 1590 and vq': "valid_queues' s" 1591 and oa: "obj_at' tcbQueued t s" 1592 shows "st_tcb_at' runnable' t s" 1593proof - 1594 from oa [THEN obj_tcb_at', THEN tcb_at'_has_tcbPriority] 1595 obtain p where tp: "obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s" 1596 by clarsimp 1597 1598 from oa [THEN obj_tcb_at', THEN tcb_at'_has_tcbDomain] 1599 obtain d where td: "obj_at' (\<lambda>tcb. tcbDomain tcb = d) t s" 1600 by clarsimp 1601 1602 with oa tp have "obj_at' (inQ d p) t s" 1603 by (fastforce simp add: inQ_def obj_at'_def) 1604 1605 with vq' have "t \<in> set (ksReadyQueues s (d, p))" 1606 unfolding valid_queues'_def 1607 by (fastforce) 1608 1609 with vq show ?thesis 1610 unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def 1611 apply - 1612 apply clarify 1613 apply (drule_tac x=d in spec) 1614 apply (drule_tac x=p in spec) 1615 apply (clarsimp simp: pred_tcb_at'_def) 1616 apply (drule(1) bspec) 1617 apply (erule obj_at'_weakenE) 1618 apply (simp) 1619 done 1620qed 1621 1622lemma tcb_at_typ_at': 1623 "tcb_at' p s = typ_at' TCBT p s" 1624 unfolding typ_at'_def 1625 apply rule 1626 apply (clarsimp simp add: obj_at'_def ko_wp_at'_def projectKOs) 1627 apply (clarsimp simp add: obj_at'_def ko_wp_at'_def projectKOs) 1628 apply (case_tac ko, simp_all) 1629 done 1630 1631 1632lemma invs'_not_runnable_not_queued: 1633 fixes s 1634 assumes inv: "invs' s" 1635 and st: "st_tcb_at' (Not \<circ> runnable') t s" 1636 shows "obj_at' (Not \<circ> tcbQueued) t s" 1637 apply (insert assms) 1638 apply (rule valid_queues_not_runnable_not_queued) 1639 apply (clarsimp simp add: invs'_def valid_state'_def)+ 1640 done 1641 1642lemma valid_queues_not_tcbQueued_not_ksQ: 1643 fixes s 1644 assumes vq: "Invariants_H.valid_queues s" 1645 and notq: "obj_at' (Not \<circ> tcbQueued) t s" 1646 shows "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))" 1647proof (rule ccontr, simp , erule exE, erule exE) 1648 fix d p 1649 assume "t \<in> set (ksReadyQueues s (d, p))" 1650 with vq have "obj_at' (inQ d p) t s" 1651 unfolding Invariants_H.valid_queues_def valid_queues_no_bitmap_def 1652 apply clarify 1653 apply (drule_tac x=d in spec) 1654 apply (drule_tac x=p in spec) 1655 apply (clarsimp) 1656 apply (drule(1) bspec) 1657 apply (erule obj_at'_weakenE) 1658 apply (simp) 1659 done 1660 hence "obj_at' tcbQueued t s" 1661 apply (rule obj_at'_weakenE) 1662 apply (simp only: inQ_def) 1663 done 1664 with notq show "False" 1665 by (clarsimp simp: obj_at'_def) 1666qed 1667 1668lemma not_tcbQueued_not_ksQ: 1669 fixes s 1670 assumes "invs' s" 1671 and "obj_at' (Not \<circ> tcbQueued) t s" 1672 shows "\<forall>d p. t \<notin> set (ksReadyQueues s (d, p))" 1673 apply (insert assms) 1674 apply (clarsimp simp add: invs'_def valid_state'_def) 1675 apply (drule(1) valid_queues_not_tcbQueued_not_ksQ) 1676 apply (clarsimp) 1677 done 1678 1679lemma ct_not_ksQ: 1680 "\<lbrakk> invs' s; ksSchedulerAction s = ResumeCurrentThread \<rbrakk> 1681 \<Longrightarrow> \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)" 1682 apply (clarsimp simp: invs'_def valid_state'_def ct_not_inQ_def) 1683 apply (frule(1) valid_queues_not_tcbQueued_not_ksQ) 1684 apply (fastforce) 1685 done 1686 1687crunch nosch[wp]: getCurThread "\<lambda>s. P (ksSchedulerAction s)" 1688 1689lemma setThreadState_rct: 1690 "\<lbrace>\<lambda>s. (runnable' st \<or> ksCurThread s \<noteq> t) 1691 \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> 1692 setThreadState st t 1693 \<lbrace>\<lambda>_ s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>" 1694 apply (simp add: setThreadState_def) 1695 apply (rule hoare_pre_disj') 1696 apply (rule hoare_seq_ext [OF _ 1697 hoare_vcg_conj_lift 1698 [OF threadSet_tcbState_st_tcb_at' [where P=runnable'] 1699 threadSet_nosch]]) 1700 apply (rule hoare_seq_ext [OF _ 1701 hoare_vcg_conj_lift [OF isRunnable_const isRunnable_inv]]) 1702 apply (clarsimp simp: when_def) 1703 apply (case_tac x) 1704 apply (clarsimp, wp)[1] 1705 apply (clarsimp) 1706 apply (rule hoare_seq_ext [OF _ 1707 hoare_vcg_conj_lift 1708 [OF threadSet_ct threadSet_nosch]]) 1709 apply (rule hoare_seq_ext [OF _ isRunnable_inv]) 1710 apply (rule hoare_seq_ext [OF _ 1711 hoare_vcg_conj_lift 1712 [OF gct_wp gct_wp]]) 1713 apply (rename_tac ct) 1714 apply (case_tac "ct\<noteq>t") 1715 apply (clarsimp simp: when_def) 1716 apply (wp)[1] 1717 apply (clarsimp) 1718 done 1719 1720lemma switchToIdleThread_invs'[wp]: 1721 "\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>" 1722 apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def) 1723 apply (wp setCurThread_invs_idle_thread) 1724 apply clarsimp 1725 1726 done 1727 1728lemma bitmapQ_lookupBitmapPriority_simp: (* neater unfold, actual unfold is really ugly *) 1729 "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; 1730 valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk> \<Longrightarrow> 1731 bitmapQ d (lookupBitmapPriority d s) s = 1732 (ksReadyQueuesL1Bitmap s d !! word_log2 (ksReadyQueuesL1Bitmap s d) \<and> 1733 ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d))) !! 1734 word_log2 (ksReadyQueuesL2Bitmap s (d, invertL1Index (word_log2 (ksReadyQueuesL1Bitmap s d)))))" 1735 unfolding bitmapQ_def lookupBitmapPriority_def 1736 apply (drule word_log2_nth_same, clarsimp) 1737 apply (drule (1) bitmapQ_no_L1_orphansD, clarsimp) 1738 apply (drule word_log2_nth_same, clarsimp) 1739 apply (frule test_bit_size[where n="word_log2 (ksReadyQueuesL2Bitmap _ _)"]) 1740 apply (clarsimp simp: numPriorities_def wordBits_def word_size) 1741 apply (subst prioToL1Index_l1IndexToPrio_or_id) 1742 apply (simp add: wordRadix_def' unat_of_nat word_size) 1743 apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def') 1744 apply (subst prioToL1Index_l1IndexToPrio_or_id) 1745 apply (simp add: wordRadix_def' unat_of_nat word_size) 1746 apply (simp add: wordRadix_def' unat_of_nat word_size l2BitmapSize_def') 1747 apply (simp add: word_ao_dist) 1748 apply (subst less_mask_eq) 1749 apply (fastforce intro: word_of_nat_less simp: wordRadix_def' unat_of_nat word_size)+ 1750 done 1751 1752lemma bitmapQ_from_bitmap_lookup: 1753 "\<lbrakk> ksReadyQueuesL1Bitmap s d \<noteq> 0 ; 1754 valid_bitmapQ s ; bitmapQ_no_L1_orphans s 1755 \<rbrakk> 1756 \<Longrightarrow> bitmapQ d (lookupBitmapPriority d s) s" 1757 apply (simp add: bitmapQ_lookupBitmapPriority_simp) 1758 apply (drule word_log2_nth_same) 1759 apply (drule (1) bitmapQ_no_L1_orphansD) 1760 apply (fastforce dest!: word_log2_nth_same 1761 simp: word_ao_dist lookupBitmapPriority_def word_size numPriorities_def 1762 wordBits_def) 1763 done 1764 1765lemma lookupBitmapPriority_obj_at': 1766 "\<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; valid_queues_no_bitmap s; valid_bitmapQ s; 1767 bitmapQ_no_L1_orphans s\<rbrakk> 1768 \<Longrightarrow> obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) 1769 (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s" 1770 apply (drule (2) bitmapQ_from_bitmap_lookup) 1771 apply (simp add: valid_bitmapQ_bitmapQ_simp) 1772 apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)", simp) 1773 apply (clarsimp, rename_tac t ts) 1774 apply (drule cons_set_intro) 1775 apply (drule (2) valid_queues_no_bitmap_objD) 1776 done 1777 1778lemma bitmapL1_zero_ksReadyQueues: 1779 "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s \<rbrakk> 1780 \<Longrightarrow> (ksReadyQueuesL1Bitmap s d = 0) = (\<forall>p. ksReadyQueues s (d,p) = [])" 1781 apply (cases "ksReadyQueuesL1Bitmap s d = 0") 1782 apply (force simp add: bitmapQ_def valid_bitmapQ_def) 1783 apply (fastforce dest: bitmapQ_from_bitmap_lookup simp: valid_bitmapQ_bitmapQ_simp) 1784 done 1785 1786lemma prioToL1Index_le_mask: 1787 "\<lbrakk> prioToL1Index p = prioToL1Index p' ; p && mask wordRadix \<le> p' && mask wordRadix \<rbrakk> 1788 \<Longrightarrow> p \<le> p'" 1789 unfolding prioToL1Index_def 1790 apply (simp add: wordRadix_def word_le_nat_alt[symmetric]) 1791 apply (drule shiftr_eq_neg_mask_eq) 1792 apply (metis add.commute word_and_le2 word_plus_and_or_coroll2 word_plus_mono_left) 1793 done 1794 1795lemma prioToL1Index_le_index: 1796 "\<lbrakk> prioToL1Index p \<le> prioToL1Index p' ; prioToL1Index p \<noteq> prioToL1Index p' \<rbrakk> 1797 \<Longrightarrow> p \<le> p'" 1798 unfolding prioToL1Index_def 1799 apply (simp add: wordRadix_def word_le_nat_alt[symmetric]) 1800 apply (erule (1) le_shiftr') 1801 done 1802 1803lemma bitmapL1_highest_lookup: 1804 "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; 1805 bitmapQ d p' s \<rbrakk> 1806 \<Longrightarrow> p' \<le> lookupBitmapPriority d s" 1807 apply (subgoal_tac "ksReadyQueuesL1Bitmap s d \<noteq> 0") 1808 prefer 2 1809 apply (clarsimp simp add: bitmapQ_def) 1810 apply (case_tac "prioToL1Index (lookupBitmapPriority d s) = prioToL1Index p'") 1811 apply (rule prioToL1Index_le_mask, simp) 1812 apply (frule (2) bitmapQ_from_bitmap_lookup) 1813 apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp) 1814 apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def) 1815 apply (subst mask_or_not_mask[where n=wordRadix and x=p', symmetric]) 1816 apply (subst word_bw_comms(2)) (* || commute *) 1817 apply (simp add: word_ao_dist mask_AND_NOT_mask mask_twice) 1818 apply (subst less_mask_eq[where x="of_nat _"]) 1819 apply (subst word_less_nat_alt) 1820 apply (subst unat_of_nat_eq) 1821 apply (rule order_less_le_trans[OF word_log2_max]) 1822 apply (simp add: word_size) 1823 apply (rule order_less_le_trans[OF word_log2_max]) 1824 apply (simp add: word_size wordRadix_def') 1825 apply (subst word_le_nat_alt) 1826 apply (subst unat_of_nat_eq) 1827 apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) 1828 apply (rule word_log2_highest) 1829 apply (subst (asm) prioToL1Index_l1IndexToPrio_or_id) 1830 apply (subst unat_of_nat_eq) 1831 apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) 1832 apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def') 1833 apply (simp add: word_size wordRadix_def') 1834 apply (drule (1) bitmapQ_no_L1_orphansD[where d=d and i="word_log2 _"]) 1835 apply (simp add: l2BitmapSize_def') 1836 apply simp 1837 apply (rule prioToL1Index_le_index[rotated], simp) 1838 apply (frule (2) bitmapQ_from_bitmap_lookup) 1839 apply (clarsimp simp: bitmapQ_lookupBitmapPriority_simp) 1840 apply (clarsimp simp: bitmapQ_def lookupBitmapPriority_def) 1841 apply (subst prioToL1Index_l1IndexToPrio_or_id) 1842 apply (subst unat_of_nat_eq) 1843 apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size) 1844 apply (rule order_less_le_trans[OF word_log2_max], simp add: word_size wordRadix_def') 1845 apply (fastforce dest: bitmapQ_no_L1_orphansD 1846 simp: wordBits_def numPriorities_def word_size wordRadix_def' l2BitmapSize_def') 1847 apply (erule word_log2_highest) 1848 done 1849 1850lemma bitmapQ_ksReadyQueuesI: 1851 "\<lbrakk> bitmapQ d p s ; valid_bitmapQ s \<rbrakk> \<Longrightarrow> ksReadyQueues s (d, p) \<noteq> []" 1852 unfolding valid_bitmapQ_def by simp 1853 1854lemma getReadyQueuesL2Bitmap_inv[wp]: 1855 "\<lbrace> P \<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>_. P\<rbrace>" 1856 unfolding getReadyQueuesL2Bitmap_def by wp 1857 1858lemma switchToThread_lookupBitmapPriority_wp: 1859 "\<lbrace>\<lambda>s. invs_no_cicd' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> 1860 t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) \<rbrace> 1861 ThreadDecls_H.switchToThread t 1862 \<lbrace>\<lambda>rv. invs'\<rbrace>" 1863proof - 1864 have switchToThread_pre: 1865 "\<And>s p t.\<lbrakk> valid_queues s ; bitmapQ (ksCurDomain s) p s ; t = hd (ksReadyQueues s (ksCurDomain s,p)) \<rbrakk> 1866 \<Longrightarrow> st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s" 1867 unfolding valid_queues_def 1868 apply (clarsimp dest!: bitmapQ_ksReadyQueuesI) 1869 apply (case_tac "ksReadyQueues s (ksCurDomain s, p)", simp) 1870 apply (rename_tac t ts) 1871 apply (drule_tac t=t and p=p and d="ksCurDomain s" in valid_queues_no_bitmap_objD) 1872 apply simp 1873 apply (fastforce elim: obj_at'_weaken simp: inQ_def tcb_in_cur_domain'_def st_tcb_at'_def) 1874 done 1875 thus ?thesis 1876 by (wp switchToThread_invs_no_cicd') (fastforce dest: invs_no_cicd'_queues) 1877qed 1878 1879lemma switchToIdleThread_invs_no_cicd': 1880 "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. invs'\<rbrace>" 1881 apply (clarsimp simp: Thread_H.switchToIdleThread_def X64_H.switchToIdleThread_def) 1882 apply (wp setCurThread_invs_no_cicd'_idle_thread storeWordUser_invs_no_cicd' 1883 setVMRoot_invs_no_cicd') 1884 apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_idle'_def) 1885 done 1886 1887crunch obj_at'[wp]: "Arch.switchToIdleThread" "\<lambda>s. obj_at' P t s" 1888 1889 1890lemma switchToIdleThread_activatable[wp]: 1891 "\<lbrace>invs'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" 1892 apply (simp add: Thread_H.switchToIdleThread_def 1893 X64_H.switchToIdleThread_def) 1894 apply (wp setCurThread_ct_in_state) 1895 apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def 1896 pred_tcb_at'_def obj_at'_def) 1897 done 1898 1899declare static_imp_conj_wp[wp_split del] 1900 1901lemma valid_queues_obj_at'_imp: 1902 "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); Invariants_H.valid_queues s; \<And>obj. runnable' obj \<Longrightarrow> P obj \<rbrakk> 1903 \<Longrightarrow> obj_at' (P \<circ> tcbState) t s" 1904 apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def o_def) 1905 apply(elim allE conjE) 1906 apply(rule obj_at'_weaken) 1907 apply(erule(1) ballE) 1908 apply(erule(1) notE) 1909 apply(clarsimp simp: obj_at'_def inQ_def) 1910done 1911 1912lemma setCurThread_const: 1913 "\<lbrace>\<lambda>_. P t \<rbrace> setCurThread t \<lbrace>\<lambda>_ s. P (ksCurThread s) \<rbrace>" 1914 by (simp add: setCurThread_def | wp)+ 1915 1916 1917 1918crunch it[wp]: switchToIdleThread "\<lambda>s. P (ksIdleThread s)" 1919crunch it[wp]: switchToThread "\<lambda>s. P (ksIdleThread s)" 1920 (ignore: ) 1921 1922lemma switchToIdleThread_curr_is_idle: 1923 "\<lbrace>\<top>\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s\<rbrace>" 1924 apply (rule hoare_weaken_pre) 1925 apply (wps switchToIdleThread_it) 1926 apply (simp add: Thread_H.switchToIdleThread_def) 1927 apply (wp setCurThread_const) 1928 apply (simp) 1929 done 1930 1931lemma chooseThread_it[wp]: 1932 "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>" 1933 by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+ 1934 1935lemma valid_queues_ct_update[simp]: 1936 "Invariants_H.valid_queues (s\<lparr>ksCurThread := t\<rparr>) = Invariants_H.valid_queues s" 1937 by (simp add: Invariants_H.valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def) 1938 1939lemma valid_queues'_ct_update[simp]: 1940 "valid_queues' (s\<lparr>ksCurThread := t\<rparr>) = valid_queues' s" 1941 by (simp add: valid_queues'_def) 1942 1943lemma valid_machine_state'_ct_update[simp]: 1944 "valid_machine_state' (s\<lparr>ksCurThread := t\<rparr>) = valid_machine_state' s" 1945 by (simp add: valid_machine_state'_def) 1946 1947lemma valid_irq_node'_ct_update[simp]: 1948 "valid_irq_node' w (s\<lparr>ksCurThread := t\<rparr>) = valid_irq_node' w s" 1949 by (simp add: valid_irq_node'_def) 1950 1951lemma switchToThread_ct_not_queued: 1952 "\<lbrace>invs' and tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>" 1953 (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 1954 apply (simp add: Thread_H.switchToThread_def) 1955 apply (wp) 1956 apply (simp add: switchToThread_def setCurThread_def) 1957 apply (wp tcbSchedDequeue_not_tcbQueued | simp )+ 1958 done 1959 1960lemma valid_irq_node'_ksCurThread: "valid_irq_node' w (s\<lparr>ksCurThread := t\<rparr>) = valid_irq_node' w s" 1961 unfolding valid_irq_node'_def 1962 by simp 1963 1964lemma threadGet_inv [wp]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>" 1965 apply (simp add: threadGet_def) 1966 apply (wp | simp)+ 1967 done 1968 1969lemma getThreadState_ct_in_state: 1970 "\<lbrace>\<lambda>s. t = ksCurThread s \<and> tcb_at' t s\<rbrace> getThreadState t \<lbrace>\<lambda>rv s. P rv \<longrightarrow> ct_in_state' P s\<rbrace>" 1971 apply (rule hoare_post_imp [where Q="\<lambda>rv s. t = ksCurThread s \<and> ((\<not> P rv) \<or> st_tcb_at' P t s)"]) 1972 apply (clarsimp simp add: ct_in_state'_def) 1973 apply (rule hoare_vcg_precond_imp) 1974 apply (wp hoare_vcg_disj_lift) 1975 apply (clarsimp simp add: pred_tcb_at'_def obj_at'_def) 1976 done 1977 1978lemma gsa_wf_invs: 1979 "\<lbrace>invs'\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. invs' and sch_act_wf sa\<rbrace>" 1980 by wp (clarsimp simp add: invs'_def valid_state'_def) 1981 1982(* Helper for schedule_corres *) 1983lemma gsa_wf_invs_and_P: 1984 "\<lbrace>invs' and P\<rbrace> getSchedulerAction \<lbrace>\<lambda>sa. invs' and P 1985 and (\<lambda>s. ksSchedulerAction s = sa) 1986 and sch_act_wf sa\<rbrace>" 1987 apply ( wp | simp ) 1988 by auto 1989 1990lemma gets_the_simp: 1991 "f s = Some y \<Longrightarrow> gets_the f s = ({(y, s)}, False)" 1992 by (simp add: gets_the_def gets_def assert_opt_def get_def bind_def return_def fail_def split: option.splits) 1993 1994lemma corres_split_sched_act: 1995 "\<lbrakk>sched_act_relation act act'; 1996 corres r P P' f1 g1; 1997 \<And>t. corres r (Q t) (Q' t) (f2 t) (g2 t); 1998 corres r R R' f3 g3\<rbrakk> 1999 \<Longrightarrow> corres r (case act of resume_cur_thread \<Rightarrow> P 2000 | switch_thread t \<Rightarrow> Q t 2001 | choose_new_thread \<Rightarrow> R) 2002 (case act' of ResumeCurrentThread \<Rightarrow> P' 2003 | SwitchToThread t \<Rightarrow> Q' t 2004 | ChooseThread \<Rightarrow> R') 2005 (case act of resume_cur_thread \<Rightarrow> f1 2006 | switch_thread t \<Rightarrow> f2 t 2007 | choose_new_thread \<Rightarrow> f3) 2008 (case act' of ResumeCurrentThread \<Rightarrow> g1 2009 | ChooseNewThread \<Rightarrow> g3 2010 | SwitchToThread t \<Rightarrow> g2 t)" 2011 apply (cases act) 2012 apply (rule corres_guard_imp, force+)+ 2013 done 2014 2015lemma get_sa_corres': 2016 "corres sched_act_relation P P' (gets scheduler_action) getSchedulerAction" 2017 by (clarsimp simp: getSchedulerAction_def state_relation_def) 2018 2019lemma corres_assert_ret: 2020 "corres dc (\<lambda>s. P) \<top> (assert P) (return ())" 2021 apply (rule corres_no_failI) 2022 apply simp 2023 apply (simp add: assert_def return_def fail_def) 2024 done 2025 2026lemma corres_assert_assume_l: 2027 "corres dc P Q (f ()) g 2028 \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g" 2029 by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) 2030 2031lemma corres_assert_assume_r: 2032 "corres dc P Q f (g ()) 2033 \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)" 2034 by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) 2035 2036lemma cur_tcb'_ksReadyQueuesL1Bitmap_upd[simp]: 2037 "cur_tcb' (s\<lparr>ksReadyQueuesL1Bitmap := x\<rparr>) = cur_tcb' s" 2038 unfolding cur_tcb'_def by simp 2039 2040lemma cur_tcb'_ksReadyQueuesL2Bitmap_upd[simp]: 2041 "cur_tcb' (s\<lparr>ksReadyQueuesL2Bitmap := x\<rparr>) = cur_tcb' s" 2042 unfolding cur_tcb'_def by simp 2043 2044crunch cur[wp]: tcbSchedEnqueue cur_tcb' 2045 (simp: unless_def) 2046 2047(* FIXME: move *) 2048lemma corres_noop3: 2049 assumes x: "\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 2050 assumes y: "\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> g \<lbrace>\<lambda>r. (=) s'\<rbrace>" 2051 assumes z: "nf' \<Longrightarrow> no_fail P' g" 2052 shows "corres_underlying sr nf nf' dc P P' f g" 2053 apply (clarsimp simp: corres_underlying_def) 2054 apply (rule conjI) 2055 apply clarsimp 2056 apply (rule use_exs_valid) 2057 apply (rule exs_hoare_post_imp) 2058 prefer 2 2059 apply (rule x) 2060 apply assumption+ 2061 apply simp_all 2062 apply (subgoal_tac "ba = b") 2063 apply simp 2064 apply (rule sym) 2065 apply (rule use_valid[OF _ y], assumption+) 2066 apply simp 2067 apply (insert z) 2068 apply (clarsimp simp: no_fail_def) 2069 done 2070 2071lemma corres_symb_exec_l': 2072 assumes z: "\<And>rv. corres_underlying sr nf nf' r (Q' rv) P' (x rv) y" 2073 assumes x: "\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 2074 assumes y: "\<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>" 2075 shows "corres_underlying sr nf nf' r (P and Q) P' (m >>= (\<lambda>rv. x rv)) y" 2076 apply (rule corres_guard_imp) 2077 apply (subst gets_bind_ign[symmetric], rule corres_split) 2078 apply (rule z) 2079 apply (rule corres_noop3) 2080 apply (erule x) 2081 apply (rule gets_wp) 2082 apply (rule non_fail_gets) 2083 apply (rule y) 2084 apply (rule gets_wp) 2085 apply simp+ 2086 done 2087 2088lemma corres_symb_exec_r': 2089 assumes z: "\<And>rv. corres_underlying sr nf nf' r P (P'' rv) x (y rv)" 2090 assumes y: "\<lbrace>P'\<rbrace> m \<lbrace>P''\<rbrace>" 2091 assumes x: "\<And>s. Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>" 2092 assumes nf: "nf' \<Longrightarrow> no_fail R' m" 2093 shows "corres_underlying sr nf nf' r P (P' and Q' and R') x (m >>= (\<lambda>rv. y rv))" 2094 apply (rule corres_guard_imp) 2095 apply (subst gets_bind_ign[symmetric], rule corres_split) 2096 apply (rule z) 2097 apply (rule_tac P'="a' and a''" for a' a'' in corres_noop3) 2098 apply (simp add: simpler_gets_def exs_valid_def) 2099 apply clarsimp 2100 apply (erule x) 2101 apply (rule no_fail_pre) 2102 apply (erule nf) 2103 apply clarsimp 2104 apply assumption 2105 apply (rule gets_wp) 2106 apply (rule y) 2107 apply simp+ 2108 done 2109 2110lemma corres_case_list: 2111 "\<lbrakk>list = list'; corres r P P' f1 g1; \<And>x xs. corres r (Q x xs) (Q' x xs) (f2 x xs) (g2 x xs)\<rbrakk> 2112 \<Longrightarrow> corres r (case list of [] \<Rightarrow> P | x # xs \<Rightarrow> Q x xs) 2113 (case list' of [] \<Rightarrow> P' | x # xs \<Rightarrow> Q' x xs) 2114 (case list of [] \<Rightarrow> f1 | x # xs \<Rightarrow> f2 x xs) 2115 (case list' of [] \<Rightarrow> g1 | x # xs \<Rightarrow> g2 x xs)" 2116 apply (cases list) 2117 apply (rule corres_guard_imp, force+)+ 2118 done 2119 2120lemma findM_corres: 2121 "\<lbrakk>\<And>x. x \<in> set xs \<Longrightarrow> corres (=) P P' (f x) (f' x); 2122 \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>r. P\<rbrace>; \<And>x. x \<in> set xs \<Longrightarrow> \<lbrace>P'\<rbrace> f' x \<lbrace>\<lambda>r. P'\<rbrace>\<rbrakk> 2123 \<Longrightarrow> corres (=) P P' (findM f xs) (findM f' xs)" 2124 apply (induct xs) 2125 apply simp 2126 apply simp 2127 apply (rule corres_guard_imp) 2128 apply (rule corres_split[where r'="(=)"]) 2129 apply (rule corres_if[where P=P and P'=P']) 2130 apply simp 2131 apply simp 2132 apply force 2133 apply force 2134 apply (atomize, (erule_tac x=a in allE)+, force)+ 2135 done 2136 2137lemma thread_get_exs_valid[wp]: 2138 "tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get f t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 2139 apply (clarsimp simp: get_thread_state_def assert_opt_def fail_def 2140 thread_get_def gets_the_def exs_valid_def gets_def 2141 get_def bind_def return_def split: option.splits) 2142 apply (erule get_tcb_at) 2143 done 2144 2145lemma gts_exs_valid[wp]: 2146 "tcb_at t s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_thread_state t \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 2147 apply (clarsimp simp: get_thread_state_def assert_opt_def fail_def 2148 thread_get_def gets_the_def exs_valid_def gets_def 2149 get_def bind_def return_def split: option.splits) 2150 apply (erule get_tcb_at) 2151 done 2152 2153lemma guarded_switch_to_corres: 2154 "corres dc (valid_arch_state and valid_objs and valid_asid_map 2155 and valid_vspace_objs and pspace_aligned and pspace_distinct 2156 and valid_vs_lookup and valid_global_objs 2157 and unique_table_refs o caps_of_state 2158 and st_tcb_at runnable t and valid_etcbs) 2159 (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues 2160 and st_tcb_at' runnable' t and cur_tcb') 2161 (guarded_switch_to t) (switchToThread t)" 2162 apply (simp add: guarded_switch_to_def) 2163 apply (rule corres_guard_imp) 2164 apply (rule corres_symb_exec_l'[OF _ gts_exs_valid]) 2165 apply (rule corres_assert_assume_l) 2166 apply (rule switch_thread_corres) 2167 apply (force simp: st_tcb_at_tcb_at) 2168 apply (wp gts_st_tcb_at) 2169 apply (force simp: st_tcb_at_tcb_at)+ 2170 done 2171 2172 lemma findM_gets_outside: 2173 assumes terminate_False: "(\<And>s s' x. (False,s') \<in> fst (g x s) \<Longrightarrow> s = s')" 2174 shows 2175 "findM (\<lambda>x. gets (\<lambda>ks. f ks x) >>= g) l = do f' \<leftarrow> gets (\<lambda>ks. f ks); findM (\<lambda>x. (g (f' x))) l od" 2176 apply (rule ext) 2177 apply (induct l) 2178 apply (clarsimp simp add: bind_def gets_def get_def return_def) 2179 apply simp 2180 apply (clarsimp simp add: bind_def gets_def get_def return_def cong: if_cong split: if_split_asm) 2181 apply safe 2182 apply (clarsimp split: if_split_asm) 2183 apply force 2184 apply (frule terminate_False) 2185 apply simp 2186 apply (rule_tac x="(False,ba)" in bexI,clarsimp+) 2187 apply (clarsimp split: if_split_asm)+ 2188 apply force 2189 apply (frule terminate_False) 2190 apply clarsimp 2191 apply (rule_tac x="(False,ba)" in bexI,clarsimp+) 2192 apply (clarsimp split: if_split_asm)+ 2193 apply (frule terminate_False) 2194 apply clarsimp 2195 apply force 2196 apply (clarsimp split: if_split_asm)+ 2197 apply (frule terminate_False) 2198 apply clarsimp 2199 apply (rule bexI [rotated], assumption) 2200 apply auto 2201 done 2202 2203lemma corres_gets_queues: 2204 "corres ready_queues_relation \<top> \<top> (gets ready_queues) (gets ksReadyQueues)" 2205 apply (simp add: state_relation_def) 2206 done 2207 2208lemma Max_lt_set: "\<forall>y\<in>A. Max B < (y::word8) \<Longrightarrow> \<forall>y\<in>A. y \<notin> B" 2209 apply clarsimp 2210 apply (drule_tac x=y in bspec,simp) 2211 apply (case_tac "B = {}") 2212 apply simp+ 2213 apply blast 2214 done 2215 2216abbreviation "enumPrio \<equiv> [0.e.maxPriority]" 2217 2218lemma enumPrio_word_div: 2219 fixes v :: "8 word" 2220 assumes vlt: "unat v \<le> unat maxPriority" 2221 shows "\<exists>xs ys. enumPrio = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y)" 2222 apply (subst upto_enum_word) 2223 apply (subst upt_add_eq_append'[where j="unat v"]) 2224 apply simp 2225 apply (rule le_SucI) 2226 apply (rule vlt) 2227 apply (simp only: upt_conv_Cons vlt[simplified less_Suc_eq_le[symmetric]]) 2228 apply (intro exI conjI) 2229 apply fastforce 2230 apply clarsimp 2231 apply (drule of_nat_mono_maybe[rotated, where 'a="8"]) 2232 apply (fastforce simp: vlt) 2233 apply simp 2234 apply (clarsimp simp: Suc_le_eq) 2235 apply (erule disjE) 2236 apply (drule of_nat_mono_maybe[rotated, where 'a="8"]) 2237 apply (simp add: maxPriority_def numPriorities_def) 2238 apply (clarsimp simp: unat_of_nat_eq) 2239 apply (erule conjE) 2240 apply (drule_tac y="unat v" and x="x" in of_nat_mono_maybe[rotated, where 'a="8"]) 2241 apply (simp add: maxPriority_def numPriorities_def)+ 2242 done 2243 2244lemma rev_enumPrio_word_div: 2245 "unat v \<le> unat maxPriority \<Longrightarrow> \<exists>xs ys. rev enumPrio = ys @ [(v::word8)] @ xs \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y)" 2246 apply (cut_tac v=v in enumPrio_word_div) 2247 apply clarsimp 2248 apply clarsimp 2249 apply (rule_tac x="rev xs" in exI) 2250 apply (rule_tac x="rev ys" in exI) 2251 apply simp 2252 done 2253 2254lemma findM_ignore_head: "\<forall>y\<in> set ys. f y = return False \<Longrightarrow> findM f (ys @ xs) = findM f xs" 2255 apply (induct ys,simp+) 2256 done 2257 2258lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)" 2259 by (simp add: curDomain_def state_relation_def) 2260 2261lemma valid_queues_non_empty: 2262 "\<And>s d p. \<lbrakk> valid_queues s; ksReadyQueues s (d, p) \<noteq> [] \<rbrakk> 2263 \<Longrightarrow> unat (Max {prio. ksReadyQueues s (d, prio) \<noteq> []}) \<le> unat maxPriority" 2264 apply (subst word_le_nat_alt[symmetric]) 2265 apply (subst Max_le_iff) 2266 apply simp 2267 apply blast 2268 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 2269 apply (drule spec) 2270 apply (drule_tac x="a" in spec) 2271 apply fastforce 2272 done 2273 2274lemma lookupBitmapPriority_Max_eqI: 2275 "\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk> 2276 \<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})" 2277 apply (rule Max_eqI[simplified eq_commute]; simp) 2278 apply (fastforce simp: bitmapL1_highest_lookup valid_bitmapQ_bitmapQ_simp) 2279 apply (metis valid_bitmapQ_bitmapQ_simp bitmapQ_from_bitmap_lookup) 2280 done 2281 2282lemma corres_gets_queues_getReadyQueuesL1Bitmap: 2283 "corres (\<lambda>qs l1. ((l1 = 0) = (\<forall>p. qs p = []))) \<top> valid_queues 2284 (gets (\<lambda>s. ready_queues s d)) (getReadyQueuesL1Bitmap d)" 2285 unfolding state_relation_def valid_queues_def getReadyQueuesL1Bitmap_def 2286 by (clarsimp simp: bitmapL1_zero_ksReadyQueues ready_queues_relation_def) 2287 2288lemma guarded_switch_to_chooseThread_fragment_corres: 2289 "corres dc 2290 (P and st_tcb_at runnable t and invs and valid_sched) 2291 (P' and st_tcb_at' runnable' t and invs_no_cicd') 2292 (guarded_switch_to t) 2293 (do runnable \<leftarrow> isRunnable t; 2294 y \<leftarrow> assert runnable; 2295 ThreadDecls_H.switchToThread t 2296 od)" 2297 unfolding guarded_switch_to_def isRunnable_def 2298 apply simp 2299 apply (rule corres_guard_imp) 2300 apply (rule corres_split[OF _ gts_corres]) 2301 apply (rule corres_assert_assume_l) 2302 apply (rule corres_assert_assume_r) 2303 apply (rule switch_thread_corres) 2304 apply (wp gts_st_tcb_at)+ 2305 apply (clarsimp simp: st_tcb_at_tcb_at invs_def valid_state_def valid_pspace_def valid_sched_def 2306 invs_valid_vs_lookup invs_unique_refs) 2307 apply (auto elim!: pred_tcb'_weakenE split: thread_state.splits 2308 simp: pred_tcb_at' runnable'_def all_invs_but_ct_idle_or_in_cur_domain'_def) 2309 done 2310 2311lemma bitmap_lookup_queue_is_max_non_empty: 2312 "\<lbrakk> valid_queues s'; (s, s') \<in> state_relation; invs s; 2313 ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<noteq> 0 \<rbrakk> 2314 \<Longrightarrow> ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s') = 2315 max_non_empty_queue (ready_queues s (cur_domain s))" 2316 unfolding all_invs_but_ct_idle_or_in_cur_domain'_def valid_queues_def 2317 by (clarsimp simp add: max_non_empty_queue_def lookupBitmapPriority_Max_eqI 2318 state_relation_def ready_queues_relation_def) 2319 2320lemma ksReadyQueuesL1Bitmap_return_wp: 2321 "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s d) s \<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>rv s. P rv s\<rbrace>" 2322 unfolding getReadyQueuesL1Bitmap_def 2323 by wp 2324 2325lemma ksReadyQueuesL2Bitmap_return_wp: 2326 "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s (d,i)) s \<rbrace> getReadyQueuesL2Bitmap d i \<lbrace>\<lambda>rv s. P rv s\<rbrace>" 2327 unfolding getReadyQueuesL2Bitmap_def 2328 by wp 2329 2330lemma ksReadyQueuesL1Bitmap_st_tcb_at': 2331 "\<lbrakk> ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0 ; valid_queues s \<rbrakk> 2332 \<Longrightarrow> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s" 2333 apply (drule bitmapQ_from_bitmap_lookup; clarsimp simp: valid_queues_def) 2334 apply (clarsimp simp add: valid_bitmapQ_bitmapQ_simp) 2335 apply (case_tac "ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)") 2336 apply simp 2337 apply (simp add: valid_queues_no_bitmap_def) 2338 apply (erule_tac x="ksCurDomain s" in allE) 2339 apply (erule_tac x="lookupBitmapPriority (ksCurDomain s) s" in allE) 2340 apply (clarsimp simp: st_tcb_at'_def) 2341 apply (erule obj_at'_weaken) 2342 apply simp 2343 done 2344 2345lemma chooseThread_corres: 2346 "corres dc (invs and valid_sched) (invs_no_cicd') 2347 choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") 2348proof - 2349 show ?thesis 2350 unfolding choose_thread_def chooseThread_def numDomains_def 2351 apply (simp only: numDomains_def return_bind Let_def) 2352 apply (simp cong: if_cong) (* clean up if 1 < numDomains *) 2353 apply (subst if_swap[where P="_ \<noteq> 0"]) (* put switchToIdleThread on first branch*) 2354 apply (rule corres_name_pre) 2355 apply (rule corres_guard_imp) 2356 apply (rule corres_split[OF _ curDomain_corres]) 2357 apply clarsimp 2358 apply (rule corres_split[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) 2359 apply (erule corres_if2[OF sym]) 2360 apply (rule switch_idle_thread_corres) 2361 apply (rule corres_symb_exec_r) 2362 apply (rule corres_symb_exec_r) 2363 apply (rule_tac 2364 P="\<lambda>s. ?PREI s \<and> queues = ready_queues s (cur_domain s) \<and> 2365 st_tcb_at runnable (hd (max_non_empty_queue queues)) s" and 2366 P'="\<lambda>s. (?PREH s \<and> st_tcb_at' runnable' (hd queue) s) \<and> 2367 l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> 2368 l1 \<noteq> 0 \<and> 2369 queue = ksReadyQueues s (ksCurDomain s, 2370 lookupBitmapPriority (ksCurDomain s) s)" and 2371 F="hd queue = hd (max_non_empty_queue queues)" in corres_req) 2372 apply (fastforce dest!: invs_no_cicd'_queues simp: bitmap_lookup_queue_is_max_non_empty) 2373 apply clarsimp 2374 apply (rule corres_guard_imp) 2375 apply (rule_tac P=\<top> and P'=\<top> in guarded_switch_to_chooseThread_fragment_corres) 2376 apply (wp ksReadyQueuesL2Bitmap_return_wp 2377 |clarsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ 2378 apply (clarsimp simp: if_apply_def2) 2379 apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) 2380 apply (simp add: curDomain_def, wp)+ 2381 apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) 2382 apply (erule_tac x="cur_domain sa" in allE) 2383 apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}" in allE) 2384 apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})") 2385 apply (clarsimp) 2386 apply (subgoal_tac 2387 "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []") 2388 apply (fastforce elim!: setcomp_Max_has_prop)+ 2389 apply (clarsimp dest!: invs_no_cicd'_queues) 2390 apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') 2391 done 2392qed 2393 2394lemma thread_get_comm: "do x \<leftarrow> thread_get f p; y \<leftarrow> gets g; k x y od = 2395 do y \<leftarrow> gets g; x \<leftarrow> thread_get f p; k x y od" 2396 apply (rule ext) 2397 apply (clarsimp simp add: gets_the_def assert_opt_def 2398 bind_def gets_def get_def return_def 2399 thread_get_def 2400 fail_def split: option.splits) 2401 done 2402 2403lemma schact_bind_inside: "do x \<leftarrow> f; (case act of resume_cur_thread \<Rightarrow> f1 x 2404 | switch_thread t \<Rightarrow> f2 t x 2405 | choose_new_thread \<Rightarrow> f3 x) od 2406 = (case act of resume_cur_thread \<Rightarrow> (do x \<leftarrow> f; f1 x od) 2407 | switch_thread t \<Rightarrow> (do x \<leftarrow> f; f2 t x od) 2408 | choose_new_thread \<Rightarrow> (do x \<leftarrow> f; f3 x od))" 2409 apply (case_tac act,simp_all) 2410 done 2411 2412interpretation tcb_sched_action_extended: is_extended' "tcb_sched_action f a" 2413 by (unfold_locales) 2414 2415lemma domain_time_corres: 2416 "corres (=) \<top> \<top> (gets domain_time) getDomainTime" 2417 by (simp add: getDomainTime_def state_relation_def) 2418 2419lemma next_domain_corres: 2420 "corres dc \<top> \<top> next_domain nextDomain" 2421 apply (simp add: next_domain_def nextDomain_def) 2422 apply (rule corres_modify) 2423 apply (simp add: state_relation_def Let_def dschLength_def dschDomain_def) 2424 done 2425 2426lemma valid_queues'_ksCurDomain[simp]: 2427 "valid_queues' (ksCurDomain_update f s) = valid_queues' s" 2428 by (simp add: valid_queues'_def) 2429 2430lemma valid_queues'_ksDomScheduleIdx[simp]: 2431 "valid_queues' (ksDomScheduleIdx_update f s) = valid_queues' s" 2432 by (simp add: valid_queues'_def) 2433 2434lemma valid_queues'_ksDomSchedule[simp]: 2435 "valid_queues' (ksDomSchedule_update f s) = valid_queues' s" 2436 by (simp add: valid_queues'_def) 2437 2438lemma valid_queues'_ksDomainTime[simp]: 2439 "valid_queues' (ksDomainTime_update f s) = valid_queues' s" 2440 by (simp add: valid_queues'_def) 2441 2442lemma valid_queues'_ksWorkUnitsCompleted[simp]: 2443 "valid_queues' (ksWorkUnitsCompleted_update f s) = valid_queues' s" 2444 by (simp add: valid_queues'_def) 2445 2446lemma valid_queues_ksCurDomain[simp]: 2447 "Invariants_H.valid_queues (ksCurDomain_update f s) = Invariants_H.valid_queues s" 2448 by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 2449 2450lemma valid_queues_ksDomScheduleIdx[simp]: 2451 "Invariants_H.valid_queues (ksDomScheduleIdx_update f s) = Invariants_H.valid_queues s" 2452 by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 2453 2454lemma valid_queues_ksDomSchedule[simp]: 2455 "Invariants_H.valid_queues (ksDomSchedule_update f s) = Invariants_H.valid_queues s" 2456 by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 2457 2458lemma valid_queues_ksDomainTime[simp]: 2459 "Invariants_H.valid_queues (ksDomainTime_update f s) = Invariants_H.valid_queues s" 2460 by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 2461 2462lemma valid_queues_ksWorkUnitsCompleted[simp]: 2463 "Invariants_H.valid_queues (ksWorkUnitsCompleted_update f s) = Invariants_H.valid_queues s" 2464 by (simp add: Invariants_H.valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 2465 2466lemma valid_irq_node'_ksCurDomain[simp]: 2467 "valid_irq_node' w (ksCurDomain_update f s) = valid_irq_node' w s" 2468 by (simp add: valid_irq_node'_def) 2469 2470lemma valid_irq_node'_ksDomScheduleIdx[simp]: 2471 "valid_irq_node' w (ksDomScheduleIdx_update f s) = valid_irq_node' w s" 2472 by (simp add: valid_irq_node'_def) 2473 2474lemma valid_irq_node'_ksDomSchedule[simp]: 2475 "valid_irq_node' w (ksDomSchedule_update f s) = valid_irq_node' w s" 2476 by (simp add: valid_irq_node'_def) 2477 2478lemma valid_irq_node'_ksDomainTime[simp]: 2479 "valid_irq_node' w (ksDomainTime_update f s) = valid_irq_node' w s" 2480 by (simp add: valid_irq_node'_def) 2481 2482lemma valid_irq_node'_ksWorkUnitsCompleted[simp]: 2483 "valid_irq_node' w (ksWorkUnitsCompleted_update f s) = valid_irq_node' w s" 2484 by (simp add: valid_irq_node'_def) 2485 2486lemma sch_act_wf_ksCurDomain [simp]: 2487 "sa = ChooseNewThread \<Longrightarrow> sch_act_wf sa (ksCurDomain_update f s) = sch_act_wf sa s" 2488 apply (cases sa) 2489 apply (simp_all add: ct_in_state'_def tcb_in_cur_domain'_def) 2490 done 2491 2492lemma next_domain_valid_sched[wp]: 2493 "\<lbrace> valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched \<rbrace>" 2494 apply (simp add: next_domain_def Let_def) 2495 apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) 2496 apply (simp add:valid_blocked_2_def) 2497 done 2498 2499lemma nextDomain_invs_no_cicd': 2500 "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)\<rbrace> nextDomain \<lbrace> \<lambda>_. invs_no_cicd' \<rbrace>" 2501 apply (simp add: nextDomain_def Let_def dschLength_def dschDomain_def) 2502 apply wp 2503 apply (clarsimp simp: invs'_def valid_state'_def valid_machine_state'_def 2504 ct_not_inQ_def cur_tcb'_def ct_idle_or_in_cur_domain'_def dschDomain_def 2505 all_invs_but_ct_idle_or_in_cur_domain'_def) 2506 done 2507 2508lemma bind_dummy_ret_val: 2509 "do y \<leftarrow> a; 2510 b 2511 od = do a; b od" 2512 by simp 2513 2514lemma schedule_ChooseNewThread_fragment_corres: 2515 "corres dc (invs and valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)) (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) 2516 (do _ \<leftarrow> when (domainTime = 0) next_domain; 2517 choose_thread 2518 od) 2519 (do _ \<leftarrow> when (domainTime = 0) nextDomain; 2520 chooseThread 2521 od)" 2522 apply (subst bind_dummy_ret_val) 2523 apply (subst bind_dummy_ret_val) 2524 apply (rule corres_guard_imp) 2525 apply (rule corres_split[OF _ corres_when]) 2526 apply simp 2527 apply (rule chooseThread_corres) 2528 apply simp 2529 apply (rule next_domain_corres) 2530 apply (wp nextDomain_invs_no_cicd')+ 2531 apply (clarsimp simp: valid_sched_def invs'_def valid_state'_def all_invs_but_ct_idle_or_in_cur_domain'_def)+ 2532 done 2533 2534lemma schedule_switch_thread_fastfail_corres: 2535 "\<lbrakk> ct \<noteq> it \<longrightarrow> (tp = tp' \<and> cp = cp') ; ct = ct' ; it = it' \<rbrakk> \<Longrightarrow> 2536 corres ((=)) (is_etcb_at ct) (tcb_at' ct) 2537 (schedule_switch_thread_fastfail ct it cp tp) 2538 (scheduleSwitchThreadFastfail ct' it' cp' tp')" 2539 by (clarsimp simp: schedule_switch_thread_fastfail_def scheduleSwitchThreadFastfail_def) 2540 2541lemma gets_is_highest_prio_expand: 2542 "gets (is_highest_prio d p) \<equiv> do 2543 q \<leftarrow> gets (\<lambda>s. ready_queues s d); 2544 return ((\<forall>p. q p = []) \<or> Max {prio. q prio \<noteq> []} \<le> p) 2545 od" 2546 by (clarsimp simp: is_highest_prio_def gets_def) 2547 2548lemma isHighestPrio_corres: 2549 assumes "d' = d" 2550 assumes "p' = p" 2551 shows 2552 "corres ((=)) \<top> valid_queues 2553 (gets (is_highest_prio d p)) 2554 (isHighestPrio d' p')" 2555 using assms 2556 apply (clarsimp simp: gets_is_highest_prio_expand isHighestPrio_def) 2557 apply (subst getHighestPrio_def') 2558 apply (rule corres_guard_imp) 2559 apply (rule corres_split[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) 2560 apply (rule corres_if_r'[where P'="\<lambda>_. True",rotated]) 2561 apply (rule_tac corres_symb_exec_r) 2562 apply (rule_tac 2563 P="\<lambda>s. q = ready_queues s d 2564 " and 2565 P'="\<lambda>s. valid_queues s \<and> 2566 l1 = ksReadyQueuesL1Bitmap s d \<and> 2567 l1 \<noteq> 0 \<and> hprio = lookupBitmapPriority d s" and 2568 F="hprio = Max {prio. q prio \<noteq> []}" in corres_req) 2569 apply (elim conjE) 2570 apply (clarsimp simp: valid_queues_def) 2571 apply (subst lookupBitmapPriority_Max_eqI; blast?) 2572 apply (fastforce simp: ready_queues_relation_def dest!: state_relationD) 2573 apply fastforce 2574 apply (wpsimp simp: if_apply_def2 wp: hoare_drop_imps ksReadyQueuesL1Bitmap_return_wp)+ 2575 done 2576 2577crunch valid_idle_etcb[wp]: set_scheduler_action valid_idle_etcb 2578 2579crunch inv[wp]: isHighestPrio P 2580crunch inv[wp]: curDomain P 2581crunch inv[wp]: schedule_switch_thread_fastfail P 2582crunch inv[wp]: scheduleSwitchThreadFastfail P 2583 2584lemma setSchedulerAction_invs': (* not in wp set, clobbered by ssa_wp *) 2585 "\<lbrace>\<lambda>s. invs' s \<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>_. invs' \<rbrace>" 2586 by (wpsimp simp: invs'_def cur_tcb'_def valid_state'_def valid_irq_node'_def ct_not_inQ_def 2587 valid_queues_def valid_queues_no_bitmap_def valid_queues'_def 2588 ct_idle_or_in_cur_domain'_def) 2589 2590lemma thread_get_tcb_state_wp: 2591 "\<lbrace>\<lambda>s. st_tcb_at (\<lambda>t. P (f t) s) ptr s\<rbrace> thread_get (\<lambda>tcb. f (tcb_state tcb)) ptr \<lbrace>P\<rbrace>" 2592 unfolding ethread_get_def 2593 by (wp | clarsimp simp add: thread_get_def st_tcb_at_def get_tcb_def obj_at_def)+ 2594 2595lemma scheduleChooseNewThread_corres: 2596 "corres dc 2597 (\<lambda>s. invs s \<and> valid_sched s \<and> scheduler_action s = choose_new_thread) 2598 (\<lambda>s. invs' s \<and> ksSchedulerAction s = ChooseNewThread) 2599 schedule_choose_new_thread scheduleChooseNewThread" 2600 unfolding schedule_choose_new_thread_def scheduleChooseNewThread_def 2601 apply (rule corres_guard_imp) 2602 apply (rule corres_split[OF _ domain_time_corres], clarsimp) 2603 apply (rule corres_split[OF _ schedule_ChooseNewThread_fragment_corres, simplified bind_assoc]) 2604 apply (rule set_sa_corres) 2605 apply (wp | simp)+ 2606 apply (wp | simp add: getDomainTime_def)+ 2607 apply auto 2608 done 2609 2610crunch static_inv[wp]: guarded_switch_to "\<lambda>_. P" 2611 2612(* ethread_get_when only corresponds with a non-when version if its condition holds *) 2613lemma ethread_get_when_corres': 2614 assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')" 2615 shows "corres r (is_etcb_at t and K b) (tcb_at' t and K b) 2616 (ethread_get_when b f t) (threadGet f' t)" 2617 apply (clarsimp simp: ethread_get_when_def) 2618 apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x) 2619 done 2620 2621lemma ethread_get_when_corres: 2622 assumes x: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> r (f etcb) (f' tcb')" 2623 shows "corres (\<lambda>rv rv'. b \<longrightarrow> r rv rv') (is_etcb_at t) (tcb_at' t) 2624 (ethread_get_when b f t) (threadGet f' t)" 2625 apply (clarsimp simp: ethread_get_when_def) 2626 apply (rule conjI; clarsimp) 2627 apply (rule corres_guard_imp, rule ethreadget_corres; simp add: x) 2628 apply (clarsimp simp: threadGet_def) 2629 apply (rule corres_noop) 2630 apply wpsimp+ 2631 done 2632 2633lemma schedule_switch_thread_fastfail_wp: 2634 "\<lbrace> P (ct \<noteq> it \<longrightarrow> tp < cp) \<rbrace> schedule_switch_thread_fastfail ct it cp tp \<lbrace>\<lambda>rv. P rv\<rbrace>" 2635 unfolding schedule_switch_thread_fastfail_def 2636 by wpsimp auto 2637 2638lemma schedule_corres: 2639 "corres dc (invs and valid_sched and valid_list) invs' (Schedule_A.schedule) ThreadDecls_H.schedule" 2640 supply ethread_get_wp[wp del] 2641 supply ssa_wp[wp del] 2642 supply tcbSchedEnqueue_invs'[wp del] 2643 supply tcbSchedEnqueue_invs'_not_ResumeCurrentThread[wp del] 2644 supply setSchedulerAction_direct[wp] 2645 supply if_split[split del] 2646 2647 apply (clarsimp simp: Schedule_A.schedule_def Thread_H.schedule_def) 2648 apply (subst thread_get_test) 2649 apply (subst thread_get_comm) 2650 apply (subst schact_bind_inside) 2651 apply (rule corres_guard_imp) 2652 apply (rule corres_split[OF _ gct_corres[THEN corres_rel_imp[where r="\<lambda>x y. y = x"],simplified]]) 2653 apply (rule corres_split[OF _ get_sa_corres]) 2654 apply (rule corres_split_sched_act,assumption) 2655 apply (rule_tac P="tcb_at ct" in corres_symb_exec_l') 2656 apply (rule_tac corres_symb_exec_l) 2657 apply simp 2658 apply (rule corres_assert_ret) 2659 apply ((wpsimp wp: thread_get_wp' gets_exs_valid)+) 2660 prefer 2 2661 (* choose thread *) 2662 apply clarsimp 2663 apply (rule corres_split[OF _ thread_get_isRunnable_corres]) 2664 apply (rule corres_split[OF _ corres_when]) 2665 apply (rule scheduleChooseNewThread_corres, simp) 2666 apply (rule tcbSchedEnqueue_corres, simp) 2667 apply (wp thread_get_wp' tcbSchedEnqueue_invs' hoare_vcg_conj_lift hoare_drop_imps 2668 | clarsimp)+ 2669 (* switch to thread *) 2670 apply (rule corres_split[OF _ thread_get_isRunnable_corres], 2671 rename_tac was_running wasRunning) 2672 apply (rule corres_split[OF _ corres_when]) 2673 apply (rule corres_split[OF _ git_corres], rename_tac it it') 2674 apply (rule_tac F="was_running \<longrightarrow> ct \<noteq> it" in corres_gen_asm) 2675 apply (rule corres_split[OF _ ethreadget_corres[where r="(=)"]], 2676 rename_tac tp tp') 2677 apply (rule corres_split[OF _ ethread_get_when_corres[where r="(=)"]], 2678 rename_tac cp cp') 2679 apply (rule corres_split[OF _ schedule_switch_thread_fastfail_corres]) 2680 apply (rule corres_split[OF _ curDomain_corres]) 2681 apply (rule corres_split[OF _ isHighestPrio_corres]; simp only:) 2682 apply (rule corres_if, simp) 2683 apply (rule corres_split[OF _ tcbSchedEnqueue_corres]) 2684 apply (simp, fold dc_def) 2685 apply (rule corres_split[OF _ set_sa_corres]) 2686 apply (rule scheduleChooseNewThread_corres, simp) 2687 2688 apply (wp | simp)+ 2689 apply (simp add: valid_sched_def) 2690 apply wp 2691 apply (rule hoare_vcg_conj_lift) 2692 apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked') 2693 apply (wpsimp wp: setSchedulerAction_invs')+ 2694 apply (wp tcb_sched_action_enqueue_valid_blocked hoare_vcg_all_lift enqueue_thread_queued) 2695 apply (wp tcbSchedEnqueue_invs'_not_ResumeCurrentThread) 2696 2697 apply (rule corres_if, fastforce) 2698 2699 apply (rule corres_split[OF _ tcbSchedAppend_corres]) 2700 apply (simp, fold dc_def) 2701 apply (rule corres_split[OF _ set_sa_corres]) 2702 apply (rule scheduleChooseNewThread_corres, simp) 2703 2704 apply (wp | simp)+ 2705 apply (simp add: valid_sched_def) 2706 apply wp 2707 apply (rule hoare_vcg_conj_lift) 2708 apply (rule_tac t=t in set_scheduler_action_cnt_valid_blocked') 2709 apply (wpsimp wp: setSchedulerAction_invs')+ 2710 apply (wp tcb_sched_action_append_valid_blocked hoare_vcg_all_lift append_thread_queued) 2711 apply (wp tcbSchedAppend_invs'_not_ResumeCurrentThread) 2712 2713 apply (rule corres_split[OF _ guarded_switch_to_corres], simp) 2714 apply (rule set_sa_corres[simplified dc_def]) 2715 apply (wp | simp)+ 2716 2717 (* isHighestPrio *) 2718 apply (clarsimp simp: if_apply_def2) 2719 apply ((wp_once hoare_drop_imp)+)[1] 2720 2721 apply (simp add: if_apply_def2) 2722 apply ((wp_once hoare_drop_imp)+)[1] 2723 apply wpsimp+ 2724 apply (wpsimp simp: etcb_relation_def)+ 2725 apply (rule tcbSchedEnqueue_corres) 2726 apply wpsimp+ 2727 2728 apply (clarsimp simp: conj_ac cong: conj_cong) 2729 apply wp 2730 apply (rule_tac Q="\<lambda>_ s. valid_blocked_except t s \<and> scheduler_action s = switch_thread t" 2731 in hoare_post_imp, fastforce) 2732 apply (wp add: tcb_sched_action_enqueue_valid_blocked_except 2733 tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp 2734 del: gets_wp)+ 2735 apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) 2736 apply (wp gets_wp)+ 2737 2738 (* abstract final subgoal *) 2739 apply clarsimp 2740 2741 subgoal for s 2742 apply (clarsimp split: Deterministic_A.scheduler_action.splits 2743 simp: invs_psp_aligned invs_distinct invs_valid_objs invs_arch_state 2744 invs_vspace_objs[simplified] tcb_at_invs) 2745 apply (rule conjI, clarsimp) 2746 apply (fastforce simp: invs_def 2747 valid_sched_def valid_sched_action_def is_activatable_def 2748 st_tcb_at_def obj_at_def valid_state_def only_idle_def 2749 ) 2750 apply (rule conjI, clarsimp) 2751 subgoal for candidate 2752 apply (clarsimp simp: valid_sched_def invs_def valid_state_def cur_tcb_def 2753 valid_arch_caps_def valid_sched_action_def 2754 weak_valid_sched_action_def tcb_at_is_etcb_at 2755 tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]] 2756 valid_blocked_except_def valid_blocked_def) 2757 apply (clarsimp simp add: pred_tcb_at_def obj_at_def is_tcb valid_idle_def) 2758 done 2759 (* choose new thread case *) 2760 apply (intro impI conjI allI tcb_at_invs 2761 | fastforce simp: invs_def cur_tcb_def valid_etcbs_def 2762 valid_sched_def st_tcb_at_def obj_at_def valid_state_def 2763 weak_valid_sched_action_def not_cur_thread_def)+ 2764 apply (simp add: valid_sched_def valid_blocked_def valid_blocked_except_def) 2765 done 2766 2767 (* haskell final subgoal *) 2768 apply (clarsimp simp: if_apply_def2 invs'_def valid_state'_def 2769 cong: imp_cong split: scheduler_action.splits) 2770 apply (fastforce simp: cur_tcb'_def valid_pspace'_def) 2771 done 2772 2773lemma ssa_all_invs_but_ct_not_inQ': 2774 "\<lbrace>all_invs_but_ct_not_inQ' and sch_act_wf sa and 2775 (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> 2776 setSchedulerAction sa \<lbrace>\<lambda>rv. all_invs_but_ct_not_inQ'\<rbrace>" 2777proof - 2778 have obj_at'_sa: "\<And>P addr f s. 2779 obj_at' P addr (ksSchedulerAction_update f s) = obj_at' P addr s" 2780 by (fastforce intro: obj_at'_pspaceI) 2781 have valid_pspace'_sa: "\<And>f s. 2782 valid_pspace' (ksSchedulerAction_update f s) = valid_pspace' s" 2783 by (rule valid_pspace'_ksPSpace, simp) 2784 have iflive_sa: "\<And>f s. 2785 if_live_then_nonz_cap' (ksSchedulerAction_update f s) 2786 = if_live_then_nonz_cap' s" 2787 by (fastforce intro: if_live_then_nonz_cap'_pspaceI) 2788 have ifunsafe_sa[simp]: "\<And>f s. 2789 if_unsafe_then_cap' (ksSchedulerAction_update f s) = if_unsafe_then_cap' s" 2790 by fastforce 2791 have idle_sa[simp]: "\<And>f s. 2792 valid_idle' (ksSchedulerAction_update f s) = valid_idle' s" 2793 by fastforce 2794 show ?thesis 2795 apply (simp add: setSchedulerAction_def) 2796 apply wp 2797 apply (clarsimp simp add: invs'_def valid_state'_def cur_tcb'_def 2798 obj_at'_sa valid_pspace'_sa Invariants_H.valid_queues_def 2799 state_refs_of'_def iflive_sa ps_clear_def 2800 valid_irq_node'_def valid_queues'_def 2801 tcb_in_cur_domain'_def ct_idle_or_in_cur_domain'_def 2802 bitmapQ_defs valid_queues_no_bitmap_def 2803 cong: option.case_cong) 2804 done 2805qed 2806 2807lemma ssa_ct_not_inQ: 2808 "\<lbrace>\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> 2809 setSchedulerAction sa \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>" 2810 by (simp add: setSchedulerAction_def ct_not_inQ_def, wp, clarsimp) 2811 2812lemma ssa_all_invs_but_ct_not_inQ''[simplified]: 2813 "\<lbrace>\<lambda>s. (all_invs_but_ct_not_inQ' s \<and> sch_act_wf sa s) 2814 \<and> (sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) 2815 \<and> (sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace> 2816 setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace>" 2817 apply (simp only: all_invs_but_not_ct_inQ_check' [symmetric]) 2818 apply (rule hoare_elim_pred_conj) 2819 apply (wp hoare_vcg_conj_lift [OF ssa_all_invs_but_ct_not_inQ' ssa_ct_not_inQ]) 2820 apply (clarsimp) 2821 done 2822 2823lemma ssa_invs': 2824 "\<lbrace>invs' and sch_act_wf sa and 2825 (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) and 2826 (\<lambda>s. sa = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s)\<rbrace> 2827 setSchedulerAction sa \<lbrace>\<lambda>rv. invs'\<rbrace>" 2828 apply (wp ssa_all_invs_but_ct_not_inQ'') 2829 apply (clarsimp simp add: invs'_def valid_state'_def) 2830 done 2831 2832lemma getDomainTime_wp[wp]: "\<lbrace>\<lambda>s. P (ksDomainTime s) s \<rbrace> getDomainTime \<lbrace> P \<rbrace>" 2833 unfolding getDomainTime_def 2834 by wp 2835 2836lemma switchToThread_ct_not_queued_2: 2837 "\<lbrace>invs_no_cicd' and tcb_at' t\<rbrace> switchToThread t \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>" 2838 (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 2839 apply (simp add: Thread_H.switchToThread_def) 2840 apply (wp) 2841 apply (simp add: X64_H.switchToThread_def setCurThread_def) 2842 apply (wp tcbSchedDequeue_not_tcbQueued | simp )+ 2843 done 2844 2845lemma hd_ksReadyQueues_runnable_2: 2846 "\<lbrakk>Invariants_H.valid_queues s; ksReadyQueues s (d, p) = a # as\<rbrakk> 2847 \<Longrightarrow> st_tcb_at' runnable' a s" 2848 apply( rule valid_queues_running) 2849 apply(rule suffix_Cons_mem) 2850 apply(simp add: suffix_def) 2851 apply(rule exI) 2852 apply(rule eq_Nil_appendI) 2853 by auto 2854 2855lemma setCurThread_obj_at': 2856 "\<lbrace> obj_at' P t \<rbrace> setCurThread t \<lbrace>\<lambda>rv s. obj_at' P (ksCurThread s) s \<rbrace>" 2857proof - 2858 have obj_at'_ct: "\<And>P addr f s. 2859 obj_at' P addr (ksCurThread_update f s) = obj_at' P addr s" 2860 by (fastforce intro: obj_at'_pspaceI) 2861 show ?thesis 2862 apply (simp add: setCurThread_def) 2863 apply wp 2864 apply (simp add: ct_in_state'_def st_tcb_at'_def obj_at'_ct) 2865 done 2866qed 2867 2868lemma switchToIdleThread_ct_not_queued_no_cicd': 2869 "\<lbrace> invs_no_cicd' \<rbrace> switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<rbrace>" 2870 apply (simp add: Thread_H.switchToIdleThread_def) 2871 apply (wp setCurThread_obj_at') 2872 apply (rule idle'_not_tcbQueued') 2873 apply (simp add: invs_no_cicd'_def)+ 2874 done 2875 2876lemma switchToIdleThread_activatable_2[wp]: 2877 "\<lbrace>invs_no_cicd'\<rbrace> switchToIdleThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" 2878 apply (simp add: Thread_H.switchToIdleThread_def 2879 X64_H.switchToIdleThread_def) 2880 apply (wp setCurThread_ct_in_state) 2881 apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_idle'_def 2882 pred_tcb_at'_def obj_at'_def) 2883 done 2884 2885lemma switchToThread_tcb_in_cur_domain': 2886 "\<lbrace>tcb_in_cur_domain' thread\<rbrace> ThreadDecls_H.switchToThread thread 2887 \<lbrace>\<lambda>y s. tcb_in_cur_domain' (ksCurThread s) s\<rbrace>" 2888 apply (simp add: Thread_H.switchToThread_def) 2889 apply (rule hoare_pre) 2890 apply (wp) 2891 apply (simp add: X64_H.switchToThread_def setCurThread_def) 2892 apply (wp tcbSchedDequeue_not_tcbQueued | simp )+ 2893 apply (simp add:tcb_in_cur_domain'_def) 2894 apply (wp tcbSchedDequeue_tcbDomain | wps)+ 2895 apply (clarsimp simp:tcb_in_cur_domain'_def) 2896 done 2897 2898lemma chooseThread_invs_no_cicd'_posts: (* generic version *) 2899 "\<lbrace> invs_no_cicd' \<rbrace> chooseThread 2900 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> 2901 ct_in_state' activatable' s \<and> 2902 (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<rbrace>" 2903 (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 2904proof - 2905 note switchToThread_invs[wp del] 2906 note switchToThread_invs_no_cicd'[wp del] 2907 note switchToThread_lookupBitmapPriority_wp[wp] 2908 note assert_wp[wp del] 2909 2910 show ?thesis 2911 unfolding chooseThread_def Let_def numDomains_def curDomain_def 2912 apply (simp only: return_bind, simp) 2913 apply (rule hoare_seq_ext[where B="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"]) 2914 apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and> 2915 rv = ksReadyQueuesL1Bitmap s curdom" in hoare_seq_ext) 2916 apply (rename_tac l1) 2917 apply (case_tac "l1 = 0") 2918 (* switch to idle thread *) 2919 apply simp 2920 apply (rule hoare_pre) 2921 apply (wp_once switchToIdleThread_ct_not_queued_no_cicd') 2922 apply (wp_once) 2923 apply ((wp hoare_disjI1 switchToIdleThread_curr_is_idle)+)[1] 2924 apply simp 2925 (* we have a thread to switch to *) 2926 apply (clarsimp simp: bitmap_fun_defs) 2927 apply (wp assert_inv switchToThread_ct_not_queued_2 assert_inv hoare_disjI2 2928 switchToThread_tcb_in_cur_domain') 2929 apply clarsimp 2930 apply (clarsimp dest!: invs_no_cicd'_queues 2931 simp: valid_queues_def lookupBitmapPriority_def[symmetric]) 2932 apply (drule (3) lookupBitmapPriority_obj_at') 2933 apply normalise_obj_at' 2934 apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) 2935 apply (wp | simp add: bitmap_fun_defs curDomain_def)+ 2936 done 2937qed 2938 2939lemma chooseThread_activatable_2: 2940 "\<lbrace>invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" 2941 apply (rule hoare_pre, rule hoare_strengthen_post) 2942 apply (rule chooseThread_invs_no_cicd'_posts) 2943 apply simp+ 2944 done 2945 2946lemma chooseThread_activatable: 2947 "\<lbrace>invs'\<rbrace> chooseThread \<lbrace>\<lambda>rv. ct_in_state' activatable'\<rbrace>" 2948 apply (rule hoare_pre, rule chooseThread_activatable_2) 2949 apply (simp add: invs'_to_invs_no_cicd'_def) 2950 done 2951 2952lemma chooseThread_ct_not_queued_2: 2953 "\<lbrace> invs_no_cicd'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>" 2954 (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 2955 apply (rule hoare_pre, rule hoare_strengthen_post) 2956 apply (rule chooseThread_invs_no_cicd'_posts) 2957 apply simp+ 2958 done 2959 2960lemma chooseThread_invs_no_cicd': 2961 "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv. invs' \<rbrace>" 2962proof - 2963 note switchToThread_invs[wp del] 2964 note switchToThread_invs_no_cicd'[wp del] 2965 note switchToThread_lookupBitmapPriority_wp[wp] 2966 note assert_wp[wp del] 2967 2968 (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *) 2969 show ?thesis 2970 unfolding chooseThread_def Let_def numDomains_def curDomain_def 2971 apply (simp only: return_bind, simp) 2972 apply (rule hoare_seq_ext[where B="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"]) 2973 apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and> 2974 rv = ksReadyQueuesL1Bitmap s curdom" in hoare_seq_ext) 2975 apply (rename_tac l1) 2976 apply (case_tac "l1 = 0") 2977 (* switch to idle thread *) 2978 apply (simp, wp_once switchToIdleThread_invs_no_cicd', simp) 2979 (* we have a thread to switch to *) 2980 apply (clarsimp simp: bitmap_fun_defs) 2981 apply (wp assert_inv) 2982 apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) 2983 apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) 2984 apply (wp | simp add: bitmap_fun_defs curDomain_def)+ 2985 done 2986qed 2987 2988lemma chooseThread_in_cur_domain': 2989 "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s\<rbrace>" 2990 apply (rule hoare_pre, rule hoare_strengthen_post) 2991 apply (rule chooseThread_invs_no_cicd'_posts, simp_all) 2992 done 2993 2994lemma scheduleChooseNewThread_invs': 2995 "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace> 2996 scheduleChooseNewThread 2997 \<lbrace> \<lambda>_ s. invs' s \<rbrace>" 2998 unfolding scheduleChooseNewThread_def 2999 apply (wpsimp wp: ssa_invs' chooseThread_invs_no_cicd' chooseThread_ct_not_queued_2 3000 chooseThread_activatable_2 chooseThread_invs_no_cicd' 3001 chooseThread_in_cur_domain' nextDomain_invs_no_cicd' chooseThread_ct_not_queued_2) 3002 apply (clarsimp simp: invs'_to_invs_no_cicd'_def) 3003 done 3004 3005lemma schedule_invs': 3006 "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. invs'\<rbrace>" 3007 supply ssa_wp[wp del] 3008 apply (simp add: schedule_def) 3009 apply (rule_tac hoare_seq_ext, rename_tac t) 3010 apply (wp, wpc) 3011 \<comment> \<open>action = ResumeCurrentThread\<close> 3012 apply (wp)[1] 3013 \<comment> \<open>action = ChooseNewThread\<close> 3014 apply (wp scheduleChooseNewThread_invs') 3015 \<comment> \<open>action = SwitchToThread candidate\<close> 3016 apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' 3017 chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct 3018 switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 3019 | wp hoare_disjI2[where Q="\<lambda>_ s. tcb_in_cur_domain' (ksCurThread s) s"] 3020 | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] 3021 | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] 3022 | strengthen invs_invs_no_cicd' 3023 | wp hoare_vcg_imp_lift)+ 3024 apply (frule invs_sch_act_wf') 3025 apply (auto simp: invs_sch_act_wf' obj_at'_activatable_st_tcb_at' 3026 st_tcb_at'_runnable_is_activatable) 3027 done 3028 3029lemma setCurThread_nosch: 3030 "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> 3031 setCurThread t 3032 \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" 3033 apply (simp add: setCurThread_def) 3034 apply wp 3035 apply simp 3036 done 3037 3038lemma stt_nosch: 3039 "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> 3040 switchToThread t 3041 \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" 3042 apply (simp add: Thread_H.switchToThread_def X64_H.switchToThread_def storeWordUser_def) 3043 apply (wp setCurThread_nosch hoare_drop_imp |simp)+ 3044 done 3045 3046lemma stit_nosch[wp]: 3047 "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> 3048 switchToIdleThread 3049 \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" 3050 apply (simp add: Thread_H.switchToIdleThread_def 3051 X64_H.switchToIdleThread_def storeWordUser_def) 3052 apply (wp setCurThread_nosch | simp add: getIdleThread_def)+ 3053 done 3054 3055lemma chooseThread_nosch: 3056 "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> 3057 chooseThread 3058 \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" 3059 unfolding chooseThread_def Let_def numDomains_def curDomain_def 3060 apply (simp only: return_bind, simp) 3061 apply (wp findM_inv | simp)+ 3062 apply (case_tac queue) 3063 apply (wp stt_nosch | simp add: curDomain_def bitmap_fun_defs)+ 3064 done 3065 3066lemma schedule_sch: 3067 "\<lbrace>\<top>\<rbrace> schedule \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>" 3068 by (wp setSchedulerAction_direct | wpc| simp add: schedule_def scheduleChooseNewThread_def)+ 3069 3070lemma schedule_sch_act_simple: 3071 "\<lbrace>\<top>\<rbrace> schedule \<lbrace>\<lambda>rv. sch_act_simple\<rbrace>" 3072 apply (rule hoare_strengthen_post [OF schedule_sch]) 3073 apply (simp add: sch_act_simple_def) 3074 done 3075 3076lemma ssa_ct: 3077 "\<lbrace>ct_in_state' P\<rbrace> setSchedulerAction sa \<lbrace>\<lambda>rv. ct_in_state' P\<rbrace>" 3078proof - 3079 have obj_at'_sa: "\<And>P addr f s. 3080 obj_at' P addr (ksSchedulerAction_update f s) = obj_at' P addr s" 3081 by (fastforce intro: obj_at'_pspaceI) 3082 show ?thesis 3083 apply (unfold setSchedulerAction_def) 3084 apply wp 3085 apply (clarsimp simp add: ct_in_state'_def pred_tcb_at'_def obj_at'_sa) 3086 done 3087qed 3088 3089lemma scheduleChooseNewThread_ct_activatable'[wp]: 3090 "\<lbrace> invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread) \<rbrace> 3091 scheduleChooseNewThread 3092 \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" 3093 unfolding scheduleChooseNewThread_def 3094 by (wpsimp simp: ct_in_state'_def 3095 wp: ssa_invs' nextDomain_invs_no_cicd' 3096 chooseThread_activatable_2[simplified ct_in_state'_def] 3097 | (rule hoare_lift_Pf[where f=ksCurThread], solves wp) 3098 | strengthen invs_invs_no_cicd')+ 3099 3100lemma schedule_ct_activatable'[wp]: 3101 "\<lbrace>invs'\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>_. ct_in_state' activatable'\<rbrace>" 3102 supply ssa_wp[wp del] 3103 apply (simp add: schedule_def) 3104 apply (rule_tac hoare_seq_ext, rename_tac t) 3105 apply (wp, wpc) 3106 \<comment> \<open>action = ResumeCurrentThread\<close> 3107 apply (wp)[1] 3108 \<comment> \<open>action = ChooseNewThread\<close> 3109 apply wpsimp 3110 \<comment> \<open>action = SwitchToThread\<close> 3111 apply (wpsimp wp: ssa_invs' setSchedulerAction_direct ssa_ct 3112 | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] 3113 | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] 3114 | strengthen invs_invs_no_cicd' 3115 | wp hoare_vcg_imp_lift)+ 3116 apply (fastforce dest: invs_sch_act_wf' elim: pred_tcb'_weakenE 3117 simp: sch_act_wf obj_at'_activatable_st_tcb_at') 3118 done 3119 3120lemma threadSet_sch_act_sane: 3121 "\<lbrace>sch_act_sane\<rbrace> threadSet f t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" 3122 by (wp sch_act_sane_lift) 3123 3124lemma rescheduleRequired_sch_act_sane[wp]: 3125 "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>" 3126 apply (simp add: rescheduleRequired_def sch_act_sane_def 3127 setSchedulerAction_def) 3128 by (wp | wpc | clarsimp)+ 3129 3130lemma tcbSchedDequeue_sch_act_sane[wp]: 3131 "\<lbrace>sch_act_sane\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" 3132 by (wp sch_act_sane_lift) 3133 3134lemma sts_sch_act_sane: 3135 "\<lbrace>sch_act_sane\<rbrace> setThreadState st t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" 3136 apply (simp add: setThreadState_def) 3137 including no_pre 3138 apply (wp hoare_drop_imps 3139 | simp add: threadSet_sch_act_sane sane_update)+ 3140 done 3141 3142lemma sbn_sch_act_sane: 3143 "\<lbrace>sch_act_sane\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" 3144 apply (simp add: setBoundNotification_def) 3145 apply (wp | simp add: threadSet_sch_act_sane sane_update)+ 3146 done 3147 3148lemma possibleSwitchTo_corres: 3149 "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) 3150 (Invariants_H.valid_queues and valid_queues' and 3151 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs') 3152 (possible_switch_to t) 3153 (possibleSwitchTo t)" 3154 supply ethread_get_wp[wp del] 3155 apply (simp add: possible_switch_to_def possibleSwitchTo_def cong: if_cong) 3156 apply (rule corres_guard_imp) 3157 apply (rule corres_split[OF _ curDomain_corres], simp) 3158 apply (rule corres_split[OF _ ethreadget_corres[where r="(=)"]]) 3159 apply (rule corres_split[OF _ get_sa_corres]) 3160 apply (rule corres_if, simp) 3161 apply (rule tcbSchedEnqueue_corres) 3162 apply (rule corres_if, simp) 3163 apply (case_tac action; simp) 3164 apply (rule corres_split[OF _ rescheduleRequired_corres]) 3165 apply (rule tcbSchedEnqueue_corres) 3166 apply (wp rescheduleRequired_valid_queues'_weak)+ 3167 apply (rule set_sa_corres, simp) 3168 apply (wpsimp simp: etcb_relation_def if_apply_def2 3169 wp: hoare_drop_imp[where f="ethread_get a b" for a b])+ 3170 apply (wp hoare_drop_imps)[1] 3171 apply wp+ 3172 apply (fastforce simp: valid_sched_def invs_def valid_state_def cur_tcb_def 3173 valid_sched_action_def weak_valid_sched_action_def 3174 tcb_at_is_etcb_at[OF st_tcb_at_tcb_at[rotated]]) 3175 apply (simp add: tcb_at_is_etcb_at) 3176 done 3177 3178lemma possibleSwitchTo_corres_runnable_abs: 3179 "corres dc (valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t) 3180 (Invariants_H.valid_queues and valid_queues' and 3181 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and valid_objs') 3182 (possible_switch_to t) 3183 (possibleSwitchTo t)" 3184 apply (rule stronger_corres_guard_imp, rule possibleSwitchTo_corres) 3185 apply clarsimp 3186 apply (clarsimp simp: st_tcb_at_runnable_coerce_concrete) 3187 done 3188 3189end 3190end 3191