RESOURCE ACCESS PROTOCOLS - Hard Real-Time Computing Systems: Predictable Scheduling Algorithms and Applications - page 241

7.8.3 PROPERTIES OF THE PROTOCOL

The main properties of the Stack Resource Policy are presented in this section. They
will be used to analyze the schedulability and compute the maximum blocking time of
each task.

Lemma 7.9 If the preemption level of a task τ is greater than the current ceiling of a
resource R , then there are sufficient units of R available to

1. meet the maximum requirement of τ and

2. meet the maximum requirement of every task that can preempt τ .

Proof. Assume π ( τ ) >C R , but suppose that the maximum request of τ for R cannot
be satisfied. Then, by definition of current ceiling of a resource, we have C R ≥ π ( τ ),

which is a contradiction.

Assume π ( τ ) >C R , but suppose that there exists a task τ H that can preempt τ such
that the maximum request of τ H for R cannot be satisfied. Since τ H can preempt τ ,it
must be π ( τ H ) >π ( τ ). Moreover, since the maximum request of τ H for R cannot be

satisfied, by definition of current ceiling of a resource, we have C R ≥ π ( τ H ) >π ( τ ),

which contradicts the assumption.

Theorem 7.5 (Baker) If no task τ is permitted to start until π ( τ ) > Π s , then no task
can be blocked after it starts.

Proof. Let N be the number of tasks that can preempt a task τ and assume that no
task is permitted to start until its preemption level is greater than Π s . The thesis will
be proved by induction on N .

If N =0, there are no tasks that can preempt τ .If τ is started when π ( τ ) > Π s ,
Lemma 7.9 guarantees that all the resources required by τ are available when τ pre-
empts; hence, τ will execute to completion without blocking.

If N> 0, suppose that τ is preempted by τ H .If τ H is started when π ( τ H ) > Π s ,
Lemma 7.9 guarantees that all the resources required by τ H are available when τ H
preempts. Since any task that preempts τ H also preempts τ , the induction hypothesis
guarantees that τ H executes to completion without blocking, as will any task that pre-
empts τ H , transitively. When all the tasks that preempted τ complete, τ can resume its