A framework for memory contention analysis in multi-core platforms

The last decade has witnessed a major shift towards the deployment of embedded applications on multi-core platforms. However, real-time applications have not been able to fully benefit from this transition, as the computational gains offered by multi-cores are often offset by performance degradation due to shared resources, such as main memory. To efficiently use multi-core platforms for real-time systems, it is hence essential to tightly bound the interference when accessing shared resources. Although there has been much recent work in this area, a remaining key problem is to address the diversity of memory arbiters in the analysis to make it applicable to a wide range of systems. This work handles diverse arbiters by proposing a general framework to compute the maximum interference caused by the shared memory bus and its impact on the execution time of the tasks running on the cores, considering different bus arbiters. Our novel approach clearly demarcates the arbiter-dependent and independent stages in the analysis of these upper bounds. The arbiter-dependent phase takes the arbiter and the task memory-traffic pattern as inputs and produces a model of the availability of the bus to a given task. Then, based on the availability of the bus, the arbiter-independent phase determines the worst-case request-release scenario that maximizes the interference experienced by the tasks due to the contention for the bus. We show that the framework addresses the diversity problem by applying it to a memory bus shared by a fixed-priority arbiter, a time-division multiplexing (TDM) arbiter, and an unspecified work-conserving arbiter using applications from the MediaBench test suite. We also experimentally evaluate the quality of the analysis by comparison with a state-of-the-art TDM analysis approach and consistently showing a considerable reduction in maximum interference.

This work was partially supported by National Funds through FCT/MEC (Portuguese Foundation for Science and Technology) and co-financed by ERDF (European Regional Development Fund) under the PT2020 Partnership, within project UID/CEC/04234/2013 (CISTER Research Centre); by FCT/MEC and the EU ARTEMIS JU within project ARTEMIS/0001/2013—JU grant nr. 621429 (EMC2); by the North Portugal Regional Operational Programme (ON.2—O Novo Norte) under the National Strategic Reference Framework (NSRF), through ERDF, and by National Funds through FCT/MEC, within project NORTE-07-0124-FEDER-000063 (BEST-CASE, New Frontiers); and by the European Union under the Seventh Framework Programme (FP7/2007-2013), grant agreement n\(^{\circ }\) 611016 (P-SOCRATES) and by the European social fund within the framework of realizing the project “Support of inter-sectoral mobility and quality enhancement of research teams at Czech Technical University in Prague”, CZ.1.07/2.3.00/30.0034.

Authors and Affiliations

1. CISTER-Research Unit, Porto, Portugal

   Dakshina Dasari & Vincent Nelis

2. Czech Technical University in Prague, Prague 6, Czech Republic

   Benny Akesson

Corresponding author

Correspondence to Dakshina Dasari.

Appendix

This appendix contains the proofs of Lemmas 3,  4, and 5. These proofs are all quite long as they are all based on case enumeration. Although many of the cases in the proof are similar, some even identical, the presented proofs cover all cases exhaustively for completeness.

1.1 Proof of Lemma 3

Proof

We prove the lemma by induction. First, we show in the basic step that the claim is true considering only the first request \({\text {req}}_{i, 1}\) and its slot assignment \(\sigma _{i}(1)\). That is, we show that the release and service times given by Eqs. (7) and (8) result in a maximum cumulative delay \(\mathcal{D}_{i}(1) = {\text {srv}}_{i, 1} - {\text {rel}}_{i, 1}\). Then, in the inductive step, we show that if the claim is true considering the set of the first k requests, \(k \ge 1\) (induction hypothesis), then the property holds for the first \((k+1)\) requests as well. In other words, assuming that Eqs. (7) and (8) assign a release and service time to the k first requests that result in a maximum cumulative delay \(\mathcal{D}_{i}(k)\), then the same equations provide a maximum cumulative delay \(\mathcal{D}_{i}( k+1)\) when applied to the first \((k+1)\) requests. Both the basic and inductive steps are proven by showing that any other choice of release and service time, for any of the requests in the considered set of requests, results in a lower cumulative delay.

Basic step By considering only the first request \({\text {req}}_{i, 1}\), it is easy to see that any release time \({\text {rel}}_{i, 1}\) different from that given by Eq. (7) leads to \({\text {rel}}_{i, 1} > \mathcal{T}^{\min }_{i}(\sigma _{i}(1) - 1) + 1\). This follows from the fact that having \({\text {rel}}_{i, 1} < \mathcal{T}^{\min }_{i}(\sigma _{i}(1) - 1) + 1\) is not possible, as shown in Lemma 1. Besides, choosing any other release time \({\text {rel}}_{i, 1} > \mathcal{T}^{\min }_{i}(\sigma _{i}(1) - 1) + 1\) would have as sole impact, a decrease in the difference \(({\text {srv}}_{i, 1} - {\text {rel}}_{i, 1})\), and subsequently a lower delay \(\mathcal{D}_{i}( 1)\) incurred by request \({\text {req}}_{i, 1}\). In short, since \(\mathcal{T}^{\min }_{i}(\sigma _{i}(1) - 1) + 1\) is a lower bound on the release time of request \({\text {req}}_{i, 1}\) (from Lemma 1), choosing \({\text {rel}}_{i, 1} = \mathcal{T}^{\min }_{i}(\sigma _{i}(1) - 1) + 1\) is the best choice to guarantee a maximum delay for the first request. Similarly, since \(\min (\mathcal{T}^{\max }_{i}(\sigma _{i}(k)), {\text {rel}}_{i, k} + \mathcal{T}^{\max }_{i}(k))\) was shown to be an upper bound on the service time of request \({\text {req}}_{i, k}\), \(\forall k\) (see Lemma 2), it is easy to see that the choice of \({\text {srv}}_{i, 1}\) by Eq. (8) also guarantees a maximum delay for this first request. In conclusion, we showed that \(\mathcal{D}_{i}( 1) = {\text {srv}}_{i, 1} - {\text {rel}}_{i, 1}\) is maximum when \({\text {rel}}_{i, 1}\) and \({\text {srv}}_{i, 1}\) are given by the equations of Lemma 3.

Inductive step Assuming that Eqs. (7) and (8) define a release and a service time for the first k requests of \(\tau _i\) such that their cumulative delay \(\mathcal{D}_{i}( k)\) is maximized, we will show that defining \({\text {rel}}_{i, k+1}\) and \({\text {srv}}_{i, k+1}\) using the equations of Lemma 3 maximizes \(\mathcal{D}_{i}( k+1)\). By applying the same reasoning as in the basic step, it is evident that choosing any other value of \({\text {rel}}_{i, k+1}\) greater than its lower bound (given in Lemma 1 and Eq. (7)) and/or any other service time \({\text {srv}}_{i, k+1}\) lower than its upper bound (given in Lemma 2 and Eq. (8)) induces a lower delay for request \({\text {req}}_{i, k+1}\), and thus a lower cumulative delay \(\mathcal{D}_{i}( k+1)\).

However, it may be noted from the release-time equation (Eq. 7) that the choice of service time \({\text {srv}}_{i, k}\) of the previous request \({\text {req}}_{i, k}\) influences the lower bound on \({\text {rel}}_{i, k+1}\), and subsequently an upper bound on \({\text {srv}}_{i, k+1}\) (see Eq. (8)). One should therefore investigate the following question: although choosing \({\text {srv}}_{i, k} = \min ( \mathcal{T}^{\max }_{i}(\sigma _{i}(k)), {\text {rel}}_{i, k} + \mathcal{T}^{\max }_{i}(1))\) guarantees a maximum cumulative delay \(\mathcal{D}_{i}( k)\) for the first k requests (from the induction hypothesis), doing so might define a range of possible values for \({\text {rel}}_{i, k+1}\) that discards those leading to a maximum cumulative delay \(\mathcal{D}_{i}( k+1)\). The remainder of this proof consists of showing that any value of \({\text {srv}}_{i, k}\) different from that given by Eq. (8) results in a lower cumulative delay \(\mathcal{D}_{i}( k+1)\).

To figure out how \({\text {srv}}_{i, k}\) affects the range of possible values for \({\text {rel}}_{i, k+1}\) and \({\text {srv}}_{i, k+1}\), let us consider different values X and Y for \({\text {srv}}_{i, k}\), where \(X = \min ( \mathcal{T}^{\max }_{i}(\sigma _{i}(k)), {\text {rel}}_{i, k} + \mathcal{T}^{\max }_{i}(1))\) (as given by Expression (8)) and Y is any positive number \(< X\). We show in the following that \(\mathcal{D}_{i}( k+1)\) is always maximum for \({\text {srv}}_{i, k} = X\).

We first introduce two symbols for compaction and readability:

We know from Lemma 1 that \({\text {rel}}_{i, k+1} \ge \max ( \mathcal{K}_{k+1}^{{\text {min}}}, {\text {srv}}_{i, k} + \varDelta _{k+1} )\) and thus three cases may arise depending on the request-to-slot assignment \(\sigma _{i}(k+1)\) of request \({\text {req}}_{i, k+1}\) (these three cases are a simple enumeration of all possible “dominance” relations between the three considered terms):

1. 1.

   \(\mathcal{K}_{k+1}^{{\text {min}}}\le Y + \varDelta _{k+1} < X +\,\varDelta _{k+1}\)

2. 2.

   \(Y +\,\varDelta _{k+1} < \mathcal{K}_{k+1}^{{\text {min}}}\le X +\,\varDelta _{k+1}\)

3. 3.

   \(Y +\,\varDelta _{k+1} \le X + \varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

We proceed by proving each of these cases.

Case 1 \(\mathcal{K}_{k+1}^{{\text {min}}}\le Y +\,\varDelta _{k+1} < X +\,\varDelta _{k+1}\)

In this case, choosing \({\text {srv}}_{i, k} = Y\) leads to \({\text {rel}}_{i, k+1} \ge Y + \varDelta _{k+1}\) (from Lemma 1). By setting \({\text {rel}}_{i, k+1}\) to \(Y + \varDelta _{k+1}\), we get

On the other hand, choosing \({\text {srv}}_{i, k} = X\) leads to \({\text {rel}}_{i, k+1}\ge X + \varDelta _{k+1}\) (from Lemma 1). Then, if we set \({\text {rel}}_{i, k+1}= X + \varDelta _{k+1}\) (i.e., the earliest possible release time) then applying the same reasoning as above leads to the same equality, i.e.,

Since (21) = (22), it is correct to claim that choosing \({\text {srv}}_{i, k} = X\) leads to a worst-case cumulative delay \(\mathcal{D}_{i}(k+1) \).

Case 2 \(Y +\,\varDelta _{k+1} < \mathcal{K}_{k+1}^{{\text {min}}}\le X +\,\varDelta _{k+1}\)

In this case, choosing \({\text {srv}}_{i, k} = Y\) leads to \({\text {rel}}_{i, k+1}\ge \mathcal{T}^{\min }_{}(\sigma _{i}(k+1)-1)\) (from Lemma 1). Let \({\text {rel}}_{i, k+1}= \mathcal{T}^{\min }_{i}(\sigma _{i}(k+1)-1)\) (i.e., the earliest possible release time-instant), from a reasoning similar to that above it holds that

On the other hand, choosing \({\text {srv}}_{i, k} = X\) leads to \({\text {rel}}_{i, k+1}\ge X + \varDelta _{k+1}\) (from Lemma 1). If \({\text {rel}}_{i, k+1}= X + \varDelta _{k+1}\), then the cumulative delay \(\mathcal{D}_{i}(k+1) \) of requests \({\text {req}}_{_, 1}, {\text {req}}_{_, 2}, \ldots , {\text {req}}_{_, k+1}\) is given by

Since (24) \(>\) (23), we can conclude that the cumulative delay is higher for \({\text {srv}}_{i, k} = X\).

Case 3 \(Y + \varDelta _{k+1} \le X + \varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

In this case, choosing either \({\text {srv}}_{i, k} = Y\) or \({\text {srv}}_{i, k} = X\) leads to \({\text {rel}}_{i, k+1}\ge \mathcal{T}^{\min }_{i}({\text {srv}}_{i, k+1}-1)\) (from Lemma 1). Therefore, the range of possible values for \({\text {rel}}_{i, k+1}\) is not affected by the choice of \({\text {srv}}_{i, k}\) and the maximum cumulative delay is obviously obtained for \({\text {srv}}_{i, k} = X\). \(\square \)

1.2 Proof of Lemma 4

Proof

The proof must show that given Conditions (9), (10), and (11), Eqs. (12), (13), and (14) hold. From the claim itself, Eq. (12) trivially holds. We stated this equality only for completeness in order to show that the situation after assigning the (\(k+1\))’th request is identical to the situation before assigning it. Let us start the proof by introducing some symbols to improve readability:

According to these new symbols and the equations of Lemma 3, the four quantities \({\text {srv}}_{i,k+1}\), \({\text {rel}}_{i,k+1}\), \({\text {srv}}_{i,k+1}'\), and \({\text {rel}}_{i,k+1}'\) can be re-written as

From (11), it holds that

By adding \(h \times {\text {TR}}\) to both sides of this inequality, we get

and the symbols \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\) can now be used to simplify this result:

In order to prove that Inequalities (13) and (14) always hold true, we must investigate three cases. These three cases simply come from an enumeration of all possible “dominance” relations between the three terms \(\mathcal{K}_{k+1}^{{\text {min}}}\), \({\text {srv}}_{i,k} + \varDelta _{k+1}\), and \({\text {srv}}_{i,k}' + \varDelta '_{k+1}\):

• Case 1 \({\text {srv}}_{i,k}' + ~\varDelta '_{k+1} \le {\text {srv}}_{i,k} + ~\varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

• Case 2 \({\text {srv}}_{i,k}' + ~\varDelta '_{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k} + ~\varDelta _{k+1}\)

• Case 3 \(\mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k}' + ~\varDelta '_{k+1} \le {\text {srv}}_{i,k} + ~\varDelta _{k+1}\)

Case 1 \({\text {srv}}_{i,k}' + \varDelta '_{k+1} \le {\text {srv}}_{i,k} + \varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

In this case, we have

These service times trivially satisfy Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Then, using \({\text {rel}}_{i,k+1} = {\text {rel}}_{i,k+1}'\), \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}'\), and \(\mathcal{D}_{i}(k) \le \mathcal{D}_{i}'(k)\) from (10), we get

This inequality can be re-written as

which satisfies Condition (13).

Case 2 \({\text {srv}}_{i,k}' +~ \varDelta '_{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k} +~ \varDelta _{k+1}\)

In this case, from (25) and (27) we have the following relation between the release time-instants of the \((k+1)\)’th request in the mappings \(\mathbb {M}_i\) and \(\mathbb {M}'_i\):

Next, we need to handle the relation between the service times \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) of this last request and we must explore three more sub-cases. These three sub-cases simply come from an enumeration of all possible “dominance” relations between the three terms \(\mathcal{K}_{k+1}^{{\text {max}}}\), \({\text {rel}}_{i,k+1} +~ \mathcal{T}^{\max }_{i}(1)\), and \({\text {rel}}_{i,k+1}' +~ \mathcal{T}^{\max }_{i}(1)\):

• Case 2.1 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

• Case 2.2 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

• Case 2.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

Case 2.1 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

In this particular sub-case, it holds from (26) and (28) that

and it immediately follows from (30), (31) and (32) that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\) , which satisfies Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) =~h\). Also from (31) and (32), it holds that \({\text {srv}}_{i,k+1} - {\text {rel}}_{i,k+1} = \mathcal{T}^{\max }_{i}(1) = {\text {srv}}_{i,k+1}' - {\text {rel}}_{i,k+1}'\) and by using this equality together with \(\mathcal{D}_{i}(k) \le \mathcal{D}_{i}'(k)\) from (10), we obtain

and thus

By re-writing this inequality we get

which satisfies Condition (13).

Case 2.2 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

In this case, we have

It thus holds from Case 2.2 that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\) and these service times trivially satisfy Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Then, assuming by contradiction that Condition (13) is not satisfied, we must have:

which can be re-written as

By replacing \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) with their values, we get

and then,

and since from Case 2.2 \(\mathcal{K}_{k+1}^{{\text {max}}}- {\text {rel}}_{i,k+1} \le \mathcal{T}^{\max }_{i}(1)\), it follows from the above inequality that

which contradicts Condition (10). This contradiction implies that Condition (13) is satisfied.

Case 2.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

In this case it holds from (26) and (28) that

and it immediately follows that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\), which satisfies Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Then, assuming by contradiction that Condition (13) is not satisfied, we must have:

which can be re-written as

By replacing \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) with their values, we get

and then,

From Eq. (30), a case condition of Case 2,we have \({\text {rel}}_{i,k+1} \ge {\text {rel}}_{i,k+1}'\) and it follows from the above inequality that

which contradicts Condition (10). This contradiction implies that Condition (13) is satisfied.

Case 3 \(\mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1} \le {\text {srv}}_{i,k} +\,\varDelta _{k+1}\)

In this case, from (25) and (27) we have the following relation between the release time-instants of the \((k+1)\)’th request in the mappings \(\mathbb {M}_i\) and \(\mathbb {M}'_i\):

Next, we need to handle the relation between the service times \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) of this last request and we hence have the same three sub-cases to explore as in Case 2, but with the slightly different case conditions of Case 3.

• Case 3.1 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

• Case 3.2 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

• Case 3.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

Case 3.1 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

From (26) and (28), we get

and it immediately follows from (33) and (34) that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\), which satisfies Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Also from (33) and (34), it holds that \({\text {srv}}_{i,k+1} - {\text {rel}}_{i,k+1} = \mathcal{T}^{\max }_{i}(1) = {\text {srv}}_{i,k+1}' - {\text {rel}}_{i,k+1}'\). Similarly to Case 2.1, by using this equality together with \(\mathcal{D}_{i}(k) \le \mathcal{D}_{i}'(k)\) from (10), we obtain

and thus

By re-writing this inequality we get

which satisfies Condition (13).

Case 3.2 \({\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

In this case, we have

It thus holds from Case 3.2 that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\) and these service times trivially satisfy Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Then, assuming by contradiction that Condition (13) is not satisfied, we must have:

which can be re-written as

By replacing \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) with their values, we get

and then,

and since from Case 3.2 \(\mathcal{K}_{k+1}^{{\text {max}}}- {\text {rel}}_{i,k+1} \le \mathcal{T}^{\max }_{i}(1)\), it follows from the above inequality that

which contradicts Condition (10). This contradiction implies that Condition (13) is satisfied.

Case 3.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\)

In this case, it holds from (26) and (28) that

and it immediately follows that \({\text {srv}}_{i,k+1} \ge {\text {srv}}_{i,k+1}'\), which satisfies Condition (14) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). Then, assuming by contradiction that Condition (13) is not satisfied, we must have:

which can be re-written as

By replacing \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) with their values, we get

and then,

From Case 3.3, we have \({\text {rel}}_{i,k+1} \ge {\text {rel}}_{i,k+1}'\) and it follows from the above inequality that

which contradicts Condition (10). This contradiction implies that Condition (13) is satisfied. \(\square \)

1.3 Proof of Lemma 5

Proof

The proof must show that given Conditions (15), (16), and (17), Eqs. (18), (19), and (20) hold. From the claim itself, Eq. (18) trivially holds since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\). We stated this equality only for completeness in order to show that the situation after assigning the (\(k+1\))’th request is same as the situation before assigning it. Let us start the proof by introducing some symbols to improve readability:

According to these new symbols and from the equations of Lemma 3, the four quantities \({\text {srv}}_{i,k+1}\), \({\text {rel}}_{i,k+1}\), \({\text {srv}}_{i,k+1}'\), and \({\text {rel}}_{i,k+1}'\) can be re-written as

According to (17), we have

and by adding “\(h \times {\text {TR}}\)” to both sides we get

which gives, by definition of \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\),

With the help of Inequality (39), we will now prove that Inequalities (19) and (20) always hold true (remember that Inequality (18) is always satisfied). Note that both Inequalities (19) and (20) are indirectly based on the release and service time of the \((k+1)\)’th request in both mappings \(\mathbb {M}_i\) and \(\mathbb {M}_i'\), i.e. they are based on the four quantities \({\text {srv}}_{i,k+1}\), \({\text {rel}}_{i,k+1}\), \({\text {srv}}_{i,k+1}'\), and \({\text {rel}}_{i,k+1}'\). Therefore, if we first focus on the relation between the release times \({\text {rel}}_{i,k+1}\) and \({\text {rel}}_{i,k+1}'\) in the two mappings \(\mathbb {M}_i\) and \(\mathbb {M}_i'\) then it holds from (39), (35), and (37) that only three cases must be investigated:

• Case 1 \({\text {srv}}_{i,k} +\,\varDelta _{k+1} \le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

• Case 2 \({\text {srv}}_{i,k} +\,\varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1}\)

• Case 3 \(\mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k} +\,\varDelta _{k+1} \le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1}\)

Case 1 \({\text {srv}}_{i,k} +\,\varDelta _{k+1} \le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\)

Proof of (20) In this case, we have from (35) and (37), \({\text {rel}}_{i,k+1} = {\text {rel}}_{i,k+1}' = \mathcal{K}_{k+1}^{{\text {min}}}\) and from (36) and (38), \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}'\) , which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) By combining (15) with (17) we get \({\text {srv}}_{i,k} \le {\text {srv}}_{i,k}'\) and thus it holds from Inequality (16) that \(\mathcal{D}_{i}(k) \le \mathcal{D}_{i}'(k)\). Therefore, since \({\text {rel}}_{i,k+1} = {\text {rel}}_{i,k+1}'\) and \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}'\) it also holds that

and thus,

and since \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}'\) in this case, we can write

which satisfies (19).

Case 2 \({\text {srv}}_{i,k} +\,\varDelta _{k+1} \le \mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1} \)

In this case, we get from (35) and (37),

Next, we need to handle the relation between the service times \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) in the two mappings \(\mathbb {M}_i\) and \(\mathbb {M}_i'\) and it holds from (36) and (38) that we have three more sub-cases to explore:

• Case 2.1 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

• Case 2.2 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

• Case 2.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

Case 2.1 \({\text {rel}}_{i,k+1} + \mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' + \mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

Proof of (20) From (36) and (38) we get

From (40), (41) and (42), it immediately follows that \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) =~h\).

Proof of (19) Also from (41) and (42), it holds that \({\text {srv}}_{i,k+1} - {\text {rel}}_{i,k+1} = \mathcal{T}^{\max }_{i}(1) = {\text {srv}}_{i,k+1}' - {\text {rel}}_{i,k+1}'\). Using \(\mathcal{D}_{i}(k) + ({\text {srv}}_{i,k}' - {\text {srv}}_{i,k}) \le \mathcal{D}_{i}'(k)\) from (16), we get

and thus

which implies

Now, we have:

Therefore it holds from the above inequality and from (43) that:

which satisfies (19).

Case 2.2 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

Proof of (20) From (36) and (38), we get \({\text {srv}}_{i,k+1} = {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\) and \({\text {srv}}_{i,k+1}' = \mathcal{K}_{k+1}^{{\text {max}}}\). We thus get \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) We use proof by contradiction. Suppose that Inequality (19) is not satisfied, we must have:

and thus,

which can be re-written as

and since it holds from (40) that \({\text {rel}}_{i,k+1}' = {\text {srv}}_{i,k+1}' +~ \varDelta '_{k+1} \ge {\text {rel}}_{i,k+1} = \mathcal{K}_{k+1}^{{\text {min}}}\) and \(\mathcal{K}_{k+1}^{{\text {min}}}\ge {\text {srv}}_{i,k} +\,\varDelta _{k+1}\) from Case 2, we get

and thus

As seen at the end of Case 2.1, we have \(\varDelta '_{k+1} - \varDelta _{k+1} \le 0\) from (15) and from the definitions of \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\), and thus it holds that

which contradicts (16). This contradiction implies that Condition (19) is always satisfied.

Case 2.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

Proof of (20) From (36) and (38), we get \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}' = \mathcal{K}_{k+1}^{{\text {max}}}\) and it immediately follows that \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) The proof is identical to the proof of (19) in Case 2.2 and is repeated here only for completeness. We use proof by contradiction. Suppose that Inequality (19) is not satisfied, we must have:

and thus,

which can be re-written as

and since it holds from (40) that \({\text {rel}}_{i,k+1}' = {\text {srv}}_{i,k+1}' + \varDelta '_{k+1} \ge {\text {rel}}_{i,k+1} = \mathcal{K}_{k+1}^{{\text {min}}}\) and \(\mathcal{K}_{k+1}^{{\text {min}}}\ge {\text {srv}}_{i,k} + \varDelta _{k+1}\) from the Case 2, we get

and thus

As seen at the end of Case 2.1, we have \(\varDelta '_{k+1} - \varDelta _{k+1} \le 0\) from (15) and from the definitions of \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\), and thus it holds that

which contradicts (16). This contradiction implies that Condition (19) is always satisfied.

Case 3 \(\mathcal{K}_{k+1}^{{\text {min}}}\le {\text {srv}}_{i,k} +\,\varDelta _{k+1} \le {\text {srv}}_{i,k}' +\,\varDelta '_{k+1}\)

In this case, we get from (35) and (37), \({\text {rel}}_{i,k+1} = {\text {srv}}_{i,k} +\,\varDelta _{k+1}\) and \({\text {rel}}_{i,k+1}' ={\text {srv}}_{i,k}' +\,\varDelta '_{k+1}\) and thus, according to (39), it holds that

Again, we need to handle the relation between the service times \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) in the two mappings \(\mathbb {M}_i\) and \(\mathbb {M}_i'\) and it holds from (36) and (38) that we have three more sub-cases to explore:

• Case 3.1 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

• Case 3.2 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

• Case 3.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

Case 3.1 \({\text {rel}}_{i,k+1} +~ \mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' +~ \mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\)

Proof of (20) From (36) and (38), we get

From (44), (45) and (46), it immediately follows that \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) From (45) and (46), it holds that \({\text {srv}}_{i,k+1} - {\text {rel}}_{i,k+1} = \mathcal{T}^{\max }_{i}(1) = {\text {srv}}_{i,k+1}' - {\text {rel}}_{i,k+1}'\). Using \(\mathcal{D}_{i}(k) + ({\text {srv}}_{i,k}' - {\text {srv}}_{i,k}) \le \mathcal{D}_{i}'(k)\) from (16), we get

and then

which implies

Now, we have:

Therefore, it holds from the above inequality and from (47) that:

which satisfies (19).

Case 3.2 \({\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1) \le \mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1}' +\,\mathcal{T}^{\max }_{i}(1)\)

Proof of (20) From (36) and (38), we get \({\text {srv}}_{i,k+1} = {\text {rel}}_{i,k+1} +\,\mathcal{T}^{\max }_{i}(1)\) and \({\text {srv}}_{i,k+1}' = \mathcal{K}_{k+1}^{{\text {max}}}\). We thus get \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) The proof is by contradiction. If Inequality (19) is not satisfied then we must have:

and thus,

which can be re-written as

By replacing the values of \({\text {rel}}_{i,k+1}\) and \({\text {rel}}_{i,k+1}'\) from Case 3, we have

and thus,

and since \(\varDelta '_{k+1} - \varDelta _{k+1} \le 0\) from (15) and the def. of \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\), it holds that

which contradicts (16). This contradiction implies that Eq. (19) is satisfied.

Case 3.3 \(\mathcal{K}_{k+1}^{{\text {max}}}\le {\text {rel}}_{i,k+1} + \mathcal{T}^{\max }_{i}(1) \le {\text {rel}}_{i,k+1}' + \mathcal{T}^{\max }_{i}(1)\)

Proof of (20) From (36) and (38), we get \({\text {srv}}_{i,k+1} = {\text {srv}}_{i,k+1}' = \mathcal{K}_{k+1}^{{\text {max}}}\) and it immediately follows that \({\text {srv}}_{i,k+1} \le {\text {srv}}_{i,k+1}'\), which satisfies (20) since \(\sigma _{i}(k+1) = \sigma _{i}'(k+1) = h\).

Proof of (19) The proof is by contradiction. If Inequality (19) is not satisfied, we must have:

and thus,

By replacing \({\text {srv}}_{i,k+1}\) and \({\text {srv}}_{i,k+1}'\) with their values, we get

and thus,

By replacing the values of \({\text {rel}}_{i,k+1}\) and \({\text {rel}}_{i,k+1}'\) from Case 3, we have

which gives

and since \(\varDelta '_{k+1} - \varDelta _{k+1} \le 0\) from (15) and the def. of \(\varDelta _{k+1}\) and \(\varDelta '_{k+1}\), it holds that

which contradicts (16). This contradiction implies that Eq. (19) is satisfied. \(\square \)

Reprints and permissions