45 the scheduling software fell victim of Priority Inversion: a low |
45 the scheduling software fell victim of Priority Inversion: a low |
46 priority task locking a resource prevented a high priority process |
46 priority task locking a resource prevented a high priority process |
47 from running in time leading to a system reset. Once the problem was found, |
47 from running in time leading to a system reset. Once the problem was found, |
48 it was rectified by enabling the \emph{Priority Inheritance Protocol} |
48 it was rectified by enabling the \emph{Priority Inheritance Protocol} |
49 (PIP) \cite{Sha90}\footnote{Sha et al.~call it the |
49 (PIP) \cite{Sha90}\footnote{Sha et al.~call it the |
50 \emph{Basic Priority Inheritance Protocol}.} in the scheduling software. |
50 \emph{Basic Priority Inheritance Protocol} \cite{Sha90}.} in the scheduling software. |
51 |
51 |
52 The idea behind PIP is to let the process $L$ temporarily |
52 The idea behind PIP is to let the process $L$ temporarily |
53 inherit the high priority from $H$ until $L$ leaves the critical |
53 inherit the high priority from $H$ until $L$ leaves the critical |
54 section by unlocking the resource. This solves the problem of $H$ |
54 section by unlocking the resource. This solves the problem of $H$ |
55 having to wait indefinitely, because $L$ cannot be |
55 having to wait indefinitely, because $L$ cannot be |
88 However, there is clearly a need for investigating correct |
88 However, there is clearly a need for investigating correct |
89 algorithms for PIP. A few specifications for PIP exist (in English) |
89 algorithms for PIP. A few specifications for PIP exist (in English) |
90 and also a few high-level descriptions of implementations (e.g.~in |
90 and also a few high-level descriptions of implementations (e.g.~in |
91 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little |
91 the textbook \cite[Section 5.6.5]{Vahalia96}), but they help little |
92 with actual implementations. That this is a problem in practise is |
92 with actual implementations. That this is a problem in practise is |
93 proved by an email by Baker, who wrote on 13 July 2009 on the Linux |
93 proved by an email from Baker, who wrote on 13 July 2009 on the Linux |
94 Kernel mailing list: |
94 Kernel mailing list: |
95 |
95 |
96 \begin{quote} |
96 \begin{quote} |
97 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
97 \it{}``I observed in the kernel code (to my disgust), the Linux PIP |
98 implementation is a nightmare: extremely heavy weight, involving |
98 implementation is a nightmare: extremely heavy weight, involving |
105 The criticism by Yodaiken, Baker and others suggests to us to look |
105 The criticism by Yodaiken, Baker and others suggests to us to look |
106 again at PIP from a more abstract level (but still concrete enough |
106 again at PIP from a more abstract level (but still concrete enough |
107 to inform an implementation) and makes PIP an ideal candidate for a |
107 to inform an implementation) and makes PIP an ideal candidate for a |
108 formal verification. One reason, of course, is that the original |
108 formal verification. One reason, of course, is that the original |
109 presentation of PIP \cite{Sha90}, despite being informally |
109 presentation of PIP \cite{Sha90}, despite being informally |
110 ``proved'' correct, is actually \emph{flawed}. Yodaiken |
110 ``proved'' correct, is actually \emph{flawed}. |
111 \cite{Yodaiken02} points to a subtlety that had been overlooked in |
111 |
112 the informal proof by Sha et al. They specify in \cite{Sha90} that after the process (whose |
112 Yodaiken \cite{Yodaiken02} points to a subtlety that had been |
113 priority has been raised) completes its critical section and releases |
113 overlooked in the informal proof by Sha et al. They specify in |
114 the lock, it ``returns to its original priority level.'' This leads |
114 \cite{Sha90} that after the process (whose priority has been raised) |
115 them to believe that an implementation of PIP is ``rather |
115 completes its critical section and releases the lock, it ``returns |
116 straightforward'' \cite{Sha90}. Unfortunately, as Yodaiken pointed |
116 to its original priority level.'' This leads them to believe that an |
117 out, this behaviour is too simplistic. Consider the case where the |
117 implementation of PIP is ``rather straightforward'' \cite{Sha90}. |
118 low priority process $L$ locks \emph{two} resources, and two |
118 Unfortunately, as Yodaiken pointed out, this behaviour is too |
119 high-priority processes $H$ and $H'$ each wait for one of |
119 simplistic. Consider the case where the low priority process $L$ |
120 them. If $L$ then releases one resource so that $H$, say, can |
120 locks \emph{two} resources, and two high-priority processes $H$ and |
121 proceed, then we still have Priority Inversion with $H'$ (which waits for |
121 $H'$ each wait for one of them. If $L$ then releases one resource |
122 the other resource). The correct behaviour for $L$ |
122 so that $H$, say, can proceed, then we still have Priority Inversion |
123 is to revert to the highest remaining priority of processes that it |
123 with $H'$ (which waits for the other resource). The correct |
124 blocks. The advantage of a formalisation of the correctness of PIP |
124 behaviour for $L$ is to revert to the highest remaining priority of |
125 in a theorem prover is that such issues clearly show up and cannot |
125 processes that it blocks. The advantage of a formalisation in a |
126 be overlooked as in informal reasoning (since we have to analyse all |
126 theorem prover for the correctness of a high-level specification of |
127 \emph{traces} that could possibly happen). |
127 PIP is that such issues clearly show up and cannot be overlooked as |
|
128 in informal reasoning (since we have to analyse all possible program |
|
129 behaviours, i.e.~\emph{traces}, that could possibly happen). |
128 |
130 |
129 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
131 There have been earlier formal investigations into PIP, but ...\cite{Faria08} |
130 *} |
132 *} |
131 |
133 |
132 section {* Preliminaries *} |
134 section {* Formal Model of the Priority Inheritance Protocol *} |
133 |
135 |
134 text {* |
136 text {* |
135 Our formal model of PIP is based on Paulson's inductive approach to protocol |
137 Our formal model of PIP is based on Paulson's inductive approach to protocol |
136 verification, where the state of the system is modelled as a list of events |
138 verification \cite{Paulson98}, where the state of the system is modelled as a list of events |
137 that happened so far. \emph{Events} will use |
139 that happened so far. \emph{Events} fall into four categories defined as the datatype |
|
140 |
|
141 \begin{isabelle}\ \ \ \ \ %%% |
|
142 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{7mm}}l} |
|
143 \isacommand{datatype} event & @{text "="} & @{term "Create thread priority"}\\ |
|
144 & @{text "|"} & @{term "Exit thread"}\\ |
|
145 & @{text "|"} & @{term "P thread cs"} & {\rm Request of a resource} @{text "cs"} {\rm by} @{text "thread"}\\ |
|
146 & @{text "|"} & @{term "V thread cs"} & {\rm Release of a resource} @{text "cs"} {\rm by} @{text "thread"} |
|
147 \end{tabular} |
|
148 \end{isabelle} |
|
149 |
|
150 \noindent |
|
151 whereby threads, priorities and resources are represented as natural numbers. |
|
152 A \emph{state} is a list of events. |
138 |
153 |
139 To define events, the identifiers of {\em threads}, |
154 To define events, the identifiers of {\em threads}, |
140 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
155 {\em priority} and {\em critical resources } (abbreviated as @{text "cs"}) |
141 need to be represented. All three are represetned using standard |
156 need to be represented. All three are represetned using standard |
142 Isabelle/HOL type @{typ "nat"}: |
157 Isabelle/HOL type @{typ "nat"}: |