# HG changeset patch # User Christian Urban # Date 1458569257 0 # Node ID a4bb5525b7b62e8dd01cf6d4e73025a19a53fa25 # Parent 8a6125caead2f9b0e6e9428808d6a7aac6804a4b updated to Isabelle 2016 diff -r 8a6125caead2 -r a4bb5525b7b6 PIPDefs.thy --- a/PIPDefs.thy Sat Feb 13 17:18:51 2016 +0800 +++ b/PIPDefs.thy Mon Mar 21 14:07:37 2016 +0000 @@ -163,80 +163,94 @@ all threads in the waiting queue are considered as waiting for the resource. *} +(* consts holding :: "'b \ thread \ cs \ bool" waiting :: "'b \ thread \ cs \ bool" RAG :: "'b \ (node \ node) set" dependants :: "'b \ thread \ thread set" +*) -defs (overloaded) +definition -- {* \begin{minipage}{0.9\textwidth} - This meaning of @{text "wq"} is reflected in the following definition of @{text "holding wq th cs"}, - where @{text "holding wq th cs"} means thread @{text "th"} is holding the critical - resource @{text "cs"}. This decision is based on @{text "wq"}. + This meaning of @{text "wq"} is reflected in the following definition of + @{text "holding wq th cs"}, where @{text "holding wq th cs"} means thread + @{text "th"} is holding the critical resource @{text "cs"}. This decision + is based on @{text "wq"}. + \end{minipage} + *} + + cs_holding_raw: + "holding_raw wq thread cs \ (thread \ set (wq cs) \ thread = hd (wq cs))" + + +definition + -- {* + \begin{minipage}{0.9\textwidth} + In accordance with the definition of @{text "holding wq th cs"}, a thread + @{text "th"} is considered waiting for @{text "cs"} if it is in the {\em + waiting queue} of critical resource @{text "cs"}, but not at the head. + This is reflected in the definition of @{text "waiting wq th cs"} as + follows: \end{minipage} *} - cs_holding_def: - "holding wq thread cs \ (thread \ set (wq cs) \ thread = hd (wq cs))" + cs_waiting_raw: + "waiting_raw wq thread cs \ (thread \ set (wq cs) \ thread \ hd (wq cs))" + +definition -- {* \begin{minipage}{0.9\textwidth} - In accordance with the definition of @{text "holding wq th cs"}, - a thread @{text "th"} is considered waiting for @{text "cs"} if - it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head. - This is reflected in the definition of @{text "waiting wq th cs"} as follows: - \end{minipage} + @{text "RAG wq"} generates RAG (a binary relations on @{text "node"}) out + of waiting queues of the system (represented by the @{text "wq"} + argument): \end{minipage} *} - cs_waiting_def: - "waiting wq thread cs \ (thread \ set (wq cs) \ thread \ hd (wq cs))" - -- {* - \begin{minipage}{0.9\textwidth} - @{text "RAG wq"} generates RAG (a binary relations on @{text "node"}) - out of waiting queues of the system (represented by the @{text "wq"} argument): - \end{minipage} - *} - cs_RAG_def: - "RAG (wq::cs \ thread list) \ - {(Th th, Cs cs) | th cs. waiting wq th cs} \ {(Cs cs, Th th) | cs th. holding wq th cs}" + + cs_RAG_raw: + "RAG_raw (wq::cs \ thread list) \ + {(Th th, Cs cs) | th cs. waiting_raw wq th cs} \ {(Cs cs, Th th) | cs th. holding_raw wq th cs}" + +definition -- {* \begin{minipage}{0.9\textwidth} - The following @{text "dependants wq th"} represents the set of threads which are RAGing on - thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}. - Here, "RAGing" means waiting directly or indirectly on the critical resource. + The following @{text "dependants wq th"} represents the set of threads + which are RAGing on thread @{text "th"} in Resource Allocation Graph + @{text "RAG wq"}. Here, "RAGing" means waiting directly or indirectly on + the critical resource. \end{minipage} *} + cs_dependants_def: - "dependants (wq::cs \ thread list) th \ {th' . (Th th', Th th) \ (RAG wq)^+}" - + "dependants_raw (wq::cs \ thread list) th \ {th' . (Th th', Th th) \ (RAG_raw wq)^+}" -text {* \noindent - The following - @{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under - state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of - Priority Inheritance that the {\em current precedence} of a thread is the precedence - inherited from the maximum of all its dependants, i.e. the threads which are waiting - directly or indirectly waiting for some resources from it. If no such thread exits, - @{text "th"}'s {\em current precedence} equals its original precedence, i.e. - @{text "preced th s"}. - *} +text {* + \noindent The following @{text "cpreced s th"} gives the {\em current + precedence} of thread @{text "th"} under state @{text "s"}. The definition + of @{text "cpreced"} reflects the basic idea of Priority Inheritance that + the {\em current precedence} of a thread is the precedence inherited from + the maximum of all its dependants, i.e. the threads which are waiting + directly or indirectly waiting for some resources from it. If no such + thread exits, @{text "th"}'s {\em current precedence} equals its original + precedence, i.e. @{text "preced th s"}. +*} definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" - where "cpreced wq s = (\th. Max ((\th'. preced th' s) ` ({th} \ dependants wq th)))" + where "cpreced wq s = (\th. Max ((\th'. preced th' s) ` ({th} \ dependants_raw wq th)))" text {* - Notice that the current precedence (@{text "cpreced"}) of one thread @{text "th"} can be boosted - (becoming larger than its own precedence) by those threads in - the @{text "dependants wq th"}-set. If one thread get boosted, we say - it inherits the priority (or, more precisely, the precedence) of - its dependants. This is how the word "Inheritance" in + Notice that the current precedence (@{text "cpreced"}) of one thread + @{text "th"} can be boosted (becoming larger than its own precedence) by + those threads in the @{text "dependants wq th"}-set. If one thread get + boosted, we say it inherits the priority (or, more precisely, the + precedence) of its dependants. This is how the word "Inheritance" in Priority Inheritance Protocol comes. *} (*<*) lemma cpreced_def2: - "cpreced wq s th \ Max ({preced th s} \ {preced th' s | th'. th' \ dependants wq th})" + "cpreced wq s th \ Max ({preced th s} \ {preced th' s | th'. th' \ dependants_raw wq th})" unfolding cpreced_def image_def apply(rule eq_reflection) apply(rule_tac f="Max" in arg_cong) @@ -244,49 +258,56 @@ (*>*) -text {* \noindent - Assuming @{text "qs"} be the waiting queue of a critical resource, - the following abbreviation "release qs" is the waiting queue after the thread - holding the resource (which is thread at the head of @{text "qs"}) released - the resource: +text {* + + \noindent Assuming @{text "qs"} be the waiting queue of a critical + resource, the following abbreviation "release qs" is the waiting queue + after the thread holding the resource (which is thread at the head of + @{text "qs"}) released the resource: *} + abbreviation "release qs \ case qs of [] => [] | (_#qs') => (SOME q. distinct q \ set q = set qs')" -text {* \noindent - It can be seen from the definition that the thread at the head of @{text "qs"} is removed - from the return value, and the value @{term "q"} is an reordering of @{text "qs'"}, the - tail of @{text "qs"}. Through this reordering, one of the waiting threads (those in @{text "qs'"} } - is chosen nondeterministically to be the head of the new queue @{text "q"}. - Therefore, this thread is the one who takes over the resource. This is a little better different - from common sense that the thread who comes the earliest should take over. - The intention of this definition is to show that the choice of which thread to take over the - release resource does not affect the correctness of the PIP protocol. + +text {* + \noindent It can be seen from the definition that the thread at the head + of @{text "qs"} is removed from the return value, and the value @{term + "q"} is an reordering of @{text "qs'"}, the tail of @{text "qs"}. Through + this reordering, one of the waiting threads (those in @{text "qs'"} } is + chosen nondeterministically to be the head of the new queue @{text "q"}. + Therefore, this thread is the one who takes over the resource. This is a + little better different from common sense that the thread who comes the + earliest should take over. The intention of this definition is to show + that the choice of which thread to take over the release resource does not + affect the correctness of the PIP protocol. *} text {* - The data structure used by the operating system for scheduling is referred to as - {\em schedule state}. It is represented as a record consisting of - a function assigning waiting queue to resources - (to be used as the @{text "wq"} argument in @{text "holding"}, @{text "waiting"} - and @{text "RAG"}, etc) and a function assigning precedence to threads: + The data structure used by the operating system for scheduling is referred + to as {\em schedule state}. It is represented as a record consisting of a + function assigning waiting queue to resources (to be used as the @{text + "wq"} argument in @{text "holding"}, @{text "waiting"} and @{text "RAG"}, + etc) and a function assigning precedence to threads: *} record schedule_state = wq_fun :: "cs \ thread list" -- {* The function assigning waiting queue. *} cprec_fun :: "thread \ precedence" -- {* The function assigning precedence. *} -text {* \noindent - The following two abbreviations (@{text "all_unlocked"} and @{text "initial_cprec"}) - are used to set the initial values of the @{text "wq_fun"} @{text "cprec_fun"} fields - respectively of the @{text "schedule_state"} record by the following function @{text "sch"}, - which is used to calculate the system's {\em schedule state}. +text {* + \noindent The following two abbreviations (@{text "all_unlocked"} and + @{text "initial_cprec"}) are used to set the initial values of the @{text + "wq_fun"} @{text "cprec_fun"} fields respectively of the @{text + "schedule_state"} record by the following function @{text "sch"}, which is + used to calculate the system's {\em schedule state}. - Since there is no thread at the very beginning to make request, all critical resources - are free (or unlocked). This status is represented by the abbreviation - @{text "all_unlocked"}. - *} + Since there is no thread at the very beginning to make request, all + critical resources are free (or unlocked). This status is represented by + the abbreviation @{text "all_unlocked"}. +*} + abbreviation "all_unlocked \ \_::cs. ([]::thread list)" @@ -371,7 +392,7 @@ lemma cpreced_initial: "cpreced (\ cs. []) [] = (\_. (Prc 0 0))" apply(simp add: cpreced_def) -apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def) +apply(simp add: cs_dependants_def cs_RAG_raw cs_waiting_raw cs_holding_raw) apply(simp add: preced_def) done @@ -413,65 +434,79 @@ fictitious {\em waiting queue function} @{text "wq"}, but on system state @{text "s"}. *} -defs (overloaded) + + +definition s_holding_abv: - "holding (s::state) \ holding (wq_fun (schs s))" + "holding (s::state) \ holding_raw (wq_fun (schs s))" + +definition s_waiting_abv: - "waiting (s::state) \ waiting (wq_fun (schs s))" + "waiting (s::state) \ waiting_raw (wq_fun (schs s))" + +definition s_RAG_abv: - "RAG (s::state) \ RAG (wq_fun (schs s))" + "RAG (s::state) \ RAG_raw (wq_fun (schs s))" + +definition s_dependants_abv: - "dependants (s::state) \ dependants (wq_fun (schs s))" + "dependants (s::state) \ dependants_raw (wq_fun (schs s))" text {* The following lemma can be proved easily, and the meaning is obvious. *} + lemma s_holding_def: "holding (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th = hd (wq_fun (schs s) cs))" - by (auto simp:s_holding_abv wq_def cs_holding_def) + by (auto simp:s_holding_abv wq_def cs_holding_raw) lemma s_waiting_def: "waiting (s::state) th cs \ (th \ set (wq_fun (schs s) cs) \ th \ hd (wq_fun (schs s) cs))" - by (auto simp:s_waiting_abv wq_def cs_waiting_def) + by (auto simp:s_waiting_abv wq_def cs_waiting_raw) lemma s_RAG_def: "RAG (s::state) = - {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \ {(Cs cs, Th th) | cs th. holding (wq s) th cs}" - by (auto simp:s_RAG_abv wq_def cs_RAG_def) + {(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \ {(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}" + by (auto simp:s_RAG_abv wq_def cs_RAG_raw) lemma s_dependants_def: - "dependants (s::state) th \ {th' . (Th th', Th th) \ (RAG (wq s))^+}" + "dependants (s::state) th \ {th' . (Th th', Th th) \ (RAG_raw (wq s))^+}" by (auto simp:s_dependants_abv wq_def cs_dependants_def) text {* - The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} - for running if it is a live thread and it is not waiting for any critical resource. + The following function @{text "readys"} calculates the set of ready + threads. A thread is {\em ready} for running if it is a live thread and it + is not waiting for any critical resource. *} + definition readys :: "state \ thread set" where "readys s \ {th . th \ threads s \ (\ cs. \ waiting s th cs)}" -text {* \noindent - The following function @{text "runing"} calculates the set of running thread, which is the ready - thread with the highest precedence. +text {* + \noindent The following function @{text "runing"} calculates the set of + running thread, which is the ready thread with the highest precedence. *} + definition runing :: "state \ thread set" where "runing s \ {th . th \ readys s \ cp s th = Max ((cp s) ` (readys s))}" -text {* \noindent - Notice that the definition of @{text "running"} reflects the preemptive scheduling strategy, - because, if the @{text "running"}-thread (the one in @{text "runing"} set) - lowered its precedence by resetting its own priority to a lower - one, it will lose its status of being the max in @{text "ready"}-set and be superseded. +text {* + \noindent Notice that the definition of @{text "running"} reflects the + preemptive scheduling strategy, because, if the @{text "running"}-thread + (the one in @{text "runing"} set) lowered its precedence by resetting its + own priority to a lower one, it will lose its status of being the max in + @{text "ready"}-set and be superseded. *} -text {* \noindent - The following function @{text "holdents s th"} returns the set of resources held by thread - @{text "th"} in state @{text "s"}. - *} -definition holdents :: "state \ thread \ cs set" +text {* + \noindent The following function @{text "holdents s th"} returns the set + of resources held by thread @{text "th"} in state @{text "s"}. *} + + +definition holdents :: "state \ thread \ cs set" where "holdents s th \ {cs . holding s th cs}" lemma holdents_test: @@ -659,9 +694,10 @@ definition "tRAG s = wRAG s O hRAG s" text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *} + lemma RAG_split: "RAG s = (wRAG s \ hRAG s)" by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv - s_holding_abv cs_RAG_def, auto) + s_holding_abv cs_RAG_raw, auto) lemma tRAG_alt_def: "tRAG s = {(Th th1, Th th2) | th1 th2.