Periodic Resource Model for Compositional Real-Time Guarantees

한종우·2021년 3월 18일

PRM Paper Real-Time System Resource Model

Paper Review

목록 보기

4/7

사담

증명들 자체는 꽤나 자명하기도 하고 식 자체로 유용한 경우가 많아서 식만 참고해도 유용할 듯 하다.

Intro

스케줄링은 아래의 3가지 element에 따라 특성화될 수 있다.

resource model
scheduling algorithm
workload model

그리고 논문에 의하면 parent와 child가 서로 다른 스케줄링 알고리즘을 사용하는 hierarchical scheduling framework가 대두되고 있다. (2003년 기준으로..) 이러한 모델을 $I(G_S, G_D)$ 로 나타낸다.

$G_S$ : parent가 child에게 주는 supply
$G_D$ : parent가 child에게 요구하는 demand

hierarchical scheduling framework는 아래의 특징들을 만족한다.

independence : schedulability 분석할 때 다른 model과 독립이다.
separation : parent model과 child model은 분리되어있어 scheduling interface model로만 상호작용한다.
universality : 아무 스케줄링 알고리즘이나 적용 가능하다.
compositionality : parent의 timing guarantee를 만족할 필요충분조건은 child의 timing guarantee르 만족하는 것

따라서 저자는 위를 만족하는 scheduling interface model을 소개할 것이라 말한다.

이미 소개된 hierarchical scheduling 방법들이다.

fractional resource

항상 $U_F$ 만큼의 부분적인 resource만을 할당받는 $R_F(U_F)$ 역시 일종의 hierarchical scheduling 방법이라고 한다.
parent scheduling modell은 child에게 $R_F(G_S)$ 만큼의 resource를 제공하고, child는 $R_F(G_D)$ 의 demand를 요구한다. $G_S$ 는 기존의 스케줄링 알고리즘들로 정해지며, $G_D$ 역시 기존의 schedulability analysis로 쉽게 구해질 수 있다.
근데 $G_D$ 에 child model의 timing requirement가 없어서 parent model에 task-level deadline 정보를 알 수 있는EDF만 쓸 수 있다는 한계가 있다고 한다.

bounded-delay resource partition model

$R_B(U_B, D_B)$ 로 나타내며 full capacity를 일부 시간 동안에는 쓸 수 있으나, 다른 시간에는 $R_F(U_B)$ 만큼의 fractional resource만을 쓸 수 있다. 특징은 $R_F$ 하에서 두 event 사이의 시간 간격이 $[t-D_B, t+D_B]$ 로 정해져 있다는 것이다. 이에 따라 모든 task들이 deadline보다 $D_B$ 만큼 일찍 끝나는 경우 schedulable하다고 한다.

여러 real-time guarantee를 고려하는 hierarchical scheduling framework

Regehr and Stankovic이 제안한 것으로, scheduling interface model $I(G_S, G_D)$ 에 대해 $G_S$ 를 $G_D$ 로 변환할 수 있다면 스케줄 가능하다고 주장한다.

Contribution

본 논문에서는 periodic resource model $\Gamma(\Pi, \Theta)$ 를 제시한다. 이 model은 시간 $\Pi$ 마다 $\Theta$ 만큼의 자원 할당을 보장한다. 이에 따라 아래 문제들을 고려할 수 있다.

Exact Schedulability Analysis : 주어진 $W$ , $\Gamma$ , $A$ 에 대해 $M(W, \Gamma, A)$ 가 schedulable할 필요충분조건을 구하는 문제
Periodic capacity bound : 주어진 $W$ , $A$ , $\Pi$ 에 대해 capacity bound $\Theta^*/\Pi$ 를 구하는 문제. 즉, $\Theta \ge \Theta^*$ 이면 $M(W, \Gamma(\Pi, \Theta), A)$ 가 schedulable하다.
utilization bound : 주어진 $\Gamma$ , $A$ 에 대해 utilization bound $UB$ 를 구하는 문제 $\sum_{T_i \in W}\frac{e_i}{p_i} \le UB$
algorithm set : 주어진 $W$ , $\Gamma$ 에 대해 $M(W, \Gamma, A)$ 가 schedulable하게 하는 알고리즘 A를 구하는 문제
Compositional Guarantee : n개의 scheduling model이 주어졌을 때, parent scheduling model을 만드는 문제. 이 때 parent model이 schedulalbe할 필요충분조건은 n개의 child model이 schedulable한 것이다.

본 논문에서는 1, 2, 3, 5에 대해서 다룬다고 한다.

System Model

Scheduling Model M은 $(W, R, A)$ 로 정의된다.

W : workload model
R : resource model
A : scheduling algorithm
본 논문에서는 Liu & Layland의 periodic task model을 채용하여 task $T = (p, e)$ 로 나타낸다. p, e는 주기와 실행 시간이다.
각 task들은 독립이고 preemptive하다.
알고리즘으로는 optimal fixed-priority algorithm인 RM과 optimal dynamic-priority algorithm인 EDF를 사용한다.
Resource model은 partitioned resource model을 사용한다. 위의 bounded-delay resource partition model $R_B(U_B, D_B)$ 도 한 가지 예시다.
workload W가 알고리즘 A로 resource R에서 schedulable하면 $M(W,R,A)$ 이 schedulable하다고 정의한다.

Periodic Resource Model

먼저 periodic resource model이 필요한 이유는,
periodic task를 가진 periodic application을 abstract하다 보면, 자연스럽게 single periodic task로 abstract할 수 없을지 생각하게 된다. resource가 workload의 periodic한 requirement를 만족하면서 할당되어있다면, resource allocation 역시 periodic behavior를 보일 것이다.

periodic resource model $\Gamma(\Pi, \Theta)$

$\Pi$ 시간마다 $\Theta$ 시간 만큼의 자원 할당을 보장한다. (그 안에서는 언제 들어오는지는 모른다.)
$\Pi$ 는 양의 정수
$\Theta$ 는 $(0, \Pi]$ 사이의 실수
$\Gamma(k, k)$ 는 항상 resource를 사용할 수 있는 model을 의미한다.

resource supply bound function $sbf_{\Gamma}(t)$

sbf_{\Gamma}(t) = \lfloor \frac{t-(\Pi-\Theta)}{\Pi} \rfloor \cdot +\ \epsilon_s \\ \epsilon_s = max(t-2(\Pi-\Theta)-\Pi\lfloor \frac{t-(\Pi-\Theta)}{\Pi} \rfloor, 0)

$sbf_{\Gamma}(t)$ 의 하한에 대한 linear function $lsbf_{\Gamma}(t)$

lsbf_{\Gamma}(t) = \frac{\Theta}{\Pi}(t - 2 \cdot (\Pi - \Theta)) \le sbf_{\Gamma}(t)

resource serveice time function $tbf_{\Gamma}(t)$

tbf_{\Gamma}(t) = \lfloor \frac{t-(\Pi-\Theta)}{\Pi} \rfloor \cdot +\ \epsilon_t \\ \epsilon_t = \begin{cases} \Pi-\Theta+t-\Theta\lfloor \frac{t}{\Theta} \rfloor & if ( t-\Theta\lfloor \frac{t}{\Theta} \rfloor > 0)\\ 0 & o.w. \end{cases}

t만큼의 resource를 얻기 위해 걸리는 시간을 의미한다.

$tbf_{\Gamma}(t)$ 의 상한에 대한 linear function $ltbf_{\Gamma}(t)$

ltbf_{\Gamma}(t) = \frac{\Theta}{\Pi} \cdot t + 2 \cdot (\Pi - \Theta) \ge tbf_{\Gamma}(t)

Schedulability Analysis

EDF (Dynamic Priority)

resource demand : workload가 request를 보낸 자원의 양 (현재 할당된 양이 아니라 request한 양이다.)

resource demand function $dbf_W(t)$

dbf_W(t) = \sum_{T_i \in W} \lfloor \frac{e_i}{p_i} \rfloor \cdot e_i

discrete step function 형태로 나타난다.
상한에 대한 linear function은 $ldbf_W(t)$ 이며
$ldbf_W(t) = U_W \cdot t \ge dbf_W(t)$

partitioned resource가 아니라 항상 다 쓸 수 있는 dedicated resource의 경우 W가 EDF로 schedulable한 필요충분조건은 resource demand가 시간 t보다 작으면 된다. (생각해보면 자명하긴 한데, 왜 hyperperiod의 2배인지는 모르겠다.)

dbf_W(t) \le t, \ \ for \ all \ 0 < t \le 2 \cdot LCM_W

$LCM_W$ 는 모든 주기의 최소공배수인 hyperperiod를 의미한다.

직관적으로는 resource demand가 resource supply보다 작으면 되는데, dedicated resource의 경우에는 resource supply가 t만큼이기 때문인거고 논문의 모델의 경우에는 sbf보다 작으면 된다.

Theorem 1 (EDF Schedulability Analysis)
주어진 Scheudling Model $M(W,\Gamma,EDF)$ 이 schedulable할 필요충분조건은 아래와 같다.
$\forall 0 < t \le 2 \cdot LCM_W : dbf_W(t) \le sbf_{\Gamma}(t)$

pf)
(i) (필요조건) =>
대우를 생각하면, resource demand가 supply보다 많으면 자명하게 schedulable하지 않다.

(ii) (충분조건) <=
마찬가지로 대우 명제를 생각하자. W가 EDF 하에서 schedulable하지 않으면, deadline miss가 발생하는 task가 존재한다. 이 task를 $T_i$ 라 하고 deadline miss가 발생하는 시간을 $t_2$ 라 하자. $t_1$ 은 deadline이 $t_2$ 보다 늦은 instant나 idle한 마지막 time instant라고 하자. 그럼 $t = t_2 - t_1$ 이라 했을 때, time interval $[t_1, t_2)$ 동안 demand는 t보다 크다. 따라서 $dbf_W(t) > sbf_{\Gamma}(t)$ 인 t가 존재한다.
$\square$

Fixed-Priority

항상 모든 자원을 쓸 수 있는 dedicated resource의 경우 WCRT (Worst Case Response Time)을 구할 수 있는 아래와 같은 iterative algorithm이 알려져 있다.

r_i^{(k)}=e_i+\sum_{T_k \in HP(W, T_i)} \lceil \frac{r_i^{(k-1)}}{p_k} \rceil \cdot e_k,\ where\ T_k = (p_k, e_k)

$r_i^{(0)} = e_i$ 이며 위 식을 $r_i^{(k-1)} = r_i^{(k)}$ 일 때까지 반복하여 이 때의 $r_i^{(k)}$ 를 $r_i$ 로 정의한다.
$HP(W, T_i)$ 는 $T_i$ 보다 priority가 높은 task들을 의미한다. 식을 해석하자면 + 뒤의 항이 preempt 당하는만큼의 시간이다.

하지만 이 경우는 t만큼의 resource supply를 위한 service duration이 t라는 가정이 있기 때문에 가능한 것이고, partitioned resource의 경우 논문에서는 아래의 새로운 method를 제안한다.

r_i^{(k)}=tbf_{\Gamma}(I_i^{(k)})\\ I_i^{(k)} = e_i+\sum_{T_k \in HP(W, T_i)} \lceil \frac{r_i^{(k-1)}(\Gamma)}{p_k} \rceil \cdot e_k

마찬가지로 $r_i^{(0)} = e_i$ 이며 위 식을 $r_i^{(k-1)} = r_i^{(k)}$ 일 때까지 반복하여 이 때의 $r_i^{(k)}$ 를 $r_i$ 로 정의한다.

Theorem 2 (Fixed-Priority Schedulability Analysis)
주어진 Scheudling Model $M(W,\Gamma,FP)$ 이 schedulable할 필요충분조건은 아래와 같다.
$\forall\ T_i \in W : r_i(\Gamma) \le p_i,\ where\ T_k = (p_k, e_k)$

pf)
$I_i$ 는 worst case interference(자신보다 높은 priroity의 job들에 의해 최대로 preempt당한 경우)를 포함하여 필요한 resource demand이고, service time을 구하는 $tbf$ 을 사용하여 response time은 해당 demand만큼의 supply를 만들기까지 걸리는 시간이다. 따라서 implicit deadline( $d_i = p_i$ )이라는 가정 하에 $r_i(\Gamma) \le p_i$ 이면 $\Gamma$ 에 대해 execution time만큼의 maximum service duration이 deadline보다 작은 것이므로 schedulable하다.
$\square$

Periodic Capacity Bounds

periodic capacity $C_{\Gamma}$
periodic resource $\Gamma(\Pi, \Theta)$ 에 대해 periodic capacity $C_{\Gamma}$ 를 $\frac{\Theta}{\Pi}$ 로 정의한다.
periodic capacity bound $PCB_W(\Pi, A)$
주어진 resource period와 algorithm에 대해 capacity의 하한을 의미한다.
따라서 $PCB_W(\Pi, A) \le \frac{\Theta}{\Pi}$ 인 경우 scheduling model $M(W, \Gamma(\Pi, \Theta), A)$ 은 schedulable하다.
PCB를 이용해서 W를 periodic workload $T(p, e)$ $(p=\Pi, e = \Pi \cdot PCB_W(\Pi, A))$ 로 쉽게 abstract할 수 있다. 뒤에 compositional method에서도 써먹는다.

EDF

Theorem 3 (Optimal Periodic Capacity Bound for EDF)
주어진 periodic workload set $W$ 이 EDF 하에서 돌아갈 때, optimal (minimum) periodic capacity bound $PCB_W^{*}(\Pi, EDF)$ 는
$\forall 0 < t \le 2 \cdot LCM_W : dbf_W(t) \le sbf_{\Gamma}(t)$
를 만족하는 가장 작은 $\Theta$ 인 $\Theta^*$ 에 대해
$PCB_W^{*}(\Pi, EDF) = \frac{\Theta^*}{\Pi}$
이고, scheduling model $M(W, \Gamma(\Pi, \Theta), EDF)$ 이 schedulable할 필요충분조건은 $PCB_W^{*}(\Pi, EDF) \le C_{\Gamma}$ 이다.

설명이 긴데 내용만 보면 자명하다. 그래서인지 증명도 4줄 정도밖에 안 되는데 간단히 설명하자면 Thm 1이 schedulable할 필요충분조건이므로 얘를 만족하는 가장 작은 capacity가 optimal이라는 의미다.

하지만 이 식을 통해서 bound를 구하기는 쉽지 않다. 따라서 논문은 더 쉽게 bound를 구할 수 있는 방법을 소개한다.

Theorem 4 (Periodic Capacity Bound for EDF)
주어진 periodic workload set $W$ 이 EDF 하에서 돌아갈 때, periodic capacity bound $PCB_W(\Pi, EDF)$ 는 아래와 같이 구할 수 있다.
$PCB_W^{*}(\Pi, EDF) = \frac{\Theta^+}{\Pi}$
$\Theta^+ = max_{\{0<t \le 2LCM_W \}} (\frac{\sqrt{(t-2\Pi)^2+8\Pi dbf_W(t)}-(t-2\Pi)}{4})$

pf)

$lsbf_{\Gamma}(t) \le sbf_{\Gamma}(t)$ 이므로 $dbf_{W}(t) \le lsbf_{\Gamma}(t)$ 인 $\Theta$ 는 Thm 3을 만족하고 capacity bound라고 할 수 있다.

dbf_{W}(t) \le lsbf_{\Gamma}(t) = \frac{\Theta}{\Pi}(t-2\Pi+2\Theta)\\ \Rightarrow 2\Theta^2+(t-2\Pi)\Theta-\Pi \cdot dbf_{W}(t) \ge 0

$\Theta \ge 0$ 이므로 근의 공식을 사용하면

\Theta \ge \frac{\sqrt{(t-2\Pi)^2+8\Pi dbf_W(t)}-(t-2\Pi)}{4}

이다.
$\square$

근데 dbf 안에도 ceiling이 있는데 Thm 3에 비해 많이 편해진 게 맞는지 싶다. 또한, 사실 dbf가 항상 lsbf보다 작을 필요는 없는데, 이에 따라 Thm 4에서 구한 $\Theta^+$ 가 Thm 3에서 구하는 $\Theta^*$ 보다는 크게 구해진다. 논문의 Example 5.1에서 구한 두 값 역시 $\Theta^+$ 가 더 크다.

RM

Optimal Fixed-Priority Scheduling Algorithm인 RM역시 마찬가지로 Thm 5에서 optimal bound를 구하고 더 쉽게 구할 수 있으나 optimal은 아닌 bound를 Thm 6에서 구한다.

Theorem 5 (Optimal Periodic Capacity Bound for RM)
주어진 periodic workload set $W$ 이 RM 하에서 돌아갈 때, optimal (minimum) periodic capacity bound $PCB_W^{*}(\Pi, RM)$ 는
$\forall\ T_i \in W : r_i(\Gamma) \le p_i,\ where\ T_k = (p_k, e_k)$
를 만족하는 가장 작은 $\Theta$ 인 $\Theta^*$ 에 대해
$PCB_W^{*}(\Pi, RM) = \frac{\Theta^*}{\Pi}$
이고, scheduling model $M(W, \Gamma(\Pi, \Theta), RM)$ 이 schedulable할 필요충분조건은 $PCB_W^{*}(\Pi, RM) \le C_{\Gamma}$ 이다.

마찬가지로 Thm2를 만족하기 때문에 schedulable하고, 그중 가장 작은 $\Theta$ 를 구했기 때문에 optimal이다.

Theorem 6 (Periodic Capacity Bound for RM)
주어진 periodic workload set $W$ 이 RM 하에서 돌아갈 때, periodic capacity bound $PCB_W(\Pi, RM)$ 는 아래와 같이 구할 수 있다.
$PCB_W^{*}(\Pi, RM) = \frac{\Theta^+}{\Pi}$
$\Theta^+ = max_{\{ \forall T_i \in W \}} (\frac{-(p_i-2\Pi)+\sqrt{(p_i-2\Pi)^2+8\Pi I_i}}{4})\\where\ I_i = e_i+\sum_{T_k \in HP(W, T_i)} \lceil \frac{p_i}{p_k} \rceil \cdot e_k$

증명을 위해 새로운 notation이 정의되는데, 원래 RM의 response time을 구하기 위한 iterative method에서

r_i^{(k)}=tbf_{\Gamma}(I_i^{(k)})\\ I_i^{(k)} = e_i+\sum_{T_k \in HP(W, T_i)} \lceil \frac{r_i^{(k-1)}(\Gamma)}{p_k} \rceil \cdot e_k

$\hat{r_i}^{(k)}=ltbf_{\Gamma}(I_i^{(k)})$ 로 정의한다. 이 때 수렴한 $I_i^{(k)}$ 에 대해서만 ltbf로 구하는 것처럼 보인다. (논문에 명시되어 있지 않다.)

위 notation을 사용하면 $tbf \le ltbf$ 이기 때문에

\forall\ T_i \in W : \hat{r}_i(\Gamma) \le p_i

을 만족하는 경우 $r_i(\Gamma)=tbf_{\Gamma}(I_i) \le ltbf_{\Gamma}(I_i) = \hat{r}_i(\Gamma) \le p_i$
이고, Thm 2를 만족하므로 위 조건도 schedulable한 필요충분조건이다.
(논문에서는 Lemma 4로 따로 표기한다.)

pf)
새로운 notation에 따르면 model이 schedulable할 필요충분 조건은 아래와 같다.

\forall\ T_i \in W : ltbf_{\Gamma}(I_i) \le p_i

따라서

ltbf_{\Gamma}(I_i) = \frac{\Pi}{\Theta} \cdot I_i + 2(\Pi - \Theta) \le p_i\\ \Rightarrow 2\Theta^2+(p_i-2\Pi)\Theta-\Pi \cdot I_i \ge 0

마찬가지로 근의 공식을 사용하면

\Theta \ge \frac{-(p_i-2\Pi)+\sqrt{(p_i-2\Pi)^2+8\Pi I_i}}{4}

이다.
$\square$

RM에서도 Thm 6에서 구한 $\Theta^+$ 가 Thm 5에서 구하는 $\Theta^*$ 보다 크게 구해진다.

Utilization Bounds

EDF

Lemma 5
W 내에서 가장 작은 period인 $p^*$ 에 대해
$lsbf_{\Gamma}(p^*) \ge ldbf_{W}(p^*)$ 이면 $M(W, \Gamma, EDF)$ 는 schedulable하다.

자리가 없어서 [13]의 증명을 참고하라고 되어있다. [13]는 같은 이름으로 된 Technical Report인데 검색해도 안나와서 없는줄 알았는데 연구실 동기 분이 찾아줬다.

pf)
먼저 짚고 갈 부분은,

ldbf_W(t) = U_W \cdot t,\ lsbf_{\Gamma}(t) = \frac{\Theta}{\Pi}(t - 2 \cdot (\Pi - \Theta))

이고, scheduling model이 schedulable하기 위해서는 $U_W \le C_{\Gamma} = \frac{\Theta}{\Pi}$ 이므로 t에 대한 기울기가 $lsbf_{\Gamma}(t)$ 쪽이 더 크다. 따라서 $ldbf_{W}(t^*) \le lsbf_{\Gamma}(t^*)$ 인 $t^*$ 에 대해 $t > t^*$ 이면 $ldbf_{W}(t) \le lsbf_{\Gamma}(t)$ 이다. 또한 model이 schedulable하다고 했으므로 가장 작은 period 이전에 resource supply가 demand보다 많아지는 지점이 존재하고 $t^* \le p^*$ 인 $t^*$ 가 존재한다.

이제 다시 본래의 증명으로 돌아가자면,
(i) $0 < t < p^*$
$dbf_W(t)$ 의 정의에 따라 $\forall 0 < t < p^* : dbf_W(t) = 0$ 이고 자명하게 $\forall 0 < t < p^* : dbf_W(t) \le sbf_{\Gamma}(t)$ 이다.

(ii) $p^* \le t$
위에 언급한대로 $\forall t \ge p^* > t^* : ldbf_{W}(t) \le lsbf_{\Gamma}(t)$ 이고,

\forall t \ge p^* : dbf_{W}(t) \le ldbf_{W}(t) \le lsbf_{\Gamma}(t) \le sbf_{\Gamma}(t)

(i), (ii)와 Thm 1에 의해 M은 schedulable하다.
$\square$

Theorem 7 (Utilization Bound for EDF)
주어진 periodic resource $\Gamma(\Pi, \Theta)$ 에 대해 EDF 알고리즘의 utilization bound $UB_{\Gamma}(EDF)$ 는 다음과 같다.
$UB_{\Gamma}(EDF) = \frac{\Theta}{\Pi}(1-\frac{2(\Pi-\Theta)}{p^*})$

pf)
Lemma 5에 의해 $lsbf_{\Gamma}(p^*) \ge ldbf_{W}(p^*)$ 이면 $M(W, \Gamma, EDF)$ 는 schedulable하고,

ldbf_{W}(p^*) = p^* \cdot U_W \le lsbf_{\Gamma}(p^*) = \frac{\Theta}{\Pi}(p^*-2\Pi+2\Theta)\\ \Rightarrow U_W \le \frac{lsbf_{\Gamma}(t)}{p^*} =\frac{\Theta}{\Pi}(\frac{p^*-2\Pi+2\Theta}{p^*})\\ = \frac{\Theta}{\Pi}(1-\frac{2(\Pi-\Theta)}{p^*})

$\square$

RM

Theorem 8 (Utilization Bound for RM)
주어진 periodic resource $\Gamma(\Pi, \Theta)$ 에 대해 RM 알고리즘의 utilization bound $UB_{\Gamma}(RM)$ 는 다음과 같다.
$UB_{\Gamma}(RM) = \frac{\Theta}{\Pi}(m(\sqrt[m]{2}-1)-\frac{\sqrt[m]{2}(\Pi-\Theta)}{p^*})$

[13]을 보니 식에 error가 있다고 한다.

$UB_{\Gamma}(RM) = \frac{\Theta}{\Pi}(ln2 -\frac{\sqrt[m]{2}(\Pi-\Theta)}{p^*}) \simeq \frac{\Theta}{\Pi}(ln2 -\frac{\Pi-\Theta}{p^*})$

Compositional Real-Time Guarantees

Definition 6.1 (Composition Method)
scheduling model $M_1, M_2, \dots, M_n$ 에 대해 새로운 scheduling model $M_P(W_P, \Gamma_P, A_P)$ 를 다음과 같이 만들 수 있다.

$A_P, \Gamma_P$ 는 주어졌다고 가정

각 child model의 resource model이 $\Gamma_i(\Pi_i, \Theta_i)$ 라 할 때, $W_P=\{ T_1(\Pi_1, \Theta_1), \dots, T_n(\Pi_n, \Theta_n) \}$

알고리즘이 EDF, RM인 것에 따라 Thm 3, Thm 5를 통해 $PCB_{W_P}^{*}(\Pi_P, A_P)$ 를 구한 뒤
$\Theta_P = \Pi_P \cdot PCB_{W_P}^{*}(\Pi_P, A_P)$
로 구한다.

Theorem 9 (Compositional Real-Time Guarantees)
individually schedulable한 scheduling model $M_1, M_2, \dots, M_n$ 으로 Def 6.1을 통해 만든 $M_P(W_P, \Gamma_P, A_P)$ 에 대해 $M_P$ 가 schedulable할 필요충분조건은 $M_1, M_2, \dots, M_n$ 이 framework 상에서 schedulable한 것이다.

각 model이 individually schedulable하다는 것과 framework 상에서 schedulable하다는 것의 정의가 모호하긴 하나, 증명 자체는 꽤나 자명해보인다.

pf)
(<=)
$M_1, ..., M_n$ 이 framework 상에서 schedulable하다고 가정하면, 각 $\Gamma_i$ 를 $T_i$ 로 변환했으므로 $T_i$ 는 timing requirement (deadline)을 만족한다고 말할 수 있다. 또한 Thm 3 혹은 Thm 5을 사용하면 주어진 period에 대해 $\Pi_P$ 보다 작은 capacity를 구할 수 있다. schedulable해지는 최소 capacity가 $\Pi_P$ 보다 작으므로 사용 가능하고 $M_P$ 역시 schedulable하다.

(=>) $M_P$ 가 schedulable하다고 가정하자. 그렇다면 모든 $T_i$ 가 $\Pi_i$ 시간에 resource를 $\Theta_i$ 만큼 받는다고 보장할 수 있다. individually하게 다 schedulable하므로 적절한 resource를 받았으므로 framework 상에서도 schedulable하다.
$\square$

Ref

Insik Shin and Insup Lee, "Periodic resource model for compositional real-time guarantees," RTSS 2003. 24th IEEE Real-Time Systems Symposium, 2003, Cancun, Mexico, 2003, pp. 2-13, doi: 10.1109/REAL.2003.1253249.
I. Shin and I. Lee. Compositional real-time scheduling framework with periodic model. ACM Trans. Embedded Comput. Syst., 7(3), 2008.