510 subsection {* Event @{text "V th cs"} *}

   511 

   512 (*<*)

   513 context step_v_cps_nt

   514 begin

   515 (*>*)

   516 

   517 text {*

   518   The context under which event @{text "V th cs"} happens is formalized as follows:

   519   \begin{enumerate}

   520     \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.

   521     \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 

   522       event @{text "V th cs"} is eligible to happen under state @{term "s'"} and

   523       state @{term "s'"} is a valid state.

   524   \end{enumerate}

   525   *}

   526 

   527 text {* \noindent

   528   Under such a context, we investigated how the current precedence @{term "cp"} of 

   529   threads change from state @{term "s'"} to @{term "s"}. 

   530 

   531 

   532   Two subcases are considerted, 

   533   where the first is that there exits @{term "th'"} 

   534   such that 

   535   @{thm [display] nt} 

   536   holds, which means there exists a thread @{term "th'"} to take over

   537   the resource release by thread @{term "th"}. 

   538   In this sub-case, the following results are obtained:

   539   \begin{enumerate}

   540   \item The change of RAG is given by lemma @{text "depend_s"}: 

   541   @{thm [display] "depend_s"}

   542   which shows two edges are removed while one is added. These changes imply how

   543   the current precedences should be re-computed.

   544   \item First all threads different from @{term "th"} and @{term "th'"} have their

   545   @{term "cp"}-value kept, therefore do not need a re-computation

   546   (@{text "cp_kept"}): @{thm [display] cp_kept}

   547   This lemma also implies, only the @{term "cp"}-values of @{term "th"} and @{term "th'"}

   548   need to be recomputed.

   549   \end{enumerate}

   550   *}

   551 

   552 (*<*)

   553 end

   554 

   555 context step_v_cps_nnt

   556 begin

   557 (*>*)

   558 

   559 text {*

   560   The other sub-case is when for all @{text "th'"}

   561   @{thm [display] nnt}

   562   holds, no such thread exists. The following results can be obtained for this 

   563   sub-case:

   564   \begin{enumerate}

   565   \item The change of RAG is given by lemma @{text "depend_s"}:

   566   @{thm [display] depend_s}

   567   which means only one edge is removed.

   568   \item In this case, no re-computation is needed (@{text "eq_cp"}):

   569   @{thm [display] eq_cp}

   570   \end{enumerate}

   571   *}

   572 

   573 (*<*)

   574 end

   575 (*>*)

   576 

   577 

   578 subsection {* Event @{text "P th cs"} *}

   579 

   580 (*<*)

   581 context step_P_cps_e

   582 begin

   583 (*>*)

   584 

   585 text {*

   586   The context under which event @{text "P th cs"} happens is formalized as follows:

   587   \begin{enumerate}

   588     \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.

   589     \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 

   590       event @{text "P th cs"} is eligible to happen under state @{term "s'"} and

   591       state @{term "s'"} is a valid state.

   592   \end{enumerate}

   593 

   594   This case is further divided into two sub-cases. The first is when @{thm ee} holds.

   595   The following results can be obtained:

   596   \begin{enumerate}

   597   \item One edge is added to the RAG (@{text "depend_s"}):

   598     @{thm [display] depend_s}

   599   \item No re-computation is needed (@{text "eq_cp"}):

   600     @{thm [display] eq_cp}

   601   \end{enumerate}

   602 *}

   603 

   604 (*<*)

   605 end

   606 

   607 context step_P_cps_ne

   608 begin

   609 (*>*)

   610 

   611 text {*

   612   The second is when @{thm ne} holds.

   613   The following results can be obtained:

   614   \begin{enumerate}

   615   \item One edge is added to the RAG (@{text "depend_s"}):

   616     @{thm [display] depend_s}

   617   \item Threads with no dependence relation with @{term "th"} do not need a re-computation

   618     of their @{term "cp"}-values (@{text "eq_cp"}):

   619     @{thm [display] eq_cp}

   620     This lemma implies all threads with a dependence relation with @{term "th"} may need 

   621     re-computation.

   622   \item Similar to the case of @{term "Set"}, the computation procedure could stop earlier

   623     (@{text "eq_up"}):

   624     @{thm [display] eq_up}

   625   \end{enumerate}

   626 

   627   *}

   628 

   629 (*<*)

   630 end

   631 (*>*)

   632 

   633 subsection {* Event @{text "Create th prio"} *}

   634 

   635 (*<*)

   636 context step_create_cps

   637 begin

   638 (*>*)

   639 

   640 text {*

   641   The context under which event @{text "Create th prio"} happens is formalized as follows:

   642   \begin{enumerate}

   643     \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.

   644     \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 

   645       event @{text "Create th prio"} is eligible to happen under state @{term "s'"} and

   646       state @{term "s'"} is a valid state.

   647   \end{enumerate}

   648   The following results can be obtained under this context:

   649   \begin{enumerate}

   650   \item The RAG does not change (@{text "eq_dep"}):

   651     @{thm [display] eq_dep}

   652   \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):

   653     @{thm [display] eq_cp}

   654   \item The @{term "cp"}-value of @{term "th"} equals its precedence 

   655     (@{text "eq_cp_th"}):

   656     @{thm [display] eq_cp_th}

   657   \end{enumerate}

   658 

   659 *}

   660 

   661 

   662 (*<*)

   663 end

   664 (*>*)

   665 

   666 subsection {* Event @{text "Exit th"} *}

   667 

   668 (*<*)

   669 context step_exit_cps

   670 begin

   671 (*>*)

   672 

   673 text {*

   674   The context under which event @{text "Exit th"} happens is formalized as follows:

   675   \begin{enumerate}

   676     \item The formation of @{term "s"} (@{text "s_def"}): @{thm s_def}.

   677     \item State @{term "s"} is a valid state (@{text "vt_s"}): @{thm vt_s}. This implies 

   678       event @{text "Exit th"} is eligible to happen under state @{term "s'"} and

   679       state @{term "s'"} is a valid state.

   680   \end{enumerate}

   681   The following results can be obtained under this context:

   682   \begin{enumerate}

   683   \item The RAG does not change (@{text "eq_dep"}):

   684     @{thm [display] eq_dep}

   685   \item All threads other than @{term "th"} do not need re-computation (@{text "eq_cp"}):

   686     @{thm [display] eq_cp}

   687   \end{enumerate}

   688   Since @{term th} does not live in state @{term "s"}, there is no need to compute 

   689   its @{term cp}-value.

   690 *}

   691 

   692 (*<*)

   693 end

   694 (*>*)

   695 

   696