Improving the Analysis of GPC in Real-Time Calculus

Abstract

Real-Time Calculus (RTC) is a framework for modeling and performance analysis of real-time networked systems. In RTC, workload and resources are modeled as arrival and service curves, and processing semantics are modeled by abstract components. Greedy Processing Component (GPC) is one of the fundamental abstract components in RTC, which processes incoming events in a greedy fashion as long as there are available resources. The relations between inputs and outputs of GPC have been established, which are consistent with its behaviors. In this paper, we first revise the original proof of calculating output curves in GPC, and then propose a new method to obtain tighter output arrival curves. Experiment results show that the precision of output arrival curves can be improved by our method compared with the original calculation and existing work.

Appendix : Proof of Theorem 2

(1) We first prove $\alpha '^u$. Suppose p is an arbitrarily small time such that the backlog satisfies $B(p) = 0$.

Then for all $p \le s \le t$,

$$\begin{aligned}&R'[s,t) \\&= R'[p,t) - R'[p,s) \\&= \sup _{p \le b \le s}\{C[p,b) - R[p,b)\}^+ - \sup _{p \le a \le t}\{C[p,a) - R[p,a)\}^+ + C[p,t) - C[p,s) \end{aligned}$$

Since $C[p,p) = R[p,p) = C[p,p) - R[p,p) = 0$, the suprema are nonnegative and we have

$$\begin{aligned}&R'[s,t) \\&= \sup \limits _{p \le b \le s}\{C[p,b) - R[p,b)\} - \sup \limits _{p \le a \le t}\{C[p,a) - R[p,a)\} + C[p,t) - C[p,s)\\&= \sup _{p \le b \le s}\{\inf _{p \le a \le t}\{R[b,a) + C[a,t) - C[b,s)\}\} \\&= \sup _{p \le b \le s}\{\inf _{p \le a \le t}\{C[s,t) + C[a,b) - R[a,b)\}\} \\&= C[s,t) + \sup _{p \le b \le s}\{\inf _{p \le a \le t}\{ C[a,b) - R[a,b)\}\} \\&= C[s,t) + \sup _{p \le b \le s}\{min\{\inf _{b \le a \le t}\{ C[a,b) - R[a,b)\}, \inf _{p \le a \le b}\{ C[a,b) - R[a,b)\}\}\} \end{aligned}$$

Let $\chi = \sup \limits _{p \le b \le s}\{min\{\inf \limits _{b \le a \le t}\{ C[a,b) - R[a,b)\}, \inf \limits _{p \le a \le b}\{ C[a,b) - R[a,b)\}\}\}$,

$\chi _1(b) = \inf \limits _{b \le a \le t}\{C[a,b) - R[a,b)\} = min\{C[b, b) -R[b, b), C[b + 1, b) -R[b+ 1, b ), ..., C[t, b) -R[t, b) \} \le 0$,

$\chi _2(b) = \inf \limits _{p \le a \le b}\{C[a,b) - R[a,b)\} = min\{C[p, b) -R[p, b), C[p + 1, b) -R[p + 1, b), ..., C[b -1, b) -R[b - 1, b), C[b, b) -R[b, b)\} \le 0$.

Next we prove $\chi = \sup \limits _{p \le b \le s} \{\chi _1(b)\}$⁷.

We consider two cases:

• (1) For any $i \in [p, s]$, $\chi _1(i) \le \chi _2(i)$, then $\chi = \sup \limits _{p \le b \le s} \{\chi _1(b)\}$.

• (2) There exists at least one $i \in [p, s]$ satisfying $\chi _1(i) > \chi _2(i)$, then $min \{\chi _1(i), \chi _2(i)\} = \chi _2(i) < 0$,

Similar as the proof for $\beta '^l$, there exists $x \in [p, s]$ such that $\min \{\chi _1(x),$ $\chi _2(x)\} = \chi _1(x) = \chi _2(x) = 0$.

Then

$$\begin{aligned} \chi&= \sup \limits _{p \le b \le s} \{min\{\chi _1(b), \chi _2(b)\}\} \\&= max \{min\{\chi _1(p), \chi _2(p) \},..., min\{\chi _1(x), \chi _2(x) \}, ...,min\{\chi _1(s), \chi _2(s)\} \} \\&= \sup \limits _{ b \in \phi }\{min\{\chi _1(b), \chi _2(b)\}\} = \sup \limits _{ b \in \phi } \{\chi _1(b)\} \end{aligned}$$

where $\psi$ is the set of values in [p, s] which satisfy for any $b \in \phi$, $\chi _1(b) \le \chi _2(b)$.

On the other hand, $\sup \limits _{p \le b \le s}\{\chi _1(b)\} = \sup \limits _{ b \in \psi }\{\chi _1(b)\}$, since when $b \in ([p,s] - \psi )$, $\chi _1(b) < 0$. Then we have $\chi = \sup \limits _{p \le b \le s}\{\chi _1(b)\}$.

So in both two cases we have $\chi = \sup \limits _{p \le b \le s}\{\chi _1(b)\}$.

Then

$$\begin{aligned}&R'[s,t) \\&= C[s,t) + \sup _{p \le b \le s}\{\inf _{p \le a \le t}\{ C[a,b) - R[a,b)\}\} \\&= C[s,t) + \sup _{p \le b \le s}\{\inf _{b \le a \le t}\{ C[a,b) - R[a,b)\}\} \\&= \sup _{p \le b \le s}\{\inf _{b \le a \le t}\{ C[s,t) + C[a,b) - R[a,b)\}\} \\&= \sup _{p \le b \le s}\{\inf _{b \le a \le t}\{R[b,a) + C[a,t) - C[b,s)\}\} \end{aligned}$$

Then with $\lambda = s - b$ and $\mu = a + \lambda -s$, we have

$$\begin{aligned}&R'[s,t) \\&= \sup _{p \le b \le s}\{\inf _{b \le a \le t}\{R[b,a) + C[a,t) - C[b,s)\}\} \\&= \sup _{0 \le \lambda \le s - p}\{\inf _{0 \le \mu \le \lambda + (t - s)}\{R[s - \lambda , \mu - \lambda + s) + C[\mu - \lambda + s,t) - C[s - \lambda ,s)\}\} \\&\le \sup _{0 \le \lambda \le s - p}\{\inf _{0 \le \mu \le \lambda + (t - s)}\{\alpha ^u(\mu ) + \beta ^u(\lambda + (t - s) - \mu ) - \beta ^l(\lambda )\}\} \\&\le \sup _{0 \le \lambda }\{\inf _{0 \le \mu \le \lambda + (t - s)}\{\alpha ^u(\mu ) + \beta ^u(\lambda + (t - s) - \mu ) - \beta ^l(\lambda )\}\} \\&= (\alpha ^u \otimes \beta ^u) \oslash \beta ^l \end{aligned}$$

Since the number of processed events can not be larger than the available resource, $R'[s,t) \le \beta ^u(t - s)$, then we have $R'[s,t) \le \min ( (\alpha ^u \otimes \beta ^u) \oslash \beta ^l , \beta ^u)$.

(2) The results for $\alpha '^l$ can be proved as with a combination of $\beta '^u$ and $\alpha '^u$ .