373   we have a deadlock. Therefore when a thread requests a resource,

   373   we have a deadlock. Therefore when a thread requests a resource,

   374   we must ensure that the resulting RAG is not circular. In practice, the 

   374   we must ensure that the resulting RAG is not circular. In practice, the 

   375   programmer has to ensure this.

   375   programmer has to ensure this.

   376 

   376 

   377 

   377 

   385   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 

   378   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 

   386   state @{text s}. It is defined as

   379   state @{text s}. It is defined as

   387 

   380 

   388   \begin{isabelle}\ \ \ \ \ %%%

   381   \begin{isabelle}\ \ \ \ \ %%%

   389   @{thm cpreced_def2}\hfill\numbered{cpreced}

   382   @{thm cpreced_def2}\hfill\numbered{cpreced}

   541   @{term threads} is empty and therefore there is neither a thread ready nor running.

   534   @{term threads} is empty and therefore there is neither a thread ready nor running.

   542   If there is one or more threads ready, then there can only be \emph{one} thread

   535   If there is one or more threads ready, then there can only be \emph{one} thread

   543   running, namely the one whose current precedence is equal to the maximum of all ready 

   536   running, namely the one whose current precedence is equal to the maximum of all ready 

   544   threads. We use sets to capture both possibilities.

   537   threads. We use sets to capture both possibilities.

   545   We can now also conveniently define the set of resources that are locked by a thread in a

   538   We can now also conveniently define the set of resources that are locked by a thread in a

   547 

   540 

   548   \begin{isabelle}\ \ \ \ \ %%%

   541   \begin{isabelle}\ \ \ \ \ %%%

   549   @{thm holdents_def}

   542   @{thm holdents_def}

   550   \end{isabelle}

   543   \end{isabelle}

   551 

   544 

   552   Finally we can define what a \emph{valid state} is in our model of PIP. For

   555   Finally we can define what a \emph{valid state} is in our model of PIP. For

   553   example we cannot expect to be able to exit a thread, if it was not

   556   example we cannot expect to be able to exit a thread, if it was not

   554   created yet. 

   557   created yet. 

   555   These validity constraints on states are characterised by the

   558   These validity constraints on states are characterised by the

   556   inductive predicate @{term "step"} and @{term vt}. We first give five inference rules

   559   inductive predicate @{term "step"} and @{term vt}. We first give five inference rules

  1209   this section closely inform an implementation of PIP, namely whether the

  1212   this section closely inform an implementation of PIP, namely whether the

  1210   @{text RAG} needs to be reconfigured or current precedences need to

  1213   @{text RAG} needs to be reconfigured or current precedences need to

  1211   be recalculated for an event. This information is provided by the lemmas we proved.

  1214   be recalculated for an event. This information is provided by the lemmas we proved.

  1212   We confirmened that our observations translate into practice by implementing

  1215   We confirmened that our observations translate into practice by implementing

  1213   a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. 

  1216   a PIP-scheduler on top of PINTOS, a small operating system for teaching purposes \cite{PINTOS}. 

  1214 *}

  1229 *}

  1215 

  1230 

  1216 section {* Conclusion *}

  1231 section {* Conclusion *}

  1217 

  1232 

  1218 text {* 

  1233 text {*