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 ArchSchedule_AI 12imports "../Schedule_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems Schedule_AI_asms 18 19lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: 20 "valid invs (do_machine_op (mapM (\<lambda>p. storeWord p 0) S)) (\<lambda>_. invs)" 21 apply (simp add: dom_mapM ef_storeWord) 22 apply (rule mapM_UNIV_wp) 23 apply (simp add: do_machine_op_def split_def) 24 apply wp 25 apply (clarsimp simp: invs_def valid_state_def cur_tcb_def 26 valid_machine_state_def) 27 apply (rule conjI) 28 apply(erule use_valid[OF _ storeWord_valid_irq_states], simp) 29 apply (erule use_valid) 30 apply (simp add: storeWord_def word_rsplit_0) 31 apply wp 32 apply simp 33 done 34 35crunch device_state_inv[wp]: clearExMonitor "\<lambda>ms. P (device_state ms)" 36 37lemma clearExMonitor_invs [wp]: 38 "\<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace>" 39 apply (wp dmo_invs) 40 apply (clarsimp simp: clearExMonitor_def machine_op_lift_def 41 machine_rest_lift_def in_monad select_f_def) 42 done 43 44global_naming Arch 45 46lemma arch_stt_invs [wp,Schedule_AI_asms]: 47 "\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>" 48 apply (simp add: arch_switch_to_thread_def) 49 apply wp 50 done 51 52lemma arch_stt_tcb [wp,Schedule_AI_asms]: 53 "\<lbrace>tcb_at t'\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. tcb_at t'\<rbrace>" 54 apply (simp add: arch_switch_to_thread_def) 55 apply (wp) 56 done 57 58lemma arch_stt_runnable[Schedule_AI_asms]: 59 "\<lbrace>st_tcb_at runnable t\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>r . st_tcb_at runnable t\<rbrace>" 60 apply (simp add: arch_switch_to_thread_def) 61 apply wp 62 done 63 64lemma arch_stit_invs[wp, Schedule_AI_asms]: 65 "\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>" 66 by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def) 67 68lemma arch_stit_tcb_at[wp]: 69 "\<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace>" 70 apply (simp add: arch_switch_to_idle_thread_def ) 71 apply wp 72 done 73 74crunch st_tcb_at[wp]: set_vm_root "st_tcb_at P t" 75 (wp: crunch_wps simp: crunch_simps) 76 77crunch ct[wp]: set_vm_root "\<lambda>s. P (cur_thread s)" 78 (wp: crunch_wps simp: crunch_simps) 79 80lemma arch_stit_activatable[wp, Schedule_AI_asms]: 81 "\<lbrace>ct_in_state activatable\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>" 82 apply (clarsimp simp: arch_switch_to_idle_thread_def) 83 apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) 84 done 85 86lemma stit_invs [wp,Schedule_AI_asms]: 87 "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. invs\<rbrace>" 88 apply (simp add: switch_to_idle_thread_def) 89 apply (wp sct_invs) 90 by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def 91 pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def) 92 93lemma stit_activatable[Schedule_AI_asms]: 94 "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>" 95 apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def) 96 apply (wp | simp add: ct_in_state_def)+ 97 apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_idle_def 98 elim!: pred_tcb_weaken_strongerE) 99 done 100 101lemma stt_invs [wp,Schedule_AI_asms]: 102 "\<lbrace>invs\<rbrace> switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>" 103 apply (simp add: switch_to_thread_def) 104 apply wp 105 apply (simp add: trans_state_update[symmetric] del: trans_state_update) 106 apply (rule_tac Q="\<lambda>_. invs and tcb_at t'" in hoare_strengthen_post, wp) 107 apply (clarsimp simp: invs_def valid_state_def valid_idle_def 108 valid_irq_node_def valid_machine_state_def) 109 apply (fastforce simp: cur_tcb_def obj_at_def 110 elim: valid_pspace_eqI ifunsafe_pspaceI) 111 apply wp+ 112 apply clarsimp 113 apply (simp add: is_tcb_def) 114 done 115end 116 117interpretation Schedule_AI_U?: Schedule_AI_U 118 proof goal_cases 119 interpret Arch . 120 case 1 show ?case 121 by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) 122 qed 123 124interpretation Schedule_AI?: Schedule_AI 125 proof goal_cases 126 interpret Arch . 127 case 1 show ?case 128 by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?) 129 qed 130 131end 132