changes by Xingyuan
authorurbanc
Tue, 14 Feb 2012 04:33:31 +0000
changeset 331 c5442db6a5cb
parent 330 f86e099ac688
child 332 5faa1b59e870
changes by Xingyuan
prio/Paper/Paper.thy
prio/paper.pdf
--- 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