|
262
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
|
3 |
\def\isabellecontext{PrioGDef}%
|
|
|
4 |
%
|
|
|
5 |
\isadelimtheory
|
|
|
6 |
%
|
|
|
7 |
\endisadelimtheory
|
|
|
8 |
%
|
|
|
9 |
\isatagtheory
|
|
|
10 |
%
|
|
|
11 |
\endisatagtheory
|
|
|
12 |
{\isafoldtheory}%
|
|
|
13 |
%
|
|
|
14 |
\isadelimtheory
|
|
|
15 |
%
|
|
|
16 |
\endisadelimtheory
|
|
|
17 |
%
|
|
|
18 |
\begin{isamarkuptext}%
|
|
|
19 |
In this section, the formal model of Priority Inheritance is presented. First, the identifiers of {\em threads},
|
|
|
20 |
{\em priority} and {\em critical resources } (abbreviated as \isa{cs}) are all represented as natural numbers,
|
|
|
21 |
i.e. standard Isabelle/HOL type \isa{nat}.%
|
|
|
22 |
\end{isamarkuptext}%
|
|
|
23 |
\isamarkuptrue%
|
|
|
24 |
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
|
|
|
25 |
\ thread\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
|
|
|
26 |
\isamarkupcmt{Type for thread identifiers.%
|
|
|
27 |
}
|
|
|
28 |
\isanewline
|
|
|
29 |
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
|
|
|
30 |
\ priority\ {\isaliteral{3D}{\isacharequal}}\ nat\ \ %
|
|
|
31 |
\isamarkupcmt{Type for priorities.%
|
|
|
32 |
}
|
|
|
33 |
\isanewline
|
|
|
34 |
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
|
|
|
35 |
\ cs\ {\isaliteral{3D}{\isacharequal}}\ nat\ %
|
|
|
36 |
\isamarkupcmt{Type for critical sections (or critical resources).%
|
|
|
37 |
}
|
|
|
38 |
%
|
|
|
39 |
\begin{isamarkuptext}%
|
|
|
40 |
Priority Inheritance protocol is modeled as an event driven system, where every event represents an
|
|
|
41 |
system call. Event format is given by the following type definition:%
|
|
|
42 |
\end{isamarkuptext}%
|
|
|
43 |
\isamarkuptrue%
|
|
|
44 |
\isacommand{datatype}\isamarkupfalse%
|
|
|
45 |
\ event\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
46 |
\ \ Create\ thread\ priority\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
47 |
\isamarkupcmt{Thread \isa{thread} is created with priority \isa{priority}.%
|
|
|
48 |
}
|
|
|
49 |
\isanewline
|
|
|
50 |
\ \ Exit\ thread\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
51 |
\isamarkupcmt{Thread \isa{thread} finishing its execution.%
|
|
|
52 |
}
|
|
|
53 |
\isanewline
|
|
|
54 |
\ \ P\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
55 |
\isamarkupcmt{Thread \isa{thread} requesting critical resource \isa{cs}.%
|
|
|
56 |
}
|
|
|
57 |
\isanewline
|
|
|
58 |
\ \ V\ thread\ cs\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
59 |
\isamarkupcmt{Thread \isa{thread} releasing critical resource \isa{cs}.%
|
|
|
60 |
}
|
|
|
61 |
\isanewline
|
|
|
62 |
\ \ Set\ thread\ priority\ %
|
|
|
63 |
\isamarkupcmt{Thread \isa{thread} resets its priority to \isa{priority}.%
|
|
|
64 |
}
|
|
|
65 |
%
|
|
|
66 |
\begin{isamarkuptext}%
|
|
|
67 |
Resource Allocation Graph (RAG for short) is used extensively in the analysis of Priority Inheritance.
|
|
|
68 |
The following type \isa{node} is used to model nodes in RAG.%
|
|
|
69 |
\end{isamarkuptext}%
|
|
|
70 |
\isamarkuptrue%
|
|
|
71 |
\isacommand{datatype}\isamarkupfalse%
|
|
|
72 |
\ node\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
73 |
\ \ \ Th\ {\isaliteral{22}{\isachardoublequoteopen}}thread{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
74 |
\isamarkupcmt{Node for thread.%
|
|
|
75 |
}
|
|
|
76 |
\isanewline
|
|
|
77 |
\ \ \ Cs\ {\isaliteral{22}{\isachardoublequoteopen}}cs{\isaliteral{22}{\isachardoublequoteclose}}\ %
|
|
|
78 |
\isamarkupcmt{Node for critical resource.%
|
|
|
79 |
}
|
|
|
80 |
%
|
|
|
81 |
\begin{isamarkuptext}%
|
|
|
82 |
The protocol is analyzed using Paulson's inductive protocol verification method, where
|
|
|
83 |
the state of the system is modelled as the list of events happened so far with the latest
|
|
|
84 |
event at the head. Therefore, the state of the system is represented by the following
|
|
|
85 |
type \isa{state}.%
|
|
|
86 |
\end{isamarkuptext}%
|
|
|
87 |
\isamarkuptrue%
|
|
|
88 |
\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
|
|
|
89 |
\ state\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}event\ list{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
90 |
\begin{isamarkuptext}%
|
|
|
91 |
The following \isa{threads} is used to calculate the set of live threads (\isa{threads\ s})
|
|
|
92 |
in state \isa{s}.%
|
|
|
93 |
\end{isamarkuptext}%
|
|
|
94 |
\isamarkuptrue%
|
|
|
95 |
\isacommand{fun}\isamarkupfalse%
|
|
|
96 |
\ threads\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
97 |
\isakeyword{where}\ \isanewline
|
|
|
98 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
99 |
\isamarkupcmt{At the start of the system, the set of threads is empty.%
|
|
|
100 |
}
|
|
|
101 |
\isanewline
|
|
|
102 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
103 |
\isamarkupcmt{New thread is added to the \isa{threads}.%
|
|
|
104 |
}
|
|
|
105 |
\isanewline
|
|
|
106 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread\ {\isaliteral{23}{\isacharhash}}\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}threads\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{7B}{\isacharbraceleft}}thread{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
107 |
\isamarkupcmt{Finished thread is removed.%
|
|
|
108 |
}
|
|
|
109 |
\isanewline
|
|
|
110 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}threads\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ threads\ s{\isaliteral{22}{\isachardoublequoteclose}}\ %
|
|
|
111 |
\isamarkupcmt{other kind of events does not affect the value of \isa{threads}.%
|
|
|
112 |
}
|
|
|
113 |
%
|
|
|
114 |
\begin{isamarkuptext}%
|
|
|
115 |
Functions such as \isa{threads}, which extract information out of system states, are called
|
|
|
116 |
{\em observing functions}. A series of observing functions will be defined in the sequel in order to
|
|
|
117 |
model the protocol.
|
|
|
118 |
Observing function \isa{original{\isaliteral{5F}{\isacharunderscore}}priority} calculates
|
|
|
119 |
the {\em original priority} of thread \isa{th} in state \isa{s}, expressed as
|
|
|
120 |
: \isa{original{\isaliteral{5F}{\isacharunderscore}}priority\ th\ s}. The {\em original priority} is the priority
|
|
|
121 |
assigned to a thread when it is created or when it is reset by system call \isa{Set\ thread\ priority}.%
|
|
|
122 |
\end{isamarkuptext}%
|
|
|
123 |
\isamarkuptrue%
|
|
|
124 |
\isacommand{fun}\isamarkupfalse%
|
|
|
125 |
\ original{\isaliteral{5F}{\isacharunderscore}}priority\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ priority{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
126 |
\isakeyword{where}\isanewline
|
|
|
127 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\ %
|
|
|
128 |
\isamarkupcmt{\isa{{\isadigit{0}}} is assigned to threads which have never been created.%
|
|
|
129 |
}
|
|
|
130 |
\isanewline
|
|
|
131 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
132 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
133 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
134 |
\ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ thread{\isaliteral{27}{\isacharprime}}\ {\isaliteral{3D}{\isacharequal}}\ thread\ then\ prio\ else\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
135 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
136 |
\begin{isamarkuptext}%
|
|
|
137 |
\isa{birthtime\ th\ s} is the time when thread \isa{th} is created, observed from state \isa{s}.
|
|
|
138 |
The time in the system is measured by the number of events happened so far since the very beginning.%
|
|
|
139 |
\end{isamarkuptext}%
|
|
|
140 |
\isamarkuptrue%
|
|
|
141 |
\isacommand{fun}\isamarkupfalse%
|
|
|
142 |
\ birthtime\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
143 |
\isakeyword{where}\isanewline
|
|
|
144 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
145 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Create\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
|
|
|
146 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
147 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}Set\ thread{\isaliteral{27}{\isacharprime}}\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{3D}{\isacharequal}}\ thread{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}\ then\ length\ s\ \isanewline
|
|
|
148 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
149 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}birthtime\ thread\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ birthtime\ thread\ s{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
150 |
\begin{isamarkuptext}%
|
|
|
151 |
The {\em precedence} is a notion derived from {\em priority}, where the {\em precedence} of
|
|
|
152 |
a thread is the combination of its {\em original priority} and {\em birth time}. The intention is
|
|
|
153 |
to discriminate threads with the same priority by giving threads with the earlier assigned priority
|
|
|
154 |
higher precedence in scheduling. This explains the following definition:%
|
|
|
155 |
\end{isamarkuptext}%
|
|
|
156 |
\isamarkuptrue%
|
|
|
157 |
\isacommand{definition}\isamarkupfalse%
|
|
|
158 |
\ preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
159 |
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}preced\ thread\ s\ {\isaliteral{3D}{\isacharequal}}\ Prc\ {\isaliteral{28}{\isacharparenleft}}original{\isaliteral{5F}{\isacharunderscore}}priority\ thread\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}birthtime\ thread\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
160 |
\begin{isamarkuptext}%
|
|
|
161 |
A number of important notions are defined here:%
|
|
|
162 |
\end{isamarkuptext}%
|
|
|
163 |
\isamarkuptrue%
|
|
|
164 |
\isacommand{consts}\isamarkupfalse%
|
|
|
165 |
\ \isanewline
|
|
|
166 |
\ \ holding\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
|
|
|
167 |
\ \ \ \ \ \ \ waiting\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
168 |
\ \ \ \ \ \ \ depend\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}node\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ node{\isaliteral{29}{\isacharparenright}}\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
169 |
\ \ \ \ \ \ \ dependents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
170 |
\begin{isamarkuptext}%
|
|
|
171 |
The definition of the following several functions, it is supposed that
|
|
|
172 |
the waiting queue of every critical resource is given by a waiting queue
|
|
|
173 |
function \isa{wq}, which servers as arguments of these functions.%
|
|
|
174 |
\end{isamarkuptext}%
|
|
|
175 |
\isamarkuptrue%
|
|
|
176 |
\isacommand{defs}\isamarkupfalse%
|
|
|
177 |
\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
|
|
|
178 |
\ \ %
|
|
|
179 |
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
|
|
|
180 |
We define that the thread which is at the head of waiting queue of resource \isa{cs}
|
|
|
181 |
is holding the resource. This definition is slightly different from tradition where
|
|
|
182 |
all threads in the waiting queue are considered as waiting for the resource.
|
|
|
183 |
This notion is reflected in the definition of \isa{holding\ wq\ th\ cs} as follows:
|
|
|
184 |
\end{minipage}%
|
|
|
185 |
}
|
|
|
186 |
\isanewline
|
|
|
187 |
\ \ cs{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
188 |
\ \ %
|
|
|
189 |
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
|
|
|
190 |
In accordance with the definition of \isa{holding\ wq\ th\ cs},
|
|
|
191 |
a thread \isa{th} is considered waiting for \isa{cs} if
|
|
|
192 |
it is in the {\em waiting queue} of critical resource \isa{cs}, but not at the head.
|
|
|
193 |
This is reflected in the definition of \isa{waiting\ wq\ th\ cs} as follows:
|
|
|
194 |
\end{minipage}%
|
|
|
195 |
}
|
|
|
196 |
\isanewline
|
|
|
197 |
\ \ cs{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ wq\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
198 |
\ \ %
|
|
|
199 |
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
|
|
|
200 |
\isa{depend\ wq} represents the Resource Allocation Graph of the system under the waiting
|
|
|
201 |
queue function \isa{wq}.
|
|
|
202 |
\end{minipage}%
|
|
|
203 |
}
|
|
|
204 |
\isanewline
|
|
|
205 |
\ \ cs{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
|
|
|
206 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ wq\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
207 |
\ \ %
|
|
|
208 |
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
|
|
|
209 |
\isa{dependents\ wq\ th} represents the set of threads which are depending on
|
|
|
210 |
thread \isa{th} in Resource Allocation Graph \isa{depend\ wq}:
|
|
|
211 |
\end{minipage}%
|
|
|
212 |
}
|
|
|
213 |
\isanewline
|
|
|
214 |
\ \ cs{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}wq{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ wq{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
215 |
\begin{isamarkuptext}%
|
|
|
216 |
The data structure used by the operating system for scheduling is referred to as
|
|
|
217 |
{\em schedule state}. It is represented as a record consisting of
|
|
|
218 |
a function assigning waiting queue to resources and a function assigning precedence to
|
|
|
219 |
threads:%
|
|
|
220 |
\end{isamarkuptext}%
|
|
|
221 |
\isamarkuptrue%
|
|
|
222 |
\isacommand{record}\isamarkupfalse%
|
|
|
223 |
\ schedule{\isaliteral{5F}{\isacharunderscore}}state\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
224 |
\ \ \ \ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ %
|
|
|
225 |
\isamarkupcmt{The function assigning waiting queue.%
|
|
|
226 |
}
|
|
|
227 |
\isanewline
|
|
|
228 |
\ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\ %
|
|
|
229 |
\isamarkupcmt{The function assigning precedence.%
|
|
|
230 |
}
|
|
|
231 |
%
|
|
|
232 |
\begin{isamarkuptext}%
|
|
|
233 |
\isa{cpreced\ s\ th} gives the {\em current precedence} of thread \isa{th} under
|
|
|
234 |
state \isa{s}. The definition of \isa{cpreced} reflects the basic idea of
|
|
|
235 |
Priority Inheritance that the {\em current precedence} of a thread is the precedence
|
|
|
236 |
inherited from the maximum of all its dependents, i.e. the threads which are waiting
|
|
|
237 |
directly or indirectly waiting for some resources from it. If no such thread exits,
|
|
|
238 |
\isa{th}'s {\em current precedence} equals its original precedence, i.e.
|
|
|
239 |
\isa{preced\ th\ s}.%
|
|
|
240 |
\end{isamarkuptext}%
|
|
|
241 |
\isamarkuptrue%
|
|
|
242 |
\isacommand{definition}\isamarkupfalse%
|
|
|
243 |
\ cpreced\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
244 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cpreced\ s\ wq\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ th{\isaliteral{2E}{\isachardot}}\ preced\ th\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ dependents\ wq\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
245 |
\begin{isamarkuptext}%
|
|
|
246 |
The following function \isa{schs} is used to calculate the schedule state \isa{schs\ s}.
|
|
|
247 |
It is the key function to model Priority Inheritance:%
|
|
|
248 |
\end{isamarkuptext}%
|
|
|
249 |
\isamarkuptrue%
|
|
|
250 |
\isacommand{fun}\isamarkupfalse%
|
|
|
251 |
\ schs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ schedule{\isaliteral{5F}{\isacharunderscore}}state{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
252 |
\isakeyword{where}\isanewline
|
|
|
253 |
\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ \isanewline
|
|
|
254 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C72706172723E}{\isasymrparr}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
255 |
\ \ %
|
|
|
256 |
\isamarkupcmt{\begin{minipage}{0.8\textwidth}
|
|
|
257 |
\begin{enumerate}
|
|
|
258 |
\item \isa{ps} is the schedule state of last moment.
|
|
|
259 |
\item \isa{pwq} is the waiting queue function of last moment.
|
|
|
260 |
\item \isa{pcp} is the precedence function of last moment.
|
|
|
261 |
\item \isa{nwq} is the new waiting queue function. It is calculated using a \isa{case} statement:
|
|
|
262 |
\begin{enumerate}
|
|
|
263 |
\item If the happening event is \isa{P\ thread\ cs}, \isa{thread} is added to
|
|
|
264 |
the end of \isa{cs}'s waiting queue.
|
|
|
265 |
\item If the happening event is \isa{V\ thread\ cs} and \isa{s} is a legal state,
|
|
|
266 |
\isa{th{\isaliteral{27}{\isacharprime}}} must equal to \isa{thread},
|
|
|
267 |
because \isa{thread} is the one currently holding \isa{cs}.
|
|
|
268 |
The case \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} may never be executed in a legal state.
|
|
|
269 |
the \isa{{\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}} is used to choose arbitrarily one
|
|
|
270 |
thread in waiting to take over the released resource \isa{cs}. In our representation,
|
|
|
271 |
this amounts to rearrange elements in waiting queue, so that one of them is put at the head.
|
|
|
272 |
\item For other happening event, the schedule state just does not change.
|
|
|
273 |
\end{enumerate}
|
|
|
274 |
\item \isa{ncp} is new precedence function, it is calculated from the newly updated waiting queue
|
|
|
275 |
function. The dependency of precedence function on waiting queue function is the reason to
|
|
|
276 |
put them in the same record so that they can evolve together.
|
|
|
277 |
\end{enumerate}
|
|
|
278 |
\end{minipage}%
|
|
|
279 |
}
|
|
|
280 |
\isanewline
|
|
|
281 |
\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}schs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}let\ ps\ {\isaliteral{3D}{\isacharequal}}\ schs\ s\ in\ \isanewline
|
|
|
282 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pwq\ {\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ ps\ in\ \isanewline
|
|
|
283 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ pcp\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ ps\ in\isanewline
|
|
|
284 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ let\ nwq\ {\isaliteral{3D}{\isacharequal}}\ case\ e\ of\isanewline
|
|
|
285 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ P\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ \ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}{\isaliteral{28}{\isacharparenleft}}pwq\ cs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}thread{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
286 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ V\ thread\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ let\ nq\ {\isaliteral{3D}{\isacharequal}}\ case\ {\isaliteral{28}{\isacharparenleft}}pwq\ cs{\isaliteral{29}{\isacharparenright}}\ of\isanewline
|
|
|
287 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{7C}{\isacharbar}}\ \isanewline
|
|
|
288 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}th{\isaliteral{27}{\isacharprime}}{\isaliteral{23}{\isacharhash}}qs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ qs{\isaliteral{29}{\isacharparenright}}\isanewline
|
|
|
289 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ pwq{\isaliteral{28}{\isacharparenleft}}cs{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}nq{\isaliteral{29}{\isacharparenright}}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
290 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ pwq\isanewline
|
|
|
291 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ in\ let\ ncp\ {\isaliteral{3D}{\isacharequal}}\ cpreced\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}\ nwq\ in\ \isanewline
|
|
|
292 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{5C3C6C706172723E}{\isasymlparr}}waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{3D}{\isacharequal}}\ nwq{\isaliteral{2C}{\isacharcomma}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{3D}{\isacharequal}}\ ncp{\isaliteral{5C3C72706172723E}{\isasymrparr}}\isanewline
|
|
|
293 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
294 |
\begin{isamarkuptext}%
|
|
|
295 |
\isa{wq} is a shorthand for \isa{waiting{\isaliteral{5F}{\isacharunderscore}}queue}.%
|
|
|
296 |
\end{isamarkuptext}%
|
|
|
297 |
\isamarkuptrue%
|
|
|
298 |
\isacommand{definition}\isamarkupfalse%
|
|
|
299 |
\ wq\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isanewline
|
|
|
300 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}wq\ s\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ waiting{\isaliteral{5F}{\isacharunderscore}}queue\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
301 |
\begin{isamarkuptext}%
|
|
|
302 |
\isa{cp} is a shorthand for \isa{cur{\isaliteral{5F}{\isacharunderscore}}preced}.%
|
|
|
303 |
\end{isamarkuptext}%
|
|
|
304 |
\isamarkuptrue%
|
|
|
305 |
\isacommand{definition}\isamarkupfalse%
|
|
|
306 |
\ cp\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ precedence{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
307 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cp\ s\ {\isaliteral{3D}{\isacharequal}}\ cur{\isaliteral{5F}{\isacharunderscore}}preced\ {\isaliteral{28}{\isacharparenleft}}schs\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
308 |
\begin{isamarkuptext}%
|
|
|
309 |
Functions \isa{holding}, \isa{waiting}, \isa{depend} and \isa{dependents} still have the
|
|
|
310 |
same meaning, but redefined so that they no longer depend on the fictitious {\em waiting queue function}
|
|
|
311 |
\isa{wq}, but on system state \isa{s}.%
|
|
|
312 |
\end{isamarkuptext}%
|
|
|
313 |
\isamarkuptrue%
|
|
|
314 |
\isacommand{defs}\isamarkupfalse%
|
|
|
315 |
\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{overloaded}{\isaliteral{29}{\isacharparenright}}\ \isanewline
|
|
|
316 |
\ \ s{\isaliteral{5F}{\isacharunderscore}}holding{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}holding\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
317 |
\ \ s{\isaliteral{5F}{\isacharunderscore}}waiting{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}waiting\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ thread\ cs\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ thread\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ hd\ {\isaliteral{28}{\isacharparenleft}}wq\ s\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
318 |
\ \ s{\isaliteral{5F}{\isacharunderscore}}depend{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}depend\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Th\ t{\isaliteral{2C}{\isacharcomma}}\ Cs\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ t\ c{\isaliteral{2E}{\isachardot}}\ waiting\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ \isanewline
|
|
|
319 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{28}{\isacharparenleft}}Cs\ c{\isaliteral{2C}{\isacharcomma}}\ Th\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ c\ t{\isaliteral{2E}{\isachardot}}\ holding\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}\ t\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
320 |
\ \ s{\isaliteral{5F}{\isacharunderscore}}dependents{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}dependents\ {\isaliteral{28}{\isacharparenleft}}s{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}state{\isaliteral{29}{\isacharparenright}}\ th\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th{\isaliteral{27}{\isacharprime}}\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{27}{\isacharprime}}{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ {\isaliteral{28}{\isacharparenleft}}wq\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
321 |
\begin{isamarkuptext}%
|
|
|
322 |
The following function \isa{readys} calculates the set of ready threads. A thread is {\em ready}
|
|
|
323 |
for running if it is a live thread and it is not waiting for any critical resource.%
|
|
|
324 |
\end{isamarkuptext}%
|
|
|
325 |
\isamarkuptrue%
|
|
|
326 |
\isacommand{definition}\isamarkupfalse%
|
|
|
327 |
\ readys\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
328 |
\isakeyword{where}\isanewline
|
|
|
329 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}readys\ s\ {\isaliteral{3D}{\isacharequal}}\ \isanewline
|
|
|
330 |
\ \ \ \ \ {\isaliteral{7B}{\isacharbraceleft}}thread\ {\isaliteral{2E}{\isachardot}}\ thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ threads\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}\ cs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ waiting\ s\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
331 |
\begin{isamarkuptext}%
|
|
|
332 |
The following function \isa{runing} calculates the set of running thread, which is the ready
|
|
|
333 |
thread with the highest precedence.%
|
|
|
334 |
\end{isamarkuptext}%
|
|
|
335 |
\isamarkuptrue%
|
|
|
336 |
\isacommand{definition}\isamarkupfalse%
|
|
|
337 |
\ runing\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
338 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}runing\ s\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}th\ {\isaliteral{2E}{\isachardot}}\ th\ {\isaliteral{5C3C696E3E}{\isasymin}}\ readys\ s\ {\isaliteral{5C3C616E643E}{\isasymand}}\ cp\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ Max\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}cp\ s{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{60}{\isacharbackquote}}\ {\isaliteral{28}{\isacharparenleft}}readys\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
339 |
\begin{isamarkuptext}%
|
|
|
340 |
The following function \isa{holdents\ s\ th} returns the set of resources held by thread
|
|
|
341 |
\isa{th} in state \isa{s}.%
|
|
|
342 |
\end{isamarkuptext}%
|
|
|
343 |
\isamarkuptrue%
|
|
|
344 |
\isacommand{definition}\isamarkupfalse%
|
|
|
345 |
\ holdents\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ set{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
346 |
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}holdents\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}cs\ {\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ depend\ s{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
347 |
\begin{isamarkuptext}%
|
|
|
348 |
\isa{cntCS\ s\ th} returns the number of resources held by thread \isa{th} in
|
|
|
349 |
state \isa{s}:%
|
|
|
350 |
\end{isamarkuptext}%
|
|
|
351 |
\isamarkuptrue%
|
|
|
352 |
\isacommand{definition}\isamarkupfalse%
|
|
|
353 |
\ cntCS\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
354 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntCS\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ card\ {\isaliteral{28}{\isacharparenleft}}holdents\ s\ th{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
355 |
\begin{isamarkuptext}%
|
|
|
356 |
The fact that event \isa{e} is eligible to happen next in state \isa{s}
|
|
|
357 |
is expressed as \isa{step\ s\ e}. The predicate \isa{step} is inductively defined as
|
|
|
358 |
follows:%
|
|
|
359 |
\end{isamarkuptext}%
|
|
|
360 |
\isamarkuptrue%
|
|
|
361 |
\isacommand{inductive}\isamarkupfalse%
|
|
|
362 |
\ step\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
363 |
\isakeyword{where}\isanewline
|
|
|
364 |
\ \ %
|
|
|
365 |
\isamarkupcmt{A thread can be created if it is not a live thread:%
|
|
|
366 |
}
|
|
|
367 |
\isanewline
|
|
|
368 |
\ \ thread{\isaliteral{5F}{\isacharunderscore}}create{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ threads\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Create\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
369 |
\ \ %
|
|
|
370 |
\isamarkupcmt{A thread can exit if it no longer hold any resource:%
|
|
|
371 |
}
|
|
|
372 |
\isanewline
|
|
|
373 |
\ \ thread{\isaliteral{5F}{\isacharunderscore}}exit{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ holdents\ s\ thread\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Exit\ thread{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
374 |
\ \ %
|
|
|
375 |
\isamarkupcmt{A thread can request for an critical resource \isa{cs}, if it is running and
|
|
|
376 |
the request does not form a loop in the current RAG. The latter condition
|
|
|
377 |
is set up to avoid deadlock. The condition also reflects our assumption all threads are
|
|
|
378 |
carefully programmed so that deadlock can not happen.%
|
|
|
379 |
}
|
|
|
380 |
\isanewline
|
|
|
381 |
\ \ thread{\isaliteral{5F}{\isacharunderscore}}P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{2C}{\isacharcomma}}\ Th\ thread{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{28}{\isacharparenleft}}depend\ s{\isaliteral{29}{\isacharparenright}}{\isaliteral{5E}{\isacharcircum}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}P\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
382 |
\ \ %
|
|
|
383 |
\isamarkupcmt{A thread can release a critical resource \isa{cs} if it is running and holding that resource.%
|
|
|
384 |
}
|
|
|
385 |
\isanewline
|
|
|
386 |
\ \ thread{\isaliteral{5F}{\isacharunderscore}}V{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{3B}{\isacharsemicolon}}\ \ holding\ s\ thread\ cs{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}V\ thread\ cs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
387 |
\ \ %
|
|
|
388 |
\isamarkupcmt{A thread can adjust its own priority as long as it is current running.%
|
|
|
389 |
}
|
|
|
390 |
\ \ \isanewline
|
|
|
391 |
\ \ thread{\isaliteral{5F}{\isacharunderscore}}set{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}thread\ {\isaliteral{5C3C696E3E}{\isasymin}}\ runing\ s{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ step\ s\ {\isaliteral{28}{\isacharparenleft}}Set\ thread\ prio{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
392 |
\begin{isamarkuptext}%
|
|
|
393 |
With predicate \isa{step}, the fact that \isa{s} is a legal state in
|
|
|
394 |
Priority Inheritance protocol can be expressed as: \isa{vt\ step\ s}, where
|
|
|
395 |
the predicate \isa{vt} can be defined as the following:%
|
|
|
396 |
\end{isamarkuptext}%
|
|
|
397 |
\isamarkuptrue%
|
|
|
398 |
\isacommand{inductive}\isamarkupfalse%
|
|
|
399 |
\ vt\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ event\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
400 |
\ \isakeyword{for}\ cs\ %
|
|
|
401 |
\isamarkupcmt{\isa{cs} is an argument representing any step predicate.%
|
|
|
402 |
}
|
|
|
403 |
\isanewline
|
|
|
404 |
\isakeyword{where}\isanewline
|
|
|
405 |
\ \ %
|
|
|
406 |
\isamarkupcmt{Empty list \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is a legal state in any protocol:%
|
|
|
407 |
}
|
|
|
408 |
\isanewline
|
|
|
409 |
\ \ vt{\isaliteral{5F}{\isacharunderscore}}nil{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}vt\ cs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
|
|
|
410 |
\ \ %
|
|
|
411 |
\isamarkupcmt{If \isa{s} a legal state, and event \isa{e} is eligible to happen
|
|
|
412 |
in state \isa{s}, then \isa{e{\isaliteral{23}{\isacharhash}}{\isaliteral{23}{\isacharhash}}s} is a legal state as well:%
|
|
|
413 |
}
|
|
|
414 |
\isanewline
|
|
|
415 |
\ \ vt{\isaliteral{5F}{\isacharunderscore}}cons{\isaliteral{5B}{\isacharbrackleft}}intro{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}vt\ cs\ s{\isaliteral{3B}{\isacharsemicolon}}\ cs\ s\ e{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ vt\ cs\ {\isaliteral{28}{\isacharparenleft}}e{\isaliteral{23}{\isacharhash}}s{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
416 |
\begin{isamarkuptext}%
|
|
|
417 |
It is easy to see that the definition of \isa{vt} is generic. It can be applied to
|
|
|
418 |
any step predicate to get the set of legal states.%
|
|
|
419 |
\end{isamarkuptext}%
|
|
|
420 |
\isamarkuptrue%
|
|
|
421 |
%
|
|
|
422 |
\begin{isamarkuptext}%
|
|
|
423 |
The following two functions \isa{the{\isaliteral{5F}{\isacharunderscore}}cs} and \isa{the{\isaliteral{5F}{\isacharunderscore}}th} are used to extract
|
|
|
424 |
critical resource and thread respectively out of RAG nodes.%
|
|
|
425 |
\end{isamarkuptext}%
|
|
|
426 |
\isamarkuptrue%
|
|
|
427 |
\isacommand{fun}\isamarkupfalse%
|
|
|
428 |
\ the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
429 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}cs\ {\isaliteral{28}{\isacharparenleft}}Cs\ cs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ cs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
430 |
\isanewline
|
|
|
431 |
\isacommand{fun}\isamarkupfalse%
|
|
|
432 |
\ the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}node\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
433 |
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}the{\isaliteral{5F}{\isacharunderscore}}th\ {\isaliteral{28}{\isacharparenleft}}Th\ th{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
434 |
\begin{isamarkuptext}%
|
|
|
435 |
The following predicate \isa{next{\isaliteral{5F}{\isacharunderscore}}th} describe the next thread to
|
|
|
436 |
take over when a critical resource is released. In \isa{next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t},
|
|
|
437 |
\isa{th} is the thread to release, \isa{t} is the one to take over.%
|
|
|
438 |
\end{isamarkuptext}%
|
|
|
439 |
\isamarkuptrue%
|
|
|
440 |
\isacommand{definition}\isamarkupfalse%
|
|
|
441 |
\ next{\isaliteral{5F}{\isacharunderscore}}th{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ cs\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
442 |
\ \ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}next{\isaliteral{5F}{\isacharunderscore}}th\ s\ th\ cs\ t\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}\ rest{\isaliteral{2E}{\isachardot}}\ wq\ s\ cs\ {\isaliteral{3D}{\isacharequal}}\ th{\isaliteral{23}{\isacharhash}}rest\ {\isaliteral{5C3C616E643E}{\isasymand}}\ rest\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ \isanewline
|
|
|
443 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ t\ {\isaliteral{3D}{\isacharequal}}\ hd\ {\isaliteral{28}{\isacharparenleft}}SOME\ q{\isaliteral{2E}{\isachardot}}\ distinct\ q\ {\isaliteral{5C3C616E643E}{\isasymand}}\ set\ q\ {\isaliteral{3D}{\isacharequal}}\ set\ rest{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
444 |
\begin{isamarkuptext}%
|
|
|
445 |
The function \isa{count\ Q\ l} is used to count the occurrence of situation \isa{Q}
|
|
|
446 |
in list \isa{l}:%
|
|
|
447 |
\end{isamarkuptext}%
|
|
|
448 |
\isamarkuptrue%
|
|
|
449 |
\isacommand{definition}\isamarkupfalse%
|
|
|
450 |
\ count\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
451 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}count\ Q\ l\ {\isaliteral{3D}{\isacharequal}}\ length\ {\isaliteral{28}{\isacharparenleft}}filter\ Q\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
452 |
\begin{isamarkuptext}%
|
|
|
453 |
\isa{cntP\ s} returns the number of operation \isa{P} happened
|
|
|
454 |
before reaching state \isa{s}.%
|
|
|
455 |
\end{isamarkuptext}%
|
|
|
456 |
\isamarkuptrue%
|
|
|
457 |
\isacommand{definition}\isamarkupfalse%
|
|
|
458 |
\ cntP\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
459 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntP\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ P\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}%
|
|
|
460 |
\begin{isamarkuptext}%
|
|
|
461 |
\isa{cntV\ s} returns the number of operation \isa{V} happened
|
|
|
462 |
before reaching state \isa{s}.%
|
|
|
463 |
\end{isamarkuptext}%
|
|
|
464 |
\isamarkuptrue%
|
|
|
465 |
\isacommand{definition}\isamarkupfalse%
|
|
|
466 |
\ cntV\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}state\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ thread\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
467 |
\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}cntV\ s\ th\ {\isaliteral{3D}{\isacharequal}}\ count\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}\ e{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}\ cs{\isaliteral{2E}{\isachardot}}\ e\ {\isaliteral{3D}{\isacharequal}}\ V\ th\ cs{\isaliteral{29}{\isacharparenright}}\ s{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
|
|
468 |
%
|
|
|
469 |
\isadelimtheory
|
|
|
470 |
%
|
|
|
471 |
\endisadelimtheory
|
|
|
472 |
%
|
|
|
473 |
\isatagtheory
|
|
|
474 |
\isacommand{end}\isamarkupfalse%
|
|
|
475 |
%
|
|
|
476 |
\endisatagtheory
|
|
|
477 |
{\isafoldtheory}%
|
|
|
478 |
%
|
|
|
479 |
\isadelimtheory
|
|
|
480 |
\isanewline
|
|
|
481 |
%
|
|
|
482 |
\endisadelimtheory
|
|
|
483 |
\isanewline
|
|
|
484 |
\end{isabellebody}%
|
|
|
485 |
%%% Local Variables:
|
|
|
486 |
%%% mode: latex
|
|
|
487 |
%%% TeX-master: "root"
|
|
|
488 |
%%% End:
|