--- a/prio/PrioGDef.thy Mon Dec 03 08:16:58 2012 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,483 +0,0 @@
-(*<*)
-theory PrioGDef
-imports Precedence_ord Moment
-begin
-(*>*)
-
-text {*
- In this section, the formal model of Priority Inheritance 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.
-
- 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
- Every event in the system corresponds to a system call, the formats of which are
- 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"}. *}
-
-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 {*
- 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
- The following function
- @{text "threads"} is used to calculate the set of live threads (@{text "threads s"})
- in state @{text "s"}.
- *}
-fun threads :: "state \<Rightarrow> 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} \<union> 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
- Functions such as @{text "threads"}, which extract information out of system states, are called
- {\em observing functions}. A series of observing functions will be defined in the sequel in order to
- model the protocol.
- Observing function @{text "original_priority"} calculates
- the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as
- : @{text "original_priority th s" }. The {\em original priority} is the priority
- assigned to a thread when it is created or when it is reset by system call
- @{text "Set thread priority"}.
-*}
-
-fun original_priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
- where
- -- {* @{text "0"} is assigned to threads which have never been created: *}
- "original_priority thread [] = 0" |
- "original_priority thread (Create thread' prio#s) =
- (if thread' = thread then prio else original_priority thread s)" |
- "original_priority thread (Set thread' prio#s) =
- (if thread' = thread then prio else original_priority thread s)" |
- "original_priority thread (e#s) = original_priority thread s"
-
-text {*
- \noindent
- In the following,
- @{text "birthtime th s"} is the time when thread @{text "th"} is created,
- 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 birthtime :: "thread \<Rightarrow> state \<Rightarrow> nat"
- where
- "birthtime thread [] = 0" |
- "birthtime thread ((Create thread' prio)#s) =
- (if (thread = thread') then length s else birthtime thread s)" |
- "birthtime thread ((Set thread' prio)#s) =
- (if (thread = thread') then length s else birthtime thread s)" |
- "birthtime thread (e#s) = birthtime 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 birth time}. 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 \<Rightarrow> state \<Rightarrow> precedence"
- where "preced thread s \<equiv> Prc (original_priority thread s) (birthtime thread s)"
-
-
-text {*
- \noindent
- A number of important notions are defined here:
- *}
-
-consts
- holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
- waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool"
- depend :: "'b \<Rightarrow> (node \<times> node) set"
- dependents :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
-
-text {*
- \noindent
- In the definition of the following several functions, it is supposed that
- the waiting queue of every critical resource is given by a waiting queue
- function @{text "wq"}, which servers as arguments of these functions.
- *}
-defs (overloaded)
- -- {*
- \begin{minipage}{0.9\textwidth}
- We define that the thread which is at the head of waiting queue of resource @{text "cs"}
- is holding the resource. This definition is slightly different from tradition where
- all threads in the waiting queue are considered as waiting for the resource.
- This notion is reflected in the definition of @{text "holding wq th cs"} as follows:
- \end{minipage}
- *}
- cs_holding_def:
- "holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> 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 \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
- -- {*
- \begin{minipage}{0.9\textwidth}
- @{text "depend wq"} represents the Resource Allocation Graph of the system under the waiting
- queue function @{text "wq"}.
- \end{minipage}
- *}
- cs_depend_def:
- "depend (wq::cs \<Rightarrow> thread list) \<equiv>
- {(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}"
- -- {*
- \begin{minipage}{0.9\textwidth}
- The following @{text "dependents wq th"} represents the set of threads which are depending on
- thread @{text "th"} in Resource Allocation Graph @{text "depend wq"}:
- \end{minipage}
- *}
- cs_dependents_def:
- "dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
-
-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 and a function assigning precedence to
- threads:
- *}
-record schedule_state =
- wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
- cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *}
-
-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 dependents, 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 \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
- where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependents wq th)))"
-
-(*<*)
-lemma
- cpreced_def2:
- "cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
- unfolding cpreced_def image_def
- apply(rule eq_reflection)
- apply(rule_tac f="Max" in arg_cong)
- by (auto)
-(*>*)
-
-abbreviation
- "all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)"
-
-abbreviation
- "initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0"
-
-abbreviation
- "release qs \<equiv> case qs of
- [] => []
- | (_#qs) => (SOME q. distinct q \<and> set q = set qs)"
-
-text {* \noindent
- The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}.
- It is the key function to model Priority Inheritance:
- *}
-fun schs :: "state \<Rightarrow> schedule_state"
- where
- "schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" |
-
- -- {*
- \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 "[] \<Longrightarrow> []"} may never be executed in a legal state.
- the @{text "(SOME q. distinct q \<and> 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 dependency 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}
- \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)|))"
-| "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 (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
-apply(simp add: cpreced_def)
-apply(simp add: cs_dependents_def cs_depend_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 \<Rightarrow> pwq(cs:=(pwq cs @ [th])) |
- V th cs \<Rightarrow> let nq = case (pwq cs) of
- [] \<Rightarrow> [] |
- (_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs)
- in pwq(cs:=nq) |
- _ \<Rightarrow> pwq
- in let ncp = cpreced nwq (e#s) in
- \<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr>
- )"
-apply(cases e)
-apply(simp_all)
-done
-
-
-text {*
- \noindent
- The following @{text "wq"} is a shorthand for @{text "wq_fun"}.
- *}
-definition wq :: "state \<Rightarrow> cs \<Rightarrow> 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 \<Rightarrow> thread \<Rightarrow> precedence"
- where "cp s \<equiv> cprec_fun (schs s)"
-
-text {* \noindent
- Functions @{text "holding"}, @{text "waiting"}, @{text "depend"} and
- @{text "dependents"} still have the
- same meaning, but redefined so that they no longer depend on the
- fictitious {\em waiting queue function}
- @{text "wq"}, but on system state @{text "s"}.
- *}
-defs (overloaded)
- s_holding_abv:
- "holding (s::state) \<equiv> holding (wq_fun (schs s))"
- s_waiting_abv:
- "waiting (s::state) \<equiv> waiting (wq_fun (schs s))"
- s_depend_abv:
- "depend (s::state) \<equiv> depend (wq_fun (schs s))"
- s_dependents_abv:
- "dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
-
-
-text {*
- The following lemma can be proved easily:
- *}
-lemma
- s_holding_def:
- "holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> 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 \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))"
- by (auto simp:s_waiting_abv wq_def cs_waiting_def)
-
-lemma s_depend_def:
- "depend (s::state) =
- {(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}"
- by (auto simp:s_depend_abv wq_def cs_depend_def)
-
-lemma
- s_dependents_def:
- "dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
- by (auto simp:s_dependents_abv wq_def cs_dependents_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 \<Rightarrow> thread set"
- where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> 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 \<Rightarrow> thread set"
- where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}"
-
-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 \<Rightarrow> thread \<Rightarrow> cs set"
- where "holdents s th \<equiv> {cs . holding s th cs}"
-
-lemma holdents_test:
- "holdents s th = {cs . (Cs cs, Th th) \<in> depend s}"
-unfolding holdents_def
-unfolding s_depend_def
-unfolding s_holding_abv
-unfolding wq_def
-by (simp)
-
-text {* \noindent
- @{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in
- state @{text "s"}:
- *}
-definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
- where "cntCS s th = card (holdents s th)"
-
-text {* \noindent
- The fact that event @{text "e"} is eligible to happen next in state @{text "s"}
- is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as
- follows:
- *}
-inductive step :: "state \<Rightarrow> event \<Rightarrow> bool"
- where
- -- {*
- A thread can be created if it is not a live thread:
- *}
- thread_create: "\<lbrakk>thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" |
- -- {*
- A thread can exit if it no longer hold any resource:
- *}
- thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>thread \<in> runing s; (Cs cs, Th thread) \<notin> (depend s)^+\<rbrakk> \<Longrightarrow>
- 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: "\<lbrakk>thread \<in> runing s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" |
- -- {*
- A thread can adjust its own priority as long as it is current running:
- *}
- thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)"
-
-text {* \noindent
- With predicate @{text "step"}, the fact that @{text "s"} is a legal state in
- Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where
- the predicate @{text "vt"} can be defined as the following:
- *}
-inductive vt :: "state \<Rightarrow> 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, and event @{text "e"} is eligible to happen
- in state @{text "s"}, then @{text "e#s"} is a legal state as well:
- \end{minipage}
- *}
- vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)"
-
-text {* \noindent
- It is easy to see that the definition of @{text "vt"} is generic. It can be applied to
- any step predicate to get the set of legal states.
- *}
-
-text {* \noindent
- The following two 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 \<Rightarrow> cs"
- where "the_cs (Cs cs) = cs"
-
-fun the_th :: "node \<Rightarrow> 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.
- *}
-definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool"
- where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and>
- t = hd (SOME q. distinct q \<and> set q = set rest))"
-
-text {* \noindent
- The function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"}
- in list @{text "l"}:
- *}
-definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat"
- where "count Q l = length (filter Q l)"
-
-text {* \noindent
- The following @{text "cntP s"} returns the number of operation @{text "P"} happened
- before reaching state @{text "s"}.
- *}
-definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
- where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
-
-text {* \noindent
- The following @{text "cntV s"} returns the number of operation @{text "V"} happened
- before reaching state @{text "s"}.
- *}
-definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
- where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
-(*<*)
-
-end
-(*>*)
-