Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PIPBasics.thy
changeset 137 785c0f6b8184
parent 136 fb3f52fe99d1
child 138 20c1d3a14143
equal deleted inserted replaced
136:fb3f52fe99d1 137:785c0f6b8184 
   917 qed
 
   917 qed
 
   918 
   918 
   919 lemma dependants_alt_def_tG_ancestors:
 
   919 lemma dependants_alt_def_tG_ancestors:
 
   920   "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
 
   920   "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
 
   921   by (unfold dependants_alt_tG ancestors_def, simp)
 
   921   by (unfold dependants_alt_tG ancestors_def, simp)
 
       
   922 
       
   923 
   922 
   924 
   923 section {* Locales used to investigate the execution of PIP *}
 
   925 section {* Locales used to investigate the execution of PIP *}
 
   924 
   926 
   925 text {* 
   927 text {* 
   926   The following locale @{text valid_trace} is used to constrain the 
   928   The following locale @{text valid_trace} is used to constrain the 
  3457     from in_RAG_E[OF this] have "th1 \<notin> readys s" by (unfold readys_def, auto)
 
  3459     from in_RAG_E[OF this] have "th1 \<notin> readys s" by (unfold readys_def, auto)
 
  3458     with assms show ?thesis by simp
 
  3460     with assms show ?thesis by simp
 
  3459   qed
 
  3461   qed
 
  3460 qed
 
  3462 qed
 
  3461 
  3463 
       
  3464 lemma root_readys:
 
       
  3465   assumes "th \<in> readys s"
 
       
  3466   shows "root (tRAG s) (Th th)"
 
       
  3467 proof -
 
       
  3468   { assume "\<not> root (tRAG s) (Th th)"
 
       
  3469     then obtain n' where "(Th th, n') \<in> (tRAG s)^+"
 
       
  3470       unfolding root_def ancestors_def by auto
 
       
  3471     then obtain cs where "(Th th, Cs cs) \<in> RAG s"
 
       
  3472       unfolding tRAG_alt_def using tranclD by fastforce 
       
  3473     then have "th \<notin> readys s" 
       
  3474       unfolding readys_def using in_RAG_E by blast 
       
  3475     with assms have False by simp
 
       
  3476   } then show "root (tRAG s) (Th th)" by auto
 
       
  3477 qed
 
       
  3478 
       
  3479 lemma root_readys_tG:
 
       
  3480   assumes "th \<in> readys s"
 
       
  3481   shows "root (tG s) th"
 
       
  3482 proof -
 
       
  3483   { assume "\<not> root (tG s) th"
 
       
  3484     then obtain th' where "(th, th') \<in> (tG s)^+"
 
       
  3485       unfolding root_def ancestors_def by auto
 
       
  3486     then have "(Th th, Th th') \<in> (tRAG s)^+" 
       
  3487       using trancl_tG_tRAG by simp
 
       
  3488     with root_readys assms 
       
  3489     have False 
       
  3490       unfolding root_def ancestors_def by auto
 
       
  3491   } then show "root (tG s) th" by auto
 
       
  3492 qed  
       
  3493 
  3462 lemma readys_indep:
 
  3494 lemma readys_indep:
 
  3463   assumes "th1 \<in> readys s"
 
  3495   assumes "th1 \<in> readys s"
 
  3464   and "th2 \<in> readys s"
 
  3496   and "th2 \<in> readys s"
 
  3465   and "th1 \<noteq> th2"
 
  3497   and "th1 \<noteq> th2"
 
  3466   shows "indep (tRAG s) (Th th1) (Th th2)"
 
  3498   shows "indep (tRAG s) (Th th1) (Th th2)"
 
  3507 
  3539 
  3508 text {*
 
  3540 text {*
 
  3509   The following two lemmas shows there is at most one running thread 
  3541   The following two lemmas shows there is at most one running thread 
  3510   in the system.
 
  3542   in the system.
 
  3511 *}
 
  3543 *}
 
       
  3544 
       
  3545 
  3512 lemma running_unique:
 
  3546 lemma running_unique:
 
  3513   assumes running_1: "th1 \<in> running s"
 
  3547   assumes running_1: "th1 \<in> running s"
 
  3514   and running_2: "th2 \<in> running s"
 
  3548   and running_2: "th2 \<in> running s"
 
  3515   shows "th1 = th2"
 
  3549   shows "th1 = th2"
 
  3516 proof -
 
  3550 proof -
 
  3517   -- {* According to lemma @{thm thread_chain}, 
  3551   -- {* 
  3518         each living threads is chained to a thread in its subtree, and this
 
  3552 
  3519         target thread holds the highest precedence of the subtree.
 
  3553   According to lemma @{thm thread_chain}, each live thread is chained to a
 
  3520 
  3554   thread in its subtree, who holds the highest precedence of the subtree.
 
  3521         The chains for @{term th1} and @{term th2} are established 
  3555 
  3522         first in the following in @{text "h1"} and @{text "h2"}:
 
  3556   The chains for @{term th1} and @{term th2} are established first in the
 
  3523      *}
 
  3557   following in @{text "chain1"} and @{text "chain2"}. These chains start
 
       
  3558   with the threads @{text "th1'"} and @{text "th2'"} respectively. *}
 
       
  3559   
  3524   have "th1 \<in> threads s" using assms
 
  3560   have "th1 \<in> threads s" using assms
 
  3525     by (unfold running_def readys_def, auto)
 
  3561     by (unfold running_def readys_def, auto)
 
  3526   from thread_chain[OF this]
 
  3562   with thread_chain
 
  3527   obtain th1' where 
  3563   obtain th1' where 
  3528       h1: "th1' \<in> subtree (tG s) th1" 
  3564       chain1: "th1' \<in> subtree (tG s) th1" 
  3529           "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
 
  3565           "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
 
  3530           "th1' \<in> threads s"
 
  3566           "th1' \<in> threads s"
 
  3531       by auto
 
  3567       by auto
 
  3532   have "th2 \<in> threads s" using assms
 
  3568   have "th2 \<in> threads s" using assms
 
  3533     by (unfold running_def readys_def, auto)
 
  3569     by (unfold running_def readys_def, auto)
 
  3534   from thread_chain[OF this]
 
  3570   with thread_chain
 
  3535   obtain th2' where 
  3571   obtain th2' where 
  3536       h2: "th2' \<in> subtree (tG s) th2" 
  3572       chain2: "th2' \<in> subtree (tG s) th2" 
  3537           "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
 
  3573           "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
 
  3538           "th2' \<in> threads s"
 
  3574           "th2' \<in> threads s"
 
  3539       by auto
 
  3575       by auto
 
  3540   -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
 
  3576   -- {* From these two chains we can be prove that the threads 
  3541         must be equal:
 
  3577         @{term th1} and @{term th2} must be equal. For this we first
 
       
  3578         show that the starting points of the chains are equal.
 
  3542      *}
 
  3579      *}
 
  3543   have eq_th': "th1' = th2'"
 
  3580   have eq_th': "th1' = th2'"
 
  3544   proof -
 
  3581   proof -
 
  3545     have "the_preced s th1' = the_preced s th2'" 
  3582     -- {* from @{text th1} and @{text th2} running, we know their 
  3546     proof -
 
  3583           cp-value is the same *}
 
  3547       from running_1 and running_2 have "cp s th1 = cp s th2"
 
  3584     from running_1 and running_2 have "cp s th1 = cp s th2"
 
  3548           unfolding running_def by auto
 
  3585       unfolding running_def by auto
 
  3549       from this[unfolded cp_alt_def2]
 
  3586     -- {* that means the preced of @{text th1'} and @{text th2'} 
  3550       have eq_max: "Max (the_preced s ` subtree (tG s) th1) = 
  3587           must be the same *}
 
  3551                     Max (the_preced s ` subtree (tG s) th2)" .
 
  3588     then 
  3552       with h1(2) h2(2)
 
  3589     have eq_max: "Max (the_preced s ` subtree (tG s) th1) = 
  3553       show ?thesis by metis
 
  3590                   Max (the_preced s ` subtree (tG s) th2)" 
  3554     qed
 
  3591       unfolding cp_alt_def2 .
 
  3555     from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
 
  3592     with chain1(2) chain2(2)
 
  3556     show ?thesis .
 
  3593     have "the_preced s th1' = the_preced s th2'" by simp
 
  3557   qed
 
  3594     -- {* since the precedences are the same, we can conclude
 
  3558   -- {* From this, it can be derived that the two sub-trees 
  3595           that  @{text th1'} and @{text th2'} are the same *}
 
  3559         rooted by @{term th1} and @{term th2} must overlap: *}
 
  3596     with preced_unique chain1(3) chain2(3)
 
  3560   have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2" 
  3597     show "th1' = th2'" unfolding the_preced_def by auto
 
  3561      using  eq_th' h1(1) h2(1) by auto
 
  3598   qed
 
  3562   -- {* However, this would be in contradiction with the fact
 
  3599   moreover
 
  3563         that two independent sub-trees can not overlap, 
  3600   have "root (tG s) th1" "root (tG s) th2" using assms
 
  3564         if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
 
  3601     using assms root_readys_tG
 
  3565         Therefore, @{term th1} and @{term th2} must be equal.
 
       
  3566      *}
 
       
  3567   { assume neq: "th1 \<noteq> th2"
 
       
  3568     -- {* According to @{thm readys_indep_tG}, two different threads 
       
  3569           in ready queue must be independent with each other: *}
 
       
  3570     have "indep (tG s) th1 th2"
 
       
  3571       by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
 
       
  3572     -- {* Therefore, according to lemma @{thm subtree_disjoint},
 
       
  3573           the two sub-trees rooted by them can not overlap: 
       
  3574     *}
 
       
  3575     from subtree_disjoint[OF this]
 
       
  3576     have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
 
       
  3577     -- {* In contradiction with @{thm overlapping}: *}
 
       
  3578     with overlapping have False by auto
 
       
  3579   } thus ?thesis by auto
 
       
  3580 qed
 
       
  3581 
       
  3582 text {*
 
       
  3583   The following two lemmas shows there is at most one running thread 
       
  3584   in the system.
 
       
  3585 *}
 
       
  3586 lemma running_unique_old:
 
       
  3587   assumes running_1: "th1 \<in> running s"
 
       
  3588   and running_2: "th2 \<in> running s"
 
       
  3589   shows "th1 = th2"
 
       
  3590 proof -
 
       
  3591   from running_1 and running_2 have "cp s th1 = cp s th2"
 
       
  3592     unfolding running_def by auto
 
  3602     unfolding running_def by auto
 
  3593   from this[unfolded cp_alt_def]
 
  3603   ultimately show "th1 = th2" using root_unique chain1(1) chain2(1)
 
  3594   have eq_max: 
  3604      by fastforce
 
  3595     "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
 
       
  3596      Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})" 
       
  3597         (is "Max ?L = Max ?R") .
 
       
  3598   have "Max ?L \<in> ?L"
 
       
  3599   proof(rule Max_in)
 
       
  3600     show "finite ?L" by (simp add: finite_subtree_threads) 
       
  3601   next
 
       
  3602     show "?L \<noteq> {}" using subtree_def by fastforce 
       
  3603   qed
 
       
  3604   then obtain th1' where 
       
  3605     h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
 
       
  3606     by auto
 
       
  3607   have "Max ?R \<in> ?R"
 
       
  3608   proof(rule Max_in)
 
       
  3609     show "finite ?R" by (simp add: finite_subtree_threads)
 
       
  3610   next
 
       
  3611     show "?R \<noteq> {}" using subtree_def by fastforce 
       
  3612   qed
 
       
  3613   then obtain th2' where 
       
  3614     h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
 
       
  3615     by auto
 
       
  3616   have "th1' = th2'"
 
       
  3617   proof(rule preced_unique)
 
       
  3618     from h_1(1)
 
       
  3619     show "th1' \<in> threads s"
 
       
  3620     proof(cases rule:subtreeE)
 
       
  3621       case 1
 
       
  3622       hence "th1' = th1" by simp
 
       
  3623       with running_1 show ?thesis by (auto simp:running_def readys_def)
 
       
  3624     next
 
       
  3625       case 2
 
       
  3626       from this(2)
 
       
  3627       have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 
       
  3628       from tranclD[OF this]
 
       
  3629       have "(Th th1') \<in> Domain (RAG s)" by auto
 
       
  3630       from dm_RAG_threads[OF this] show ?thesis .
 
       
  3631     qed
 
       
  3632   next
 
       
  3633     from h_2(1)
 
       
  3634     show "th2' \<in> threads s"
 
       
  3635     proof(cases rule:subtreeE)
 
       
  3636       case 1
 
       
  3637       hence "th2' = th2" by simp
 
       
  3638       with running_2 show ?thesis by (auto simp:running_def readys_def)
 
       
  3639     next
 
       
  3640       case 2
 
       
  3641       from this(2)
 
       
  3642       have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 
       
  3643       from tranclD[OF this]
 
       
  3644       have "(Th th2') \<in> Domain (RAG s)" by auto
 
       
  3645       from dm_RAG_threads[OF this] show ?thesis .
 
       
  3646     qed
 
       
  3647   next
 
       
  3648     have "the_preced s th1' = the_preced s th2'" 
       
  3649      using eq_max h_1(2) h_2(2) by metis
 
       
  3650     thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
 
       
  3651   qed
 
       
  3652   from h_1(1)[unfolded this]
 
       
  3653   have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
 
       
  3654   from h_2(1)[unfolded this]
 
       
  3655   have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
 
       
  3656   from star_rpath[OF star1] obtain xs1 
       
  3657     where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
 
       
  3658     by auto
 
       
  3659   from star_rpath[OF star2] obtain xs2 
       
  3660     where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
 
       
  3661     by auto
 
       
  3662   from rp1 rp2
 
       
  3663   show ?thesis
 
       
  3664   proof(cases)
 
       
  3665     case (less_1 xs')
 
       
  3666     moreover have "xs' = []"
 
       
  3667     proof(rule ccontr)
 
       
  3668       assume otherwise: "xs' \<noteq> []"
 
       
  3669       from rpath_plus[OF less_1(3) this]
 
       
  3670       have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
 
       
  3671       from tranclD[OF this]
 
       
  3672       obtain cs where "waiting s th1 cs"
 
       
  3673         by (unfold s_RAG_def, fold s_waiting_abv, auto)
 
       
  3674       with running_1 show False
 
       
  3675         by (unfold running_def readys_def, auto)
 
       
  3676     qed
 
       
  3677     ultimately have "xs2 = xs1" by simp
 
       
  3678     from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 
       
  3679     show ?thesis by simp
 
       
  3680   next
 
       
  3681     case (less_2 xs')
 
       
  3682     moreover have "xs' = []"
 
       
  3683     proof(rule ccontr)
 
       
  3684       assume otherwise: "xs' \<noteq> []"
 
       
  3685       from rpath_plus[OF less_2(3) this]
 
       
  3686       have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
 
       
  3687       from tranclD[OF this]
 
       
  3688       obtain cs where "waiting s th2 cs"
 
       
  3689         by (unfold s_RAG_def, fold s_waiting_abv, auto)
 
       
  3690       with running_2 show False
 
       
  3691         by (unfold running_def readys_def, auto)
 
       
  3692     qed
 
       
  3693     ultimately have "xs2 = xs1" by simp
 
       
  3694     from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 
       
  3695     show ?thesis by simp
 
       
  3696   qed
 
       
  3697 qed
 
  3605 qed
 
  3698 
  3606 
  3699 lemma card_running: 
  3607 lemma card_running: 
  3700   shows "card (running s) \<le> 1"
 
  3608   shows "card (running s) \<le> 1"
 
  3701 proof(cases "running s = {}")
 
  3609 proof(cases "running s = {}")
pip