--- a/prio/Paper/Paper.thy Tue Feb 14 04:14:18 2012 +0000
+++ b/prio/Paper/Paper.thy Tue Feb 14 04:33:31 2012 +0000
@@ -559,7 +559,7 @@
some meaningful statements about PIP.\footnote{This situation is
similar to the infamous occurs check in Prolog: In order to say
anything meaningful about unification, one needs to perform an occurs
- check. But in practice the occurs check is ommited and the
+ check. But in practice the occurs check is omitted and the
responsibility for avoiding problems rests with the programmer.}
\begin{center}
@@ -633,7 +633,7 @@
running or it is blocked by a thread that was alive in the state
@{text s} and was in the possession of a lock in @{text s}. Since in @{text s}, as in every state, the set of alive
threads is finite, @{text th} can only be blocked a finite number of
- times. We will actually prove astronger statement where we also provide
+ times. We will actually prove a stronger statement where we also provide
the current precedence of the blocking thread. However, this
correctness criterion hinges upon a number of assumptions about the
states @{text s} and @{text "s' @ s"}, the thread @{text th} and the
@@ -667,7 +667,7 @@
\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 happen if threads with higher priority
- than @{text th} are continously created in @{text s'}. Therefore we have to assume that
+ than @{text th} are continuously created in @{text s'}. Therefore we have to assume that
events in @{text s'} can only create (respectively set) threads with equal or lower
priority than @{text prio} of @{text th}. We also need to assume that the
priority of @{text "th"} does not get reset and also that @{text th} does
@@ -705,10 +705,10 @@
Like in the argument by Sha et al.~our
finite bound does not guarantee absence of indefinite Priority
Inversion. For this we further have to assume that every thread
- gives up its resources after a finite amount of time. We found that
+ gives up its resources (that means get detached) after a finite amount of time. We found that
this assumption is awkward to formalise in our model. Therefore we
leave it out and let the programmer assume the responsibility to
- program threads in such a benign manner (in addition to causeing no
+ program threads in such a benign manner (in addition to causing no
circularity in the @{text RAG}). In this detail, we do not
make any progress in comparison with the work by Sha et al.
However, we are able to combine their two separate bounds into a
@@ -1109,7 +1109,7 @@
\noindent
For @{text th} and @{text th'} we need to use Lemma~\ref{childrenlem} to
- recalculate their current prcedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
+ recalculate their current precedence since their children have changed. *}(*<*)end context step_v_cps_nnt begin (*>*)text {*
\noindent
In the other case where there is no thread that takes over @{text cs}, we can show how
to recalculate the @{text RAG} and also show that no current precedence needs
@@ -1146,7 +1146,7 @@
This means we do not need to add a holding edge to the @{text RAG} and no
current precedence needs to be recalculated.*}(*<*)end context step_P_cps_ne begin(*>*) text {*
\noindent
- In the second case we know that resouce @{text cs} is locked. We can show that
+ In the second case we know that resource @{text cs} is locked. We can show that
\begin{isabelle}\ \ \ \ \ %%%
\begin{tabular}{@ {}l}
Binary file prio/paper.pdf has changed