pip: comparison Journal/Paper.thy

equal deleted inserted replaced

-:8a13b37b4d95
+:9b5da0327d43
 is made in the textbook \cite[Section 2.3.1]{book} which specifies
 for a process that inherited a higher priority and exits a critical
 section ``{\it it resumes the priority it had at the point of entry
 into the critical section}''.  This error can also be found in the
 textbook \cite[Section 16.4.1]{LiYao03} where the authors write
-``{\it its priority is immediately lowered to the level originally assigned}'';
+about this process: ``{\it its priority is immediately lowered to the level originally assigned}'';
-or in the
+and also in the
 more recent textbook \cite[Page 119]{Laplante11} where the authors
 state: ``{\it when [the task] exits the critical section that caused
 the block, it reverts to the priority it had when it entered that
 section}''. The textbook \cite[Page 286]{Liu00} contains a simlar
 flawed specification and even goes on to develop pseudo-code based
 broadly specified as containing ``{\it [h]istorical information on
 how the thread inherited its current priority}'' \cite[Page
 527]{Liu00}. Unfortunately, the important information about actually
 computing the priority to be restored solely from this log is not
 explained in \cite{Liu00} but left as an ``{\it excercise}'' to the
-reader.  Of course, a correct version of PIP does not need to
+reader.  As we shall see, a correct version of PIP does not need to
 maintain this (potentially expensive) data structure at
 all. Surprisingly also the widely read and frequently updated
 textbook \cite{Silberschatz13} gives the wrong specification. For
 example on Page 254 the authors write: ``{\it Upon releasing the
 lock, the [low-priority] thread will revert to its original
-priority.}'' The same error is also repeated later in this textbook.
+priority.}'' The same error is also repeated later in this popular textbook.
 While \cite{Laplante11,LiYao03,Liu00,book,Sha90,Silberschatz13} are the only
 formal publications we have found that specify the incorrect
 behaviour, it seems also many informal descriptions of PIP overlook
 for PIP being correct---a fact that has not been mentioned in the
 literature and not been used in the reference implementation of PIP
 in PINTOS.  This fact, however, is important for an efficient
 implementation of PIP, because we can give the lock to the thread
 with the highest priority so that it terminates more quickly.  We
-were also being able to generalise the scheduler of Sha et
+are also being able to generalise the scheduler of Sha et
 al.~\cite{Sha90} to the practically relevant case where critical
 sections can overlap; see Figure~\ref{overlap} \emph{a)} below for
 an example of this restriction. In the existing literature there is
 no proof and also no proving method that cover this generalised
 case.
 \noindent
 whereby threads, priorities and (critical) resources are represented
 as natural numbers. The event @{term Set} models the situation that
 a thread obtains a new priority given by the programmer or
-user (for example via the {\tt nice} utility under UNIX).  As in Paulson's work, we
+user (for example via the {\tt nice} utility under UNIX).  For states
-need to define functions that allow us to make some observations
+we define the following type-synonym:
-about states.  One, called @{term threads}, calculates the set of
-``live'' threads that we have seen so far:
+\begin{isabelle}\ \ \ \ \ %%%
+\isacommand{type\_synonym} @{text "state = event list"}
+\end{isabelle}
+\noindent As in Paulson's work, we need to define functions that
+allow us to make some observations about states.  One function,
+called @{term threads}, calculates the set of ``live'' threads that
+we have seen so far in a state:
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{lcl}
 @{thm (lhs) threads.simps(1)} & @{text "\<equiv>"} &
 @{thm (rhs) threads.simps(1)}\\
 advantages in practice. On the contrary, according to their work having a policy
 like our FIFO-scheduling of threads with equal priority reduces the number of
 tasks involved in the inheritance process and thus minimises the number
 of potentially expensive thread-switches.
-We will also need counters for @{term P} and @{term V} events of a thread @{term th}
+{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
 in a state @{term s}. This can be straightforwardly defined in Isabelle as
 \begin{isabelle}\ \ \ \ \ %%%
 \mbox{\begin{tabular}{@ {}l}
 @{thm cntP_def}\\
 \noindent
 If there is no cycle, then every RAG can be pictured as a forrest of trees, as
 for example in Figure~\ref{RAGgraph}.
-We will design our scheduler
+While there are few formalisations for graphs already implemented in
+Isabelle, we choose to introduce our own library of graphs for
+PIP. The reason for this is that we wanted to be able to reason with
+potentially infinite graphs (in the sense of infinitely branching
+and infinite size): the property that our RAGs are forrests of
+finitely branching trees having only an finite depth should be a
+something we can \emph{prove} for our model of PIP---it should not
+be an assumption we build already into our model. It seemed  for our purposes the most convenient
+represeantation of graphs are binary relations given by
+sets of pairs. The pairs stand for the edges in graphs. This
+relation-based representation is convenient since we can use the notions
+of transitive closure operations @{term "trancl DUMMY"} and
+@{term "rtrancl DUMMY"}, as well as relation composition @{term "DUMMY O DUMMY"}.
+A \emph{forrest} is defined as the relation @{text rel} that is \emph{single valued}
+and \emph{acyclic}:
+\begin{isabelle}\ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+@{thm single_valued_def[where ?r="rel", THEN eq_reflection]}\\
+@{thm acyclic_def[where ?r="rel", THEN eq_reflection]}
+\end{tabular}
+\end{isabelle}
+\noindent
+The \emph{children}, \emph{subtree} and \emph{ancestors} of a node in a graph are
+defined as
+\begin{isabelle}\ \ \ \ \ %%%
+\begin{tabular}{@ {}l}
+@{thm children_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
+@{thm subtree_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
+@{thm ancestors_def[where ?r="rel" and ?x="node", THEN eq_reflection]}\\
+\end{tabular}
+\end{isabelle}
+\noindent Note that forests can have trees with infinte depth and
+containing nodes with infinitely many children.  A \emph{finite
+forrest} is a forest which is well-founded and every node has
+finitely many children (is only finitely branching).
+We will design our PIP-scheduler
 so that every thread can be in the possession of several resources, that is
 it has potentially several incoming holding edges in the RAG, but has at most one outgoing
 waiting edge. The reason is that when a thread asks for resource that is locked
 already, then the thread is blocked and cannot ask for another resource.
 Clearly, also every resource can only have at most one outgoing holding edge---indicating

changeset 135	9b5da0327d43
parent 134	8a13b37b4d95
child 136	fb3f52fe99d1