2996 using h_b(1)[unfolded trancl_converse] eq_b by auto |
3006 using h_b(1)[unfolded trancl_converse] eq_b by auto |
2997 ultimately show ?thesis using that by metis |
3007 ultimately show ?thesis using that by metis |
2998 qed |
3008 qed |
2999 |
3009 |
3000 text {* \noindent |
3010 text {* \noindent |
3001 The following lemma is proved easily by instantiating @{thm "chain_building"}. |
3011 The following lemma says for any living thread, |
|
3012 either it is ready or there is a path in @{term RAG} |
|
3013 leading from it to a ready thread. The lemma is proved easily |
|
3014 by instantiating @{thm "chain_building"}. |
3002 *} |
3015 *} |
3003 lemma th_chain_to_ready: |
3016 lemma th_chain_to_ready: |
3004 assumes th_in: "th \<in> threads s" |
3017 assumes th_in: "th \<in> threads s" |
3005 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)" |
3018 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)" |
3006 proof(cases "th \<in> readys s") |
3019 proof(cases "th \<in> readys s") |
3012 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
3025 by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def) |
3013 from chain_building [rule_format, OF this] |
3026 from chain_building [rule_format, OF this] |
3014 show ?thesis by auto |
3027 show ?thesis by auto |
3015 qed |
3028 qed |
3016 |
3029 |
|
3030 text {* |
|
3031 The following lemma is a technical one to show |
|
3032 that the set of threads in the subtree of any thread |
|
3033 is finite. |
|
3034 *} |
3017 lemma finite_subtree_threads: |
3035 lemma finite_subtree_threads: |
3018 "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A") |
3036 "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A") |
3019 proof - |
3037 proof - |
3020 have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
3038 have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}" |
3021 by (auto, insert image_iff, fastforce) |
3039 by (auto, insert image_iff, fastforce) |
3154 from runing_unique[OF this] |
3176 from runing_unique[OF this] |
3155 have "runing s = {th}" by auto |
3177 have "runing s = {th}" by auto |
3156 thus ?thesis by auto |
3178 thus ?thesis by auto |
3157 qed |
3179 qed |
3158 |
3180 |
3159 end |
3181 text {* |
3160 |
3182 The following two lemmas show that the set of living threads |
3161 |
3183 in the system can be partitioned into subtrees of those |
3162 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *} |
3184 threads in the @{term readys} set. The first lemma |
3163 |
3185 @{text threads_alt_def} shows the union of |
3164 context valid_trace |
3186 these subtrees equals to the set of living threads |
3165 begin |
3187 and the second lemma @{text "readys_subtree_disjoint"} shows |
3166 |
3188 subtrees of different threads in @{term readys}-set |
3167 lemma le_cp: |
3189 are disjoint. |
3168 shows "preced th s \<le> cp s th" |
3190 *} |
3169 proof(unfold cp_alt_def, rule Max_ge) |
|
3170 show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
3171 by (simp add: finite_subtree_threads) |
|
3172 next |
|
3173 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
3174 by (simp add: subtree_def the_preced_def) |
|
3175 qed |
|
3176 |
|
3177 lemma finite_threads: |
|
3178 shows "finite (threads s)" |
|
3179 using vt by (induct) (auto elim: step.cases) |
|
3180 |
|
3181 lemma cp_le: |
|
3182 assumes th_in: "th \<in> threads s" |
|
3183 shows "cp s th \<le> Max (the_preced s ` threads s)" |
|
3184 proof(unfold cp_alt_def, rule Max_f_mono) |
|
3185 show "finite (threads s)" by (simp add: finite_threads) |
|
3186 next |
|
3187 show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}" |
|
3188 using subtree_def by fastforce |
|
3189 next |
|
3190 show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s" |
|
3191 using assms |
|
3192 by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq |
|
3193 node.inject(1) rtranclD subsetI subtree_def trancl_domain) |
|
3194 qed |
|
3195 |
|
3196 lemma max_cp_eq: |
|
3197 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
|
3198 (is "?L = ?R") |
|
3199 proof - |
|
3200 have "?L \<le> ?R" |
|
3201 proof(cases "threads s = {}") |
|
3202 case False |
|
3203 show ?thesis |
|
3204 by (rule Max.boundedI, |
|
3205 insert cp_le, |
|
3206 auto simp:finite_threads False) |
|
3207 qed auto |
|
3208 moreover have "?R \<le> ?L" |
|
3209 by (rule Max_fg_mono, |
|
3210 simp add: finite_threads, |
|
3211 simp add: le_cp the_preced_def) |
|
3212 ultimately show ?thesis by auto |
|
3213 qed |
|
3214 |
3191 |
3215 lemma threads_alt_def: |
3192 lemma threads_alt_def: |
3216 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
3193 "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
3217 (is "?L = ?R") |
3194 (is "?L = ?R") |
3218 proof - |
3195 proof - |
3239 show ?thesis . |
3216 show ?thesis . |
3240 qed |
3217 qed |
3241 } ultimately show ?thesis by auto |
3218 } ultimately show ?thesis by auto |
3242 qed |
3219 qed |
3243 |
3220 |
|
3221 lemma readys_subtree_disjoint: |
|
3222 assumes "th1 \<in> readys s" |
|
3223 and "th2 \<in> readys s" |
|
3224 and "th1 \<noteq> th2" |
|
3225 shows "subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2) = {}" |
|
3226 proof - |
|
3227 { fix n |
|
3228 assume "n \<in> subtree (RAG s) (Th th1) \<inter> subtree (RAG s) (Th th2)" |
|
3229 hence "(n, Th th1) \<in> (RAG s)^*" "(n, Th th2) \<in> (RAG s)^*" |
|
3230 by (auto simp:subtree_def) |
|
3231 from star_rpath[OF this(1)] star_rpath[OF this(2)] |
|
3232 obtain xs1 xs2 where "rpath (RAG s) n xs1 (Th th1)" |
|
3233 "rpath (RAG s) n xs2 (Th th2)" by metis |
|
3234 hence False |
|
3235 proof(cases rule:rtree_RAG.rpath_overlap') |
|
3236 case (less_1 xs3) |
|
3237 from rpath_star[OF this(3)] |
|
3238 have "Th th1 \<in> subtree (RAG s) (Th th2)" |
|
3239 by (auto simp:subtree_def) |
|
3240 thus ?thesis |
|
3241 proof(cases rule:subtreeE) |
|
3242 case 1 |
|
3243 with assms(3) show ?thesis by auto |
|
3244 next |
|
3245 case 2 |
|
3246 hence "(Th th1, Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
3247 from tranclD[OF this] |
|
3248 obtain z where "(Th th1, z) \<in> RAG s" by auto |
|
3249 from this[unfolded s_RAG_def, folded wq_def] |
|
3250 obtain cs' where "waiting s th1 cs'" |
|
3251 by (auto simp:waiting_eq) |
|
3252 with assms(1) show False by (auto simp:readys_def) |
|
3253 qed |
|
3254 next |
|
3255 case (less_2 xs3) |
|
3256 from rpath_star[OF this(3)] |
|
3257 have "Th th2 \<in> subtree (RAG s) (Th th1)" |
|
3258 by (auto simp:subtree_def) |
|
3259 thus ?thesis |
|
3260 proof(cases rule:subtreeE) |
|
3261 case 1 |
|
3262 with assms(3) show ?thesis by auto |
|
3263 next |
|
3264 case 2 |
|
3265 hence "(Th th2, Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def) |
|
3266 from tranclD[OF this] |
|
3267 obtain z where "(Th th2, z) \<in> RAG s" by auto |
|
3268 from this[unfolded s_RAG_def, folded wq_def] |
|
3269 obtain cs' where "waiting s th2 cs'" |
|
3270 by (auto simp:waiting_eq) |
|
3271 with assms(2) show False by (auto simp:readys_def) |
|
3272 qed |
|
3273 qed |
|
3274 } thus ?thesis by auto |
|
3275 qed |
|
3276 |
|
3277 end |
|
3278 |
|
3279 (* ccc *) |
|
3280 section {* Relating @{term cp} and @{term the_preced} and @{term preced} *} |
|
3281 |
|
3282 context valid_trace |
|
3283 begin |
|
3284 |
|
3285 lemma finite_threads: |
|
3286 shows "finite (threads s)" |
|
3287 using vt by (induct) (auto elim: step.cases) |
|
3288 |
3244 lemma finite_readys: "finite (readys s)" |
3289 lemma finite_readys: "finite (readys s)" |
3245 using finite_threads readys_threads rev_finite_subset by blast |
3290 using finite_threads readys_threads rev_finite_subset by blast |
3246 |
3291 |
3247 text {* (* ccc *) \noindent |
3292 lemma le_cp: |
|
3293 shows "preced th s \<le> cp s th" |
|
3294 proof(unfold cp_alt_def, rule Max_ge) |
|
3295 show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
|
3296 by (simp add: finite_subtree_threads) |
|
3297 next |
|
3298 show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}" |
|
3299 by (simp add: subtree_def the_preced_def) |
|
3300 qed |
|
3301 |
|
3302 lemma cp_le: |
|
3303 assumes th_in: "th \<in> threads s" |
|
3304 shows "cp s th \<le> Max (the_preced s ` threads s)" |
|
3305 proof(unfold cp_alt_def, rule Max_f_mono) |
|
3306 show "finite (threads s)" by (simp add: finite_threads) |
|
3307 next |
|
3308 show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}" |
|
3309 using subtree_def by fastforce |
|
3310 next |
|
3311 show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s" |
|
3312 using assms |
|
3313 by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq |
|
3314 node.inject(1) rtranclD subsetI subtree_def trancl_domain) |
|
3315 qed |
|
3316 |
|
3317 lemma max_cp_eq: |
|
3318 shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)" |
|
3319 (is "?L = ?R") |
|
3320 proof - |
|
3321 have "?L \<le> ?R" |
|
3322 proof(cases "threads s = {}") |
|
3323 case False |
|
3324 show ?thesis |
|
3325 by (rule Max.boundedI, |
|
3326 insert cp_le, |
|
3327 auto simp:finite_threads False) |
|
3328 qed auto |
|
3329 moreover have "?R \<le> ?L" |
|
3330 by (rule Max_fg_mono, |
|
3331 simp add: finite_threads, |
|
3332 simp add: le_cp the_preced_def) |
|
3333 ultimately show ?thesis by auto |
|
3334 qed |
|
3335 |
|
3336 text {* (* ddd *) \noindent |
3248 Since the current precedence of the threads in ready queue will always be boosted, |
3337 Since the current precedence of the threads in ready queue will always be boosted, |
3249 there must be one inside it has the maximum precedence of the whole system. |
3338 there must be one inside it has the maximum precedence of the whole system. |
3250 *} |
3339 *} |
3251 lemma max_cp_readys_threads: |
3340 lemma max_cp_readys_threads: |
3252 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") |
3341 shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R") |