author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
Sat, 24 May 2014 12:39:12 +0100 | |
changeset 37 | c820ac0f3088 |
parent 35 | 92f61f6a0fe7 |
child 48 | c0f14399c12f |
permissions | -rw-r--r-- |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*<*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory PrioGDef |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
imports Precedence_ord Moment |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
(*>*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
In this section, the formal model of Priority Inheritance is presented. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
9 |
The model is based on Paulson's inductive protocol verification method, where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
the state of the system is modelled as a list of events happened so far with the latest |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
11 |
event put at the head. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
12 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
To define events, the identifiers of {\em threads}, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
{\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
need to be represented. All three are represetned using standard |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
Isabelle/HOL type @{typ "nat"}: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
17 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
18 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
19 |
type_synonym thread = nat -- {* Type for thread identifiers. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
type_synonym priority = nat -- {* Type for priorities. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
type_synonym cs = nat -- {* Type for critical sections (or critical resources). *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
24 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
25 |
Every event in the system corresponds to a system call, the formats of which are |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
26 |
defined as follows: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
27 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
28 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
29 |
datatype event = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
30 |
Create thread priority | -- {* Thread @{text "thread"} is created with priority @{text "priority"}. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
31 |
Exit thread | -- {* Thread @{text "thread"} finishing its execution. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
P thread cs | -- {* Thread @{text "thread"} requesting critical resource @{text "cs"}. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
Resource Allocation Graph (RAG for short) is used extensively in our formal analysis. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
The following type @{text "node"} is used to represent nodes in RAG. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
datatype node = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
Th "thread" | -- {* Node for thread. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
43 |
Cs "cs" -- {* Node for critical resource. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
46 |
In Paulson's inductive method, the states of system are represented as lists of events, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
47 |
which is defined by the following type @{text "state"}: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
type_synonym state = "event list" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
51 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
The following function |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
@{text "threads"} is used to calculate the set of live threads (@{text "threads s"}) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
in state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
fun threads :: "state \<Rightarrow> thread set" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
-- {* At the start of the system, the set of threads is empty: *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
"threads [] = {}" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
-- {* New thread is added to the @{text "threads"}: *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
"threads (Create thread prio#s) = {thread} \<union> threads s" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
-- {* Finished thread is removed: *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
64 |
"threads (Exit thread # s) = (threads s) - {thread}" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
65 |
-- {* Other kind of events does not affect the value of @{text "threads"}: *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
66 |
"threads (e#s) = threads s" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
67 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
68 |
Functions such as @{text "threads"}, which extract information out of system states, are called |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
69 |
{\em observing functions}. A series of observing functions will be defined in the sequel in order to |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
70 |
model the protocol. |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
71 |
Observing function @{text "priority"} calculates |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
72 |
the {\em original priority} of thread @{text "th"} in state @{text "s"}, expressed as |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
73 |
: @{text "priority th s" }. The {\em original priority} is the priority |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
74 |
assigned to a thread when it is created or when it is reset by system call |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
75 |
@{text "Set thread priority"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
76 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
77 |
|
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
78 |
fun priority :: "thread \<Rightarrow> state \<Rightarrow> priority" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
79 |
where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
80 |
-- {* @{text "0"} is assigned to threads which have never been created: *} |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
81 |
"priority thread [] = 0" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
82 |
"priority thread (Create thread' prio#s) = |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
83 |
(if thread' = thread then prio else priority thread s)" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
84 |
"priority thread (Set thread' prio#s) = |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
85 |
(if thread' = thread then prio else priority thread s)" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
86 |
"priority thread (e#s) = priority thread s" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
87 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
88 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
89 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
90 |
In the following, |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
91 |
@{text "last_set th s"} is the time when thread @{text "th"} is created, |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
92 |
observed from state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
93 |
The time in the system is measured by the number of events happened so far since the very beginning. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
94 |
*} |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
95 |
fun last_set :: "thread \<Rightarrow> state \<Rightarrow> nat" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
where |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
97 |
"last_set thread [] = 0" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
98 |
"last_set thread ((Create thread' prio)#s) = |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
99 |
(if (thread = thread') then length s else last_set thread s)" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
100 |
"last_set thread ((Set thread' prio)#s) = |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
101 |
(if (thread = thread') then length s else last_set thread s)" | |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
102 |
"last_set thread (_#s) = last_set thread s" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
103 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
104 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
105 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
106 |
The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
107 |
a thread is the combination of its {\em original priority} and {\em birth time}. The intention is |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
108 |
to discriminate threads with the same priority by giving threads whose priority |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
109 |
is assigned earlier higher precedences, becasue such threads are more urgent to finish. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
110 |
This explains the following definition: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
111 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
112 |
definition preced :: "thread \<Rightarrow> state \<Rightarrow> precedence" |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
113 |
where "preced thread s \<equiv> Prc (priority thread s) (last_set thread s)" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
114 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
115 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
116 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
117 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
118 |
A number of important notions are defined here: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
119 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
120 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
121 |
consts |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
122 |
holding :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
123 |
waiting :: "'b \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> bool" |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
124 |
RAG :: "'b \<Rightarrow> (node \<times> node) set" |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
125 |
dependants :: "'b \<Rightarrow> thread \<Rightarrow> thread set" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
126 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
127 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
128 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
129 |
In the definition of the following several functions, it is supposed that |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
130 |
the waiting queue of every critical resource is given by a waiting queue |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
131 |
function @{text "wq"}, which servers as arguments of these functions. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
132 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
133 |
defs (overloaded) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
134 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
135 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
136 |
We define that the thread which is at the head of waiting queue of resource @{text "cs"} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
137 |
is holding the resource. This definition is slightly different from tradition where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
138 |
all threads in the waiting queue are considered as waiting for the resource. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
139 |
This notion is reflected in the definition of @{text "holding wq th cs"} as follows: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
140 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
141 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
142 |
cs_holding_def: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
143 |
"holding wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread = hd (wq cs))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
144 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
145 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
146 |
In accordance with the definition of @{text "holding wq th cs"}, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
147 |
a thread @{text "th"} is considered waiting for @{text "cs"} if |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
148 |
it is in the {\em waiting queue} of critical resource @{text "cs"}, but not at the head. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
149 |
This is reflected in the definition of @{text "waiting wq th cs"} as follows: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
150 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
151 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
152 |
cs_waiting_def: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
153 |
"waiting wq thread cs \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
154 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
155 |
\begin{minipage}{0.9\textwidth} |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
156 |
@{text "RAG wq"} represents the Resource Allocation Graph of the system under the waiting |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
queue function @{text "wq"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
158 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
159 |
*} |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
160 |
cs_RAG_def: |
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
161 |
"RAG (wq::cs \<Rightarrow> thread list) \<equiv> |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
{(Th th, Cs cs) | th cs. waiting wq th cs} \<union> {(Cs cs, Th th) | cs th. holding wq th cs}" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
163 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
164 |
\begin{minipage}{0.9\textwidth} |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
165 |
The following @{text "dependants wq th"} represents the set of threads which are RAGing on |
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
166 |
thread @{text "th"} in Resource Allocation Graph @{text "RAG wq"}: |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
168 |
*} |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
169 |
cs_dependants_def: |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
170 |
"dependants (wq::cs \<Rightarrow> thread list) th \<equiv> {th' . (Th th', Th th) \<in> (RAG wq)^+}" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
171 |
|
17
105715a0a807
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
0
diff
changeset
|
172 |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
174 |
The data structure used by the operating system for scheduling is referred to as |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
{\em schedule state}. It is represented as a record consisting of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
176 |
a function assigning waiting queue to resources and a function assigning precedence to |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
threads: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
179 |
record schedule_state = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
wq_fun :: "cs \<Rightarrow> thread list" -- {* The function assigning waiting queue. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
181 |
cprec_fun :: "thread \<Rightarrow> precedence" -- {* The function assigning precedence. *} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
183 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
The following |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
@{text "cpreced s th"} gives the {\em current precedence} of thread @{text "th"} under |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
state @{text "s"}. The definition of @{text "cpreced"} reflects the basic idea of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
187 |
Priority Inheritance that the {\em current precedence} of a thread is the precedence |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
188 |
inherited from the maximum of all its dependants, i.e. the threads which are waiting |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
directly or indirectly waiting for some resources from it. If no such thread exits, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
@{text "th"}'s {\em current precedence} equals its original precedence, i.e. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
191 |
@{text "preced th s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
192 |
*} |
33
9b9f2117561f
simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
32
diff
changeset
|
193 |
|
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
194 |
definition cpreced :: "(cs \<Rightarrow> thread list) \<Rightarrow> state \<Rightarrow> thread \<Rightarrow> precedence" |
33
9b9f2117561f
simplified the cp_rec proof
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
32
diff
changeset
|
195 |
where "cpreced wq s = (\<lambda>th. Max ((\<lambda>th'. preced th' s) ` ({th} \<union> dependants wq th)))" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
196 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
197 |
(*<*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
198 |
lemma |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
199 |
cpreced_def2: |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
200 |
"cpreced wq s th \<equiv> Max ({preced th s} \<union> {preced th' s | th'. th' \<in> dependants wq th})" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
201 |
unfolding cpreced_def image_def |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
202 |
apply(rule eq_reflection) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
203 |
apply(rule_tac f="Max" in arg_cong) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
204 |
by (auto) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
205 |
(*>*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
206 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
207 |
abbreviation |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
208 |
"all_unlocked \<equiv> \<lambda>_::cs. ([]::thread list)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
209 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
210 |
abbreviation |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
211 |
"initial_cprec \<equiv> \<lambda>_::thread. Prc 0 0" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
212 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
213 |
abbreviation |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
214 |
"release qs \<equiv> case qs of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
215 |
[] => [] |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
216 |
| (_#qs) => (SOME q. distinct q \<and> set q = set qs)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
217 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
218 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
219 |
The following function @{text "schs"} is used to calculate the schedule state @{text "schs s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
220 |
It is the key function to model Priority Inheritance: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
221 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
222 |
fun schs :: "state \<Rightarrow> schedule_state" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
223 |
where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
224 |
"schs [] = (| wq_fun = \<lambda> cs. [], cprec_fun = (\<lambda>_. Prc 0 0) |)" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
225 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
226 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
227 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
228 |
\begin{enumerate} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
229 |
\item @{text "ps"} is the schedule state of last moment. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
230 |
\item @{text "pwq"} is the waiting queue function of last moment. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
231 |
\item @{text "pcp"} is the precedence function of last moment (NOT USED). |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
232 |
\item @{text "nwq"} is the new waiting queue function. It is calculated using a @{text "case"} statement: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
233 |
\begin{enumerate} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
234 |
\item If the happening event is @{text "P thread cs"}, @{text "thread"} is added to |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
235 |
the end of @{text "cs"}'s waiting queue. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
236 |
\item If the happening event is @{text "V thread cs"} and @{text "s"} is a legal state, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
237 |
@{text "th'"} must equal to @{text "thread"}, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
238 |
because @{text "thread"} is the one currently holding @{text "cs"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
239 |
The case @{text "[] \<Longrightarrow> []"} may never be executed in a legal state. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
240 |
the @{text "(SOME q. distinct q \<and> set q = set qs)"} is used to choose arbitrarily one |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
241 |
thread in waiting to take over the released resource @{text "cs"}. In our representation, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
242 |
this amounts to rearrange elements in waiting queue, so that one of them is put at the head. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
243 |
\item For other happening event, the schedule state just does not change. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
244 |
\end{enumerate} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
245 |
\item @{text "ncp"} is new precedence function, it is calculated from the newly updated waiting queue |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
246 |
function. The RAGency of precedence function on waiting queue function is the reason to |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
247 |
put them in the same record so that they can evolve together. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
248 |
\end{enumerate} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
249 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
250 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
251 |
"schs (Create th prio # s) = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
252 |
(let wq = wq_fun (schs s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
253 |
(|wq_fun = wq, cprec_fun = cpreced wq (Create th prio # s)|))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
254 |
| "schs (Exit th # s) = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
255 |
(let wq = wq_fun (schs s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
256 |
(|wq_fun = wq, cprec_fun = cpreced wq (Exit th # s)|))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
257 |
| "schs (Set th prio # s) = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
258 |
(let wq = wq_fun (schs s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
259 |
(|wq_fun = wq, cprec_fun = cpreced wq (Set th prio # s)|))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
260 |
| "schs (P th cs # s) = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
261 |
(let wq = wq_fun (schs s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
262 |
let new_wq = wq(cs := (wq cs @ [th])) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
263 |
(|wq_fun = new_wq, cprec_fun = cpreced new_wq (P th cs # s)|))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
264 |
| "schs (V th cs # s) = |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
265 |
(let wq = wq_fun (schs s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
266 |
let new_wq = wq(cs := release (wq cs)) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
267 |
(|wq_fun = new_wq, cprec_fun = cpreced new_wq (V th cs # s)|))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
268 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
269 |
lemma cpreced_initial: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
270 |
"cpreced (\<lambda> cs. []) [] = (\<lambda>_. (Prc 0 0))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
271 |
apply(simp add: cpreced_def) |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
272 |
apply(simp add: cs_dependants_def cs_RAG_def cs_waiting_def cs_holding_def) |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
273 |
apply(simp add: preced_def) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
274 |
done |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
275 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
276 |
lemma sch_old_def: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
277 |
"schs (e#s) = (let ps = schs s in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
278 |
let pwq = wq_fun ps in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
279 |
let nwq = case e of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
P th cs \<Rightarrow> pwq(cs:=(pwq cs @ [th])) | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
V th cs \<Rightarrow> let nq = case (pwq cs) of |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
282 |
[] \<Rightarrow> [] | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
(_#qs) \<Rightarrow> (SOME q. distinct q \<and> set q = set qs) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
in pwq(cs:=nq) | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
_ \<Rightarrow> pwq |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
in let ncp = cpreced nwq (e#s) in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
\<lparr>wq_fun = nwq, cprec_fun = ncp\<rparr> |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
288 |
)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
289 |
apply(cases e) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
290 |
apply(simp_all) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
291 |
done |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
292 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
293 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
294 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
295 |
\noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
296 |
The following @{text "wq"} is a shorthand for @{text "wq_fun"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
297 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
298 |
definition wq :: "state \<Rightarrow> cs \<Rightarrow> thread list" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
299 |
where "wq s = wq_fun (schs s)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
300 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
301 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
302 |
The following @{text "cp"} is a shorthand for @{text "cprec_fun"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
303 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
304 |
definition cp :: "state \<Rightarrow> thread \<Rightarrow> precedence" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
305 |
where "cp s \<equiv> cprec_fun (schs s)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
306 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
307 |
text {* \noindent |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
308 |
Functions @{text "holding"}, @{text "waiting"}, @{text "RAG"} and |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
309 |
@{text "dependants"} still have the |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
310 |
same meaning, but redefined so that they no longer RAG on the |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
311 |
fictitious {\em waiting queue function} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
312 |
@{text "wq"}, but on system state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
313 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
314 |
defs (overloaded) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
315 |
s_holding_abv: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
316 |
"holding (s::state) \<equiv> holding (wq_fun (schs s))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
317 |
s_waiting_abv: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
318 |
"waiting (s::state) \<equiv> waiting (wq_fun (schs s))" |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
319 |
s_RAG_abv: |
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
320 |
"RAG (s::state) \<equiv> RAG (wq_fun (schs s))" |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
321 |
s_dependants_abv: |
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
322 |
"dependants (s::state) \<equiv> dependants (wq_fun (schs s))" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
323 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
324 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
325 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
326 |
The following lemma can be proved easily: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
327 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
328 |
lemma |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
329 |
s_holding_def: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
330 |
"holding (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th = hd (wq_fun (schs s) cs))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
331 |
by (auto simp:s_holding_abv wq_def cs_holding_def) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
332 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
333 |
lemma s_waiting_def: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
334 |
"waiting (s::state) th cs \<equiv> (th \<in> set (wq_fun (schs s) cs) \<and> th \<noteq> hd (wq_fun (schs s) cs))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
335 |
by (auto simp:s_waiting_abv wq_def cs_waiting_def) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
336 |
|
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
337 |
lemma s_RAG_def: |
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
338 |
"RAG (s::state) = |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
339 |
{(Th th, Cs cs) | th cs. waiting (wq s) th cs} \<union> {(Cs cs, Th th) | cs th. holding (wq s) th cs}" |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
340 |
by (auto simp:s_RAG_abv wq_def cs_RAG_def) |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
341 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
342 |
lemma |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
343 |
s_dependants_def: |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
344 |
"dependants (s::state) th \<equiv> {th' . (Th th', Th th) \<in> (RAG (wq s))^+}" |
32
e861aff29655
made some modifications.
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
17
diff
changeset
|
345 |
by (auto simp:s_dependants_abv wq_def cs_dependants_def) |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
346 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
347 |
text {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
348 |
The following function @{text "readys"} calculates the set of ready threads. A thread is {\em ready} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
349 |
for running if it is a live thread and it is not waiting for any critical resource. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
350 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
351 |
definition readys :: "state \<Rightarrow> thread set" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
352 |
where "readys s \<equiv> {th . th \<in> threads s \<and> (\<forall> cs. \<not> waiting s th cs)}" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
353 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
354 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
355 |
The following function @{text "runing"} calculates the set of running thread, which is the ready |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
356 |
thread with the highest precedence. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
357 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
358 |
definition runing :: "state \<Rightarrow> thread set" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
359 |
where "runing s \<equiv> {th . th \<in> readys s \<and> cp s th = Max ((cp s) ` (readys s))}" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
360 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
361 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
362 |
The following function @{text "holdents s th"} returns the set of resources held by thread |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
363 |
@{text "th"} in state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
364 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
365 |
definition holdents :: "state \<Rightarrow> thread \<Rightarrow> cs set" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
366 |
where "holdents s th \<equiv> {cs . holding s th cs}" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
367 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
368 |
lemma holdents_test: |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
369 |
"holdents s th = {cs . (Cs cs, Th th) \<in> RAG s}" |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
370 |
unfolding holdents_def |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
371 |
unfolding s_RAG_def |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
372 |
unfolding s_holding_abv |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
373 |
unfolding wq_def |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
374 |
by (simp) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
375 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
376 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
377 |
@{text "cntCS s th"} returns the number of resources held by thread @{text "th"} in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
378 |
state @{text "s"}: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
379 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
380 |
definition cntCS :: "state \<Rightarrow> thread \<Rightarrow> nat" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
381 |
where "cntCS s th = card (holdents s th)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
382 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
383 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
384 |
The fact that event @{text "e"} is eligible to happen next in state @{text "s"} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
385 |
is expressed as @{text "step s e"}. The predicate @{text "step"} is inductively defined as |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
386 |
follows: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
387 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
388 |
inductive step :: "state \<Rightarrow> event \<Rightarrow> bool" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
389 |
where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
390 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
391 |
A thread can be created if it is not a live thread: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
392 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
393 |
thread_create: "\<lbrakk>thread \<notin> threads s\<rbrakk> \<Longrightarrow> step s (Create thread prio)" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
394 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
395 |
A thread can exit if it no longer hold any resource: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
396 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
397 |
thread_exit: "\<lbrakk>thread \<in> runing s; holdents s thread = {}\<rbrakk> \<Longrightarrow> step s (Exit thread)" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
398 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
399 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
400 |
A thread can request for an critical resource @{text "cs"}, if it is running and |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
401 |
the request does not form a loop in the current RAG. The latter condition |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
402 |
is set up to avoid deadlock. The condition also reflects our assumption all threads are |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
403 |
carefully programmed so that deadlock can not happen: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
404 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
405 |
*} |
35
92f61f6a0fe7
added a bit more text to the paper and separated a theory about Max
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
33
diff
changeset
|
406 |
thread_P: "\<lbrakk>thread \<in> runing s; (Cs cs, Th thread) \<notin> (RAG s)^+\<rbrakk> \<Longrightarrow> |
0
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
407 |
step s (P thread cs)" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
408 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
409 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
410 |
A thread can release a critical resource @{text "cs"} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
411 |
if it is running and holding that resource: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
412 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
413 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
414 |
thread_V: "\<lbrakk>thread \<in> runing s; holding s thread cs\<rbrakk> \<Longrightarrow> step s (V thread cs)" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
415 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
416 |
A thread can adjust its own priority as long as it is current running: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
417 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
418 |
thread_set: "\<lbrakk>thread \<in> runing s\<rbrakk> \<Longrightarrow> step s (Set thread prio)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
419 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
420 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
421 |
With predicate @{text "step"}, the fact that @{text "s"} is a legal state in |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
422 |
Priority Inheritance protocol can be expressed as: @{text "vt step s"}, where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
423 |
the predicate @{text "vt"} can be defined as the following: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
424 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
425 |
inductive vt :: "state \<Rightarrow> bool" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
426 |
where |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
427 |
-- {* Empty list @{text "[]"} is a legal state in any protocol:*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
428 |
vt_nil[intro]: "vt []" | |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
429 |
-- {* |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
430 |
\begin{minipage}{0.9\textwidth} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
431 |
If @{text "s"} a legal state, and event @{text "e"} is eligible to happen |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
432 |
in state @{text "s"}, then @{text "e#s"} is a legal state as well: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
433 |
\end{minipage} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
434 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
435 |
vt_cons[intro]: "\<lbrakk>vt s; step s e\<rbrakk> \<Longrightarrow> vt (e#s)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
436 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
437 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
438 |
It is easy to see that the definition of @{text "vt"} is generic. It can be applied to |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
439 |
any step predicate to get the set of legal states. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
440 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
441 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
442 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
443 |
The following two functions @{text "the_cs"} and @{text "the_th"} are used to extract |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
444 |
critical resource and thread respectively out of RAG nodes. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
445 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
446 |
fun the_cs :: "node \<Rightarrow> cs" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
447 |
where "the_cs (Cs cs) = cs" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
448 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
449 |
fun the_th :: "node \<Rightarrow> thread" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
450 |
where "the_th (Th th) = th" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
451 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
452 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
453 |
The following predicate @{text "next_th"} describe the next thread to |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
454 |
take over when a critical resource is released. In @{text "next_th s th cs t"}, |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
455 |
@{text "th"} is the thread to release, @{text "t"} is the one to take over. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
456 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
457 |
definition next_th:: "state \<Rightarrow> thread \<Rightarrow> cs \<Rightarrow> thread \<Rightarrow> bool" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
458 |
where "next_th s th cs t = (\<exists> rest. wq s cs = th#rest \<and> rest \<noteq> [] \<and> |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
459 |
t = hd (SOME q. distinct q \<and> set q = set rest))" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
460 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
461 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
462 |
The function @{text "count Q l"} is used to count the occurrence of situation @{text "Q"} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
463 |
in list @{text "l"}: |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
464 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
465 |
definition count :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> nat" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
466 |
where "count Q l = length (filter Q l)" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
467 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
468 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
469 |
The following @{text "cntP s"} returns the number of operation @{text "P"} happened |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
470 |
before reaching state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
471 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
472 |
definition cntP :: "state \<Rightarrow> thread \<Rightarrow> nat" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
473 |
where "cntP s th = count (\<lambda> e. \<exists> cs. e = P th cs) s" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
474 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
475 |
text {* \noindent |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
476 |
The following @{text "cntV s"} returns the number of operation @{text "V"} happened |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
477 |
before reaching state @{text "s"}. |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
478 |
*} |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
479 |
definition cntV :: "state \<Rightarrow> thread \<Rightarrow> nat" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
480 |
where "cntV s th = count (\<lambda> e. \<exists> cs. e = V th cs) s" |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
481 |
(*<*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
482 |
|
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
483 |
end |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
484 |
(*>*) |
110247f9d47e
added
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
485 |