Hardware Reference
In-Depth Information
Lemma 7.3 If there are l i lower-priority tasks that can block a task τ i , then τ i can be
blocked for at most the duration of l i
critical sections (one for each of the l i
lower-
priority tasks), regardless of the number of semaphores used by τ i .
Proof. A task τ i can be blocked by a lower-priority task τ j only if τ j has been
preempted within a critical section, say z j,k , that can block τ i . Once τ j exits z j,k ,it
can be preempted by τ i ; thus, τ i cannot be blocked by τ j again. The same situation
may happen for each of the l i lower-priority tasks; therefore, τ i can be blocked at most
l i times.
Lemma 7.4 If there are s i distinct semaphores that can block a task τ i , then τ i can
be blocked for at most the duration of s i critical sections, one for each of the s i
semaphores, regardless of the number of critical sections used by τ i .
Proof. Since semaphores are binary, only one of the lower-priority tasks, say τ j , can
be within a blocking critical section corresponding to a particular semaphore S k . Once
S k
is unlocked, τ j
can be preempted and no longer block τ i . If all s i
semaphores that
can block τ i
are locked by the s i
lower-priority tasks, then τ i
can be blocked at most
s i times.
Theorem 7.2 (Sha, Rajkumar, Lehoczky) Under the Priority Inheritance Protocol,
a task τ i can be blocked for at most the duration of α i =min( l i ,s i ) critical sections,
where l i
is the number of lower-priority tasks that can block τ i
and s i
is the number
of distinct semaphores that can block τ i .
Proof. It immediately follows from Lemma 7.3 and Lemma 7.4.
7.6.3
BLOCKING TIME COMPUTATION
The evaluation of the maximum blocking time for each task can be computed based
on the result of Theorem 7.2. However, a precise evaluation of the blocking factor B i
is quite complex because each critical section of the lower-priority tasks may interfere
with τ i via direct blocking, push-through blocking, or transitive inheritance. In this
section, we present a simplified algorithm that can be used to compute the blocking
Search WWH ::




Custom Search