diff -r f86e099ac688 -r c5442db6a5cb prio/Paper/Paper.thy --- 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}