--- a/PIPDefs.thy Thu Jun 02 13:15:03 2016 +0100
+++ b/PIPDefs.thy Tue Jun 07 13:51:39 2016 +0100
@@ -7,10 +7,10 @@
chapter {* Definitions *}
text {*
- In this section, the formal model of Priority Inheritance Protocol (PIP) is presented.
+ 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.
+ 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 {*
@@ -32,11 +32,11 @@
*}
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"}. *}
+ 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" |
@@ -45,6 +45,7 @@
"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
@@ -60,27 +61,23 @@
"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"}:
- *}
+ 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.
- *}
+ 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 thread. *}
- Cs "cs" -- {* Node for critical resource. *}
+ Th "thread" -- {* Node for a thread. *}
+| Cs "cs" -- {* Node for a 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"}.
- *}
+ 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: *}
@@ -93,28 +90,28 @@
"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"}).
-*}
+ \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 \<Rightarrow> state \<Rightarrow> priority"
where
@@ -127,11 +124,12 @@
"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.
-*}
+
+ \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 thread [] = 0" |
@@ -142,28 +140,31 @@
"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:
- *}
+
+ \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 \<Rightarrow> state \<Rightarrow> precedence"
where "preced thread s \<equiv> 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.
- *}
+
+ \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
@@ -173,8 +174,7 @@
dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set"
*)
-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
@@ -183,6 +183,7 @@
\end{minipage}
*}
+definition
cs_holding_raw:
"holding_raw wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))"