prio/Paper/Paper.thy
changeset 264 24199eb2c423
parent 262 4190df6f4488
child 265 993068ce745f
equal deleted inserted replaced
263:f1e6071a4613 264:24199eb2c423
     1 (*<*)
     1 (*<*)
     2 theory Paper
     2 theory Paper
     3 imports CpsG ExtGG
     3 imports CpsG ExtGG LaTeXsugar
     4 begin
     4 begin
     5 (*>*)
     5 (*>*)
     6 
     6 
     7 section {* Introduction *}
     7 section {* Introduction *}
     8 
     8 
   111 text {*
   111 text {*
   112   \input{../../generated/PrioGDef}
   112   \input{../../generated/PrioGDef}
   113 *}
   113 *}
   114 
   114 
   115 section {* General properties of Priority Inheritance \label{general} *}
   115 section {* General properties of Priority Inheritance \label{general} *}
       
   116 (*<*)
       
   117 ML {*
       
   118   val () = show_question_marks_default := false;
       
   119 *}
       
   120 (*>*)
       
   121 
       
   122 text {*
       
   123   The following are several very basic prioprites:
       
   124   \begin{enumerate}
       
   125   \item All runing threads must be ready (@{text "runing_ready"}):
       
   126           @{thm[display] "runing_ready"}  
       
   127   \item All ready threads must be living (@{text "readys_threads"}):
       
   128           @{thm[display] "readys_threads"} 
       
   129   \item There are finite many living threads at any moment (@{text "finite_threads"}):
       
   130           @{thm[display] "finite_threads"} 
       
   131   \item Every waiting queue does not contain duplcated elements (@{text "wq_distinct"}): 
       
   132           @{thm[display] "wq_distinct"} 
       
   133   \item All threads in waiting queues are living threads (@{text "wq_threads"}): 
       
   134           @{thm[display] "wq_threads"} 
       
   135   \item The event which can get a thread into waiting queue must be @{term "P"}-events
       
   136          (@{text "block_pre"}): 
       
   137           @{thm[display] "block_pre"}   
       
   138   \item A thread may never wait for two different critical resources
       
   139          (@{text "waiting_unique"}): 
       
   140           @{thm[display] waiting_unique[of _ _ "cs\<^isub>1" "cs\<^isub>2"]}
       
   141   \item Every resource can only be held by one thread
       
   142          (@{text "held_unique"}): 
       
   143           @{thm[display] held_unique[of _ "th\<^isub>1" _ "th\<^isub>2"]}
       
   144   \item Every living thread has an unique precedence
       
   145          (@{text "preced_unique"}): 
       
   146           @{thm[display] preced_unique[of "th\<^isub>1" _ "th\<^isub>2"]}
       
   147   \end{enumerate}
       
   148 *}
       
   149 
       
   150 text {* \noindent
       
   151   The following lemmas show how RAG is changed with the execution of events:
       
   152   \begin{enumerate}
       
   153   \item Execution of @{term "Set"} does not change RAG (@{text "depend_set_unchanged"}):
       
   154     @{thm[display] depend_set_unchanged}
       
   155   \item Execution of @{term "Create"} does not change RAG (@{text "depend_create_unchanged"}):
       
   156     @{thm[display] depend_create_unchanged}
       
   157   \item Execution of @{term "Exit"} does not change RAG (@{text "depend_exit_unchanged"}):
       
   158     @{thm[display] depend_exit_unchanged}
       
   159   \item Execution of @{term "P"} (@{text "step_depend_p"}):
       
   160     @{thm[display] step_depend_p}
       
   161   \item Execution of @{term "V"} (@{text "step_depend_v"}):
       
   162     @{thm[display] step_depend_v}
       
   163   \end{enumerate}
       
   164   *}
       
   165 
       
   166 text {* \noindent
       
   167   These properties are used to derive the following important results about RAG:
       
   168   \begin{enumerate}
       
   169   \item RAG is loop free (@{text "acyclic_depend"}):
       
   170   @{thm [display] acyclic_depend}
       
   171   \item RAGs are finite (@{text "finite_depend"}):
       
   172   @{thm [display] finite_depend}
       
   173   \item Reverse paths in RAG are well founded (@{text "wf_dep_converse"}):
       
   174   @{thm [display] wf_dep_converse}
       
   175   \item The dependence relation represented by RAG has a tree structure (@{text "unique_depend"}):
       
   176   @{thm [display] unique_depend[of _ _ "n\<^isub>1" "n\<^isub>2"]}
       
   177   \item All threads in RAG are living threads 
       
   178     (@{text "dm_depend_threads"} and @{text "range_in"}):
       
   179     @{thm [display] dm_depend_threads range_in}
       
   180   \end{enumerate}
       
   181   *}
       
   182 
       
   183 text {* \noindent
       
   184   The following lemmas show how every node in RAG can be chased to ready threads:
       
   185   \begin{enumerate}
       
   186   \item Every node in RAG can be chased to a ready thread (@{text "chain_building"}):
       
   187     @{thm [display] chain_building[rule_format]}
       
   188   \item The ready thread chased to is unique (@{text "dchain_unique"}):
       
   189     @{thm [display] dchain_unique[of _ _ "th\<^isub>1" "th\<^isub>2"]}
       
   190   \end{enumerate}
       
   191   *}
       
   192 
       
   193 text {* \noindent
       
   194   Properties about @{term "next_th"}:
       
   195   \begin{enumerate}
       
   196   \item The thread taking over is different from the thread which is releasing
       
   197   (@{text "next_th_neq"}):
       
   198   @{thm [display] next_th_neq}
       
   199   \item The thread taking over is unique
       
   200   (@{text "next_th_unique"}):
       
   201   @{thm [display] next_th_unique[of _ _ _ "th\<^isub>1" "th\<^isub>2"]}  
       
   202   \end{enumerate}
       
   203   *}
       
   204 
       
   205 text {* \noindent
       
   206   Some deeper results about the system:
       
   207   \begin{enumerate}
       
   208   \item There can only be one running thread (@{text "runing_unique"}):
       
   209   @{thm [display] runing_unique[of _ "th\<^isub>1" "th\<^isub>2"]}
       
   210   \item The maximum of @{term "cp"} and @{term "preced"} are equal (@{text "max_cp_eq"}):
       
   211   @{thm [display] max_cp_eq}
       
   212   \item There must be one ready thread having the max @{term "cp"}-value 
       
   213   (@{text "max_cp_readys_threads"}):
       
   214   @{thm [display] max_cp_readys_threads}
       
   215   \end{enumerate}
       
   216   *}
       
   217 
       
   218 text {* \noindent
       
   219   The relationship between the count of @{text "P"} and @{text "V"} and the number of 
       
   220   critical resources held by a thread is given as follows:
       
   221   \begin{enumerate}
       
   222   \item The @{term "V"}-operation decreases the number of critical resources 
       
   223     one thread holds (@{text "cntCS_v_dec"})
       
   224      @{thm [display]  cntCS_v_dec}
       
   225   \item The number of @{text "V"} never exceeds the number of @{text "P"} 
       
   226     (@{text "cnp_cnv_cncs"}):
       
   227     @{thm [display]  cnp_cnv_cncs}
       
   228   \item The number of @{text "V"} equals the number of @{text "P"} when 
       
   229     the relevant thread is not living:
       
   230     (@{text "cnp_cnv_eq"}):
       
   231     @{thm [display]  cnp_cnv_eq}
       
   232   \item When a thread is not living, it does not hold any critical resource 
       
   233     (@{text "not_thread_holdents"}):
       
   234     @{thm [display] not_thread_holdents}
       
   235   \item When the number of @{text "P"} equals the number of @{text "V"}, the relevant 
       
   236     thread does not hold any critical resource, therefore no thread can depend on it
       
   237     (@{text "count_eq_dependents"}):
       
   238     @{thm [display] count_eq_dependents}
       
   239   \end{enumerate}
       
   240   *}
   116 
   241 
   117 section {* Key properties \label{extension} *}
   242 section {* Key properties \label{extension} *}
   118 
   243 
       
   244 (*<*)
       
   245 context extend_highest_gen
       
   246 begin
       
   247 (*>*)
       
   248 
       
   249 text {*
       
   250   The essential of {\em Priority Inheritance} is to avoid indefinite priority inversion. For this 
       
   251   purpose, we need to investigate what happens after one thread takes the highest precedence. 
       
   252   A locale is used to describe such a situation, which assumes:
       
   253   \begin{enumerate}
       
   254   \item @{term "s"} is a valid state (@{text "vt_s"}):
       
   255     @{thm  vt_s}.
       
   256   \item @{term "th"} is a living thread in @{term "s"} (@{text "threads_s"}):
       
   257     @{thm threads_s}.
       
   258   \item @{term "th"} has the highest precedence in @{term "s"} (@{text "highest"}):
       
   259     @{thm highest}.
       
   260   \item The precedence of @{term "th"} is @{term "Prc prio tm"} (@{text "preced_th"}):
       
   261     @{thm preced_th}.
       
   262   \end{enumerate}
       
   263   *}
       
   264 
       
   265 text {* \noindent
       
   266   Under these assumptions, some basic priority can be derived for @{term "th"}:
       
   267   \begin{enumerate}
       
   268   \item The current precedence of @{term "th"} equals its own precedence (@{text "eq_cp_s_th"}):
       
   269     @{thm [display] eq_cp_s_th}
       
   270   \item The current precedence of @{term "th"} is the highest precedence in 
       
   271     the system (@{text "highest_cp_preced"}):
       
   272     @{thm [display] highest_cp_preced}
       
   273   \item The precedence of @{term "th"} is the highest precedence 
       
   274     in the system (@{text "highest_preced_thread"}):
       
   275     @{thm [display] highest_preced_thread}
       
   276   \item The current precedence of @{term "th"} is the highest current precedence 
       
   277     in the system (@{text "highest'"}):
       
   278     @{thm [display] highest'}
       
   279   \end{enumerate}
       
   280   *}
       
   281 
       
   282 text {* \noindent
       
   283   To analysis what happens after state @{term "s"} a sub-locale is defined, which 
       
   284   assumes:
       
   285   \begin{enumerate}
       
   286   \item @{term "t"} is a valid extension of @{term "s"} (@{text "vt_t"}): @{thm vt_t}.
       
   287   \item Any thread created in @{term "t"} has priority no higher than @{term "prio"}, therefore
       
   288     its precedence can not be higher than @{term "th"},  therefore
       
   289     @{term "th"} remain to be the one with the highest precedence
       
   290     (@{text "create_low"}):
       
   291     @{thm [display] create_low}
       
   292   \item Any adjustment of priority in 
       
   293     @{term "t"} does not happen to @{term "th"} and 
       
   294     the priority set is no higher than @{term "prio"}, therefore
       
   295     @{term "th"} remain to be the one with the highest precedence (@{text "set_diff_low"}):
       
   296     @{thm [display] set_diff_low}
       
   297   \item Since we are investigating what happens to @{term "th"}, it is assumed 
       
   298     @{term "th"} does not exit during @{term "t"} (@{text "exit_diff"}):
       
   299     @{thm [display] exit_diff}
       
   300   \end{enumerate}
       
   301 *}
       
   302 
       
   303 text {* \noindent
       
   304   All these assumptions are put into a predicate @{term "extend_highest_gen"}. 
       
   305   It can be proved that @{term "extend_highest_gen"} holds 
       
   306   for any moment @{text "i"} in it @{term "t"} (@{text "red_moment"}):
       
   307   @{thm [display] red_moment}
       
   308   
       
   309   From this, an induction principle can be derived for @{text "t"}, so that 
       
   310   properties already derived for @{term "t"} can be applied to any prefix 
       
   311   of @{text "t"} in the proof of new properties 
       
   312   about @{term "t"} (@{text "ind"}):
       
   313   \begin{center}
       
   314   @{thm[display] ind}
       
   315   \end{center}
       
   316 
       
   317   The following properties can be proved about @{term "th"} in @{term "t"}:
       
   318   \begin{enumerate}
       
   319   \item In @{term "t"}, thread @{term "th"} is kept live and its 
       
   320     precedence is preserved as well
       
   321     (@{text "th_kept"}): 
       
   322     @{thm [display] th_kept}
       
   323   \item In @{term "t"}, thread @{term "th"}'s precedence is always the maximum among 
       
   324     all living threads
       
   325     (@{text "max_preced"}): 
       
   326     @{thm [display] max_preced}
       
   327   \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum precedence
       
   328     among all living threads
       
   329     (@{text "th_cp_max_preced"}): 
       
   330     @{thm [display] th_cp_max_preced}
       
   331   \item In @{term "t"}, thread @{term "th"}'s current precedence is always the maximum current 
       
   332     precedence among all living threads
       
   333     (@{text "th_cp_max"}): 
       
   334     @{thm [display] th_cp_max}
       
   335   \item In @{term "t"}, thread @{term "th"}'s current precedence equals its precedence at moment 
       
   336     @{term "s"}
       
   337     (@{text "th_cp_preced"}): 
       
   338     @{thm [display] th_cp_preced}
       
   339   \end{enumerate}
       
   340   *}
       
   341 
       
   342 text {* \noindent
       
   343   The main theorem is to characterizing the running thread during @{term "t"} 
       
   344   (@{text "runing_inversion_2"}):
       
   345   @{thm [display] runing_inversion_2}
       
   346   According to this, if a thread is running, it is either @{term "th"} or was
       
   347   already live and held some resource 
       
   348   at moment @{text "s"} (expressed by: @{text "cntV s th' < cntP s th'"}).
       
   349 
       
   350   Since there are only finite many threads live and holding some resource at any moment,
       
   351   if every such thread can release all its resources in finite duration, then after finite
       
   352   duration, none of them may block @{term "th"} anymore. So, no priority inversion may happen
       
   353   then.
       
   354   *}
       
   355 
       
   356 (*<*)
       
   357 end
       
   358 (*>*)
       
   359 
   119 section {* Properties to guide implementation \label{implement} *}
   360 section {* Properties to guide implementation \label{implement} *}
       
   361 
       
   362 text {*
       
   363   The properties (especially @{text "runing_inversion_2"}) convinced us that model defined 
       
   364   in section \ref{model} does prevent indefinite priority inversion and therefore fulfills 
       
   365   the fundamental requirement of Priority Inheritance protocol. Another purpose of this paper 
       
   366   is to show how this model can be used to guide a concrete implementation.
       
   367   *}
       
   368 
   120 
   369 
   121 section {* Related works \label{related} *}
   370 section {* Related works \label{related} *}
   122 
   371 
   123 text {*
   372 text {*
   124   \begin{enumerate}
   373   \begin{enumerate}