
diff -r d62b19b641c5 -r a5afc26b1d62 Journal/Paper.thy
--- a/Journal/Paper.thy	Fri Jul 06 22:18:39 2018 +0100
+++ b/Journal/Paper.thy	Wed Jan 02 21:09:05 2019 +0000
@@ -251,9 +251,9 @@
   with the highest priority so that it terminates more quickly.  We
   are also able to generalise the scheduler of Sha et
   al.~\cite{Sha90} to the practically relevant case where critical
-  sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
+  sections can overlap; see Fig.~\ref{overlap} \emph{a)} for
   an example of this restriction. In the existing literature there is
-  no proof and also no method for proving which covers this generalised
+  no proof and also no proof method that covers this generalised
   case.
 
   \begin{figure}
@@ -427,7 +427,7 @@
 
   \noindent
   where we use Isabelle's notation for list-comprehensions. This
-  notation is very similar to notation used in Haskell for list-comprehensions.  
+  notation is very similar to the notation used in Haskell for list-comprehensions.  
   A \emph{precedence} of a thread @{text th} in a
   state @{text s} is the pair of natural numbers defined as
   
@@ -562,7 +562,7 @@
 
   \noindent
   If there is no cycle, then every @{text RAG} can be pictured as a forest of trees, as
-  for example in Figure~\ref{RAGgraph}.
+  for example in Fig.~\ref{RAGgraph}.
 
   Because of the @{text RAG}s, we will need to formalise some results
   about graphs.
@@ -609,7 +609,7 @@
   \mbox{}\hfill\numbered{children}
   \end{isabelle}
   
-  \noindent Note that forests can have trees with infinte depth and
+  \noindent Note that forests can have trees with infinite depth and
   containing nodes with infinitely many children.  A \emph{finite
   forest} is a forest whose underlying relation is
   well-founded\footnote{For \emph{well-founded} we use the quite natural
@@ -652,7 +652,7 @@
   \noindent This definition is the relation that one thread is waiting for
   another to release a resource, but the corresponding 
   resource is ``hidden''. 
-  In Figure~\ref{RAGgraph} this means the @{text TDG} connects 
+  In Fig.~\ref{RAGgraph} this means the @{text TDG} connects 
   @{text "th\<^sub>1"} and @{text "th\<^sub>2"} to @{text "th\<^sub>0"}, which both wait for
   resource @{text "cs\<^sub>1"} to be released; and @{text "th\<^sub>3"} to @{text "th\<^sub>2"}, which
   cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
@@ -712,7 +712,7 @@
   function is defined in \eqref{allunlocked}) and the
   current precedence of every thread is initialised with @{term "Prc 0 0"}; that means 
   \mbox{@{abbrev initial_cprec}}. Therefore
-  we have for the initial shedule state
+  we have for the initial schedule state
 
   \begin{isabelle}\ \ \ \ \ %%%
   \begin{tabular}{@ {}l}
@@ -1244,7 +1244,7 @@
 %  \endnote{{\bf OUTLINE}
 
 %  Since @{term "th"} is the most urgent thread, if it is somehow
-%  blocked, people want to know why and wether this blocking is
+%  blocked, people want to know why and whether this blocking is
 %  reasonable.
 
 %  @{thm [source] th_blockedE} @{thm th_blockedE}
@@ -1262,7 +1262,7 @@
 
 %  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
 
-%  It is basic propery with non-trival proof. 
+%  It is basic property with non-trivial proof. 
 
 %  THEN
 
@@ -1342,9 +1342,9 @@
   %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
   %thread ``normally'' has).
   %So we want to show what the cp of th' is in state t @ s.
-  %We look at all the assingned precedences in the subgraph starting from th'
+  %We look at all the assigned precedences in the subgraph starting from th'
   %We are looking for the maximum of these assigned precedences.
-  %This subgraph must contain the thread th, which actually has the highest precednence
+  %This subgraph must contain the thread th, which actually has the highest precedence
   %so cp of th' in t @ s has this (assigned) precedence of th
   %We know that cp (t @ s) th' 
   %is the Maximum of the threads in the subgraph starting from th'
@@ -1433,7 +1433,7 @@
 %  @{term "cp (s' @ s) th"} can not be higher than this and can not be lower either (by 
 %  definition of @{term "cp"}). Consequently, we have @{term "prec th (s' @ s) = cp (s' @ s) th"}.
 %  Finally we have @{term "cp (s' @ s) th' < cp (s' @ s) th"}.
-%  By defintion of @{text "running"}, @{text "th'"} can not be running in state
+%  By definition of @{text "running"}, @{text "th'"} can not be running in state
 %  @{text "s' @ s"}, as we had to show.\qed
 %  \end{proof}
 
@@ -1511,9 +1511,9 @@
   %  @  {thm [display] count_eq_dependants}
   %\end{enumerate}
 
-  %The reason that only threads which already held some resoures
+  %The reason that only threads which already held some resources
   %can be running and block @{text "th"} is that if , otherwise, one thread 
-  %does not hold any resource, it may never have its prioirty raised
+  %does not hold any resource, it may never have its priority raised
   %and will not get a chance to run. This fact is supported by 
   %lemma @{text "moment_blocked"}:
   %@   {thm [display] moment_blocked}
@@ -1579,18 +1579,18 @@
   %then.
 
  % NOTE: about bounds in sha et al and ours: they prove a bound on the length of individual
- % blocages. We prove a bound for the overall-blockage.
+ % blockages. We prove a bound for the overall-blockage.
 
  % There are low priority threads, 
  % which do not hold any resources, 
  % such thread will not block th. 
  % Their Theorem 3 does not exclude such threads.
 
- % There are resources, which are not held by any low prioirty threads,
+ % There are resources, which are not held by any low priority threads,
  % such resources can not cause blockage of th neither. And similiary, 
- % theorem 6 does not exlude them.
+ % theorem 6 does not exclude them.
 
- % Our one bound excudle them by using a different formaulation. "
+ % Our one bound exclude them by using a different formulation. "
 
   *}
 (*<*)
@@ -1684,7 +1684,7 @@
   \end{isabelle}
 
   \noindent This set contains all threads that are not detached in
-  state @{text s}. According to our definiton of @{text "detached"},
+  state @{text s}. According to our definition of @{text "detached"},
   this means a thread in @{text "blockers"} either holds or waits for
   some resource in state @{text s} . Our Thm.~1 implies that only 
   these threads can all potentially block @{text th} after state
@@ -1837,7 +1837,7 @@
   \noindent This theorem is the main conclusion we obtain for the
   Priority Inheritance Protocol. It is based on the fact that the set of
   @{text blockers} is fixed at state @{text s} when @{text th} becomes
-  the thread with highest priority. Then no additional blocker of
+  the thread with the 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.
@@ -1875,7 +1875,7 @@
   computed by considering the static precedence of @{text th}
   and 
   the current precedences of the children of @{text th}. Their 
-  @{text "cprec"}s, in general, need to be computed by recursively decending into 
+  @{text "cprec"}s, in general, need to be computed by recursively descending into 
   deeper ``levels'' of the @{text TDG}. 
   However, the current precedence of a thread @{text th}, say, 
   only needs to be recomputed when @{text "(i)"} its static
@@ -1899,7 +1899,7 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Create th prio"}:} We assume that the current state @{text s} and 
+  \colorbox{mygrey}{@{term "Create th prio"}:} \\ We assume that the current state @{text s} and 
   the next state @{term "e#s"}, whereby \mbox{@{term "e \<equiv> Create th prio"}}, are both valid (meaning the event
   @{text "Create"} is allowed to occur in @{text s}). In this situation we can show that
 
@@ -1920,7 +1920,7 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Exit th"}:} We again assume that the current state @{text s} and 
+  \colorbox{mygrey}{@{term "Exit th"}:}\\ We again assume that the current state @{text s} and 
   the next state @{term "e#s"}, whereby this time  @{term "e \<equiv> Exit th"}, are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1940,7 +1940,7 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "Set th prio"}:} We assume that @{text s} and 
+  \colorbox{mygrey}{@{term "Set th prio"}:}\\ We assume that @{text s} and 
   @{term "e#s"} with @{term "e \<equiv> Set th prio"} are both valid. We can show that
 
   \begin{isabelle}\ \ \ \ \ %%%
@@ -1989,7 +1989,7 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "V th cs"}:} We assume that @{text s} and 
+  \colorbox{mygrey}{@{term "V th cs"}:}\\ We assume that @{text s} and 
   @{term "e#s"} with @{text e} being @{term "V th cs"} are both valid. 
   We have to consider two
   subcases: one where there is a thread to ``take over'' the released
@@ -2057,7 +2057,7 @@
 
 text {*
   \noindent
-  \colorbox{mygrey}{@{term "P th cs"}:} We assume that @{text s} and 
+  \colorbox{mygrey}{@{term "P th cs"}:}\\ We assume that @{text s} and 
   @{term "e#s"} with @{term "e \<equiv> P th cs"} are both valid. 
   We again have to analyse two subcases, namely
   the one where @{text cs} is not locked, and one where it is. We 
@@ -2075,7 +2075,7 @@
   RAG}. However, note that while the @{text RAG} changes the corresponding
   @{text TDG} does not change. Together with the fact that the
   precedences of all threads are unchanged, no @{text cprec} value is
-  changed. Therefore, no recalucation of the @{text cprec} value 
+  changed. Therefore, no recalculation of the @{text cprec} value 
   of any thread @{text "th''"} is needed.
 
 *} 
@@ -2100,7 +2100,7 @@
   "cprecs"}. Whereas in all other event we might have to make
   modifications to the @{text "RAG"}, no recalculation of @{text
   cprec} depends on the @{text RAG}. This is the only case where
-  the recalulation needs to take the connections in the @{text RAG} into
+  the recalculation needs to take the connections in the @{text RAG} into
   account.
   To do this we can start from @{term "th"} and follow the
   @{term "children"}-edges to recompute the @{term "cp"} of every
@@ -2176,7 +2176,7 @@
   
   Apart from having to implement relatively complex data\-structures in C
   using pointers, our experience with the implementation has been very positive: our specification 
-  and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
+  and formalisation of PIP translates smoothly to an efficient implementation in PINTOS. 
   Let us illustrate this with the C-code for the function @{ML_text "lock_acquire"}, 
   shown in Figure~\ref{code}.  This function implements the operation of requesting and, if free, 
   locking of a resource by the current running thread. The convention in the PINTOS
@@ -2277,7 +2277,7 @@
   The very last step is to enable interrupts again thus leaving the protected section.
   
 
-  Similar operations need to be implementated for the @{ML_text lock_release} function, which
+  Similar operations need to be implemented for the @{ML_text lock_release} function, which
   we however do not show. The reader should note though that we did \emph{not} verify our C-code. 
   This is in contrast, for example, to the work on seL4, which actually verified in Isabelle/HOL
   that their C-code satisfies its specification, though this specification does not contain 
@@ -2316,7 +2316,7 @@
   programmer who wants to implement PIP (similarly Sha et al.~\cite{Sha90}).  
   That this is an issue in practice is illustrated by the
   email from Baker we cited in the Introduction. We achieved also this
-  goal: The formalisation allowed us to efficently implement our version
+  goal: The formalisation allowed us to efficiently implement our version
   of PIP on top of PINTOS, a simple instructional operating system for the x86 
   architecture implemented by Pfaff \cite{PINTOS}. It also gives the first author enough data to enable
   his undergraduate students to implement PIP (as part of their OS course).




