601   Main lemma

   599   Sha et al.~\cite{Sha90} state their correctness criterion of PIP in terms

   602 

   600   of the number of critical resources: if there are @{text m} critical

   603   \begin{enumerate}

   601   resources, then a blocked job can only be blocked @{text m} times---that is

   604   \item @{term "s"} is a valid state (@{text "vt_s"}):

   602   a bounded number of times.

   605     @{thm  vt_s}.

   603   For their version of PIP, this is \emph{not} true (as pointed out by 

   606   \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):

   604   Yodaiken \cite{Yodaiken02}) as a high-priority thread can be

   607     @{thm threads_s}.

   605   blocked an unbounded number of times by creating medium-priority

   608   \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):

   606   threads that block a thread locking a critical resource and having 

   609     @{thm highest}.

   607   a too low priority. In the way we have set up our formal model of PIP, 

   610   \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):

   608   their proof idea, even when fixed, does not seem to go through.

   611     @{thm preced_th}.

   609 

   612  

   610   The idea behind our correctness criterion of PIP is as follows: for all states

   613   \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.

   611   @{text s}, we know the corresponding thread @{text th} with the highest precedence;

   614   \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore

   612   we show that in every future state (denoted by @{text "s' @ s"}) in which

   615     its precedence can not be higher than @{term "th"},  therefore

   613   @{text th} is still active, either @{text th} is running or it is blocked by a 

   616     @{term "th"} remain to be the one with the highest precedence

   614   thread that was active in the state @{text s}. Since in @{text s}, as in every 

   617     (@{text "create_low"}):

   615   state, the set of active threads is finite, @{text th} can only blocked a

   618     @{thm [display] create_low}

   616   finite number of time. We will actually prove a stricter bound. However,

   619   \item Any adjustment of priority in 

   617   this correctness criterion depends on a number of assumptions about the states

   620     @{term "t"} does not happen to @{term "th"} and 

   618   @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening

   621     the priority set is no higher than @{term "prio"}, therefore

   619   in @{text s'}.

   622     @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):

   620 

   623     @{thm [display] set_diff_low}

   621   \begin{quote}

   624   \item Since we are investigating what happens to @{term "th"}, it is assumed 

   622   {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make 

   625     @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):

   623   any meaningful statement, we need to require that @{text "s"} and 

   626     @{thm [display] exit_diff}

   624   @{text "s' @ s"} are valid states, namely

   627   \end{enumerate}

   625   \begin{isabelle}\ \ \ \ \ %%%

   628 

   626   \begin{tabular}{l}

   629   \begin{lemma}

   627   @{term "vt s"}\\

   630   @{thm[mode=IfThen] moment_blocked}

   628   @{term "vt (s' @ s)"} 

   631   \end{lemma}

   629   \end{tabular}

   630   \end{isabelle}

   631   \end{quote}

   632 

   633   \begin{quote}

   634   {\bf Assumptions on the thread @{text "th"}:} The thread @{text th} must be active in @{text s} and 

   635   has the highest precedence of all active threads in @{text s}. Furthermore the

   636   priority of @{text th} is @{text prio}.

   637   \begin{isabelle}\ \ \ \ \ %%%

   638   \begin{tabular}{l}

   639   @{term "th \<in> threads s"}\\

   640   @{term "prec th s = Max (cprec s ` threads s)"}\\

   641   @{term "prec th s = (prio, DUMMY)"}

   642   \end{tabular}

   643   \end{isabelle}

   644   \end{quote}

   645   

   646   \begin{quote}

   647   {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot

   648   be blocked indefinitely. Of course this can by violated if threads with higher priority

   649   than @{text th} are created in @{text s'}. Therefore we have to assume that  

   650   events in @{text s'} can only create (respectively set) threads with lower or equal 

   651   priority than @{text prio} of @{text th}. We also have to assume that @{text th} does

   652   not get ``exited'' in @{text "s'"}.

   653   \begin{isabelle}\ \ \ \ \ %%%

   654   \begin{tabular}{l}

   655   {If}~~@{text "Create _ prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\

   656   {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\

   657   {If}~~@{text "Exit th' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}\\

   658   \end{tabular}

   659   \end{isabelle}

   660   \end{quote}

   661 

   662   \noindent

   663   Under these assumption we will prove the following property:

   664 

   665   \begin{theorem}

   666   Given the assumptions about states @{text "s"} and @{text "s' @ s"},

   667   the thread @{text th} and the events in @{text "s'"}.

   668   @{thm[mode=IfThen] runing_inversion_3[where ?th'="th'", THEN

   669   conjunct1]}

   670   \end{theorem}

   637   \begin{theorem}

   676  

   638   @{thm[mode=IfThen] runing_inversion_3}

   639   \end{theorem}