Mercurial Mercurial > hg > regexp / 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.
prio/Paper/Paper.thy
changeset 291 5ef9f6ebe827
parent 290 6a6d0bd16035
child 292 1f16ff7fea94
equal deleted inserted replaced
290:6a6d0bd16035 291:5ef9f6ebe827 
    20   Cs ("C") and
 
    20   Cs ("C") and
 
    21   readys ("ready") and
 
    21   readys ("ready") and
 
    22   depend ("RAG") and 
    22   depend ("RAG") and 
    23   preced ("prec") and
 
    23   preced ("prec") and
 
    24   cpreced ("cprec") and
 
    24   cpreced ("cprec") and
 
       
    25   dependents ("dependants") and
 
       
    26   waiting_queue ("wq_fun") and
 
       
    27   cur_preced ("cprec_fun") and
 
    25   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 
    28   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 
    26 (*>*)
 
    29 (*>*)
 
    27 
    30 
    28 section {* Introduction *}
 
    31 section {* Introduction *}
 
    29 
    32 
   253   this choice would translate to a quite natural a FIFO-scheduling of processes with 
   256   this choice would translate to a quite natural a FIFO-scheduling of processes with 
   254   the same priority.
 
   257   the same priority.
 
   255 
   258 
   256   Next, we introduce the concept of \emph{waiting queues}. They are
 
   259   Next, we introduce the concept of \emph{waiting queues}. They are
 
   257   lists of threads associated with every resource. The first thread in
 
   260   lists of threads associated with every resource. The first thread in
 
   258   this list (the head, or short @{term hd}) is chosen to be in the one 
   261   this list (the head, or short @{term hd}) is chosen to be the one 
   259   that is in possession of the
 
   262   that is in possession of the
 
   260   ``lock'' of the corresponding resource. We model waiting queues as
 
   263   ``lock'' of the corresponding resource. We model waiting queues as
 
   261   functions, below abbreviated as @{text wq}, taking a resource as
 
   264   functions, below abbreviated as @{text wq}, taking a resource as
 
   262   argument and returning a list of threads.  This allows us to define
 
   265   argument and returning a list of threads.  This allows us to define
 
   263   when a thread \emph{holds}, respectively \emph{waits} for, a
 
   266   when a thread \emph{holds}, respectively \emph{waits} for, a
 
   270   \end{tabular}
 
   273   \end{tabular}
 
   271   \end{isabelle}
 
   274   \end{isabelle}
 
   272 
   275 
   273   \noindent
 
   276   \noindent
 
   274   In this definition we assume @{text "set"} converts a list into a set.
 
   277   In this definition we assume @{text "set"} converts a list into a set.
 
       
   278   At the beginning, that is in the state where no process is created yet, 
       
   279   the waiting queue function will be just the function that returns the
 
       
   280   empty list.
 
       
   281 
       
   282   \begin{isabelle}\ \ \ \ \ %%%
 
       
   283   @{abbrev all_unlocked}
 
       
   284   \end{isabelle}
 
       
   285 
       
   286   \noindent
 
   275   Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
   287   Using @{term "holding"} and @{term waiting}, we can introduce \emph{Resource Allocation Graphs} 
   276   (RAG), which represent the dependencies between threads and resources.
 
   288   (RAG), which represent the dependencies between threads and resources.
 
   277   We represent RAGs as relations using pairs of the form
 
   289   We represent RAGs as relations using pairs of the form
 
   278 
   290 
   279   \begin{isabelle}\ \ \ \ \ %%%
 
   291   \begin{isabelle}\ \ \ \ \ %%%
 
   293 
   305 
   294   \noindent
 
   306   \noindent
 
   295   An instance of a RAG is as follows:
 
   307   An instance of a RAG is as follows:
 
   296 
   308 
   297   \begin{center}
 
   309   \begin{center}
 
   298   Picture
 
   310   \begin{tikzpicture}[scale=1]
 
       
   311   \draw[step=2mm] (0,0) grid (3,2);
 
       
   312 
       
   313   \draw[rounded corners=1mm, very thick] (0,0) rectangle (0.6,0.6);
 
       
   314   \draw[rounded corners=1mm, very thick] (3,0) rectangle (3.6,0.6);
 
       
   315 
       
   316   \draw (0.3,0.3) node {\small$th_0$};
 
       
   317   \draw (3.3,0.3) node {\small$th_1$};
 
       
   318   \end{tikzpicture}
 
   299   \end{center}
 
   319   \end{center}
 
   300 
   320 
   301   \noindent
 
   321   \noindent
 
   302   The use or relations for representing RAGs allows us to conveninetly define
 
   322   The use or relations for representing RAGs allows us to conveninetly define
 
   303   the notion of the \emph{dependants} of a thread. This is defined as
 
   323   the notion of the \emph{dependants} of a thread. This is defined as
 
   310   This definition needs to account for all threads that wait for tread to
 
   330   This definition needs to account for all threads that wait for tread to
 
   311   release a resource. This means we need to include threads that transitively
 
   331   release a resource. This means we need to include threads that transitively
 
   312   wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"}, 
   332   wait for a resource being realeased (in the picture this means also @{text "th\<^isub>3"}, 
   313   which cannot make any progress unless @{text "th\<^isub>2"} makes progress which
 
   333   which cannot make any progress unless @{text "th\<^isub>2"} makes progress which
 
   314   in turn waits for @{text "th\<^isub>1"}). If there is a cirle in a RAG, then clearly
 
   334   in turn waits for @{text "th\<^isub>1"}). If there is a cirle in a RAG, then clearly
 
   315   we have a deadlock. Therefore when we state our correctness property for PIP
 
   335   we have a deadlock. Therefore when a thread requests a resource,
 
   316   we must ensure that RAGs are not circular. This allows us to define the notion
 
   336   we must ensure that the resulting RAG is not not circular. 
   317   of the \emph{current precedence} of a thread @{text th} in a state @{text s}.
 
   337 
   318 
   338   Next we introduce the notion of \emph{current precedence} for a thread @{text th} in a 
   319   \begin{isabelle}\ \ \ \ \ %%%
 
   339   state @{text s}, which is defined as
 
   320   @{thm cpreced_def2}\\
 
   340 
   321   \end{isabelle}
 
   341   \begin{isabelle}\ \ \ \ \ %%%
 
   322 
   342   @{thm cpreced_def2}
 
   323 
   343   \end{isabelle}
 
   324 
   344 
       
   345   \noindent
 
       
   346   While the precedence of a thread is determined by the programmer (for example when the thread is
 
       
   347   created), the point of the current precedence is to let scheduler increase this
 
       
   348   priority, if needed according to PIP. Therefore the current precedence of @{text th} is
 
       
   349   given as the maximum of the precedence @{text th} has in state @{text s} \emph{and} all 
       
   350   processes that are dependants of @{text th}. Since the notion @{term "dependents"} is
 
       
   351   defined as the transitive closure of all dependent threads, we deal correctly with the 
       
   352   problem in the algorithm by Sha et al.~\cite{Sha90} where a priority of a thread is
 
       
   353   lowered prematurely.
 
       
   354   
       
   355   The next function, called @{term schs}, defines the behaviour of the scheduler. It is defined
 
       
   356   by recursion on the state (a list of events); @{term "schs"} takes a state as argument
 
       
   357   and returns a \emph{schedule state}, which we defined as a record consisting of ...
 
       
   358 
       
   359   In the initial state, the scheduler starts with all resources unlocked and the
 
       
   360   precedence of every thread is initialised with @{term "Prc 0 0"}. 
       
   361 
       
   362   \begin{isabelle}\ \ \ \ \ %%%
 
       
   363   \begin{tabular}{@ {}l}
 
       
   364   @{thm (lhs) schs.simps(1)} @{text "\<equiv>"}\\ 
       
   365   \hspace{5mm}@{term "(|waiting_queue = all_unlocked, cur_preced = (\<lambda>_::thread. Prc 0 0)|)"}
 
       
   366   \end{tabular}
 
       
   367   \end{isabelle}
 
       
   368 
       
   369   \noindent
 
       
   370   The cases for @{term Create}, @{term Exit} and @{term Set} are straightforward:
 
       
   371   we calculuate the waiting queue function of the (previous) state @{text s}; 
       
   372   this waiting queue function @{text wq} is unchanged in the next schedule state; for calculuating 
       
   373   the next @{term "cprec_fun"} we use @{text wq} and the function @{term cpreced}. 
       
   374   This gives the following clauses:
 
       
   375 
       
   376   \begin{isabelle}\ \ \ \ \ %%%
 
       
   377   \begin{tabular}{@ {}l}
 
       
   378   @{thm (lhs) schs.simps(2)} @{text "\<equiv>"}\\ 
       
   379   \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
 
       
   380   \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Create th prio # s)|)"}\\
 
       
   381   @{thm (lhs) schs.simps(3)} @{text "\<equiv>"}\\
 
       
   382   \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
 
       
   383   \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Exit th # s)|)"}\smallskip\\
 
       
   384   @{thm (lhs) schs.simps(4)} @{text "\<equiv>"}\\ 
       
   385   \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
 
       
   386   \hspace{8mm}@{term "(|waiting_queue = wq\<iota>, cur_preced = cpreced wq\<iota> (Set th prio # s)|)"}
 
       
   387   \end{tabular}
 
       
   388   \end{isabelle}
 
       
   389 
       
   390   \noindent 
       
   391   More interesting are the cases when a resource, say @{text cs}, is locked or relaesed. In this case
 
       
   392   we need to calculate a new waiting queue function. In case of @{term P} we update
 
       
   393   the function so that the new thread list for @{text cs} is old thread list with the waiting 
       
   394   thread appended to the end (remember the head of this list is in the possession of the
 
       
   395   resource).
 
       
   396 
       
   397   \begin{isabelle}\ \ \ \ \ %%%
 
       
   398   \begin{tabular}{@ {}l}
 
       
   399   @{thm (lhs) schs.simps(5)} @{text "\<equiv>"}\\ 
       
   400   \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
 
       
   401   \hspace{5mm}@{text "let"} @{text "new_wq = wq(cs := (wq cs @ [th]))"} @{text "in"}\\
 
       
   402   \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (P th cs # s)|)"}
 
       
   403   \end{tabular}
 
       
   404   \end{isabelle}
 
       
   405 
       
   406   \noindent
 
       
   407   The case for @{term V} is similarly, except that we update the waiting queue function
 
       
   408   using the auxiliary definition
 
       
   409 
       
   410   \begin{isabelle}\ \ \ \ \ %%%
 
       
   411   @{abbrev release}
 
       
   412   \end{isabelle}
 
       
   413 
       
   414   \noindent
 
       
   415   This gives for @{term schs} the clause:
 
       
   416  
       
   417   \begin{isabelle}\ \ \ \ \ %%%
 
       
   418   \begin{tabular}{@ {}l}
 
       
   419   @{thm (lhs) schs.simps(6)} @{text "\<equiv>"}\\
 
       
   420   \hspace{5mm}@{text "let"} @{text "wq = waiting_queue (schs s)"} @{text "in"}\\
 
       
   421   \hspace{5mm}@{text "let"} @{text "new_wq = release (wq cs)"} @{text "in"}\\
 
       
   422   \hspace{8mm}@{term "(|waiting_queue = new_wq, cur_preced = cpreced new_wq (V th cs # s)|)"}
 
       
   423   \end{tabular}
 
       
   424   \end{isabelle}
 
       
   425 
       
   426 
       
   427   TODO
 
   325 
   428 
   326   \begin{isabelle}\ \ \ \ \ %%%
 
   429   \begin{isabelle}\ \ \ \ \ %%%
 
   327   \begin{tabular}{@ {}l}
 
   430   \begin{tabular}{@ {}l}
 
   328   @{thm s_depend_def}\\
 
   431   @{thm s_depend_def}\\
 
   329   \end{tabular}
 
   432   \end{tabular}
regexp