# HG changeset patch
# User urbanc
# Date 1327916673 0
# Node ID 78523b3ae2ad8a343d8477270a0f0b6acc1af1b1
# Parent  d98435b93063adee1bd2d1cd7499e3a02d772b12
spell check

diff -r d98435b93063 -r 78523b3ae2ad prio/Paper/Paper.thy
--- a/prio/Paper/Paper.thy	Mon Jan 30 09:33:39 2012 +0000
+++ b/prio/Paper/Paper.thy	Mon Jan 30 09:44:33 2012 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports CpsG ExtGG LaTeXsugar
+imports CpsG ExtGG "~~/src/HOL/Library/LaTeXsugar"
 begin
 ML {*
   Printer.show_question_marks_default := false;
@@ -12,7 +12,7 @@
 text {*
   Many realtime systems need to support processes with priorities and
   locking of resources. Locking of resources ensures mutual exclusion
-  when accessing shared data or devices. Priorities allow schedulling
+  when accessing shared data or devices. Priorities allow scheduling
   of processes that need to finish their work within hard deadlines.
   Unfortunately, both features can interact in subtle ways leading to
   a problem, called \emph{Priority Inversion}. Suppose three processes
@@ -40,11 +40,11 @@
   normal operation of the craft could only resume the next day (the
   mission and data already collected were fortunately not lost, because
   of a clever system design).  The reason for the shutdowns was that
-  the schedulling software fell victim of Priority Inversion: a low
+  the scheduling software fell victim of Priority Inversion: a low
   priority task locking a resource prevented a high priority process
   from running in time leading to a system reset. Once the problem was found,
   it was rectified by enabling the Priority Inheritance Protocol in
-  the schedulling software.
+  the scheduling software.
 
   The idea behind the \emph{Priority Inheritance Protocol} (PIP) is to
   let the process $L$ temporarily inherit the high priority from $H$ 
@@ -52,7 +52,7 @@
   $H$ having to wait indefinitely, because $L$ cannot, for example, be blocked by 
   processes having priority $M$. This solution to the Priority
   Inversion problem has been known since \cite{Lampson:Redell:cacm:1980}
-  but Lui et al give the first thourough analysis and present a correctness
+  but Lui et al give the first thorough analysis and present a correctness
   proof for an algorithm \cite{journals/tc/ShaRL90}.
 
   However, there are further subtleties: just lowering the priority 
diff -r d98435b93063 -r 78523b3ae2ad prio/paper.pdf
Binary file prio/paper.pdf has changed