pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:c1028969401a
+:1b72810a2d61
 %@{thm "th_blockedE_pretty"} -- thm-blockedE??
 %
 % @{text "th_kept"} shows that th is a thread in s'-s
 % }
-Given our assumptions (on @{text th}), the first property we show that a running thread @{text "th'"} must either wait for or
+Given our assumptions (on @{text th}), the first property we show
-hold a resource in state @{text s}.
+that a running thread @{text "th'"} must either wait for or hold a
+resource in state @{text s}.
 \begin{lemma}\label{notdetached}
 If @{term "th' \<in> running (s' @ s)"} and @{term "th \<noteq> th'"} then @{term "\<not>detached s th'"}.
 \end{lemma}
 s}. Otherwise our PIP scheduler could be ``swamped'' with @{text
 "Create"}-requests.  So our first assumption states:
 \begin{quote} {\bf Assumption on the number of threads created
 after the state {\boldmath@{text s}}:} Given the
-state @{text s}, in every ``future'' valid state @{text "t @ s"}, we
+state @{text s}, in every ``future'' valid state @{text "es @ s"}, we
 require that the number of created threads is less than
 a bound @{text "BC"}, that is
-\[@{text "len (filter isCreate t) < BC"}\;.\]
+\[@{text "len (filter isCreate es) < BC"}\;\]
+wherby @{text es} is a list of events.
 \end{quote}
 \noindent Note that it is not enough to just to state that there are
 only finite number of threads created up until a single state @{text
 "s' @ s"} after @{text s}.  Instead, we need to put this bound on
 the @{text "Create"} events for all valid states after @{text s}.
-This ensures that no matter which ``future'' state is reached, the number
+This ensures that no matter which ``future'' state is reached, the
-of @{text "Create"}-events is finite.
+number of @{text "Create"}-events is finite. We use @{text "es @ s"}
+to stand for \emph{future states} after @{text s}---it is @{text s}
+extended with some list of events.
 For our second assumption about giving up resources after a finite
 amount of ``time'', let us introduce the following definition about
 threads that can potentially block @{text th}:
 \begin{quote}
 {\bf Assumptions on the threads {\boldmath{@{term "th' \<in> blockers"}}}:}
 For each such @{text "th'"} there exists a finite bound @{text "BND(th')"}
 such that for all future
-valid states @{text "t @ s"},
+valid states @{text "es @ s"},
-we have that if \mbox{@{term "\<not>(detached (t @ s) th')"}}, then
+we have that if \mbox{@{term "\<not>(detached (es @ s) th')"}}, then
-\[@{text "len (actions_of {th'} t) < BND(th')"}\]
+\[@{text "len (actions_of {th'} es) < BND(th')"}\]
 \end{quote}
 \noindent By this assumption we enforce that any thread potentially
 blocking @{term th} must become detached (that is lock no resource
-anymore) after a finite number of events in @{text "t @ s"}. Again
+anymore) after a finite number of events in @{text "es @ s"}. Again
 we have to state this bound to hold in all valid states after @{text
 s}. The bound reflects how each thread @{text "th'"} is programmed:
 Though we cannot express what instructions a thread is executing,
 the events in our model correspond to the system calls made by
 thread. Our @{text "BND(th')"} binds the number of these ``calls''.
 @{text th} is not running (that is where Priority Inversion occurs)
 can be bounded by the number of actions the threads in @{text
 blockers} perform and how many threads are newly created.  To state
 our bound formally, we need to make a definition of what we mean by
 intermediate states; it will be the list of states starting from
-@{text s} upto the state @{text "t @ s"}. For example, suppose
+@{text s} upto the state @{text "es @ s"}. For example, suppose
-$\textit{t} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
+$\textit{es} = [\textit{e}_n, \textit{e}_{n-1}, \ldots, \textit{e}_2,
 \textit{e}_1]$, then the intermediate states from @{text s} upto
-@{text "t @ s"} are
+@{text "es @ s"} are
 \begin{center}
 \begin{tabular}{l}
 $\textit{s}$\\
 $\textit{e}_1 :: \textit{s}$\\
 the following recursive function
 \begin{center}
 \begin{tabular}{lcl}
 @{text "s upto []"} & $\dn$ & $[]$\\
-@{text "s upto (e::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
+@{text "s upto (_::es)"} & $\dn$ & @{text "(es @ s) :: s upto es"}
 \end{tabular}
 \end{center}
+\noindent
-\noindent Assume you have an extension @{text t}, this essentially
+Our theorem can then be stated as follows:
-defines in out list representation of states all the postfixes of
-@{text t}.
 \begin{theorem}
 Given our assumptions about bounds, we have that
 \[
 @{text "len"}\,[@{text "s'"}
-\leftarrow @{text "s upto t"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq 1 +
+\leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \;\;\leq\;\;
+@{text "BC"} + \sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}\;.
 \]
-\[@{thm bounded_extend_highest.priority_inversion_is_finite_upto}\]
 \end{theorem}
+\begin{proof} There are two characterisations for the number of
-Theorem:
+events in @{text es}: First, for each corresponding state in @{text
+"s upto es"}, either @{text th} is running or not running. That
-\begin{isabelle}\ \ \ \ \ %%%
+means
-@{text "len (filter (\<lambda>t'. th \<notin> running t') (s upto t)) \<le>
-1 + len (actions_of blockers t) + len (filter isCreate t)"}
+\begin{equation}\label{firsteq}
-\end{isabelle}
+@{text "len es"} =
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}] +
-Proof:
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
+\end{equation}
-Consider the states @{text "s upto t"}. It holds that all the states where
-@{text "th"} runs and all the states where @{text "th"} does not run is
+\noindent Second by Thm~\ref{mainthm}, the events are either the
-equalt to @{text "len t"}. That means
+actions of @{text th} or @{text "Create"}-events or actions of the
+threads in blockers. That is
-\begin{center}
-@{text "states where th does not run = len t - states where th runs"} (*)
+\begin{equation}\label{secondeq}
-\end{center}
+@{text "len es"} = @{text "len (actions_of {th} es)"} +
+@{text "len (filter isCreate es)"} +
-It also holds that all the actions of @{text "th"} are less or equal to
+@{text "len (actions_of blockers es)"}
-the states where @{text th} runs. That is
+\end{equation}
-\begin{center}
+\noindent
-@{text "len (actions_of {th} t) \<le> states where th runs"}
+Further we know that an action of @{text th} can only be taken when @{text th} is running. Therefore
-\end{center}
+\[
-That means in $(*)$ we have
+@{text "len (actions_of {th} es)"} \leq
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \in @{text "running s'"}]
-\begin{center}
+\]
-@{text "states where th does not run \<le> len t - len (actions_of {th} t)"}
-\end{center}
+\noindent Substituting this into \eqref{firsteq} gives
-If we look at all the events that can occur in @{text "s upto t"}, we have that
+\[
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}]
-\begin{center}
+\leq @{text "len es"} - @{text "len (actions_of {th} es)"}
-@{text "len t = len (action_of {th}) + len (action_of blockers t) +
+\]
-len (filter isCreate t)"}
-\end{center}
+into which we can substitute \eqref{secondeq} yielding
-This gives us finally our theorem. \hfill\qed\medskip
+\[
+@{text len} [@{text "s'"} \leftarrow @{text "s upto es"}.\;\; @{text "th"} \not\in @{text "running s'"}] \leq
-\noindent In order to now show the absence of indefinite Priority
+@{text "len (filter isCreate es)"} + @{text "len (actions_of blockers es)"}
-Inversion, we need to show that the number of actions of the @{text
+\]
-"blockers"} is bounded---the number of @{text "Creates"} is clearly
-bounded by our first assumption. The number of actions of each
+\noindent By our first assumption we know that the @{text
-individual thread in @{text "blockers"} is bound by our second
+"Create"}-events are bounded by the bound @{text BC}.  By our second
-assumption.  Since there can only be a finite number of @{text
+assumption we can prove that the actions of all blockers is bounded
-blockers} in state @{text s} their overall sum is also bounded.
+by the sum of bounds of the individual blocking threads, that is
-This is actually the main conclusion we obtain for the Priority
-Inheritance Protocol: this above theorem shows is that set of @{text
+\[
-blockers} is fixed at state @{text s} when the Priority Inversion
+@{text "len (actions_of blockers es)"} \;\;\leq\;\;
-occured and no additional blocker of @{text th} can appear after the
+\sum @{text "th'"} \in @{text "blockers"}.\;\; @{text "BND(th')"}
-state @{text s}. And in this way we can bound the number of states
+\]
-where the thread @{text th} with the highest priority is prevented
-fropm running.
+\noindent With this in place we can conclude our theorem.\hfill\qed
+\end{proof}
+\noindent This theorem is the main conclusion we obtain for the
+Priority Inheritance Protocol: it shows that set of @{text blockers}
+is fixed at state @{text s} when @{text th} becomes the thread with
+highest priority. Then no additional blocker of @{text th} can
+appear after the state @{text s}. And in this way we can bound the
+number of states where the thread @{text th} with the highest
+priority is prevented from running.
 *}
 (*<*)
 end
 (*>*)

changeset 174	1b72810a2d61
parent 173	c1028969401a
child 175	170e59f2d645