(*<*)
theory PIPDefs
imports Precedence_ord Moment RTree Max
begin
(*>*)
chapter {* Definitions *}
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 (trace) 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 where
"actor (Exit th) = th" |
"actor (P th cs) = th" |
"actor (V th cs) = th" |
"actor (Set th pty) = th" |
"actor (Create th prio) = th"
-- {* The actions of a set of threads *}
definition "actions_of ths s = filter (\<lambda> e. actor e \<in> ths) s"
fun isCreate :: "event \<Rightarrow> bool" where
"isCreate (Create th pty) = True" |
"isCreate _ = False"
fun isP :: "event \<Rightarrow> bool" where
"isP (P th cs) = True" |
"isP _ = False"
fun isV :: "event \<Rightarrow> 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 {*
The 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 th prio#s) = {th} \<union> threads s" |
-- {* Finished thread is removed: *}
"threads (Exit th # s) = (threads s) - {th}" |
-- {* Other kind of events does not affect the value of @{text "threads"}: *}
"threads (e # s) = threads s"
text {*
\noindent The function @{text "threads"} is one of the {\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 \<Rightarrow> state \<Rightarrow> priority"
where
-- {* @{text "0"} is assigned to threads which have never been created: *}
"priority th [] = 0" |
"priority th (Create th' prio # s) =
(if th' = th then prio else priority th s)" |
"priority th (Set th' prio # s) =
(if th' = th then prio else priority th s)" |
"priority th (e # s) = priority th 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 \<Rightarrow> state \<Rightarrow> nat"
where
"last_set th [] = 0" |
"last_set th ((Create th' prio) # s) =
(if (th = th') then length s else last_set th s)" |
"last_set th ((Set th' prio) # s) =
(if (th = th') then length s else last_set th s)" |
"last_set th (_ # s) = last_set th 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 the {\em time} the priority was set. The intention
is to discriminate threads with the same priority by giving threads whose
priority is assigned earlier higher precedences, because such threads are
assumed more urgent to finish. *}
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence"
where "preced th s \<equiv> Prc (priority th s) (last_set th s)"
definition preceds :: "thread set \<Rightarrow> state \<Rightarrow> precedence set"
where "preceds ths s \<equiv> {preced th s | th. th \<in> ths}"
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
resource, which is slightly different from tradition where all threads in
the waiting queue are considered as waiting for the resource. *}
text {*
\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} *}
definition
"holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"
text {*
\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} *}
definition
"waiting_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
text {*
Resource Allocation Graphs (RAG for short) are used extensively in our
formal analysis. The following type @{text "node"} is used to represent
the two types of nodes in RAGs. *}
datatype node =
Th "thread" -- {* Node for a thread. *}
| Cs "cs" -- {* Node for a critical resource. *}
text {*
\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} *}
definition
RAG_raw :: "(cs \<Rightarrow> thread list) => (node * node) set"
where
"RAG_raw wq \<equiv>
{(Th th, Cs cs) | th cs. waiting_raw wq th cs} \<union>
{(Cs cs, Th th) | cs th. holding_raw wq th cs}"
text {*
\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} *}
definition
dependants_raw :: "(cs \<Rightarrow> thread list) \<Rightarrow> thread \<Rightarrow> thread set"
where
"dependants_raw wq th \<equiv> {th' . (Th th', Th th) \<in> (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"}. *}
definition
cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence"
where
"cpreced wq s th = Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants_raw wq th))"
text {*
Notice that the current precedence (@{text "cpreced"}) of one thread
@{text "th"} can be boosted (increased) by those threads in the @{text
"dependants wq th"}-set. If one thread gets boosted, we say it inherits
the priority (or, more precisely, the precedence) of its dependants. This
is whrere the word "Inheritance" in Priority Inheritance Protocol comes
from. *}
lemma cpreced_def2:
"cpreced wq s th \<equiv> Max ({preced th s} \<union> preceds (dependants_raw wq th) s)"
unfolding cpreced_def image_def preceds_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 \<equiv> case qs of
[] => []
| (_#qs') => (SOME q. distinct q \<and> 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 \<Rightarrow> thread list" -- {* The function assigning waiting queue. *}
cprec_fun :: "thread \<Rightarrow> 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 \<equiv> \<lambda>_::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 \<equiv> \<lambda>_::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.
\begin{minipage}{0.9\textwidth}
Setting the initial value of the @{text "schedule_state"} record
(see the explanations above).
\end{minipage}
*}
-- {*
\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 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}
*}
fun schs :: "state \<Rightarrow> schedule_state"
where
"schs [] = (| wq_fun = all_unlocked, cprec_fun = initial_cprec |)"
| "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 (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))"
apply(rule ext)
apply(simp add: cpreced_def)
apply(simp add: dependants_raw_def RAG_raw_def waiting_raw_def holding_raw_def)
apply(simp add: preced_def)
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 "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"}. *}
definition
s_holding_abv:
"holding (s::state) \<equiv> holding_raw (wq_fun (schs s))"
definition
s_waiting_abv:
"waiting (s::state) \<equiv> waiting_raw (wq_fun (schs s))"
definition
s_RAG_abv:
"RAG (s::state) \<equiv> RAG_raw (wq_fun (schs s))"
definition
s_dependants_abv:
"dependants (s::state) \<equiv> dependants_raw (wq_fun (schs s))"
text {*
The following four lemmas relate the @{term wq} and non-@{term wq}
versions of @{term waiting}, @{term holding}, @{term dependants} and
@{term cp}. *}
lemma waiting_eq:
shows "waiting s th cs = waiting_raw (wq s) th cs"
by (simp add: s_waiting_abv wq_def)
lemma holding_eq:
shows "holding s th cs = holding_raw (wq s) th cs"
by (simp add: s_holding_abv wq_def)
lemma eq_dependants:
shows "dependants_raw (wq s) = dependants s"
by (simp add: s_dependants_abv wq_def)
lemma cp_eq:
shows "cp s th = cpreced (wq s) s th"
unfolding cp_def wq_def
apply(induct s rule: schs.induct)
apply(simp add: Let_def cpreced_initial)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
apply(subst (2) schs.simps)
apply(simp add: Let_def)
done
text {*
The following lemma can be proved easily, and the meaning is obvious. *}
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 holding_raw_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 waiting_raw_def)
lemma s_RAG_def:
"RAG (s::state) =
{(Th th, Cs cs) | th cs. waiting_raw (wq s) th cs} \<union>
{(Cs cs, Th th) | cs th. holding_raw (wq s) th cs}"
by (auto simp:s_RAG_abv wq_def RAG_raw_def)
lemma eq_RAG:
"RAG_raw (wq s) = RAG s"
by (unfold RAG_raw_def s_RAG_def, auto)
lemma s_dependants_def:
shows "dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG s)^+}"
using dependants_raw_def eq_RAG s_dependants_abv wq_def by auto
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 "running"} calculates the set of
running thread, which is the ready thread with the highest precedence. *}
definition running :: "state \<Rightarrow> thread set"
where "running s \<equiv> {th . th \<in> readys s \<and> 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 "running"} 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 \<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> RAG s}"
unfolding holdents_def
unfolding s_RAG_def
unfolding s_holding_abv
unfolding wq_def
by (simp)
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 \<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> running 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> running s; (Cs cs, Th thread) \<notin> (RAG 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> running s; holding s thread cs\<rbrakk> \<Longrightarrow> 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: "\<lbrakk>thread \<in> running s\<rbrakk> \<Longrightarrow> 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 \<equiv> 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 \<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 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]: "\<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 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) \<Longrightarrow> vt s"
by(ind_cases "vt (e#s)", simp)
lemma step_back_step: "vt (e#s) \<Longrightarrow> 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 \<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.
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 \<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 aux 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 {*
The operation @{term P} is used by a thread to request for resources, while
@{term V} is used to release. Therefore, the number of resources
held by a thread roughly equals to the number of @{term P} it made minus
the number of @{term V}. The equality is rough because the @{term P}-operation
might be blocked and fail to give back the holding of the requested resource.
In the following, @{text "cntP"} and @{text "cntV"} are the number of @{term P}
and @{term "V"} respectively, while @{term cntCS} is the number
resources held by a thread and @{text "pvD"} is introduced to account for
the above mentioned situation when @{term P} is blocked, so that
a equation between @{text cntP}, @{text "cntV"}, @{text "cntCS"} can be established
(in the lemma named @{text "valid_trace.cnp_cnv_cncs"}).
Such a equation, once established, is very handy, because the number of resources
held by a thread can be calculated by counting the number of @{term P} and @{text V},
which is relatively easy.
*}
definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s"
definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s"
definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat"
where "cntCS s th = card (holdents s th)"
definition "pvD s th = (if (th \<in> readys s \<or> th \<notin> threads s) then 0 else (1::nat))"
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 \<Rightarrow> 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 \<union> hRAG s)"
by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
s_holding_abv RAG_raw_def, auto)
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.
\<exists> cs. (Th th1, Cs cs) \<in> RAG s \<and> (Cs cs, Th th2) \<in> RAG s}"
by (auto simp:tRAG_def RAG_split wRAG_def hRAG_def)
(*<*)
end
(*>*)