816 

   817 subsection {* Proof idea *}

   818 

   819 (*<*)

   820 context extend_highest_gen

   821 begin

   822 print_locale extend_highest_gen

   823 thm extend_highest_gen_def

   824 thm extend_highest_gen_axioms_def

   825 thm highest_gen_def

   826 (*>*)

   827 

   828 text {*

   829 The reason that only threads which already held some resoures

   830 can be runing and block @{text "th"} is that if , otherwise, one thread 

   831 does not hold any resource, it may never have its prioirty raised

   832 and will not get a chance to run. This fact is supported by 

   833 lemma @{text "moment_blocked"}:

   834 @{thm [display] moment_blocked}

   835 When instantiating  @{text "i"} to @{text "0"}, the lemma means threads which did not hold any

   836 resource in state @{text "s"} will not have a change to run latter. Rephrased, it means 

   837 any thread which is running after @{text "th"} became the highest must have already held

   838 some resource at state @{text "s"}.

   839 

   840 

   841   When instantiating @{text "i"} to a number larger than @{text "0"}, the lemma means 

   842   if a thread releases all its resources at some moment in @{text "t"}, after that, 

   843   it may never get a change to run. If every thread releases its resource in finite duration,

   844   then after a while, only thread @{text "th"} is left running. This shows how indefinite 

   845   priority inversion can be avoided. 

   846 

   847   So, the key of the proof is to establish the correctness of @{text "moment_blocked"}.

   848   We are going to show how this lemma is proved. At the heart of this proof, is 

   849   lemma @{text "pv_blocked"}:

   850   @{thm [display] pv_blocked}

   851   This lemma says: for any @{text "s"}-extension {text "t"}, if thread @{text "th'"}

   852   does not hold any resource, it can not be running at @{text "t@s"}.

   853 

   854 

   855   \noindent Proof: 

   856   \begin{enumerate}

   857   \item Since thread @{text "th'"} does not hold any resource, no thread may depend on it, 

   858     so its current precedence @{text "cp (t@s) th'"} equals to its own precedence

   859    @{text "preced th' (t@s)"}.  \label{arg_1}

   860   \item Since @{text "th"} has the highest precedence in the system and 

   861     precedences are distinct among threads, we have

   862     @{text "preced th' (t@s) < preced th (t@s)"}. From this and item \ref{arg_1}, 

   863     we have @{text "cp (t@s) th' < preced th (t@s)"}.

   864   \item Since @{text "preced th (t@s)"} is already the highest in the system, 

   865     @{text "cp (t@s) th"} can not be higher than this and can not be lower neither (by 

   866     the definition of @{text "cp"}), we have @{text "preced th (t@s) = cp (t@s) th"}.

   867   \item Finally we have @{text "cp (t@s) th' < cp (t@s) th"}.

   868   \item By defintion of @{text "running"}, @{text "th'"} can not be runing at 

   869     @{text "t@s"}.

   870   \end{enumerate}

   871   Since @{text "th'"} is not able to run at state @{text "t@s"}, it is not able to 

   872   make either {text "P"} or @{text "V"} action, so if @{text "t@s"} is extended

   873   one step further, @{text "th'"} still does not hold any resource. 

   874   The situation will not unchanged in further extensions as long as 

   875   @{text "th"} holds the highest precedence. Since this @{text "t"} is arbitarily chosen 

   876   except being constrained by predicate @{text "extend_highest_gen"} and 

   877   this predicate has the property that if it holds for @{text "t"}, it also holds

   878   for any moment @{text "i"} inside @{text "t"}, as shown by lemma @{text "red_moment"}:

   879 @{thm [display] "extend_highest_gen.red_moment"}

   880   so @{text "pv_blocked"} can be applied to any @{text "moment i t"}. 

   881   From this, lemma @{text "moment_blocked"} follows.

   882 *}

   883 

   884 (*<*)

   885 end

   886 (*>*)

   887