diff -r 4805c6333fef -r c7ba70dc49bd PIPDefs.thy~ --- a/PIPDefs.thy~ Thu Jan 28 14:57:36 2016 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,663 +0,0 @@ -chapter {* Definitions *} -(*<*) -theory PIPDefs -imports Precedence_ord Moment RTree Max -begin -(*>*) - -text {* - In this section, the formal model of Priority Inheritance Protocol (PIP) is presented. - The model is based on Paulson's inductive protocol verification method, where - the state of the system is modelled as a list of events happened so far with the latest - event put at the head. -*} - -text {* - To define events, the identifiers of {\em threads}, - {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) - need to be represented. All three are represetned using standard - Isabelle/HOL type @{typ "nat"}: -*} - -type_synonym thread = nat -- {* Type for thread identifiers. *} -type_synonym priority = nat -- {* Type for priorities. *} -type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} - -text {* - \noindent - The abstraction of Priority Inheritance Protocol (PIP) is set at the system call level. - Every system call is represented as an event. The format of events is defined - defined as follows: - *} - -datatype event = - Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *} - Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} - P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} - V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} - Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} - -fun actor :: "event \ thread" where - "actor (Create th pty) = th" | - "actor (Exit th) = th" | - "actor (P th cs) = th" | - "actor (V th cs) = th" | - "actor (Set th pty) = th" - -fun isCreate :: "event \ bool" where - "isCreate (Create th pty) = True" | - "isCreate _ = False" - -fun isP :: "event \ bool" where - "isP (P th cs) = True" | - "isP _ = False" - -fun isV :: "event \ bool" where - "isV (V th cs) = True" | - "isV _ = False" - -text {* - As mentioned earlier, in Paulson's inductive method, the states of system are represented as lists of events, - which is defined by the following type @{text "state"}: - *} -type_synonym state = "event list" - - -text {* -\noindent - Resource Allocation Graph (RAG for short) is used extensively in our formal analysis. - The following type @{text "node"} is used to represent nodes in RAG. - *} -datatype node = - Th "thread" | -- {* Node for thread. *} - Cs "cs" -- {* Node for critical resource. *} - -text {* - \noindent - The following function - @{text "threads"} is used to calculate the set of live threads (@{text "threads s"}) - in state @{text "s"}. - *} -fun threads :: "state \ thread set" - where - -- {* At the start of the system, the set of threads is empty: *} - "threads [] = {}" | - -- {* New thread is added to the @{text "threads"}: *} - "threads (Create thread prio#s) = {thread} \ threads s" | - -- {* Finished thread is removed: *} - "threads (Exit thread # s) = (threads s) - {thread}" | - -- {* Other kind of events does not affect the value of @{text "threads"}: *} - "threads (e#s) = threads s" - -text {* - \noindent - The function @{text "threads"} defined above is one of - the so called {\em observation function}s which forms - the very basis of Paulson's inductive protocol verification method. - Each observation function {\em observes} one particular aspect (or attribute) - of the system. For example, the attribute observed by @{text "threads s"} - is the set of threads living in state @{text "s"}. - The protocol being modelled - The decision made the protocol being modelled is based on the {\em observation}s - returned by {\em observation function}s. Since {\observation function}s forms - the very basis on which Paulson's inductive method is based, there will be - a lot of such observation functions introduced in the following. In fact, any function - which takes event list as argument is a {\em observation function}. - *} - -text {* \noindent - Observation @{text "priority th s"} is - the {\em original priority} of thread @{text "th"} in state @{text "s"}. - The {\em original priority} is the priority - assigned to a thread when it is created or when it is reset by system call - (represented by event @{text "Set thread priority"}). -*} - -fun priority :: "thread \ state \ priority" - where - -- {* @{text "0"} is assigned to threads which have never been created: *} - "priority thread [] = 0" | - "priority thread (Create thread' prio#s) = - (if thread' = thread then prio else priority thread s)" | - "priority thread (Set thread' prio#s) = - (if thread' = thread then prio else priority thread s)" | - "priority thread (e#s) = priority thread s" - -text {* - \noindent - Observation @{text "last_set th s"} is the last time when the priority of thread @{text "th"} is set, - observed from state @{text "s"}. - The time in the system is measured by the number of events happened so far since the very beginning. -*} -fun last_set :: "thread \ state \ nat" - where - "last_set thread [] = 0" | - "last_set thread ((Create thread' prio)#s) = - (if (thread = thread') then length s else last_set thread s)" | - "last_set thread ((Set thread' prio)#s) = - (if (thread = thread') then length s else last_set thread s)" | - "last_set thread (_#s) = last_set thread s" - -text {* - \noindent - The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of - a thread is the combination of its {\em original priority} and {\em time} the priority is set. - The intention is to discriminate threads with the same priority by giving threads whose priority - is assigned earlier higher precedences, becasue such threads are more urgent to finish. - This explains the following definition: - *} -definition preced :: "thread \ state \ precedence" - where "preced thread s \ Prc (priority thread s) (last_set thread s)" - - -text {* - \noindent - A number of important notions in PIP are represented as the following functions, - defined in terms of the waiting queues of the system, where the waiting queues - , as a whole, is represented by the @{text "wq"} argument of every notion function. - The @{text "wq"} argument is itself a functions which maps every critical resource - @{text "cs"} to the list of threads which are holding or waiting for it. - The thread at the head of this list is designated as the thread which is current - holding the resrouce, which is slightly different from tradition where - 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) - -- {* - \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"}. - \end{minipage} - *} - - cs_holding_def: - "holding wq thread cs \ (thread \ set (wq cs) \ thread = hd (wq cs))" - -- {* - \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_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}" - -- {* - \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. - \end{minipage} - *} - cs_dependants_def: - "dependants (wq::cs \ thread list) th \ {th' . (Th th', Th th) \ (RAG 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"}. - *} - -definition cpreced :: "(cs \ thread list) \ state \ thread \ precedence" - where "cpreced wq s = (\th. Max ((\th'. preced th' s) ` ({th} \ dependants 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 - Priority Inheritance Protocol comes. -*} - -(*<*) -lemma - cpreced_def2: - "cpreced wq s th \ Max ({preced th s} \ {preced th' s | th'. th' \ dependants wq th})" - unfolding cpreced_def image_def - apply(rule eq_reflection) - apply(rule_tac f="Max" in arg_cong) - by (auto) -(*>*) - - -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 {* - 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}. - - 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)" - - -text {* \noindent - The initial current precedence for a thread can be anything, because there is no thread then. - We simply assume every thread has precedence @{text "Prc 0 0"}. - *} - -abbreviation - "initial_cprec \ \_::thread. Prc 0 0" - - -text {* \noindent - The following function @{text "schs"} is used to calculate the system's schedule state @{text "schs s"} - out of the current system state @{text "s"}. It is the central function to model Priority Inheritance: - *} -fun schs :: "state \ schedule_state" - where - -- {* - \begin{minipage}{0.9\textwidth} - Setting the initial value of the @{text "schedule_state"} record (see the explanations above). - \end{minipage} - *} - "schs [] = (| wq_fun = all_unlocked, cprec_fun = initial_cprec |)" | - - -- {* - \begin{minipage}{0.9\textwidth} - \begin{enumerate} - \item @{text "ps"} is the schedule state of last moment. - \item @{text "pwq"} is the waiting queue function of last moment. - \item @{text "pcp"} is the precedence function of last moment (NOT USED). - \item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement: - \begin{enumerate} - \item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to - the end of @{text "cs"}'s waiting queue. - \item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state, - @{text "th'"} must equal to @{text "thread"}, - because @{text "thread"} is the one currently holding @{text "cs"}. - The case @{text "[] \ []"} may never be executed in a legal state. - the @{text "(SOME q. distinct q \ set q = set qs)"} is used to choose arbitrarily one - thread in waiting to take over the released resource @{text "cs"}. In our representation, - this amounts to rearrange elements in waiting queue, so that one of them is put at the head. - \item For other happening event, the schedule state just does not change. - \end{enumerate} - \item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue - function. The RAGency of precedence function on waiting queue function is the reason to - put them in the same record so that they can evolve together. - \end{enumerate} - - - The calculation of @{text "cprec_fun"} depends on the value of @{text "wq_fun"}. - Therefore, in the following cases, @{text "wq_fun"} is always calculated first, in - the name of @{text "wq"} (if @{text "wq_fun"} is not changed - by the happening event) or @{text "new_wq"} (if the value of @{text "wq_fun"} is changed). - \end{minipage} - *} - "schs (Create th prio # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))" -| "schs (Exit th # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))" -| "schs (Set th prio # s) = - (let wq = wq_fun (schs s) in - (|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))" - -- {* - \begin{minipage}{0.9\textwidth} - Different from the forth coming cases, the @{text "wq_fun"} field of the schedule state - is changed. So, the new value is calculated first, in the name of @{text "new_wq"}. - \end{minipage} - *} -| "schs (P th cs # s) = - (let wq = wq_fun (schs s) in - let new_wq = wq(cs := (wq cs @ [th])) in - (|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))" -| "schs (V th cs # s) = - (let wq = wq_fun (schs s) in - let new_wq = wq(cs := release (wq cs)) in - (|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" - -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: preced_def) -done - -lemma sch_old_def: - "schs (e#s) = (let ps = schs s in - let pwq = wq_fun ps in - let nwq = case e of - P th cs \ pwq(cs:=(pwq cs @ [th])) | - V th cs \ let nq = case (pwq cs) of - [] \ [] | - (_#qs) \ (SOME q. distinct q \ set q = set qs) - in pwq(cs:=nq) | - _ \ pwq - in let ncp = cpreced nwq (e#s) in - \wq_fun = nwq, cprec_fun = ncp\ - )" -apply(cases e) -apply(simp_all) -done - - -text {* - \noindent - The following @{text "wq"} is a shorthand for @{text "wq_fun"}. - *} -definition wq :: "state \ cs \ thread list" - where "wq s = wq_fun (schs s)" - -text {* \noindent - The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. - *} -definition cp :: "state \ thread \ precedence" - where "cp s \ cprec_fun (schs s)" - -text {* \noindent - Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and - @{text "dependants"} still have the - same meaning, but redefined so that they no longer RAG on the - fictitious {\em waiting queue function} - @{text "wq"}, but on system state @{text "s"}. - *} -defs (overloaded) - s_holding_abv: - "holding (s::state) \ holding (wq_fun (schs s))" - s_waiting_abv: - "waiting (s::state) \ waiting (wq_fun (schs s))" - s_RAG_abv: - "RAG (s::state) \ RAG (wq_fun (schs s))" - s_dependants_abv: - "dependants (s::state) \ dependants (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) - -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) - -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) - -lemma - s_dependants_def: - "dependants (s::state) th \ {th' . (Th th', Th th) \ (RAG (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. - *} -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. - *} -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 - 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: - "holdents s th = {cs . (Cs cs, Th th) \ RAG s}" -unfolding holdents_def -unfolding s_RAG_def -unfolding s_holding_abv -unfolding wq_def -by (simp) - -text {* \noindent - Observation @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in - state @{text "s"}: - *} -definition cntCS :: "state \ thread \ nat" - where "cntCS s th = card (holdents s th)" - -text {* \noindent - According to the convention of Paulson's inductive method, - the decision made by a protocol that event @{text "e"} is eligible to happen next under state @{text "s"} - is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as - follows (notice how the decision is based on the {\em observation function}s - defined above, and also notice how a complicated protocol is modeled by a few simple - observations, and how such a kind of simplicity gives rise to improved trust on - faithfulness): - *} -inductive step :: "state \ event \ bool" - where - -- {* - A thread can be created if it is not a live thread: - *} - thread_create: "\thread \ threads s\ \ step s (Create thread prio)" | - -- {* - A thread can exit if it no longer hold any resource: - *} - thread_exit: "\thread \ runing s; holdents s thread = {}\ \ step s (Exit thread)" | - -- {* - \begin{minipage}{0.9\textwidth} - A thread can request for an critical resource @{text "cs"}, if it is running and - the request does not form a loop in the current RAG. The latter condition - is set up to avoid deadlock. The condition also reflects our assumption all threads are - carefully programmed so that deadlock can not happen: - \end{minipage} - *} - thread_P: "\thread \ runing s; (Cs cs, Th thread) \ (RAG s)^+\ \ - step s (P thread cs)" | - -- {* - \begin{minipage}{0.9\textwidth} - A thread can release a critical resource @{text "cs"} - if it is running and holding that resource: - \end{minipage} - *} - thread_V: "\thread \ runing s; holding s thread cs\ \ step s (V thread cs)" | - -- {* - \begin{minipage}{0.9\textwidth} - A thread can adjust its own priority as long as it is current running. - With the resetting of one thread's priority, its precedence may change. - If this change lowered the precedence, according to the definition of @{text "running"} - function, - \end{minipage} - *} - thread_set: "\thread \ runing s\ \ step s (Set thread prio)" - -text {* - In Paulson's inductive method, every protocol is defined by such a @{text "step"} - predicate. For instance, the predicate @{text "step"} given above - defines the PIP protocol. So, it can also be called "PIP". -*} - -abbreviation - "PIP \ step" - - -text {* \noindent - For any protocol defined by a @{text "step"} predicate, - the fact that @{text "s"} is a legal state in - the protocol is expressed as: @{text "vt step s"}, where - the predicate @{text "vt"} can be defined as the following: - *} -inductive vt :: "state \ bool" - where - -- {* Empty list @{text "[]"} is a legal state in any protocol:*} - vt_nil[intro]: "vt []" | - -- {* - \begin{minipage}{0.9\textwidth} - If @{text "s"} a legal state of the protocol defined by predicate @{text "step"}, - and event @{text "e"} is allowed to happen under state @{text "s"} by the protocol - predicate @{text "step"}, then @{text "e#s"} is a new legal state rendered by the - happening of @{text "e"}: - \end{minipage} - *} - vt_cons[intro]: "\vt s; step s e\ \ vt (e#s)" - -text {* \noindent - It is easy to see that the definition of @{text "vt"} is generic. It can be applied to - any specific protocol specified by a @{text "step"}-predicate to get the set of - legal states of that particular protocol. - *} - -text {* - The following are two very basic properties of @{text "vt"}. -*} - -lemma step_back_vt: "vt (e#s) \ vt s" - by(ind_cases "vt (e#s)", simp) - -lemma step_back_step: "vt (e#s) \ step s e" - by(ind_cases "vt (e#s)", simp) - -text {* \noindent - The following two auxiliary functions @{text "the_cs"} and @{text "the_th"} are used to extract - critical resource and thread respectively out of RAG nodes. - *} -fun the_cs :: "node \ cs" - where "the_cs (Cs cs) = cs" - -fun the_th :: "node \ thread" - where "the_th (Th th) = th" - -text {* \noindent - The following predicate @{text "next_th"} describe the next thread to - take over when a critical resource is released. In @{text "next_th s th cs t"}, - @{text "th"} is the thread to release, @{text "t"} is the one to take over. - Notice how this definition is backed up by the @{text "release"} function and its use - in the @{text "V"}-branch of @{text "schs"} function. This @{text "next_th"} function - is not needed for the execution of PIP. It is introduced as an auxiliary function - to state lemmas. The correctness of this definition will be confirmed by - lemmas @{text "step_v_hold_inv"}, @{text " step_v_wait_inv"}, - @{text "step_v_get_hold"} and @{text "step_v_not_wait"}. - *} -definition next_th:: "state \ thread \ cs \ thread \ bool" - where "next_th s th cs t = (\ rest. wq s cs = th#rest \ rest \ [] \ - t = hd (SOME q. distinct q \ set q = set rest))" - -text {* \noindent - The aux function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"} - in list @{text "l"}: - *} -definition count :: "('a \ bool) \ 'a list \ nat" - where "count Q l = length (filter Q l)" - -text {* \noindent - The following observation @{text "cntP s"} returns the number of operation @{text "P"} happened - before reaching state @{text "s"}. - *} -definition cntP :: "state \ thread \ nat" - where "cntP s th = count (\ e. \ cs. e = P th cs) s" - -text {* \noindent - The following observation @{text "cntV s"} returns the number of operation @{text "V"} happened - before reaching state @{text "s"}. - *} -definition cntV :: "state \ thread \ nat" - where "cntV s th = count (\ e. \ cs. e = V th cs) s" - -text {* @{text "the_preced"} is also the same as @{text "preced"}, the only - difference is the order of arguemts. *} -definition "the_preced s th = preced th s" - -text {* @{term "the_thread"} extracts thread out of RAG node. *} -fun the_thread :: "node \ thread" where - "the_thread (Th th) = th" - -text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *} -definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}" - -text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *} -definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}" - -text {* - The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}. - It characterizes the dependency between threads when calculating current - precedences. It is defined as the composition of the above two sub-graphs, - names @{term "wRAG"} and @{term "hRAG"}. - *} -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) - -definition "cp_gen s x = - Max ((the_preced s \ the_thread) ` subtree (tRAG s) x)" - -(*<*) - -end -(*>*) -