--- a/prio/Slides/Slides1.thy Mon Aug 13 10:37:37 2012 +0000
+++ b/prio/Slides/Slides1.thy Mon Aug 13 12:08:52 2012 +0000
@@ -110,13 +110,13 @@
\begin{itemize}
\item Undergraduate OS course in our university \pause
\begin{itemize}
- \item {\large Experiments using intrutional OSs }
- \item {\large PINTOS (Stanford) is choosen }
+ \item {\large Experiments using instrutional OSs }
+ \item {\large PINTOS (Stanford) is chosen }
\item {\large Core project: Implementing PIP in it}
\end{itemize} \pause
- \item Understanding is crucial to implemention \pause
- \item Little help was found in the literature \pause
- \item Some mentioning the complication
+ \item Understanding is crucial for the implemention \pause
+ \item Existing literature of little help \pause
+ \item Some mention the complication
\end{itemize}
\end{frame}}
@@ -189,7 +189,7 @@
\large
\begin{itemize}
- \item Purpose: gurantee the most urgent task be processed in time
+ \item Purpose: gurantee the most urgent task to be processed in time
\item Processes have priorities\\
\item Resources can be locked and unlocked
\end{itemize}
@@ -342,7 +342,7 @@
\frametitle{Event Abstraction}
\begin{itemize}\large
- \item Use Inductive Approch of L. Paulson \pause
+ \item Use Inductive Approach of L. Paulson \pause
\item System is event-driven \pause
\item A \alert{state} is a list of events
\end{itemize}
@@ -537,7 +537,7 @@
\begin{itemize}
\item @{text "RAG s' = RAG s"}
- \item No precedence needs to recalculate
+ \item No precedence needs to be recomputed
\end{itemize}
\end{frame}}
@@ -557,7 +557,7 @@
\begin{itemize}
\item @{text "RAG s' = RAG s"}
- \item No precedence needs to recalculate
+ \item No precedence needs to be recomputed
\end{itemize}
\end{frame}}
@@ -636,12 +636,12 @@
\item using Isabelle/HOL in OS code development \medskip
\item through the Inductive Approach
\end{itemize} \pause
- \item Future researches \pause
+ \item Future research \pause
\begin{itemize}
\item scheduler in RT-Linux\medskip
\item multiprocessor case\medskip
\item other ``nails'' ? (networks, \ldots) \medskip \pause
- \item Refinement to real code and relation between implemenations
+ \item Refinement to real code and relation between implementations
\end{itemize}
\end{itemize}
\end{frame}}