456 by (metis Max.coboundedI finite_imageI highest not_le order.trans |
454 by (metis Max.coboundedI finite_imageI highest not_le order.trans |
457 preced_linorder rev_image_eqI threads_s vat_s.finite_threads |
455 preced_linorder rev_image_eqI threads_s vat_s.finite_threads |
458 vat_s.le_cp) |
456 vat_s.le_cp) |
459 |
457 |
460 text {* |
458 text {* |
|
459 The following lemmas shows that the @{term cp}-value |
|
460 of the blocking thread @{text th'} equals to the highest |
|
461 precedence in the whole system. |
|
462 *} |
|
463 lemma runing_preced_inversion: |
|
464 assumes runing': "th' \<in> runing (t@s)" |
|
465 shows "cp (t@s) th' = preced th s" (is "?L = ?R") |
|
466 proof - |
|
467 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms |
|
468 by (unfold runing_def, auto) |
|
469 also have "\<dots> = ?R" |
|
470 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
|
471 finally show ?thesis . |
|
472 qed |
|
473 |
|
474 section {* The `blocking thread` *} |
|
475 |
|
476 text {* |
461 Counting of the number of @{term "P"} and @{term "V"} operations |
477 Counting of the number of @{term "P"} and @{term "V"} operations |
462 is the cornerstone of a large number of the following proofs. |
478 is the cornerstone of a large number of the following proofs. |
463 The reason is that this counting is quite easy to calculate and |
479 The reason is that this counting is quite easy to calculate and |
464 convenient to use in the reasoning. |
480 convenient to use in the reasoning. |
465 |
481 |
466 The following lemma shows that the counting controls whether |
482 The following lemma shows that the counting controls whether |
467 a thread is running or not. |
483 a thread is running or not. |
468 *} |
484 *} (* ccc *) |
469 |
485 |
470 lemma pv_blocked_pre: (* ddd *) |
486 lemma eq_pv_blocked: (* ddd *) |
471 assumes th'_in: "th' \<in> threads (t@s)" |
487 assumes neq_th': "th' \<noteq> th" |
472 and neq_th': "th' \<noteq> th" |
|
473 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
488 and eq_pv: "cntP (t@s) th' = cntV (t@s) th'" |
474 shows "th' \<notin> runing (t@s)" |
489 shows "th' \<notin> runing (t@s)" |
475 proof |
490 proof |
476 assume otherwise: "th' \<in> runing (t@s)" |
491 assume otherwise: "th' \<in> runing (t@s)" |
477 show False |
492 show False |
478 proof - |
493 proof - |
|
494 have th'_in: "th' \<in> threads (t@s)" |
|
495 using otherwise readys_threads runing_def by auto |
479 have "th' = th" |
496 have "th' = th" |
480 proof(rule preced_unique) |
497 proof(rule preced_unique) |
|
498 -- {* The proof goes like this: |
|
499 it is first shown that the @{term preced}-value of @{term th'} |
|
500 equals to that of @{term th}, then by uniqueness |
|
501 of @{term preced}-values (given by lemma @{thm preced_unique}), |
|
502 @{term th'} equals to @{term th}: *} |
481 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") |
503 show "preced th' (t @ s) = preced th (t @ s)" (is "?L = ?R") |
482 proof - |
504 proof - |
|
505 -- {* Since the counts of @{term th'} are balanced, the subtree |
|
506 of it contains only itself, so, its @{term cp}-value |
|
507 equals its @{term preced}-value: *} |
483 have "?L = cp (t@s) th'" |
508 have "?L = cp (t@s) th'" |
484 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
509 by (unfold cp_eq_cpreced cpreced_def count_eq_dependants[OF eq_pv], simp) |
485 also have "... = cp (t @ s) th" using otherwise |
510 -- {* Since @{term "th'"} is running by @{thm otherwise}, |
486 by (metis (mono_tags, lifting) mem_Collect_eq |
511 it has the highest @{term cp}-value, by definition, |
487 runing_def th_cp_max vat_t.max_cp_readys_threads) |
512 which in turn equals to the @{term cp}-value of @{term th}. *} |
488 also have "... = ?R" by (metis th_cp_preced th_kept) |
513 also have "... = ?R" |
|
514 using runing_preced_inversion[OF otherwise] th_kept by simp |
489 finally show ?thesis . |
515 finally show ?thesis . |
490 qed |
516 qed |
491 qed (auto simp: th'_in th_kept) |
517 qed (auto simp: th'_in th_kept) |
492 moreover have "th' \<noteq> th" using neq_th' . |
518 moreover have "th' \<noteq> th" using neq_th' . |
493 ultimately show ?thesis by simp |
519 ultimately show ?thesis by simp |
494 qed |
520 qed |
495 qed |
521 qed |
496 |
522 |
497 lemmas pv_blocked = pv_blocked_pre[folded detached_eq] |
523 text {* |
498 |
524 The following lemma is the extrapolation of @{thm eq_pv_blocked}. |
499 lemma runing_precond_pre: (* ddd *) |
525 It says if a thread, different from @{term th}, |
500 fixes th' |
526 does not hold any resource at the very beginning, |
501 assumes th'_in: "th' \<in> threads s" |
527 it will keep hand-emptied in the future @{term "t@s"}. |
|
528 *} |
|
529 lemma eq_pv_persist: (* ddd *) |
|
530 assumes neq_th': "th' \<noteq> th" |
502 and eq_pv: "cntP s th' = cntV s th'" |
531 and eq_pv: "cntP s th' = cntV s th'" |
503 and neq_th': "th' \<noteq> th" |
532 shows "cntP (t@s) th' = cntV (t@s) th'" |
504 shows "th' \<in> threads (t@s) \<and> |
533 proof(induction rule:ind) -- {* The proof goes by induction. *} |
505 cntP (t@s) th' = cntV (t@s) th'" |
534 -- {* The nontrivial case is for the @{term Cons}: *} |
506 proof(induct rule:ind) |
|
507 case (Cons e t) |
535 case (Cons e t) |
508 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
536 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
509 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
537 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
510 show ?case |
538 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
511 proof(cases e) |
539 show ?case |
512 case (P thread cs) |
540 proof - |
513 show ?thesis |
541 -- {* It can be proved that @{term cntP}-value of @{term th'} does not change |
514 proof - |
542 by the happening of event @{term e}: *} |
515 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
543 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
516 proof - |
544 proof(rule ccontr) -- {* Proof by contradiction. *} |
517 have "thread \<noteq> th'" |
545 -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} |
518 proof - |
546 assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'" |
519 have "step (t@s) (P thread cs)" using Cons P by auto |
547 -- {* Then the actor of @{term e} must be @{term th'} and @{term e} |
520 thus ?thesis |
548 must be a @{term P}-event: *} |
521 proof(cases) |
549 hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) |
522 assume "thread \<in> runing (t@s)" |
550 with vat_t.actor_inv[OF Cons(2)] |
523 moreover have "th' \<notin> runing (t@s)" using Cons(5) |
551 -- {* According to @{thm actor_inv}, @{term th'} must be running at |
524 by (metis neq_th' vat_t.pv_blocked_pre) |
552 the moment @{term "t@s"}: *} |
525 ultimately show ?thesis by auto |
553 have "th' \<in> runing (t@s)" by (cases e, auto) |
526 qed |
554 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
527 qed with Cons show ?thesis |
555 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
528 by (unfold P, simp add:cntP_def cntV_def count_def) |
556 moreover have "th' \<notin> runing (t@s)" |
529 qed |
557 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
530 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp) |
558 -- {* Contradiction is finally derived: *} |
531 ultimately show ?thesis by auto |
559 ultimately show False by simp |
532 qed |
|
533 next |
|
534 case (V thread cs) |
|
535 show ?thesis |
|
536 proof - |
|
537 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
|
538 proof - |
|
539 have "thread \<noteq> th'" |
|
540 proof - |
|
541 have "step (t@s) (V thread cs)" using Cons V by auto |
|
542 thus ?thesis |
|
543 proof(cases) |
|
544 assume "thread \<in> runing (t@s)" |
|
545 moreover have "th' \<notin> runing (t@s)" using Cons(5) |
|
546 by (metis neq_th' vat_t.pv_blocked_pre) |
|
547 ultimately show ?thesis by auto |
|
548 qed |
|
549 qed with Cons show ?thesis |
|
550 by (unfold V, simp add:cntP_def cntV_def count_def) |
|
551 qed |
|
552 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp) |
|
553 ultimately show ?thesis by auto |
|
554 qed |
|
555 next |
|
556 case (Create thread prio') |
|
557 show ?thesis |
|
558 proof - |
|
559 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
|
560 proof - |
|
561 have "thread \<noteq> th'" |
|
562 proof - |
|
563 have "step (t@s) (Create thread prio')" using Cons Create by auto |
|
564 thus ?thesis using Cons(5) by (cases, auto) |
|
565 qed with Cons show ?thesis |
|
566 by (unfold Create, simp add:cntP_def cntV_def count_def) |
|
567 qed |
|
568 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp) |
|
569 ultimately show ?thesis by auto |
|
570 qed |
|
571 next |
|
572 case (Exit thread) |
|
573 show ?thesis |
|
574 proof - |
|
575 have neq_thread: "thread \<noteq> th'" |
|
576 proof - |
|
577 have "step (t@s) (Exit thread)" using Cons Exit by auto |
|
578 thus ?thesis apply (cases) using Cons(5) |
|
579 by (metis neq_th' vat_t.pv_blocked_pre) |
|
580 qed |
|
581 hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons |
|
582 by (unfold Exit, simp add:cntP_def cntV_def count_def) |
|
583 moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread |
|
584 by (unfold Exit, simp) |
|
585 ultimately show ?thesis by auto |
|
586 qed |
|
587 next |
|
588 case (Set thread prio') |
|
589 with Cons |
|
590 show ?thesis |
|
591 by (auto simp:cntP_def cntV_def count_def) |
|
592 qed |
560 qed |
593 next |
561 -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change |
594 case Nil |
562 by the happening of event @{term e}: *} |
595 with assms |
563 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
596 show ?case by auto |
564 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
597 qed |
565 proof(rule ccontr) -- {* Proof by contradiction. *} |
598 |
566 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
599 text {* Changing counting balance to detachedness *} |
567 hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) |
600 lemmas runing_precond_pre_dtc = runing_precond_pre |
568 with vat_t.actor_inv[OF Cons(2)] |
601 [folded vat_t.detached_eq vat_s.detached_eq] |
569 have "th' \<in> runing (t@s)" by (cases e, auto) |
602 |
570 moreover have "th' \<notin> runing (t@s)" |
603 section {* The blocking thread *} |
571 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
|
572 ultimately show False by simp |
|
573 qed |
|
574 -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} |
|
575 value for @{term th'} are still in balance, so @{term th'} |
|
576 is still hand-emptied after the execution of event @{term e}: *} |
|
577 ultimately show ?thesis using Cons(5) by metis |
|
578 qed |
|
579 qed (auto simp:eq_pv) |
|
580 |
|
581 text {* |
|
582 By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, |
|
583 it can be derived easily that @{term th'} can not be running in the future: |
|
584 *} |
|
585 lemma eq_pv_blocked_persist: |
|
586 assumes neq_th': "th' \<noteq> th" |
|
587 and eq_pv: "cntP s th' = cntV s th'" |
|
588 shows "th' \<notin> runing (t@s)" |
|
589 using assms |
|
590 by (simp add: eq_pv_blocked eq_pv_persist) |
604 |
591 |
605 text {* |
592 text {* |
606 The purpose of PIP is to ensure that the most |
593 The purpose of PIP is to ensure that the most |
607 urgent thread @{term th} is not blocked unreasonably. |
594 urgent thread @{term th} is not blocked unreasonably. |
608 Therefore, a clear picture of the blocking thread is essential |
595 Therefore, a clear picture of the blocking thread is essential |
609 to assure people that the purpose is fulfilled. |
596 to assure people that the purpose is fulfilled. |
610 |
597 |
611 The following lemmas will give us such a picture: |
598 The following lemmas will give us such a picture: |
612 *} |
599 *} |
613 |
600 |
614 (* ccc *) |
|
615 |
|
616 text {* |
601 text {* |
617 The following lemma shows the blocking thread @{term th'} |
602 The following lemma shows the blocking thread @{term th'} |
618 must hold some resource in the very beginning. |
603 must hold some resource in the very beginning. |
619 *} |
604 *} |
620 lemma runing_cntP_cntV_inv: (* ddd *) |
605 lemma runing_cntP_cntV_inv: (* ddd *) |
621 assumes th'_in: "th' \<in> threads s" |
606 assumes is_runing: "th' \<in> runing (t@s)" |
622 and neq_th': "th' \<noteq> th" |
607 and neq_th': "th' \<noteq> th" |
623 and is_runing: "th' \<in> runing (t@s)" |
|
624 shows "cntP s th' > cntV s th'" |
608 shows "cntP s th' > cntV s th'" |
625 using assms |
609 using assms |
626 proof - |
610 proof - |
|
611 -- {* First, it can be shown that the number of @{term P} and |
|
612 @{term V} operations can not be equal for thred @{term th'} *} |
627 have "cntP s th' \<noteq> cntV s th'" |
613 have "cntP s th' \<noteq> cntV s th'" |
628 by (metis is_runing neq_th' pv_blocked_pre runing_precond_pre th'_in) |
614 proof |
|
615 -- {* The proof goes by contradiction, suppose otherwise: *} |
|
616 assume otherwise: "cntP s th' = cntV s th'" |
|
617 -- {* By applying @{thm eq_pv_blocked_persist} to this: *} |
|
618 from eq_pv_blocked_persist[OF neq_th' otherwise] |
|
619 -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} |
|
620 have "th' \<notin> runing (t@s)" . |
|
621 -- {* This is obvious in contradiction with assumption @{thm is_runing} *} |
|
622 thus False using is_runing by simp |
|
623 qed |
|
624 -- {* However, the number of @{term V} is always less or equal to @{term P}: *} |
629 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto |
625 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto |
|
626 -- {* Thesis is finally derived by combining the these two results: *} |
630 ultimately show ?thesis by auto |
627 ultimately show ?thesis by auto |
631 qed |
|
632 |
|
633 lemma moment_blocked_pre: |
|
634 assumes neq_th': "th' \<noteq> th" |
|
635 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
636 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
|
637 shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and> |
|
638 th' \<in> threads ((moment (i+j) t)@s)" |
|
639 proof - |
|
640 interpret h_i: red_extend_highest_gen _ _ _ _ _ i |
|
641 by (unfold_locales) |
|
642 interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" |
|
643 by (unfold_locales) |
|
644 interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" |
|
645 proof(unfold_locales) |
|
646 show "vt (moment i t @ s)" by (metis h_i.vt_t) |
|
647 next |
|
648 show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept) |
|
649 next |
|
650 show "preced th (moment i t @ s) = |
|
651 Max (cp (moment i t @ s) ` threads (moment i t @ s))" |
|
652 by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) |
|
653 next |
|
654 show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) |
|
655 next |
|
656 show "vt (moment j (restm i t) @ moment i t @ s)" |
|
657 using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) |
|
658 next |
|
659 fix th' prio' |
|
660 assume "Create th' prio' \<in> set (moment j (restm i t))" |
|
661 thus "prio' \<le> prio" using assms |
|
662 by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) |
|
663 next |
|
664 fix th' prio' |
|
665 assume "Set th' prio' \<in> set (moment j (restm i t))" |
|
666 thus "th' \<noteq> th \<and> prio' \<le> prio" |
|
667 by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) |
|
668 next |
|
669 fix th' |
|
670 assume "Exit th' \<in> set (moment j (restm i t))" |
|
671 thus "th' \<noteq> th" |
|
672 by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) |
|
673 qed |
|
674 show ?thesis |
|
675 by (metis add.commute append_assoc eq_pv h.runing_precond_pre |
|
676 moment_plus_split neq_th' th'_in) |
|
677 qed |
|
678 |
|
679 lemma moment_blocked_eqpv: (* ddd *) |
|
680 assumes neq_th': "th' \<noteq> th" |
|
681 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
682 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
|
683 and le_ij: "i \<le> j" |
|
684 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
|
685 th' \<in> threads ((moment j t)@s) \<and> |
|
686 th' \<notin> runing ((moment j t)@s)" |
|
687 proof - |
|
688 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
|
689 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
|
690 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
|
691 moreover have "th' \<notin> runing ((moment j t)@s)" |
|
692 proof - |
|
693 interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) |
|
694 show ?thesis |
|
695 using h.pv_blocked_pre h1 h2 neq_th' by auto |
|
696 qed |
|
697 ultimately show ?thesis by auto |
|
698 qed |
|
699 |
|
700 (* The foregoing two lemmas are preparation for this one, but |
|
701 in long run can be combined. Maybe I am wrong. |
|
702 This one is useless (* XY *) |
|
703 *) |
|
704 lemma moment_blocked: |
|
705 assumes neq_th': "th' \<noteq> th" |
|
706 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
707 and dtc: "detached (moment i t @ s) th'" |
|
708 and le_ij: "i \<le> j" |
|
709 shows "detached (moment j t @ s) th' \<and> |
|
710 th' \<in> threads ((moment j t)@s) \<and> |
|
711 th' \<notin> runing ((moment j t)@s)" |
|
712 proof - |
|
713 interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) |
|
714 interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) |
|
715 have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" |
|
716 by (metis dtc h_i.detached_elim) |
|
717 from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] |
|
718 show ?thesis by (metis h_j.detached_intro) |
|
719 qed |
|
720 |
|
721 |
|
722 text {* |
|
723 The following lemmas shows that the @{term cp}-value |
|
724 of the blocking thread @{text th'} equals to the highest |
|
725 precedence in the whole system. |
|
726 *} |
|
727 lemma runing_preced_inversion: |
|
728 assumes runing': "th' \<in> runing (t@s)" |
|
729 shows "cp (t@s) th' = preced th s" (is "?L = ?R") |
|
730 proof - |
|
731 have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms |
|
732 by (unfold runing_def, auto) |
|
733 also have "\<dots> = ?R" |
|
734 by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) |
|
735 finally show ?thesis . |
|
736 qed |
628 qed |
737 |
629 |
738 |
630 |
739 text {* |
631 text {* |
740 The following lemmas shows the blocking thread @{text th'} must be live |
632 The following lemmas shows the blocking thread @{text th'} must be live |
741 at the very beginning, i.e. the moment (or state) @{term s}. |
633 at the very beginning, i.e. the moment (or state) @{term s}. |
742 *} |
634 |
743 lemma runing_threads_inv: (* ddd *) |
635 The proof is a simple combination of the results above: |
|
636 *} |
|
637 lemma runing_threads_inv: |
744 assumes runing': "th' \<in> runing (t@s)" |
638 assumes runing': "th' \<in> runing (t@s)" |
745 and neq_th': "th' \<noteq> th" |
639 and neq_th': "th' \<noteq> th" |
746 shows "th' \<in> threads s" |
640 shows "th' \<in> threads s" |
747 proof - |
641 proof(rule ccontr) -- {* Proof by contradiction: *} |
748 -- {* The proof is by contradiction: *} |
642 assume otherwise: "th' \<notin> threads s" |
749 { assume otherwise: "\<not> ?thesis" |
643 have "th' \<notin> runing (t @ s)" |
750 have "th' \<notin> runing (t @ s)" |
644 proof - |
751 proof - |
645 from vat_s.cnp_cnv_eq[OF otherwise] |
752 -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} |
646 have "cntP s th' = cntV s th'" . |
753 have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def) |
647 from eq_pv_blocked_persist[OF neq_th' this] |
754 -- {* However, @{text "th'"} does not exist at very beginning. *} |
648 show ?thesis . |
755 have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise |
649 qed |
756 by (metis append.simps(1) moment_zero) |
650 with runing' show False by simp |
757 -- {* Therefore, there must be a moment during @{text "t"}, when |
|
758 @{text "th'"} came into being. *} |
|
759 -- {* Let us suppose the moment being @{text "i"}: *} |
|
760 from p_split_gen[OF th'_in th'_notin] |
|
761 obtain i where lt_its: "i < length t" |
|
762 and le_i: "0 \<le> i" |
|
763 and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre") |
|
764 and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto) |
|
765 interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) |
|
766 interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) |
|
767 from lt_its have "Suc i \<le> length t" by auto |
|
768 -- {* Let us also suppose the event which makes this change is @{text e}: *} |
|
769 from moment_head[OF this] obtain e where |
|
770 eq_me: "moment (Suc i) t = e # moment i t" by blast |
|
771 hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) |
|
772 hence "PIP (moment i t @ s) e" by (cases, simp) |
|
773 -- {* It can be derived that this event @{text "e"}, which |
|
774 gives birth to @{term "th'"} must be a @{term "Create"}: *} |
|
775 from create_pre[OF this, of th'] |
|
776 obtain prio where eq_e: "e = Create th' prio" |
|
777 by (metis append_Cons eq_me lessI post pre) |
|
778 have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto |
|
779 have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" |
|
780 proof - |
|
781 have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" |
|
782 by (metis h_i.cnp_cnv_eq pre) |
|
783 thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) |
|
784 qed |
|
785 show ?thesis |
|
786 using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge |
|
787 by auto |
|
788 qed |
|
789 with `th' \<in> runing (t@s)` |
|
790 have False by simp |
|
791 } thus ?thesis by auto |
|
792 qed |
651 qed |
793 |
652 |
794 text {* |
653 text {* |
795 The following lemma summarizes several foregoing |
654 The following lemma summarizes several foregoing |
796 lemmas to give an overall picture of the blocking thread @{text "th'"}: |
655 lemmas to give an overall picture of the blocking thread @{text "th'"}: |
797 *} |
656 *} |
798 lemma runing_inversion: |
657 lemma runing_inversion: (* ddd, one of the main lemmas to present *) |
799 assumes runing': "th' \<in> runing (t@s)" |
658 assumes runing': "th' \<in> runing (t@s)" |
800 and neq_th: "th' \<noteq> th" |
659 and neq_th: "th' \<noteq> th" |
801 shows "th' \<in> threads s" |
660 shows "th' \<in> threads s" |
802 and "\<not>detached s th'" |
661 and "\<not>detached s th'" |
803 and "cp (t@s) th' = preced th s" |
662 and "cp (t@s) th' = preced th s" |
804 proof - |
663 proof - |
805 from runing_threads_inv[OF assms] |
664 from runing_threads_inv[OF assms] |
806 show "th' \<in> threads s" . |
665 show "th' \<in> threads s" . |
807 next |
666 next |
808 from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing'] |
667 from runing_cntP_cntV_inv[OF runing' neq_th] |
809 show "\<not>detached s th'" using vat_s.detached_eq by simp |
668 show "\<not>detached s th'" using vat_s.detached_eq by simp |
810 next |
669 next |
811 from runing_preced_inversion[OF runing'] |
670 from runing_preced_inversion[OF runing'] |
812 show "cp (t@s) th' = preced th s" . |
671 show "cp (t@s) th' = preced th s" . |
813 qed |
672 qed |
|
673 |
|
674 section {* The existence of `blocking thread` *} |
814 |
675 |
815 text {* |
676 text {* |
816 Suppose @{term th} is not running, it is first shown that |
677 Suppose @{term th} is not running, it is first shown that |
817 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
678 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
818 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
679 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |