diff -r c89f82fb95f8 -r 21428f38e506 prio/Slides/Slides1.thy --- 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}}