Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Journal/Paper.thy
changeset 179 f9e6c4166476
parent 178 da27bece9575
child 180 cfd17cb339d1
equal deleted inserted replaced
178:da27bece9575 179:f9e6c4166476 
    34   Prc ("'(_, _')") and
 
    34   Prc ("'(_, _')") and
 
    35   holding_raw ("holds") and
 
    35   holding_raw ("holds") and
 
    36   holding ("holds") and
 
    36   holding ("holds") and
 
    37   waiting_raw ("waits") and
 
    37   waiting_raw ("waits") and
 
    38   waiting ("waits") and
 
    38   waiting ("waits") and
 
    39   dependants_raw ("dependants") and
 
    39   tG_raw ("TDG") and
 
    40   dependants ("dependants") and
 
    40   tG ("TDG") and
 
    41   RAG_raw ("RAG") and
 
    41   RAG_raw ("RAG") and
 
    42   RAG ("RAG") and
 
    42   RAG ("RAG") and
 
    43   Th ("T") and
 
    43   Th ("T") and
 
    44   Cs ("C") and
 
    44   Cs ("C") and
 
    45   readys ("ready") and
 
    45   readys ("ready") and
 
   457   %\endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
 
   457   %\endnote{{\bf NEEDED?} We will also need counters for @{term P} and @{term V} events of a thread @{term th}
 
   458   %in a state @{term s}. This can be straightforwardly defined in Isabelle as
 
   458   %in a state @{term s}. This can be straightforwardly defined in Isabelle as
 
   459   %
 
   459   %
 
   460   %\begin{isabelle}\ \ \ \ \ %%%
 
   460   %\begin{isabelle}\ \ \ \ \ %%%
 
   461   %\mbox{\begin{tabular}{@ {}l}
 
   461   %\mbox{\begin{tabular}{@ {}l}
 
   462   %@{thm cntP_def}\\
 
   462   %@ {thm cntP_def}\\
 
   463   %@{thm cntV_def}
 
   463   %@ {thm cntV_def}
 
   464   %\end{tabular}}
 
   464   %\end{tabular}}
 
   465   %\end{isabelle}
 
   465   %\end{isabelle}
 
   466   % 
   466   % 
   467   %\noindent using the predefined function @{const count} for lists.}
 
   467   %\noindent using the predefined function @{const count} for lists.}
 
   468 
   468 
   621   only have at most one outgoing holding edge---indicating that the
 
   621   only have at most one outgoing holding edge---indicating that the
 
   622   resource is locked. So if the @{text "RAG"} is well-founded and
 
   622   resource is locked. So if the @{text "RAG"} is well-founded and
 
   623   finite, we can always start at a thread waiting for a resource and
 
   623   finite, we can always start at a thread waiting for a resource and
 
   624   ``chase'' outgoing arrows leading to a single root of a tree.
 
   624   ``chase'' outgoing arrows leading to a single root of a tree.
 
   625   
   625   
   626   The use of relations for representing RAGs allows us to conveniently define
 
   626   The use of relations for representing @{text RAG}s allows us to conveniently define
 
   627   the notion of the \emph{dependants} of a thread
 
   627   the \emph{thread dependants graph} 
   628 
   628 
   629   \begin{isabelle}\ \ \ \ \ %%%
 
   629   \begin{isabelle}\ \ \ \ \ %%%
 
   630   @{thm dependants_raw_def}\hfill\numbered{dependants}
 
   630   @{thm tG_raw_def}\\
 
   631   \end{isabelle}
 
   631   \mbox{}\hfill\numbered{dependants}
 
   632 
   632   \end{isabelle}
 
   633   \noindent This definition needs to account for all threads that wait
 
   633 
   634   for a thread to release a resource. This means we need to include
 
   634   \noindent This definition represents all threads in a @{text RAG} that wait
 
   635   threads that transitively wait for a resource to be released (in the
 
   635   for a thread to release a resource, but the resource is ``hidden''. 
   636   picture above this means the dependants of @{text "th\<^sub>0"} are
 
   636   In the
 
   637   @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which wait for
 
   637   picture above this means the @{text TDG} connects @{text "th\<^sub>0"} with
 
   638   resource @{text "cs\<^sub>1"}, but also @{text "th\<^sub>3"}, which
 
   638   @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, which both wait for
 
   639   cannot make any progress unless @{text "th\<^sub>2"} makes progress,
 
   639   resource @{text "cs\<^sub>1"}; and @{text "th\<^sub>2"} with @{text "th\<^sub>3"}, which
 
   640   which in turn needs to wait for @{text "th\<^sub>0"} to finish). If
 
   640   cannot make any progress unless @{text "th\<^sub>2"} makes progress. 
   641   there is a circle of dependencies in a RAG, then clearly we have a
 
   641   Similarly for the other threads.
 
       
   642   If
 
       
   643   there is a circle of dependencies in a @{text RAG} (and thus @{text TDG}), then clearly we have a
 
   642   deadlock. Therefore when a thread requests a resource, we must
 
   644   deadlock. Therefore when a thread requests a resource, we must
 
   643   ensure that the resulting RAG is not circular. In practice, the
 
   645   ensure that the resulting @{text RAG} and @{text TDG} are not circular. In practice, the
 
   644   programmer has to ensure this. Our model will enforce that critical 
   646   programmer has to ensure this. Our model will enforce that critical 
   645   resources can only be requested provided no circularity can arise.
 
   647   resources can only be requested provided no circularity can arise.
 
   646 
   648 
   647   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   649   Next we introduce the notion of the \emph{current precedence} of a thread @{text th} in a 
   648   state @{text s}. It is defined as
 
   650   state @{text s}. It is defined as
 
   649 
   651 
   650   \begin{isabelle}\ \ \ \ \ %%%
 
   652   \begin{isabelle}\ \ \ \ \ %%%
 
   651   @{thm cpreced_def3}\hfill\numbered{cpreced}
 
   653   @{thm cpreced_def}
 
   652   \end{isabelle}
 
   654   \hfill\numbered{cpreced}
 
   653 
   655   \end{isabelle}
 
   654    \noindent where the dependants of @{text th} are given by the
 
   656 
   655   waiting queue function.  While the precedence @{term prec} of any
 
   657    \noindent 
       
   658   While the precedence @{term prec} of any
 
   656   thread is determined statically (for example when the thread is
 
   659   thread is determined statically (for example when the thread is
 
   657   created), the point of the current precedence is to dynamically
 
   660   created), the point of the current precedence is to dynamically
 
   658   increase this precedence, if needed according to PIP. Therefore the
 
   661   increase this precedence, if needed according to PIP. Therefore the
 
   659   current precedence of @{text th} is given as the maximum of the
 
   662   current precedence of @{text th} is given as the maximum of the
 
   660   precedence of @{text th} \emph{and} all threads that are dependants
 
   663   precedence of @{text th} \emph{and} all threads that are dependants
 
   661   of @{text th} in the state @{text s}. Since the notion @{term
 
   664   of @{text th} in the state @{text s}. Since the notion of current precedence is defined as the 
   662   "dependants"} is defined as the transitive closure of all dependent
 
   665   transitive closure of the dependent
 
   663   threads, we deal correctly with the problem in the informal
 
   666   threads in the @{text TDG}, we deal correctly with the problem in the informal
 
   664   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 
   667   algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 
   665   lowered prematurely (see Introduction). We again introduce an abbreviation for current
 
   668   lowered prematurely (see Introduction). We again introduce an abbreviation for current
 
   666   precedeces of a set of threads, written @{text "cprecs wq s ths"}.
 
   669   precedeces of a set of threads, written @{text "cprecs wq s ths"}.
 
   667   
   670   
   668   \begin{isabelle}\ \ \ \ \ %%%
 
   671   \begin{isabelle}\ \ \ \ \ %%%
 
   779   \end{tabular}
 
   782   \end{tabular}
 
   780   \end{isabelle}
 
   783   \end{isabelle}
 
   781 
   784 
   782   Having the scheduler function @{term schs} at our disposal, we can
 
   785   Having the scheduler function @{term schs} at our disposal, we can
 
   783   ``lift'', or overload, the notions @{term waiting}, @{term holding},
 
   786   ``lift'', or overload, the notions @{term waiting}, @{term holding},
 
   784   @{term RAG}, @{term dependants} and @{term cp} to operate on states
 
   787   @{term RAG}, %%@ {term dependants} 
   785   only.
 
   788   and @{term cp} to operate on states only.
 
   786 
   789 
   787   \begin{isabelle}\ \ \ \ \ %%%
 
   790   \begin{isabelle}\ \ \ \ \ %%%
 
   788   \begin{tabular}{@ {}rcl}
 
   791   \begin{tabular}{@ {}rcl}
 
   789   @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\
 
   792   @{thm (lhs) s_holding_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_holding_abv[simplified wq_def]}\\
 
   790   @{thm (lhs) s_waiting_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv[simplified wq_def]}\\
 
   793   @{thm (lhs) s_waiting_abv}  & @{text "\<equiv>"} & @{thm (rhs) s_waiting_abv[simplified wq_def]}\\
 
   791   @{thm (lhs) s_RAG_abv}      & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv[simplified wq_def]}\\
 
   794   @{thm (lhs) s_RAG_abv}      & @{text "\<equiv>"} & @{thm (rhs) s_RAG_abv[simplified wq_def]}\\
 
   792   @{thm (lhs) s_dependants_abv}& @{text "\<equiv>"} & @{thm (rhs) s_dependants_abv[simplified wq_def]}\\
 
   795   @{thm (lhs) s_tG_abv}& @{text "\<equiv>"} & @{thm (rhs) s_tG_abv[simplified wq_def]}\\
 
   793   @{thm (lhs) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\  
   796   @{thm (lhs) cp_def}         & @{text "\<equiv>"} & @{thm (rhs) cp_def}\\  
   794   \end{tabular}
 
   797   \end{tabular}
 
   795   \end{isabelle}
 
   798   \end{isabelle}
 
   796 
   799 
   797   \noindent
 
   800   \noindent
 
   798   With these abbreviations in place we can derive for every valid trace @{text s} 
   801   With these abbreviations in place we can derive for every valid trace @{text s} 
   799   the following two facts about  @{term dependants} and @{term cprec} (see \eqref{dependants} 
   802   the following two facts about  ???????
 
   800   and \eqref{cpreced}): Given @{thm (prem 1) valid_trace.cp_alt_def}, then 
   803   %@ {term dependants} 
       
   804   and @{term cprec} (see \eqref{dependants} 
       
   805   and \eqref{cpreced}): Given ????? %@ {thm (prem 1) valid_trace.cp_alt_def}, 
       
   806   then 
   801 
   807 
   802   \begin{isabelle}\ \ \ \ \ %%%
 
   808   \begin{isabelle}\ \ \ \ \ %%%
 
   803   \begin{tabular}{@ {}rcl}
 
   809   \begin{tabular}{@ {}rcl}
 
   804   @{thm (concl) valid_trace.cp_alt_def3}\\
 
   810   @{thm tG_alt_def}\\
 
       
   811   @{thm cp_s_def}\\
 
   805   \end{tabular}\hfill\numbered{overloaded}
 
   812   \end{tabular}\hfill\numbered{overloaded}
 
   806   \end{isabelle}
 
   813   \end{isabelle}
 
   807 
   814 
   808 
   815 
   809   can introduce 
   816   can introduce 
  1837   @{text th} in the @{term RAG} (and waiting for @{text th} to release
 
  1844   @{text th} in the @{term RAG} (and waiting for @{text th} to release
 
  1838   a resource). We can prove the following lemma.
 
  1845   a resource). We can prove the following lemma.
 
  1839 
  1846 
  1840   \begin{center}
 
  1847   \begin{center}
 
  1841   @{thm tG_alt_def}\\
 
  1848   @{thm tG_alt_def}\\
 
  1842   @{thm dependants_alt_tG} 
  1849   ???? %@ {thm dependants_alt_tG} 
  1843   \end{center}
 
  1850   \end{center}
 
  1844 
  1851 
  1845   \begin{center}
 
  1852   \begin{center}
 
  1846   @{thm valid_trace.cp_alt_def3} 
  1853   ???? %@ {thm valid_trace.cp_alt_def3} 
  1847   \end{center}
 
  1854   \end{center}
 
  1848 
  1855 
  1849 
  1856 
  1850   \begin{lemma}\label{childrenlem}
 
  1857   \begin{lemma}\label{childrenlem}
 
  1851   HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
 
  1858   HERE %@ {text "If"} @ {thm (prem 1) cp_rec} @{text "then"}
pip