regexp: comparison prio/Paper/Paper.thy

equal deleted inserted replaced

-:a401d2dff7d0
+:e44c4055d430
 \end{isabelle}
 \noindent
 In this definition @{term "DUMMY ` DUMMY"} stands for the image of a set under a function.
 Note that in the initial state, that is where the list of events is empty, the set
-@{term threads} is empty and therefore there is no thread ready nor a running.
+@{term threads} is empty and therefore there is neither a thread ready nor running.
 If there is one or more threads ready, then there can only be \emph{one} thread
 running, namely the one whose current precedence is equal to the maximum of all ready
 threads. We use the set-comprehension to capture both possibilities.
 We can now also conveniently define the set of resources that are locked by a thread in a
 given state.
 \end{tabular}
 \end{center}
 \noindent
 This completes our formal model of PIP. In the next section we present
-properties that show our version of PIP is correct.
+properties that show our model of PIP is correct.
 *}
 section {* Correctness Proof *}
 (*<*)
 text {*
 Sha et al.~\cite{Sha90} state their correctness criterion of PIP in terms
 of the number of critical resources: if there are @{text m} critical
 resources, then a blocked job can only be blocked @{text m} times---that is
 a bounded number of times.
-For their version of PIP, this is \emph{not} true (as pointed out by
+For their version of PIP, this property is \emph{not} true (as pointed out by
 Yodaiken \cite{Yodaiken02}) as a high-priority thread can be
 blocked an unbounded number of times by creating medium-priority
 threads that block a thread locking a critical resource and having
 a too low priority. In the way we have set up our formal model of PIP,
 their proof idea, even when fixed, does not seem to go through.
 The idea behind our correctness criterion of PIP is as follows: for all states
 @{text s}, we know the corresponding thread @{text th} with the highest precedence;
 we show that in every future state (denoted by @{text "s' @ s"}) in which
 @{text th} is still active, either @{text th} is running or it is blocked by a
 thread that was active in the state @{text s}. Since in @{text s}, as in every
-state, the set of active threads is finite, @{text th} can only blocked a
+state, the set of active threads is finite, @{text th} can only be blocked a
-finite number of time. We will actually prove a stricter bound. However,
+finite number of times. We will actually prove a stricter bound. However,
-this correctness criterion depends on a number of assumptions about the states
+this correctness criterion hinges on a number of assumptions about the states
 @{text s} and @{text "s' @ s"}, the thread @{text th} and the events happening
-in @{text s'}.
+in @{text s'}. We list them next.
 \begin{quote}
 {\bf Assumptions on the states @{text s} and @{text "s' @ s"}:} In order to make
 any meaningful statement, we need to require that @{text "s"} and
 @{text "s' @ s"} are valid states, namely
 \end{isabelle}
 \end{quote}
 \begin{quote}
 {\bf Assumptions on the events in @{text "s'"}:} We want to prove that @{text th} cannot
-be blocked indefinitely. Of course this can by violated if threads with higher priority
+be blocked indefinitely. Of course this can happen if threads with higher priority
-than @{text th} are created in @{text s'}. Therefore we have to assume that
+than @{text th} are continously created in @{text s'}. Therefore we have to assume that
-events in @{text s'} can only create (respectively set) threads with lower or equal
+events in @{text s'} can only create (respectively set) threads with equal or lower
-priority than @{text prio} of @{text th}. We also have to assume that @{text th} does
+priority than @{text prio} of the thread @{text th}. We also have to assume that @{text th} does
 not get ``exited'' in @{text "s'"}.
 \begin{isabelle}\ \ \ \ \ %%%
 \begin{tabular}{l}
 {If}~~@{text "Create _ prio' \<in> set s'"}~~{then}~~@{text "prio' \<le> prio"}\\
 {If}~~@{text "Set th' prio' \<in> set s'"}~~{then}~~@{text "th' \<noteq> th"}~~{and}~~@{text "prio' \<le> prio"}\\
 \noindent
 This theorem ensures that the thread @{text th}, which has the highest
 precedence in the state @{text s}, can only be blocked in the state @{text "s' @ s"}
 by a thread @{text th'} that already existed in @{text s}. As we shall see shortly,
 that means by only finitely many threads. Consequently, indefinite wait of
-@{text th}, that is Priority Inversion, cannot occur.
+@{text th}---whcih is Priority Inversion---cannot occur.
-The following are several very basic prioprites:
+In what follows we will describe properties of PIP that allow us to prove
-\begin{enumerate}
+Theorem~\ref{mainthm}. It is relatively easily to see that
-\item All runing threads must be ready (@{text "runing_ready"}):
-@{thm[display] "runing_ready"}
+\begin{isabelle}\ \ \ \ \ %%%
-\item All ready threads must be living (@{text "readys_threads"}):
+\begin{tabular}{@ {}l}
-@{thm[display] "readys_threads"}
+@{text "running s \<subseteq> ready s \<subseteq> threads s"}\\
-\item There are finite many living threads at any moment (@{text "finite_threads"}):
+@{thm[mode=IfThen]  finite_threads}
-@{thm[display] "finite_threads"}
+\end{tabular}
-\item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}):
+\end{isabelle}
-@{thm[display] "wq_distinct"}
-\item All threads in waiting queues are living threads (@{text "wq_threads"}):
+\noindent
-@{thm[display] "wq_threads"}
+where the second property is by induction of @{term vt}. The next three
-\item The event which can get a thread into waiting queue must be @{term "P"}-events
+properties are
-(@{text "block_pre"}):
-@{thm[display] "block_pre"}
+\begin{isabelle}\ \ \ \ \ %%%
-\item A thread may never wait for two different critical resources
+\begin{tabular}{@ {}l}
-(@{text "waiting_unique"}):
+@{thm[mode=IfThen] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}\\
-@{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
+@{thm[mode=IfThen] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}\\
-\item Every resource can only be held by one thread
+@{thm[mode=IfThen] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
-(@{text "held_unique"}):
+\end{tabular}
-@{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
+\end{isabelle}
-\item Every living thread has an unique precedence
-(@{text "preced_unique"}):
+\noindent
-@{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
+The first one states that every waiting thread can only wait for a single
-\end{enumerate}
+resource (because it gets suspended after requesting that resource), and
-*}
+the second that every resource can only be held by a single thread. The
+third property establishes that in every given valid state, there is
-text {* \noindent
+at most one running thread.
+TODO
+\noindent
 The following lemmas show how RAG is changed with the execution of events:
 \begin{enumerate}
 \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
 @{thm[display] depend_set_unchanged}
 \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
 *}
 text {* \noindent
 Some deeper results about the system:
 \begin{enumerate}
-\item There can only be one running thread (@{text "runing_unique"}):
-@{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
 \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
 @{thm [display] max_cp_eq}
 \item There must be one ready thread having the max @{term "cp"}-value
 (@{text "max_cp_readys_threads"}):
 @{thm [display] max_cp_readys_threads}

changeset 309	e44c4055d430
parent 308	a401d2dff7d0
child 310	4d93486cb302