204 computing the priority to be restored solely from this log is not |
204 computing the priority to be restored solely from this log is not |
205 explained in \cite{Liu00} but left as an ``{\it excercise}'' to the |
205 explained in \cite{Liu00} but left as an ``{\it excercise}'' to the |
206 reader. As we shall see, a correct version of PIP does not need to |
206 reader. As we shall see, a correct version of PIP does not need to |
207 maintain this (potentially expensive) data structure at |
207 maintain this (potentially expensive) data structure at |
208 all. Surprisingly also the widely read and frequently updated |
208 all. Surprisingly also the widely read and frequently updated |
209 textbook \cite{Silberschatz13} gives the wrong specification. For |
209 textbook \cite{Silberschatz13} gives the wrong specification. On Page 254 the authors write: ``{\it Upon releasing the |
210 example on Page 254 the authors write: ``{\it Upon releasing the |
|
211 lock, the [low-priority] thread will revert to its original |
210 lock, the [low-priority] thread will revert to its original |
212 priority.}'' The same error is also repeated later in this popular textbook. |
211 priority.}'' The same error is also repeated later in this popular textbook. |
213 |
212 |
214 |
213 |
215 While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only |
214 While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only |
313 Following good experience in earlier work \cite{Wang09}, |
312 Following good experience in earlier work \cite{Wang09}, |
314 our model of PIP is based on Paulson's inductive approach for protocol |
313 our model of PIP is based on Paulson's inductive approach for protocol |
315 verification \cite{Paulson98}. In this approach a \emph{state} of a system is |
314 verification \cite{Paulson98}. In this approach a \emph{state} of a system is |
316 given by a list of events that happened so far (with new events prepended to the list). |
315 given by a list of events that happened so far (with new events prepended to the list). |
317 \emph{Events} of PIP fall |
316 \emph{Events} of PIP fall |
318 into five categories defined as the datatype: |
317 into five categories defined as the Isabelle datatype: |
319 |
318 |
320 \begin{isabelle}\ \ \ \ \ %%% |
319 \begin{isabelle}\ \ \ \ \ %%% |
321 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
320 \mbox{\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
322 \isacommand{datatype} event |
321 \isacommand{datatype} event |
323 & @{text "="} & @{term "Create thread priority\<iota>"}\\ |
322 & @{text "="} & @{term "Create thread priority\<iota>"}\\ |
418 |
417 |
419 \begin{isabelle}\ \ \ \ \ %%% |
418 \begin{isabelle}\ \ \ \ \ %%% |
420 @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}. |
419 @{thm actions_of_def[where ?s="s" and ?ths="ths", THEN eq_reflection]}. |
421 \end{isabelle} |
420 \end{isabelle} |
422 |
421 |
|
422 \noindent |
423 where we use Isabelle's notation for list-comprehensions. This |
423 where we use Isabelle's notation for list-comprehensions. This |
424 notation is very similar to notation used in Haskell for list |
424 notation is very similar to notation used in Haskell for list-comprehensions. |
425 comprehensions. A \emph{precedence} of a thread @{text th} in a |
425 A \emph{precedence} of a thread @{text th} in a |
426 state @{text s} is the pair of natural numbers defined as |
426 state @{text s} is the pair of natural numbers defined as |
427 |
427 |
428 \begin{isabelle}\ \ \ \ \ %%% |
428 \begin{isabelle}\ \ \ \ \ %%% |
429 @{thm preced_def} |
429 @{thm preced_def} |
430 \end{isabelle} |
430 \end{isabelle} |