pip: comparison PrioGDef.thy

equal deleted inserted replaced

-:8f026b608378
+:e861aff29655
 "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
+Observing function @{text "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
+: @{text "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"
+fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority"
 where
 -- {* @{text "0"} is assigned to threads which have never been created: *}
-"original_priority thread [] = 0" |
+"priority thread [] = 0" |
-"original_priority thread (Create thread' prio#s) =
+"priority thread (Create thread' prio#s) =
-(if thread' = thread then prio else original_priority thread s)" |
+(if thread' = thread then prio else priority thread s)" |
-"original_priority thread (Set thread' prio#s) =
+"priority thread (Set thread' prio#s) =
-(if thread' = thread then prio else original_priority thread s)" |
+(if thread' = thread then prio else priority thread s)" |
-"original_priority thread (e#s) = original_priority thread s"
+"priority thread (e#s) = priority thread s"
 text {*
 \noindent
 In the following,
-@{text "birthtime th s"} is the time when thread @{text "th"} is created,
+@{text "last_set 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"
+fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat"
 where
-"birthtime thread [] = 0" |
+"last_set thread [] = 0" |
-"birthtime thread ((Create thread' prio)#s) =
+"last_set thread ((Create thread' prio)#s) =
-(if (thread = thread') then length s else birthtime thread s)" |
+(if (thread = thread') then length s else last_set thread s)" |
-"birthtime thread ((Set thread' prio)#s) =
+"last_set thread ((Set thread' prio)#s) =
-(if (thread = thread') then length s else birthtime thread s)" |
+(if (thread = thread') then length s else last_set thread s)" |
-"birthtime thread (e#s) = birthtime 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 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)"
+where "preced thread s \<equiv> Prc (priority thread s) (last_set 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"
+dependants :: "'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
 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
+The following @{text "dependants 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:
+cs_dependants_def:
-"dependents (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (depend wq)^+}"
+"dependants (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
 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
+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 \<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)))"
+where "cpreced wq s = (\<lambda> th. Max ((\<lambda> th. preced th s) ` ({th} \<union> dependants wq th)))"
 (*<*)
 lemma
 cpreced_def2:
-"cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependents wq th})"
+"cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})"
 unfolding cpreced_def image_def
 apply(rule eq_reflection)
 apply(rule_tac f="Max" in arg_cong)
 by (auto)
 (*>*)
 (|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: cs_dependants_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
 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
+@{text "dependants"} 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)
 "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:
+s_dependants_abv:
-"dependents (s::state) \<equiv> dependents (wq_fun (schs s))"
+"dependants (s::state) \<equiv> dependants (wq_fun (schs s))"
 text {*
 The following lemma can be proved easily:
 *}
 "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:
+s_dependants_def:
-"dependents (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
+"dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (depend (wq s))^+}"
-by (auto simp:s_dependents_abv wq_def cs_dependents_def)
+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.
 *}

changeset 32	e861aff29655
parent 17	105715a0a807
child 33	9b9f2117561f