A Backward Algorithm for the Multiprocessor Online Feasibility of Sporadic Tasks

TL;DR

This paper introduces an optimized backward algorithm using antichain techniques to efficiently solve the online feasibility problem for multiprocessor sporadic tasks, significantly improving performance over previous methods.

Contribution

It adapts and enhances the classical attractor algorithm with antichain techniques to address the intractability of the game graph in multiprocessor feasibility testing.

Findings

Dramatic performance improvements in solving the feasibility game.

Effective handling of large game graphs with antichain optimization.

Potential for practical application in real-time multiprocessor scheduling.

Abstract

The online feasibility problem (for a set of sporadic tasks) asks whether there is a scheduler that always prevents deadline misses (if any), whatever the sequence of job releases, which is a priori} unknown to the scheduler. In the multiprocessor setting, this problem is notoriously difficult. The only exact test for this problem has been proposed by Bonifaci and Marchetti-Spaccamela: it consists in modelling all the possible behaviours of the scheduler and of the tasks as a graph; and to interpret this graph as a game between the tasks and the scheduler, which are seen as antagonistic players. Then, computing a correct scheduler is equivalent to finding a winning strategy for the `scheduler player', whose objective in the game is to avoid deadline misses. In practice, however this approach is limited by the intractable size of the graph. In this work, we consider the classical attractor algorithm to solve such games, and introduce antichain techniques to optimise its performance in practice and overcome the huge size of the game graph. These techniques are inspired from results from the formal methods community, and exploit the specific structure of the feasibility problem. We demonstrate empirically that our approach allows to dramatically improve the performance of the game solving algorithm.

Figures

Tables

Table 1. Table 1 : The task set used as our running example

	$C_i$	$D_i$	$T_i$
${\tau }_1$	1	1	2
${\tau }_2$	2	2	2
${\tau }_3$	1	4	2

Table 2. Table 2: Percentage of systems with n 𝑛 n tasks for which the ratio on the number of explored nodes ( BW-TBA / OTFUR-TBA ) falls in the ( 0 , 10 % ) 0 percent 10 (0,10\%) , [ 10 % , 50 % ) percent 10 percent 50 [10\%,50\%) or ( 50 % , 100 % ) percent 50 percent 100 (50\%,100\%) interval.

Ratio	$𝒏=\mathrm{𝟑}$	$𝒏=\mathrm{𝟒}$	$𝒏=\mathrm{𝟓}$	$𝒏=\mathrm{𝟔}$
$(\mathrm{𝟎},\mathrm{𝟏𝟎}\%)$	0%	4.44%	46.67%	64.44%
$[\mathrm{𝟏𝟎}\%,\mathrm{𝟓𝟎}\%)$	88.88%	95.56%	53.33%	35.56%
$(\mathrm{𝟓𝟎}\%,\mathrm{𝟏𝟎𝟎}\%)$	11.12%	0 %	0 %	0%

Table 3. Table 3: The ratio on the number of systems for which BW-TBA runs faster than OTFUR-TBA .

Num. tasks	$𝒏=\mathrm{𝟑}$	$𝒏=\mathrm{𝟒}$	$𝒏=\mathrm{𝟓}$	$𝒏=\mathrm{𝟔}$
Ratio	84.44%	64.44%	44.44%	37.77%

Equations

$$\exists \mathsf{Pre}\left(V\right)$$

$$\forall \mathsf{Pre}\left(V\right)$$

$${\mathsf{Attr}}_i\cup \mathsf{UPre}\left({\mathsf{Attr}}_i\right)=\uparrow \left({\mathsf{Attr}}_i\cup \mathsf{UPre}\left({\mathsf{Attr}}_i\right)\right),$$

$${\mathsf{UPre}}^{\#}\left(\mathcal{A}\right)$$

$${\mathsf{Attr}}_{k-1}\cup \mathsf{UPre}\left({\mathsf{Attr}}_{k-1}\right)$$

$$=\uparrow \left({\mathsf{AntiLosing}}_{k-1}\cup {\mathsf{UPre}}^{\#}\left({\mathsf{AntiLosing}}_{k-1}\right)\right)$$

$$=\uparrow \left({\mathsf{AntiLosing}}_{k-1}\right)\cup \uparrow \left({\mathsf{UPre}}^{\#}\left({\mathsf{AntiLosing}}_{k-1}\right)\right).$$

$${\mathsf{Attr}}_{k-1}$$

$$\mathsf{UPre}\left({\mathsf{Attr}}_i\right)$$

$${\mathsf{Bad}}_{⊒{\tau }_i}$$

$$\text{ and }\text{textsc}{rct}_v({\tau }_i)=C_i-(j+1)\}.$$

$${\mathsf{UPre}}^{\#}\left(\mathcal{A}\right)$$

$$\exists {\mathsf{Pre}}^{\#}\left(\mathcal{A}\right)$$

$$\forall {\mathsf{Pre}}^{\#}\left(\mathcal{A}\right)$$

$$\exists \mathsf{Pre}\left(\uparrow \left(\mathcal{A}\right)\right)$$

$${\mathsf{AntiLosing}}_{i+1}=\lfloor$$

$$\cup {\mathsf{AntiLosing}}_i\rfloor .$$

$$\forall {\mathsf{Pre}}^{\#}\left({\mathsf{AntiLosing}}_i\right)\setminus \uparrow \left({\mathsf{AntiLosing}}_i\right)$$

$${\mathsf{Frontier}}_{i+1}=\lfloor {\mathsf{UPre}}^{\ast }\left({\mathsf{AntiLosing}}_i,{\mathsf{Frontier}}_i\right)\rfloor ,$$

$${\mathsf{UPre}}^{\ast }\left({\mathsf{AntiLosing}}_i,{\mathsf{Frontier}}_i\right)$$

$$=$$

$$\exists \mathsf{Pre}\left({\mathsf{Frontier}}_i\cap V_{\mathcal{S}}\right)\cup \forall {\mathsf{Pre}}^{\ast }\left({\mathsf{AntiLosing}}_i,{\mathsf{Frontier}}_i\cap V_{\mathcal{T}}\right).$$

$${\mathsf{Frontier}}_{i+1}\subseteq {\mathsf{AntiLosing}}_{i+1},$$

$${\mathsf{Frontier}}_{i+1}$$

$$=\lfloor \exists \mathsf{Pre}\left({\mathsf{Frontier}}_i\cap V_{\mathcal{S}}\right)\cup \forall {\mathsf{Pre}}^{\ast }\left({\mathsf{AntiLosing}}_i,{\mathsf{Frontier}}_i\cap V_{\mathcal{T}}\right)\rfloor .$$

$${\mathsf{AntiLosing}}_{i+1}=\lfloor {\mathsf{AntiLosing}}_i\cup {\mathsf{Frontier}}_{i+1}\rfloor .$$

$${\mathsf{AntiLosing}}_1$$

$${\mathsf{UPre}}^{\#}\left({\mathsf{AntiLosing}}_0\right)$$

$${\mathsf{Frontier}}_1$$

$$=\lfloor \exists \mathsf{Pre}\left({\mathsf{Frontier}}_0\cap V_{\mathcal{S}}\right)\cup \forall {\mathsf{Pre}}^{\ast }\left({\mathsf{AntiLosing}}_0,{\mathsf{Frontier}}_0\cap V_{\mathcal{T}}\right)\rfloor .$$

$$\forall {\mathsf{Pre}}^{\#}\left({\mathsf{AntiLosing}}_0\right)=\forall {\mathsf{Pre}}^{\ast }\left({\mathsf{AntiLosing}}_0,{\mathsf{Frontier}}_0\right).$$

$$\lfloor {\mathsf{AntiLosing}}_{i+1}\cup \exists \mathsf{Pre}\left({\mathsf{AntiLosing}}_{i+1}\cap V_{\mathcal{S}}\right)\cup \forall {\mathsf{Pre}}^{\#}\left({\mathsf{AntiLosing}}_{i+1}\cap V_{\mathcal{T}}\right)\rfloor$$

$$=$$

$$\displaystyle\left\lfloor\begin{array}[]{c}{\sf AntiLosing}_{i+1}\cup\exists{\sf Pre}\left({\sf Frontier}_{i+1}\cap V_{\mathcal{S}}\right)\\ \cup\\ \forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i+1},{\sf Frontier}_{i+1}\cap V_{\mathcal{T}}\right)\end{array}\right\rfloor.$$

$$\lfloor {\mathsf{AntiLosing}}_{i+1}\cup \exists \mathsf{Pre}\left({\mathsf{AntiLosing}}_{i+1}\right)\rfloor$$

$$=$$

$$\lfloor {\mathsf{AntiLosing}}_{i+1}\cup \exists \mathsf{Pre}\left({\mathsf{Frontier}}_{i+1}\right)\rfloor .$$

$$\lfloor {\mathsf{AntiLosing}}_{i+1}\cup \forall {\mathsf{Pre}}^{\#}\left({\mathsf{AntiLosing}}_{i+1}\right)\rfloor$$

Full text

1 Introduction

The model of sporadic tasks is nowadays a well-established model for real-time systems. In this model, one considers a set of real-time tasks, that regularly release jobs. The jobs are the actual computational payloads, and the scheduler must assign those jobs to the available processor(s) of the platform in a way that ensures no job misses its deadline (i.e., ensuring that all jobs are granted enough computation time within a given time frame). The term sporadic refers to the fact that there is some uncertainty on the moment at which tasks release jobs: in the sporadic model, an inter-arrival time $T_{i}$ is associated with each task $\tau_{i}$. This means that at least $T_{i}$ time units will elapse in-between two job releases of the task $\tau_{i}$, but the release can be delayed by an arbitrary long time (this is in contrast with the Liu and Layland model [LL73] where the tasks release jobs periodically, i.e., every $T_{i}$ time unit).

In the present paper, we consider the so-called online feasibility problem for such sporadic tasks on a multiprocessor platform, i.e., a platform that boasts several identical computational units on which the scheduler can choose to run any active job. The online feasibility problem asks, given a set of (sporadic) tasks to compute—if possible—a scheduling policy for those tasks ensuring that no task ever misses its deadline. An important assumption is that the scheduler is not clairvoyant, i.e., it has no information on the future job releases, apart from the information that can be deduced from the current history of execution. Hence, the scheduler that has to be computed must be able to react to any potential sequence of job releases (it is thus an online scheduler222Note that our approach requires a significant offline preprocessing phase, hence the schedulers that are produced can be characterised as semionline, according to some authors.).

This feasibility problem of sporadic tasks on multiprocessor platforms is appealing both from the practical and the theoretical point of view. On the practical side, the problem is rich enough to model realistic situations. On the theoretical side, the different degrees of non-determinism of the model (the exact release times of the jobs, the exact execution duration of jobs, the many possible decisions of the scheduler when there are more active tasks than available CPUs) make its behaviour difficult to predict.

Indeed, while several necessary and sufficient conditions have been identified for feasibility, these criteria are not able to decide feasibility of all systems. Moreover, while a collection of optimal schedulers for uniprocessors is known, optimal online multiprocessor scheduling of sporadic real-time tasks is known to be impossible [FGB10], at least for constrained or arbitrary deadline systems.

In this paper, we build on the ideas introduced by Bonifaci and Marchetti-Spaccamela [BM10], and consider a game-based model for our feasibility problem. Intuitively, we regard the scheduler as a player that competes against the coalition of the tasks. The moves of the scheduler are the possible assignments of active jobs to the CPUs, and the moves of the tasks are the possible job releases. The objective of the scheduler in this game is to avoid deadline misses, and we assume that the tasks have the opposite objective. This models the fact that the tasks will not collaborate (i.e., release jobs in a way that avoids deadline misses) with the scheduler. Then, it should be clear that the system of tasks is feasible iff there is a winning strategy for the scheduler (one that enforces the scheduler’s objective whatever the tasks play). When the system is feasible, a scheduler can be extracted from this winning strategy. To the best of our knowledge, this is the only exact feasibility test that has been proposed so far for this problem.

Concretely, the game we consider is a special case of game played on graph, that we call scheduling games: the nodes of the graph model the possible states of the system, and the edges model the possible moves of the players. This approach is akin to the controller synthesis problem which has been extensively considered in the formal methods community for the past 25 years [PR89]: given a model of a computer system interacting with an environment and given a property that this system must satisfy (typically, a safety property), the controller synthesis problem consists in computing a controller that enforces the property, whatever the environment does. The parallel with our feasibility problem should be clear: the scheduler corresponds to the controller, the environment to the tasks, and the property is to avoid deadline misses. In the formal methods literature, the classical approach to the synthesis problem boils down to computing a winning strategy in a game.

The main practical limitation to this approach is the intractable size of the game graph—the so-called ‘state explosion problem’, a typical limitation of exhaustive verification (e.g. model-checking) and synthesis techniques that consider all possible system sates. In our case, this graph is exponential in the size of the problem, so, building the whole graph, then analysing it (as proposed by Bonifaci and Marchetti-Spaccamela [BM10]) is infeasible in practice, even though the algorithms that compute winning strategies for games played on graphs are efficient (they run in polynomial time wrt the size of the graph). Nevertheless, the community of formal methods has proposed several techniques (such as efficient data structures, heuristics to avoid the exploration of all states, etc…) that do overcome this barrier in practice (see for example [BCM*+*92]). Building on these results, we have shown, in previous works, that the same techniques have the potential to dramatically improve the running time of some graph-based algorithms solving real-time scheduling problems. More precisely, in [GGL13] and [GGNS] we have applied so-called antichain [DR10] techniques (introduced originally a.o. to speed up model checking algorithms) and demonstrated experimentally their practical interest.

Contributions In this paper, we continue our line of research and apply the antichain approach to the improve the efficiency of the classical attractor (or backward induction) algorithm to solve scheduling games. At the core of our optimisation is a so-called simulation relation that allows one to avoid exploring a significant portion the game’s nodes. While the antichain approach is a generic one, the definition of the simulation relation has to be tailored to the specific class of problem under consideration. Our simulation relation exploits tightly the peculiar structure of scheduling games. We perform a series of experiments (see Section 5) to demonstrate the usefulness of our new approach. Our enhanced algorithm performs one order of magnitude better that the un-optimised attractor algorithm (see Figure 4). Moreover, we manage to compute schedulers for systems that are not schedulable under the classical EDF scheduler: in particular, when the load of the system is close to 100%, our approach outperforms vastly EDF (see Figure 3).

Related works The feasibility problem for sporadic tasks is a well-studied problem in the real-time scheduling community. Apart for the very particular case where for each task the deadline corresponds to the period (implicit deadline systems), where polynomial time feasibility tests exist, it exhibits a high complexity. For instance, even in the uniprocessor case, the feasibility problem of recurrent (periodic or sporadic) constrained deadline tasks is strongly coNP complete [EY15]. For constrained/arbitrary deadline and sporadic task systems, several necessary or sufficient conditions have been identified for feasibility. However, these criteria are not sufficient to decide feasibility for all systems: there are some systems that do not meet any sufficient conditions (hence, are not surely feasible) and respect all identified necessary conditions (hence are not surely infeasible). We refer the reader to a survey by Davis and Burns [DB11].

As already mentioned, the only exact test (i.e., algorithm to decide the problem) is the one of Bonifaci and Marchetti-Spaccamela [BM10] that consists in reducing the problem to the computation of a winning strategy in a game. However no optimisations are proposed to make this approach practical. In a previous work [GGNS], we have already presented a game solving algorithm, enhanced by antichains, to solve the feasibility problem. Compared to the present paper, [GGNS] relies on the same model (Section 2) and the same partial order $\sqsupseteq$. However, the algorithm we consider here (Algorithm 1) is completely different. Its improvement based on antichains (Algorithm 2, discussed from Section 3.2 onward) is non-trivial and constitutes original work. Our experimental evaluation (Section 5) compares our two approaches and show that they are actually complementary.

2 Feasibility as a game

Let us now define precisely the online feasibility problem of sporadic tasks on a multiprocessor platform. Remember that online means that the scheduler has no a priori knowledge of the behaviour of the tasks; but must react, during the execution of the systems to the requests made by the tasks. To formalise this problem, we consider a set $\tau=\{\tau_{1},\ldots,\tau_{n}\}$ of sporadic tasks to be scheduled on $m$ identical processors. Each task $\tau_{i}$ is characterised by three non-negative integer parameters $C_{i}$, $D_{i}$, $T_{i}$. Parameter $C_{i}$ is the worst case execution time (WCET), i.e. an upper bound on the number of CPU ticks that are needed to complete the job. $D_{i}$ is the deadline, relative to each job arrival. Each job needs to have been assigned $C_{i}$ units of CPU time before its deadline, lest it will miss its deadline (for example if some job of task $\tau_{i}$ is released at instant $t$, it will need $C_{i}$ units of CPU time before $t+D_{i}$). Finally, $T_{i}$ is the minimal interarrival time: at least $T_{i}$ time units must elapse between two job releases of $\tau_{i}$. We assume that jobs can be preempted and can be freely migrated between CPUs, without incurring any delay. An example of system with three tasks is given in Table 1. Finally, we assume that each job requires its WCET. Since the case where all jobs consume their WCET is always a possible scenario, this assumption is without loss of generality. Indeed, if there is no scheduler when the tasks are restricted to consume their whole WCET, then there will be no scheduler in the case where the tasks also have the option to complete earlier; and, if jobs complete earlier at runtime, it is always possible to keep the CPU idle for the remaining allocated ticks.

In such a real-time system, tasks freely submit new jobs, respecting their minimal interarrival time. Then, the scheduler is responsible to allocate the jobs to the CPUs (ensuring that no job misses its deadline), a CPU tick occurs (note that we consider a discrete time model), and a new round begins with the tasks submitting new jobs, etc. To model formally this semantics, we rely on the notion of scheduling game, as sketched in the introduction. Before defining formally this notion, let us introduce it through an example. Given a set of tasks $\tau$ and a number of CPUs $m$, a scheduling game is played on a graph $G_{\tau,m}$, by two players which are the scheduler (called player $\mathcal{S}$) and the coalition of the tasks (player $\mathcal{T}$). In the case of the task set $\tau$ of Table 1 upon a 2-CPUs platform ($m=2$), a prefix of $G_{\tau,m}$ is given in Figure 1. In this graph, the nodes model the system states and the edges model the possible moves of the players (all these notions will be defined precisely hereinafter). Each path is a possible execution of the system. The actual path which is played stems from the interaction of the players which play in turn: the square (respectively round) nodes ‘belong’ to $\mathcal{T}$ ($\mathcal{S}$), which means that $\mathcal{T}$ ($\mathcal{S}$) decides in those nodes what will be the successor node. The game starts in $\mathrm{init}^{\mathcal{T}}$, where the tasks ($\mathcal{T}$) decide which jobs to submit. In the full graph $G_{\tau,m}$, there are $2^{3}=8$ different possibilities, but we display here only the case where all tasks ($\tau_{1}$, $\tau_{2}$ and $\tau_{3}$) submit a job, which moves the system to state $\mathcal{S}_{1}$. In this state, the scheduler must decide which tasks to schedule on the $m=2$ available CPUs. If it decides to schedule only $\tau_{1}$, we obtain state $\mathcal{T}_{2}$ after one clock tick. From the game graph in Figure 1, it is easy to see that this is bad choice for the scheduler. Indeed, from $\mathcal{T}_{2}$, player $\mathcal{T}$ can move the system to $\mathcal{S}_{2}$, and in all successors ($\mathcal{T}_{4}$,…, $\mathcal{T}_{7}$) of $\mathcal{S}_{2}$ a task misses its deadline (depicted by thick node borders). Hence, whatever the scheduler plays from $\mathcal{S}_{2}$ and $\mathcal{T}_{2}$, he loses the game. On the other hand, scheduling $\{\tau_{1},\tau_{2}\}$ and $\{\tau_{2},\tau_{3}\}$ from $\mathcal{S}_{1}$ and $\mathcal{S}_{3}$ respectively, guarantees the scheduler to win the game (all successors of $\mathcal{T}_{11}$ that are not shown are winning too).

2.1 Scheduling games

Let us now formally define scheduling games. We start by the notion of system state that models the current status of all tasks in the system [BC07]. In all states $S$ of the system, we store two pieces of information for each task $\tau_{i}$:

(i) The earliest next arrival time $\textsc{nat}_{S}(\tau_{i})$ of the next job of $\tau_{i}$ and

(ii) the remaining computing time $\textsc{rct}_{S}(\tau_{i})$ of the current job333If several jobs of the same task are active at the same time, they are treated one at a time, in FIFO order. of $\tau_{i}$.

Definition 1** (System states).**

*Let $\tau=\{\tau_{1},\ldots,\tau_{n}\}$ be a set of sporadic tasks. A system state $S$ of $\tau$ is a pair ($\textsc{nat}_{S},\textsc{rct}_{S}$) where:

(i) $\textsc{nat}_{S}$is a function assigning to all tasks $\tau_{i}$ a value $\textsc{nat}_{S}(\tau_{i})\leq T_{i}$; and

(ii) $\textsc{rct}_{S}$is a function assigning to all tasks $\tau_{i}$ a value $\textsc{rct}_{S}(\tau_{i})\leq C_{i}$

Observe that, since the nat parameter is not bounded below, there are infinitely many system states. We will limit the number of states to a finite set when defining the game. A task $\tau_{i}$ is said to be active in state $S$ if it currently has a job that has not finished in $S$, i.e., the set of active tasks in $S$ is $\textsc{Active}(S)=\{\tau_{i}\mid\textsc{rct}_{S}(\tau_{i})>0\}$. To the contrary, we say that $\tau_{i}$ is idle in $S$ iff $\textsc{rct}_{S}(\tau_{i})=0$. A task $\tau_{i}$ is eligible in $S$ if it can submit a job from this configuration, i.e., the set of eligible tasks in $S$ is: $\textsc{Eligible}(S)=\{\tau_{i}\mid\textsc{nat}_{S}(\tau_{i})\leq 0\wedge\textsc{rct}_{S}(\tau_{i})=0\}$. Finally, The laxity of $\tau_{i}$ in $S$ is the value $\textsc{Laxity}_{S}(\tau_{i})=\textsc{nat}_{S}(\tau_{i})-(T_{i}-D_{i})-\textsc{rct}_{S}(\tau_{i})$. Intuitively, the laxity of a task measures the amount of forthcoming CPU steps that the task could remain idle without taking the risk to miss its deadline. In particular, states where the laxity is negative will be declared as losing states.

Now let us define the possible moves of both players. Let $S\in\textsc{States}(\tau)$ be a system state. We first define the possible moves of player $\mathcal{S}$, i.e. the scheduler. One move of $\mathcal{S}$ is characterised by the choice of the set $\tau^{\prime}$ of tasks that will be scheduled. Formally, for all $\tau^{\prime}\subseteq\textsc{Active}(S)$ s.t. $|\tau^{\prime}|\leq m$ (i.e., $\tau^{\prime}$ does not contain more tasks than the $m$ available CPUs), we let $Succ_{\mathcal{S}}(S,\tau^{\prime})$ be the (unique) state $S^{\prime}$ s.t.:

(i) $\textsc{nat}_{S^{\prime}}(\tau_{i})=\textsc{nat}_{S}(\tau_{i})-1$; and

(ii) $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})$if $\tau_{i}\not\in\tau^{\prime}$. Otherwise, $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})-1$.

Let us now define the possible moves of player $\mathcal{T}$, i.e. the tasks. Each move of $\mathcal{T}$ is characterised by a set $\tau^{\prime}$ of eligible tasks. We let $Succ_{\mathcal{T}}(S,\tau^{\prime})\subseteq\textsc{States}(\tau)$ be the set of system states s.t. $S^{\prime}\in Succ_{\mathcal{T}}(S,\tau^{\prime})$ iff:

(i) $\textsc{nat}_{S^{\prime}}(\tau_{i})=\textsc{nat}_{S}(\tau_{i})$if $\tau_{i}\not\in\tau^{\prime}$. Otherwise, $\textsc{nat}_{S^{\prime}}(\tau_{i})=T_{i}$;

(ii) And if $\tau_{i}\not\in\tau^{\prime}$, $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})$. Otherwise, $\textsc{rct}_{S^{\prime}}(\tau_{i})=C_{i}$.

Finally, we let ${\sf Succ}\left(S\right)=Succ_{\mathcal{S}}\cup Succ_{\mathcal{T}}$.

Example 1**.**

The initial state of the game $G_{\tau,m}$ in our running example (state $\mathrm{init}^{\mathcal{T}}$ in Figure 1) contains the system state $\left\langle(0,0),(0,0),(0,0)\right\rangle$ (we denote a system state $S$ by the tuple $\left\langle(\textsc{rct}(\tau_{1}),\textsc{nat}(\tau_{1})),\ldots,(\textsc{rct}(\tau_{n}),\textsc{nat}(\tau_{n}))\right\rangle$). Then, $\mathcal{S}_{1}=\left\langle(1,2),(2,2),(1,2)\right\rangle$. In $\mathcal{S}_{1}$ all tasks are eligible, $\textsc{Laxity}_{\mathcal{S}_{1}}(\tau_{1})=0$ and $\textsc{Laxity}_{\mathcal{S}_{1}}(\tau_{3})=3$. Also, $\mathcal{T}_{3}=\left\langle(0,1),(1,1),(1,1)\right\rangle$, which shows that the job of $\tau_{1}$ that had been initially submitted has now completed (so, $\tau_{1}$ is idle in $\mathcal{T}_{3}$), but we must still wait one time unit before all tasks can submit a new job (their nat are all equal to $1$). This explains why the only successor of $\mathcal{T}_{3}$ is $Succ_{\mathcal{T}}(\mathcal{T}_{3},\emptyset)$. Finally, $\tau_{2}$ has now missed its deadline in $\mathcal{T}_{10}=\left\langle(0,0),(1,0),(0,0)\right\rangle$. Indeed $\textsc{Laxity}_{\mathcal{T}_{10}}(\tau_{2})<0$.

For a set $\tau=\{\tau_{1},\ldots,\tau_{n}\}$ of sporadic tasks, and $m$ CPUs, we let $G_{\tau,m}=\left\langle V_{\mathcal{S}},V_{\mathcal{T}},E,I,{\sf Bad}\right\rangle$ where:

• •

$V_{\mathcal{S}}=\{S\in\textsc{States}(\tau)\mid\forall 1\leq i\leq n:\textsc{Laxity}_{S}(\tau_{i})\geq-1\}\times\{\mathcal{S}\}$ is the set of scheduler-controlled nodes.

• •

$V_{\mathcal{T}}=\{S\in\textsc{States}(\tau)\mid\forall 1\leq i\leq n:\textsc{Laxity}_{S}(\tau_{i})\geq-1\}\times\{\mathcal{T}\}$ is the set of nodes controlled by the tasks.

• •

$E=E_{\mathcal{S}}\cup E_{\mathcal{T}}$ is the set of edges where:

• –

$E_{\mathcal{S}}$ is the set of scheduler moves. It contains an edge \big{(}(S,\mathcal{S}),(S^{\prime},\mathcal{T})\big{)} iff there is $\tau^{\prime}\subseteq\textsc{Active}(S)$ s.t.  $|\tau^{\prime}|\leq m$ and $S^{\prime}=Succ_{\mathcal{S}}(S,\tau^{\prime})$. In this case, we sometimes abuse the notations, and consider that this edge is labelled by $\tau^{\prime}$, denoting it \big{(}(S,\mathcal{S}),\tau^{\prime},(S^{\prime},\mathcal{T})\big{)}.

• –

$E_{\mathcal{T}}$ is the set of tasks moves. It contains an edge \big{(}(S,\mathcal{T}),(S^{\prime},\mathcal{S})\big{)} iff there exists $\tau^{\prime}\subseteq\textsc{Eligible}(S)$ s.t. $S^{\prime}\in Succ_{\mathcal{T}}(S,\tau^{\prime})$. Again, we abuse notations and denote this edge by \big{(}(S,\mathcal{T}),\tau^{\prime},(S^{\prime},\mathcal{S})\big{)}.

• •

$I=(S_{0},\mathcal{T})$, where for all $1\leq i\leq n$: $\textsc{rct}_{S_{0}}(\tau_{i})=\textsc{nat}_{S_{0}}(\tau_{i})=0$ is the initial state.

• •

${\sf Bad}=\{(S,\mathcal{T})\in V_{\mathcal{T}}\mid\exists\tau_{i}\in\textsc{Active}(S)$ such that $\textsc{Laxity}_{S}(\tau_{i})<0\}$, i.e. ${\sf Bad}$ is the set of failure states.

Observe that in this definition, we consider only states where the laxity of all tasks is $\geq-1$. It is easy to check (see [GGL13, BC07] for the details) that this restriction guarantees the number of game nodes to be finite. Moreover, this is sufficient to detect all deadline misses, as any execution of the system where a task misses a deadline will necessarily traverse a state with a laxity equal to $-1$ for one of the tasks [GGL13, BC07]. In the sequel we lift the nat and rct notations to nodes of the games, i.e., for a node $v=(S,\mathcal{P})$, we let $\textsc{nat}_{v}=\textsc{nat}_{S}$ and $\textsc{rct}_{v}=\textsc{rct}_{S}$.

2.2 Computation of winning strategies

Now note that the syntax of scheduling games is fixed, let us explain what we want to compute on those games, i.e. winning strategies for player $\mathcal{S}$. Fix a scheduling game $G_{\tau,m}=\left\langle V_{\mathcal{S}},V_{\mathcal{T}},E,I,{\sf Bad}\right\rangle$. First, a play in $G_{\tau,m}$ is a path in the game graph, i.e. a sequence $v_{0},v_{1},\ldots,v_{i},\ldots$ of graph vertices (for all $i\geq 0$: $v_{i}\in V_{\mathcal{S}}\cup V_{\mathcal{T}}$) s.t. for all $i\geq 0$: $(v_{i},v_{i+1})\in E$. Then, a strategy for player $\mathcal{S}$ is a function $\sigma:V_{\mathcal{S}}\rightarrow V_{\mathcal{T}}$ s.t. for all $v\in V_{\mathcal{S}}$: $(v,\sigma(v))\in E$. That is, $\sigma$ assigns, to each node of $V_{\mathcal{S}}$, one of its successor 444In general, strategies might need to have access to the whole prefix of execution to determine what to play next. However, since scheduling games are a special case of safety games [Tho95], it is well-known that positional strategies are sufficient, i.e. strategies whose output depends only on the current game vertex. to be played when $v$ is reached. Given a strategy $\sigma$, the outcome of $\sigma$ from a node $v\in V_{\mathcal{S}}\cup V_{\mathcal{T}}$ is the set $\mathsf{Outcome}\left(\sigma,v\right)$ of all possible plays in $G_{\tau,m}$ that start in $v$ and are obtained with $\mathcal{S}$ playing according to $\sigma$, i.e., $v_{0},v_{1},\ldots,v_{i},\ldots\in\mathsf{Outcome}\left(\sigma,v\right)$ iff

(i) $v_{0}=v$; and

(ii) for all $i\geq 0$: $v_{i}\in V_{\mathcal{S}}$ implies $v_{i+1}=\sigma(v_{i})$.

We denote by $\mathsf{Outcome}\left(\sigma\right)$ the set $\mathsf{Outcome}\left(\sigma,I\right)$. Then, a strategy $\sigma$ is winning from a node $v$ iff it ensures $\mathcal{S}$ to always avoid ${\sf Bad}$ (from $v$) whatever $\mathcal{T}$ does, i.e., $\sigma$ is winning from $v$ iff for all plays $v_{0},v_{1},\ldots,v_{i},\ldots\in\mathsf{Outcome}\left(\sigma,v\right)$, for all $i\geq 0$: $v_{i}\not\in{\sf Bad}$. A strategy $\sigma$ is simply said winning if it is winning from the initial node $I$. We say that a node $v$ is winning (respectively losing) iff there exists a (there is no) strategy that is winning from $v$. We denote by ${\sf Win}$ and ${\sf Lose}$ the sets of winning and losing nodes respectively. It is well-known 555This property is called determinacy and can be established using the classical result of Donald Martin [Mar75]. that, in our setting, all nodes are either winning or losing, i.e., ${\sf Win}\cup{\sf Lose}=V_{\mathcal{T}}\cup V_{\mathcal{S}}$. Hence, computing one of those sets is sufficient to deduce the other.

It is easy to check that, given a set of sporadic tasks $\tau$ and a number $m$ of CPUs, the scheduling game $G_{\tau,m}$ captures all the possible behaviours of $\tau$ on a platform of $m$ identical CPUs, running under any possible online scheduler. Then, the answer to the online feasibility problem is positive (i.e., there exists an online scheduler) iff there is a winning strategy in the game, i.e., iff $I\in{\sf Win}$, or, equivalently, iff $I\not\in{\sf Lose}$ (this is the condition that our algorithms will check). Actually, the winning strategy $\sigma$ is the scheduler itself: by definition, every pair $(v,\sigma(v))$ corresponds to an edge $(v,\tau^{\prime},\sigma(v))$ in $G_{\tau,m^{\prime}}$, which means that, in state $v$, the scheduler must grant the CPUs to all tasks in $\tau^{\prime}$. Since $\sigma$ is winning no bad state will ever be reached, hence, no deadline will be missed.

Example 2**.**

In the example graph of Figure 1, a winning strategy is a strategy $\sigma$ s.t. $\sigma(\mathcal{S}_{1})=\mathcal{T}_{3}$ and $\sigma(\mathcal{S}_{3})=\mathcal{T}_{11}$. It is easy to check that (on this graph excerpt), playing this strategy allows to avoid ${\sf Bad}=\{\mathcal{T}_{4},\mathcal{T}_{5},\ldots,\mathcal{T}_{10}\}$, whatever choice $\mathcal{T}$ makes.

Let us now recall a classical algorithm to solve safety games, a broad class of games played on graphs to which scheduling games belong. The algorithm is a variant of backward induction: it consists in computing the set of all nodes from which $\mathcal{S}$ cannot guarantee to avoid ${\sf Bad}$. This set, denoted ${\sf Attr}$ is called the attractor of ${\sf Bad}$; in Figure 1, it corresponds to the gray nodes. The computation is done inductively, starting from ${\sf Bad}$, and following the graph edges in a backward fashion (hence the name). Formally, the algorithm relies on the two following operators, for a set $V\subseteq V_{\mathcal{T}}\cup V_{\mathcal{S}}$.

[TABLE]

That is, $v\in\exists{\sf Pre}\left(V\right)$ iff there exists a successor of $v$ which is in $V$; and $v\in\forall{\sf Pre}\left(V\right)$ iff all successors of $v$ belong to $V$. Then, given $V\subseteq V_{\mathcal{T}}\cup V_{\mathcal{S}}$, we let ${\sf UPre}\left(V\right)$ be the set of uncontrollable predecessors of $V$: ${\sf UPre}\left(V\right)=\exists{\sf Pre}\left(V\cap V_{\mathcal{S}}\right)\cup\forall{\sf Pre}\left(V\cap V_{\mathcal{T}}\right)$. Intuitively, $v\in{\sf UPre}\left(V\right)$ iff $\mathcal{S}$ cannot prevent the game to reach $V$ (in one step) from $v$, either because $v$ is a $\mathcal{T}$-node that has a successor (which is necessarily a $\mathcal{S}$-node) in $V$, or because $v$ is an $\mathcal{S}$-node that has all its successors (that are all $\mathcal{T}$-nodes) in $V$. Thus, if $V$ contains only losing nodes, then all nodes in ${\sf UPre}\left(V\right)$ are losing too.

Equipped with these definitions, we can describe now the backward algorithm (Algorithm 1) for solving scheduling games, that will be the basis of our contribution. It computes a sequence $\left({\sf Attr}_{i}\right)_{i\geq 0}$ of sets of states with the following property: $v\in{\sf Attr}_{i}$ iff player $\mathcal{T}$ has a strategy to force the game to reach ${\sf Bad}$ in at most $i$ steps from $v$. Since the sets ${\sf Attr}_{i}$ (which contain nodes of the game graph) grow along with the iterations of the algorithm, and since the graph is finite, the algorithm necessarily terminates. It is well-known that it computes exactly the set of losing states:

Theorem 1** (Taken from [Tho95]).**

*When applied to a

scheduling game $G=\left\langle V_{\mathcal{S}},V_{\mathcal{T}},E,I,{\sf Bad}\right\rangle$, Algorithm 1 terminates in at most $|V_{\mathcal{T}}\cup V_{\mathcal{S}}|$ steps and returns the set of losing states ${\sf Lose}$.*

Thus, the answer to the online feasibility problem is positive iff $I$ does not belong to the set returned by the algorithm. When it is the case, a winning strategy (hence also a scheduler) can easily be obtained: in all nodes $v\in V_{\mathcal{S}}$ that are visited, we let $\sigma(v)$ be any node $v^{\prime}$ s.t. $(v,v^{\prime})\in E$ and $v^{\prime}\not\in{\sf Lose}$. Such a node $v^{\prime}$ is guaranteed to exist by construction (otherwise, by definition of $\forall{\sf Pre}$, $v$ would have been added to the attractor, and would not be winning).

Example 3**.**

On the graph in Figure 1, we have: ${\sf Attr}_{0}=\{\mathcal{T}_{4},\mathcal{T}_{5},\ldots,\mathcal{T}_{10}\}$; ${\sf Attr}_{1}={\sf Attr}_{0}\cup\{\mathcal{S}_{2}\}$; ${\sf Attr}_{2}={\sf Attr}_{1}\cup\{\mathcal{T}_{2}\}$; and ${\sf Attr}_{2}={\sf Attr}_{3}$, so the algorithm converges after 3 steps.

While this algorithm is a nice theoretical solution, one needs to answer the following questions to obtain a practical implementation:

(i) how can we compute a representation of ${\sf Bad}$? and

(ii) given ${\sf Attr}_{i}$, how can we compute ${\sf Attr}_{i+1}$?

Since the game graph is finite, these two questions can be solved by building the whole game graph, and analysing it. However, in practice, the graph has a size which is exponential in the description of the problem instance [BM10], so applying this algorithm straightforwardly is not possible in practice. The core contribution of the present work is to propose heuristics that exploit the particular structure of scheduling games, in order to speed up Algorithm 1.

3 Antichain techniques for sporadic tasks

In this section, we introduce the main technical contribution of the paper: an antichain-based [DR10] heuristic to speed up the performance of the backward algorithm for solving scheduling games. Let us start with an intuitive discussion of our heuristic. It relies on the definition of a partial order $\sqsupseteq$ that compares the state of the game graph, with the following important property: if $v$ is a losing node, then, all ‘bigger’ nodes $v^{\prime}$ (i.e., with $v^{\prime}\sqsupseteq v$) are also losing666Actually, the symmetrical property is also true: if $v\in{\sf Win}$, then, $v\sqsupseteq v^{\prime}$ implies $v^{\prime}\in{\sf Win}$.. Then, the optimisation of Algorithm 1 consists, roughly speaking, in keeping in the sets ${\sf Attr}_{i}$ the minimal elements only. This has two consequences. First, since there are, in practice, many comparable elements in the sets ${\sf Attr}_{i}$, the memory footprint of the algorithm is dramatically reduced. Second, we perform the computation of the uncontrollable predecessors on the minimal elements only (instead of computing the uncontrollable predecessors of all the elements in ${\sf Attr}_{i}$), which reduces significantly the running time of each iteration of the algorithm. It should now be clear that the definition of $\sqsupseteq$ partial order is central to our improved algorithm. Its formal definition will be given later, but we can already sketch its intuition through the following example:

Example 4**.**

On the graph given in Figure 1, we have $\mathcal{T}_{4}\sqsupseteq\mathcal{T}_{5}$. This means that since $\mathcal{T}_{5}$ is losing (it is in ${\sf Bad}$), then $\mathcal{T}_{4}$ should be too (it is indeed the case). So, intuitively, $\mathcal{T}_{4}$ is a node which (from the scheduler’s point of view) is ‘harder’ to win from than $\mathcal{T}_{5}$. Indeed, one can check that $\mathcal{T}_{4}$ corresponds to system state $\left\langle(0,1),(2,0),(1,0)\right\rangle$ and $\mathcal{T}_{5}$ to $\left\langle(0,1),(1,0),(1,0)\right\rangle$. So, $\textsc{rct}_{\mathcal{T}_{4}}(\tau_{2})>\textsc{rct}_{\mathcal{T}_{5}}(\tau_{2})$, while all the other parameters of the states are equal. It is thus not surprising that $\mathcal{T}_{4}$ is ‘harder’ than $\mathcal{T}_{5}$, since $\tau_{2}$ needs more CPU time in $\mathcal{T}_{4}$ than in $\mathcal{T}_{5}$ with the same time remaining to its deadline. This also means that in our improved algorithm, we will not keep $\mathcal{T}_{4}$ in the initial set of states we compute ${\sf Attr}_{0}$, since $\mathcal{T}_{4}$ is not minimal in ${\sf Bad}$.

3.1 Partial orders, antichains and closed sets

Let us now introduce the definitions on which our techniques rely. Fix a finite set $S$. A relation $\operatorname{\unrhd}\in S\times S$ is a partial order iff $\operatorname{\unrhd}$ is reflexive, transitive and antisymmetric. As usual, we often write $s\operatorname{\unrhd}s^{\prime}$ and $s\operatorname{\not\!\!\unrhd}s^{\prime}$ instead of $(s,s^{\prime})\in\operatorname{\unrhd}$ and $(s,s^{\prime})\not\in\operatorname{\unrhd}$, respectively. The $\operatorname{\unrhd}$-upward closure $\uparrow^{\operatorname{\unrhd}}\!\left(S^{\prime}\right)$ of a set $S^{\prime}\subseteq S$ is the smallest set containing $S^{\prime}$ and all the elements that are larger than some element in $S$’, i.e., $\uparrow^{\operatorname{\unrhd}}\!\left(S^{\prime}\right)=\{s\mid\exists s^{\prime}\in S^{\prime}:s\operatorname{\unrhd}s^{\prime}\}$. Then, a set $S^{\prime}$ is upward closed iff $S^{\prime}=\uparrow^{\operatorname{\unrhd}}\!\left(S^{\prime}\right)$. When the partial order is clear from the context, we often write $\uparrow\!\left(S\right)$ instead of $\uparrow^{\operatorname{\unrhd}}\!\left(S\right)$. A subset $\mathcal{A}$ of some set $S^{\prime}\subseteq S$ is an antichain on $S^{\prime}$ with respect to $\operatorname{\unrhd}$ iff it contains only elements that are incomparable wrt $\operatorname{\unrhd}$, i.e. for all $s,s^{\prime}\in\mathcal{A}$: $s\neq s^{\prime}$ implies $s\operatorname{\not\!\!\unrhd}s^{\prime}$. An antichain $\mathcal{A}$ on $S^{\prime}$ is said to be a set of minimal elements of $S^{\prime}$ (or a minimal antichain of $S^{\prime}$) iff for all $s_{1}\in S^{\prime}$ there is $s_{2}\in\mathcal{A}$: $s_{1}\operatorname{\unrhd}s_{2}$. It is easy to check that if $\mathcal{A}$ is a minimal antichain of $S^{\prime}$, then $\uparrow\!\left(\mathcal{A}\right)=\uparrow\!\left(S^{\prime}\right)$. This is a key observation for our improved algorithm: intuitively, $\mathcal{A}$ can be regarded as a compact representation of $\uparrow\!\left(S^{\prime}\right)$, which is of minimal size in the sense that it contains no pair of $\operatorname{\unrhd}$-comparable elements. Moreover, since $\operatorname{\unrhd}$ is a partial order, each subset $S^{\prime}$ of the finite set $S$ admits a unique minimal antichain, that we denote by $\left\lfloor S^{\prime}\right\rfloor$. Observe that one can always effectively build $\left\lfloor S^{\prime}\right\rfloor$, simply by iteratively removing from $S^{\prime}$, all the elements that strictly dominate another one.

In our game setting, we will be interested in a particular class of partial orders, which are called turn-based alternating simulations:

Definition 2** ([AHKV98, GGS14]).**

*Let $G=(V_{\mathcal{S}},V_{\mathcal{T}},E,I,{\sf Bad})$ be a safety game. A partial order $\operatorname{\unrhd}\subseteq(V_{\mathcal{S}}\times V_{\mathcal{S}})\cup(V_{\mathcal{T}}\times V_{\mathcal{T}})$ is a turn-based alternating simulation relation for $G$ (tba-simulation for short) iff for all $v_{1}$, $v_{2}$ s.t. $v_{1}\operatorname{\unrhd}v_{2}$, either $v_{1}\in{\sf Bad}$ or the three following conditions hold:

(i) If $v_{1}\in V_{\mathcal{S}}$, then, for all $v_{1}^{\prime}\in{\sf Succ}\left(v_{1}\right)$, there is $v_{2}^{\prime}\in{\sf Succ}\left(v_{2}\right)$ s.t.  $v^{\prime}_{1}\operatorname{\unrhd}v^{\prime}_{2}$;

(ii) If $v_{1}\in V_{\mathcal{T}}$, then, for all $v_{2}^{\prime}\in{\sf Succ}\left(v_{2}\right)$, there is $v^{\prime}_{1}\in{\sf Succ}\left(v_{1}\right)$ s.t. $v^{\prime}_{1}\operatorname{\unrhd}v^{\prime}_{2}$; and

(iii) $v_{2}\in{\sf Bad}$implies $v_{1}\in{\sf Bad}$.

inline]Some intuition? G.

3.2 Improved algorithm

The key observation to our improved algorithm can now be stated formally: the sets ${\sf Attr}_{i}$ computed by Algorithm 1 are actually upward-closed sets (for any partial order which is a tba-simulation), which justifies that we can a manipulate them compactly through their minimal elements only:

Lemma 1**.**

Given a set $V$ which is upward-closed for a tba-simulation $\operatorname{\unrhd}$: ${\sf UPre}\left(V\right)=\uparrow^{\operatorname{\unrhd}}\!\left({\sf UPre}\left(V\right)\right)$.

Proof.

We need to prove that ${\sf UPre}\left(V\right)\subseteq\uparrow\!\left({\sf UPre}\left(V\right)\right)$ and $\uparrow\!\left({\sf UPre}\left(V\right)\right)\subseteq{\sf UPre}\left(V\right)$. The first item is trivially correct. Now we will prove the second item by showing that $\forall v\in\uparrow\!\left({\sf UPre}\left(V\right)\right)$ then $v\in{\sf UPre}\left(V\right)$. Since $v\in\uparrow\!\left({\sf UPre}\left(V\right)\right)$, there hence exists $v^{\prime}\in{\sf UPre}\left(V\right)$ such that $v\operatorname{\unrhd}v^{\prime}$. We divide into two cases as follows.

• •

In case $v,v^{\prime}\in V\cap V_{\mathcal{T}}$: By Definition 2, for all $\overline{v^{\prime}}\in{\sf Succ}\left(v^{\prime}\right)$, there exists $\overline{v}\in{\sf Succ}\left(v\right)$ such that $\overline{v}\operatorname{\unrhd}\overline{v^{\prime}}$. By the definition of $\forall{\sf Pre}\left(V\cap V_{\mathcal{T}}\right)$ (see equation (2)), $\overline{v^{\prime}}\in V$ therefore $\overline{v}\in V$. Finally, by the definition of $\exists{\sf Pre}\left(V\cap V_{\mathcal{S}}\right)$ (see (1)), we derive that $v\in\exists{\sf Pre}\left(V\cap V_{\mathcal{S}}\right)$ therefore $v\in{\sf UPre}\left(V\right)$.

• •

In case $v,v^{\prime}\in V\cap V_{\mathcal{S}}$: By Definition 2, for all $\overline{v}\in{\sf Succ}\left(v\right)$, then there exists $\overline{v^{\prime}}\in{\sf Succ}\left(v^{\prime}\right)$ such that $\overline{v}\operatorname{\unrhd}\overline{v^{\prime}}$. Then since $v^{\prime}\in{\sf UPre}\left(V\right)$ then ${\sf Succ}\left(v^{\prime}\right)\subseteq V$ (by the definition of $\forall{\sf Pre}\left(V\cup V_{\mathcal{T}}\right)$). Therefore ${\sf Succ}\left(v\right)\subseteq V$, we derive that $v\in\forall{\sf Pre}\left(V\cup V_{\mathcal{T}}\right)$ (see equation (2)) and finally $v\in{\sf UPre}\left(V\right)$.

∎

Proposition 1**.**

Let $G$ be a scheduling game and let $\operatorname{\unrhd}$ a tba-simulation for $G$. Then the sets ${\sf Attr}_{i}$ computed are upward-closed for $\operatorname{\unrhd}$, i.e. for all $i\geq 0$: ${\sf Attr}_{i}=\uparrow^{\operatorname{\unrhd}}\!\left({\sf Attr}_{i}\right)$.

Proof.

We prove the lemma by induction on $i$.

**Base case: ** When $i=0$, by the definition, ${\sf Attr}_{0}={\sf Bad}$. We need to prove that ${\sf Bad}=\uparrow\!\left({\sf Bad}\right)$. It is trivial to conclude that ${\sf Bad}\subseteq\uparrow\!\left({\sf Bad}\right)$. It remains to prove that $\uparrow\!\left({\sf Bad}\right)\subseteq{\sf Bad}$. For each $v\in\uparrow\!\left({\sf Bad}\right)$, there exists $v^{\prime}\in{\sf Bad}$ such that $v\operatorname{\unrhd}v^{\prime}$. Since $v^{\prime}$ is a losing state, than $v^{\prime}$ is losing as well (by the definition of tba-simulation). Hence, $v\in{\sf Bad}$.

**Inductive case: ** For all $i\geq 1$, given ${\sf Attr}_{i}=\uparrow\!\left({\sf Attr}_{i}\right)$, we will prove that ${\sf Attr}_{i+1}=\uparrow\!\left({\sf Attr}_{i+1}\right)$. By the definition of the sequences of ${\sf Attr}$, ${\sf Attr}_{i+1}={\sf Attr}_{i}\cup{\sf UPre}\left({\sf Attr}_{i}\right)$. Then we need to prove that:

[TABLE]

i.e. ${\sf UPre}\left({\sf Attr}_{i}\right)=\uparrow\!\left({\sf UPre}\left({\sf Attr}_{i}\right)\right)$ that has been done by Lemma 1. ∎

We can now define the improvement to Algorithm 1, that consists in manipulating the sequence of sets $({\sf Attr}_{i})_{i\geq 0}$ by their minimal elements only. To this end, we define ${\sf UPre}^{\#}$, a variant of the ${\sf UPre}$ operator that works directly on the minimal elements. It receives an antichain of minimal elements $\mathcal{A}$ (that represents the upward-closed set $\uparrow\!\left(\mathcal{A}\right)$) and returns the antichain of minimal elements of ${\sf UPre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$:

[TABLE]

Clearly, since the game graph is finite and since ${\sf UPre}$ can be computed, $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$ is computable too: it suffices to ‘expand’ the antichain $\mathcal{A}$ to $\uparrow\!\left(\mathcal{A}\right)$ (which is a finite set), compute ${\sf UPre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$, then keep only the minimal elements. However, this procedure deceives the purpose of using a compact representation of upward-closed sets, so we will introduce later an efficient way to compute $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$ for a given partial order. Equipped with ${\sf UPre}^{\#}$, we can now define our improved algorithm, given in Algorithm 2. As announced, it computes a sequence $({\sf AntiLosing}_{i})_{i\geq 0}$ of antichains representing respectively the sets in the $({\sf Attr}_{i})_{i\geq 0}$ sequence, as stated by the following proposition:

Proposition 2**.**

For all $i\in\mathbb{N}$: ${\sf Attr}_{i}=\uparrow\!\left({\sf AntiLosing}_{i}\right)$

Proof.

The proof is by induction on $i$.

Base case ($i=0$): When $i=0$, ${\sf Attr}_{0}={\sf Bad}$ and ${\sf AntiLosing}_{0}=\left\lfloor{\sf Bad}\right\rfloor$. This case is hence trivially correct.

Inductive case ($i=k$): The induction hypothesis is that, ${\sf Attr}_{k-1}=\uparrow\!\left({\sf AntiLosing}_{k-1}\right)$. Let us prove that ${\sf Attr}_{k}=\uparrow{\sf AntiLosing}_{k}$. By the definitions of the two sequences, it is necessary to prove that

[TABLE]

However:

[TABLE]

by induction hypothesis and:

[TABLE]

by definition of ${\sf UPre}^{\#}$, see equation (3). ∎

Based on this proposition, and on the fact that Algorithm 1 computes the sequence $({\sf Attr}_{i})_{i\geq 0}$ and returns ${\sf Lose}$, we conclude that Algorithm 2 is correct, in the sense that it computes the minimal elements of ${\sf Lose}$:

Theorem 2**.**

When applied to a scheduling game $G$ equipped with a tba-simulation $\operatorname{\unrhd}$, Algorithm 2 terminates and returns $\left\lfloor{\sf Lose}\right\rfloor$.

Proof.

By Theorem 1, we know that there is $k$ s.t. ${\sf Attr}_{k}={\sf Attr}_{k+1}={\sf Lose}$. Hence, by Proposition 2, ${\sf AntiLosing}_{k}=\left\lfloor{\sf Attr}_{k}\right\rfloor=\left\lfloor{\sf Attr}_{k+1}\right\rfloor={\sf AntiLosing}_{k+1}$. Hence, Algorithm 2 terminates, and returns a set which is equal to $\left\lfloor{\sf Attr}_{k}\right\rfloor=\left\lfloor{\sf Lose}\right\rfloor$ (remark that Algorithm 2 could converge earlier than Algorithm 1). ∎

4 The improved algorithm in practice

Until now, we have proven that given a scheduling game $G$, and a tba-simulation $\operatorname{\unrhd}$ for $G$, Algorithm 2 terminates and returns the minimal elements of the set of losing states. However, this algorithm is parameterised by the definition of a proper tba-simulation (from which the definition of ${\sf UPre}^{\#}$ depends too), which is strong enough to ensure that the sets $({\sf AntiLosing}_{i})_{i\geq 0}$ will be much smaller than their $({\sf Attr}_{i})_{i\geq 0}$ counterparts. The purpose of this section is twofold:

(i) to define a tba-simulation $\sqsupseteq$ that exploits adequately the structure of scheduling games, as sketched above; and

(ii) to show how to compute efficiently the set $\left\lfloor{\sf Bad}\right\rfloor$ and the operator ${\sf UPre}^{\#}$ (based on $\sqsupseteq$).

For the tba-simulation, we rely on our previous works [GGNS], where we have introduced the idle-ext task simulation partial order and proved that it is tba-simulation:

Definition 3** (Idle-ext task simulation).**

*Let $\tau$ be a set of sporadic tasks on a platform of $m$ processors and let $G=(V_{\mathcal{S}},V_{\mathcal{T}},E,I,{\sf Bad})$ be a scheduling game of $\tau$ on the platform. Then, the idle-ext tasks partial order $\sqsupseteq\subseteq V_{\mathcal{S}}\times V_{\mathcal{S}}\cup V_{\mathcal{T}}\times V_{\mathcal{T}}$ is a simulation relation for all $v_{1}=(S_{1},{\cal P})$, $v_{2}=(S_{2},{\cal P}^{\prime})$: $v_{1}\sqsupseteq v_{2}$ iff ${\cal P}={\cal P}^{\prime}$ and, for all $\tau_{i}\in\tau$, the three following conditions hold:

(i) $\textsc{rct}_{S_{1}}(\tau_{i})\geq\textsc{rct}_{S_{2}}(\tau_{i})$; and

(ii) $\textsc{rct}_{S_{2}}(\tau_{i})=0$implies $\textsc{rct}_{S_{1}}(\tau_{i})=0$; and

(iii) \textsc{nat}_{S_{1}}(\tau_{i})$$\leq\textsc{nat}_{S_{2}}(\tau_{i}).

Theorem 3** (Taken from [GGNS]).**

$\sqsupseteq$* is a tba-simulation*

4.1 Computation of $\left\lfloor{\sf Bad}\right\rfloor$

Given the $\sqsupseteq$ tba-simulation, let us now show how to compute ${\sf AntiLosing}_{0}=\left\lfloor{\sf Attr}_{0}\right\rfloor=\left\lfloor{\sf Bad}\right\rfloor$ (i.e., the initial set in Algorithm 2), without computing first the whole set ${\sf Bad}$. Recall that, by definition ${\sf Bad}$ contains only $\mathcal{T}$ states (this is sufficient since, if a task misses a deadline at a $\mathcal{S}$ state, then all its predecessors—which are $\mathcal{T}$ states—are losing too).

We build the set $\left\lfloor{\sf Bad}\right\rfloor$ by considering each task separately. Let us first consider a game containing only one task $\tau_{i}$. Let $v$ be a state from ${\sf Bad}$. Then, $\textsc{Laxity}_{v}(\tau_{i})=\textsc{nat}_{v}(\tau_{i})-T_{i}+D_{i}-\textsc{rct}_{v}(\tau_{i})<0$. Therefore, $v\in{\sf Bad}$ iff $\textsc{rct}_{v}(\tau_{i})\in\{1,\ldots,C_{i}\}$ and $\textsc{nat}_{v}(\tau_{i})\leq T_{i}-D_{i}+\textsc{rct}_{s}(\tau_{i})-1$. We denote by ${\sf Bad}_{\sqsupseteq\tau_{i}}$ the set:

[TABLE]

It is easy to check (see hereinafter) that, in this game with a single task $\tau_{i}$, $\left\lfloor{\sf Bad}\right\rfloor={\sf Bad}_{\sqsupseteq\tau_{i}}$.

Let us consider now a scheduling game on a set $\tau=\{\tau_{1},\ldots,\tau_{n}\}$ of $n$ tasks. Let $v$ be a state from ${\sf Bad}$. Then, there exists at least one task $\tau_{i}\in\tau$ such that $\textsc{Laxity}_{v}(\tau_{i})<0$. Hence the compact representation of all states that are bad because $\tau_{i}$ has missed its deadline is ${\sf Bad}_{\sqsupseteq\tau_{i},\tau}$, where $v\in{\sf Bad}_{\sqsupseteq\tau_{i},\tau}$ iff

(i) there is $B\in{\sf Bad}_{\sqsupseteq\tau_{i}}$ s.t. $\textsc{nat}_{B}(\tau_{i})=\textsc{nat}_{v}(\tau_{i})$ and $\textsc{rct}_{B}(\tau_{i})=\textsc{rct}_{v}(\tau_{i})$; and

(ii) for all $j\neq i$: $\textsc{nat}_{v}(\tau_{j})=T_{j}$ and $\textsc{rct}_{v}(\tau_{j})\in\{0,1\}$.

Finally, we claim that the antichain covering all bad states is ${\sf Bad}_{\sqsupseteq}=\cup_{1\leq i\leq n}{\sf Bad}_{\sqsupseteq\tau_{i},\tau}$.

Lemma 2**.**

${\sf Bad}_{\sqsupseteq}$* is an antichain and ${\sf Bad}=\uparrow\!\left({\sf Bad}_{\sqsupseteq}\right)$.*

Proof.

Let us first prove that ${\sf Bad}_{\sqsupseteq}$ is an antichain. Since $\forall\tau_{i},{\sf Bad}_{\sqsupseteq\tau_{i}}$ is an antichain, ${\sf Bad}_{\sqsupseteq\tau_{i},\tau}$ is either. Hence if ${\sf Bad}_{\sqsupseteq}$ is not an antichain than there must exist $v_{i}\in{\sf Bad}_{\sqsupseteq\tau_{i},\tau}$ and $v_{k}\in{\sf Bad}_{\sqsupseteq\tau_{k},\tau}$ such that $v_{i}$ and $v_{k}$ are comparable w.r.t $\sqsupseteq$. By the definition above, $\textsc{nat}_{v_{i}}(\tau_{i})=T_{i}-D_{i}+C_{i}-j,\textsc{nat}_{v_{i}}(\tau_{k})=T_{k}$ and $\textsc{nat}_{v_{k}}(\tau_{i})=T_{i},\textsc{nat}_{v_{k}}(\tau_{k})=T_{k}-D_{k}+C_{k}-j^{\prime}$ where $j,j^{\prime}\geq 1$. Since $C_{i}\leq D_{i}$ and $C_{k}\leq D_{k}$, $\textsc{nat}_{v_{i}}(\tau_{i})<\textsc{nat}_{v_{k}}(\tau_{i})$ and $\textsc{nat}_{v_{k}}(\tau_{k})<\textsc{nat}_{v_{i}}(\tau_{k})$. Then $v_{i}$ and $v_{k}$ cannot be comparable (see Definition 3).

For the second item, firstly, we will prove that ${\sf Bad}\subseteq\uparrow{\sf Bad}_{\sqsupseteq}$. Given a state $s^{\prime}\in{\sf Bad}$, assume that $\tau_{i}\in\tau$ misses its deadline in $s$ We will prove that there exists a state $s\in{\sf Bad}_{\sqsupseteq}$ such that $s^{\prime}\sqsupseteq s$.

(i) For $\tau_{i}$, because $\textsc{Laxity}_{s^{\prime}}(\tau_{i})=\textsc{nat}_{s^{\prime}}(\tau_{i})-T_{i}+D_{i}-\textsc{rct}_{s^{\prime}}(\tau_{i})<0$ and $1<\textsc{rct}_{s^{\prime}}(\tau_{i})<C_{i}$. Then rct and nat of $\tau_{i}$ at $s$ is computed as follows: $\textsc{rct}_{s}(\tau_{i})=\textsc{rct}_{s^{\prime}}(\tau_{i})$ and $\textsc{nat}_{s}(\tau_{i})=T_{i}-D_{i}+\textsc{rct}_{s^{\prime}}(\tau_{i})-1$ (i.e. $(\textsc{nat}_{s}(\tau_{i}),\textsc{rct}_{s}(\tau_{i}))\in{\sf Bad}_{\sqsupseteq\tau_{i}}$). It is easy to see that $(\textsc{nat}_{s^{\prime}}(\tau_{i}),\textsc{rct}_{s^{\prime}}(\tau_{i}))\sqsupseteq(\textsc{nat}_{s}(\tau_{i}),\textsc{rct}_{s}(\tau_{i}))$

(ii) For $\tau^{\prime}_{i}$, if $\textsc{rct}_{s^{\prime}}(\tau^{\prime}_{i})=0$ than $\textsc{rct}_{s}(\tau^{\prime}_{i})=0$. And if $\textsc{rct}_{s^{\prime}}(\tau^{\prime}_{i})>0$ than $\textsc{rct}_{s}(\tau^{\prime}_{i})=1$. In both the two cases, $\textsc{nat}_{s}(\tau^{\prime}_{i})=T^{\prime}_{i}$. Finally, we see that $(\textsc{nat}_{s^{\prime}}(\tau^{\prime}_{i}),\textsc{rct}_{s^{\prime}}(\tau^{\prime}_{i}))\sqsupseteq(\textsc{nat}_{s}(\tau^{\prime}_{i}),\textsc{rct}_{s}(\tau^{\prime}_{i}))$.

Now let us prove that ${\sf Bad}\supseteq\uparrow{\sf Bad}_{\sqsupseteq}$. Given $v\in\uparrow{\sf Bad}_{\sqsupseteq}$, then $\exists\tau_{i}\in\tau$ s.t. $\textsc{nat}_{s}(\tau_{i})\leq T_{i}-D_{i}+C_{i}-j$ and $\textsc{rct}_{s}(\tau_{i})\geq C_{i}-(j-1)$ where $j=1..C_{i}$. Then $\textsc{Laxity}_{s}(\tau_{i})\leq T_{i}-D_{i}+C_{i}-j-T_{i}+D_{i}-C_{i}-(j+1)$. Therefore, $\textsc{Laxity}_{s}(\tau_{i})\leq-1$. In consequence $v\in{\sf Bad}$. ∎

4.2 Computation of ${\sf UPre}^{\#}\left(\mathcal{A}\right)$

Given this tba-simulation $\sqsupseteq$, let us now show how to compute ${\sf UPre}^{\#}$. As for the definition of ${\sf UPre}$, we split the computation of uncontrollable predecessors according to the types of the nodes, and let:

[TABLE]

where the specifications for these two new operators are:

[TABLE]

Computation of $\exists{\sf Pre}^{\#}$

The computation of $\exists{\sf Pre}^{\#}\left(\mathcal{A}\right)$ for some antichain $\mathcal{A}$ of $\mathcal{S}$ nodes turns out to be easy, as shown by the next lemma. Intuitively, it says that, computing $\exists{\sf Pre}\left(U\right)$ for some upward-closed set $U\subseteq V_{\mathcal{T}}$ which is given to us by its compact representation (minimal antichain) $\mathcal{A}=\left\lfloor U\right\rfloor$, boils down to computing $\exists{\sf Pre}\left(\mathcal{A}\right)$ (i.e., computing the predecessors of the minimal elements). After minimisation, $\left\lfloor\exists{\sf Pre}\left(\mathcal{A}\right)\right\rfloor$ gives us the compact representation of $\exists{\sf Pre}\left(U\right)$. Observe that this Lemma holds for any tba-simulation $\operatorname{\unrhd}$, and not only for $\sqsupseteq$:

Lemma 3**.**

For all antichains $\mathcal{A}\subseteq V_{\mathcal{S}}$, for all tba-simulations $\operatorname{\unrhd}$: $\exists{\sf Pre}^{\#}\left(\mathcal{A}\right)=\left\lfloor\exists{\sf Pre}\left(\mathcal{A}\right)\right\rfloor$

Proof.

To show this lemma, one must show that $\left\lfloor\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)\right\rfloor=\left\lfloor\exists{\sf Pre}\left(\mathcal{A}\right)\right\rfloor$, since by definition of $\exists{\sf Pre}^{\#}$, $\exists{\sf Pre}^{\#}\left(\mathcal{A}\right)=\left\lfloor\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)\right\rfloor$. We thus prove that:

[TABLE]

We show the inclusion in both directions.

First, $\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)\subseteq\uparrow\!\left(\exists{\sf Pre}\left(\mathcal{A}\right)\right)$. For all $v\in\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$, there exists $v^{\prime}$ s.t. $v^{\prime}\in{\sf Succ}\left(v\right)\cap\uparrow\!\left(\mathcal{A}\right)$, by definition of $\exists{\sf Pre}$. Then $v^{\prime}\in\uparrow\!\left({\sf Succ}\left(v\right)\cap\mathcal{A}\right)$. Hence ${\sf Succ}\left(v\right)\cap\mathcal{A}\neq\emptyset$. Therefore $v\in\exists{\sf Pre}\left(\mathcal{A}\right)$ (see equation (1)), in consequence $v\in\uparrow\!\left(\exists{\sf Pre}\left(\mathcal{A}\right)\right)$. Next, let us show that $\uparrow\!\left(\exists{\sf Pre}\left(\mathcal{A}\right)\right)\subseteq\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$. For each $v\in\uparrow\exists{\sf Pre}\left(\mathcal{A}\right)$, there exists $v^{\prime}$ s.t. $v^{\prime}\in\exists{\sf Pre}\left(\mathcal{A}\right)$ and $v\operatorname{\unrhd}v^{\prime}$. There hence exists $\overline{v^{\prime}}$, a successor of $v^{\prime}$ and $v^{\prime}\in\mathcal{A}$ (since ${\sf Succ}\left(v^{\prime}\right)\cap\mathcal{A}\neq\emptyset$). By Definition 2, there exists $\overline{v}\in{\sf Succ}\left(v\right)$ such that $\overline{v}\operatorname{\unrhd}\overline{v^{\prime}}$. Since $\overline{v^{\prime}}\in\mathcal{A}$ then $\overline{v}\in\uparrow\mathcal{A}$. Hence, $v\in\exists{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$. ∎

It remains to observe that, given any set $V^{\prime}\subseteq V_{\mathcal{S}}$, computing $\left\lfloor\exists{\sf Pre}\left(V^{\prime}\right)\right\rfloor$ can be done directly (i.e., without the need of building and exploring a large portion of the game graph), by ‘inverting’ the definition of the successor relation, and making sure to keep minimal elements only. More precisely, let $v=(S,\mathcal{S})\in V_{\mathcal{S}}$ be a $\mathcal{S}$ node. Then, $v^{\prime}=(S^{\prime},\mathcal{T})\in\exists{\sf Pre}\left(\{v\}\right)$ iff the following conditions hold for all $\tau_{i}\in\tau$:

(i) if $\textsc{rct}_{S}(\tau_{i})<C_{i}$, then $\textsc{rct}_{S}(\tau_{i})=\textsc{rct}_{S^{\prime}}(\tau_{i})$ and $\textsc{nat}_{S}(\tau_{i})=\textsc{nat}_{S^{\prime}}(\tau_{i})$; and (ii) if $\textsc{rct}_{S}(\tau_{i})=C_{i}$ than either $\textsc{rct}_{S^{\prime}}(\tau_{i})=0$ and $\textsc{nat}_{S^{\prime}}(\tau_{i})=0$ or $\textsc{rct}_{S^{\prime}}(\tau_{i})=C_{i}$ and $\textsc{nat}_{S^{\prime}}(\tau_{i})=\textsc{nat}_{S}(\tau_{i})$.

In the end, $\left\lfloor\exists{\sf Pre}\left(V^{\prime}\right)\right\rfloor$ = $\left\lfloor\bigcup_{v\in V^{\prime}}\exists{\sf Pre}\left(\{v\}\right)\right\rfloor$.

Computation of $\forall{\sf Pre}^{\#}$

Let us now show how to compute, in an efficient fashion, the operator $\forall{\sf Pre}^{\#}$. Remember that we are given an antichain $\mathcal{A}\subseteq V_{\mathcal{T}}$ which is a compact representation of some upward-closed set $\uparrow\!\left(\mathcal{A}\right)$, and that we want to compute $\left\lfloor\forall{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)\right\rfloor$, without needing to compute the full $\uparrow\!\left(\mathcal{A}\right)$ set. Unfortunately, and contrary to $\exists{\sf Pre}^{\#}$, it is not sufficient to consider the predecessors of the elements in $\mathcal{A}$ to deduce $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$, as shown by the example in Figure 2. In this example, the antichain $\mathcal{A}$ is $\{\mathcal{T}_{1},\mathcal{T}_{2}\}$. The gray cones depict the upward-closures of those states. Now, if we consider the predecessors of $\mathcal{T}_{1}\in\mathcal{A}$, we obtain $\mathcal{S}_{1}$, however this state has a successor $\mathcal{T}_{3}$ which is not in $\uparrow\!\left(\mathcal{A}\right)$, so $\mathcal{S}_{1}\not\in\forall{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$, hence $\mathcal{S}_{1}\not\in\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$. Yet, on this example, there is a state $\mathcal{S}_{1}^{\prime}\sqsupseteq\mathcal{S}_{1}$ which has all its successors in $\uparrow\!\left(\mathcal{A}\right)$, but which is neither in $\exists{\sf Pre}\left(\mathcal{A}\right)$ nor in $\forall{\sf Pre}\left(\mathcal{A}\right)$.

Unfortunately, we haven’t managed to find a direct way to compute $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$ from $\mathcal{A}$; i.e., without enumerating some elements of $\uparrow\!\left(\mathcal{A}\right)$ that are not in $\mathcal{A}$. We propose a method that, while not working only on elements of $\mathcal{A}$, avoids the full enumeration of $\uparrow\!\left(\mathcal{A}\right)$, and performs well in practice. It is described in Algorithm 3. Instead of computing $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$, it returns the subset $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)\setminus\uparrow\!\left(\mathcal{A}\right)$. Observe that this subset is sufficient for Algorithm 2, because, at each step, one computes, from ${\sf AntiLosing}_{i}$, the set ${\sf AntiLosing}_{i+1}$ as:

[TABLE]

Hence, it is easy to check that replacing $\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i}\right)$ in (7) by:

[TABLE]

does not change the value of the expression. Yet, computing $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)\setminus\uparrow\!\left(\mathcal{A}\right)$ instead of $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$ allows us to avoid considering elements which are already computed (in $\mathcal{A}$), which makes Algorithm 3 efficient in practice. This algorithm works as follows. First, we build a set $\mathrm{ToSearch}$ of candidates nodes for the set $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$, then we explore it. $\mathrm{ToSearch}$ is initialised by the loop starting at line 3. In this loop, we consider all the predecessors $v$ of $\mathcal{A}$ (we will explain hereinafter how these predecessors can be computed efficiently). We keep only the predecessors $v$ that are not covered by $\mathcal{A}$, and check whether all successors of $v$ are in $\uparrow\!\left(\mathcal{A}\right)$. If yes, $v\in\forall{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$, and we add $v$ to the antichain $\mathcal{B}$ (that will eventually be returned). Remark that the test ${\sf Succ}\left(v\right)\subseteq\uparrow\!\left(\mathcal{A}\right)$ can be performed without computing explicitly $\uparrow\!\left(\mathcal{A}\right)$, by checking that, for all $v^{\prime}\in{\sf Succ}\left(v\right)$, there is $v^{\prime\prime}\in\mathcal{A}$ s.t. $v^{\prime}\sqsupseteq v^{\prime\prime}$. If there are some successors of $v$ that are not in $\uparrow\!\left(\mathcal{A}\right)$, we must consider all nodes larger than $v$ as candidates for $\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$, but not those that are already in $\uparrow\!\left(\mathcal{A}\right)$, hence, we add to $\mathrm{ToSearch}$ the set $\uparrow\!\left(v\right)\setminus\uparrow\!\left(\mathcal{A}\right)$. The fact that we add $\uparrow\!\left(v\right)\setminus\uparrow\!\left(\mathcal{A}\right)$ instead of $\uparrow\!\left(v\right)$ is important to keep $\mathrm{ToSearch}$ small, which is a key optimisation of the algorithm. Then, once $\mathrm{ToSearch}$ has been built, we examine all the elements $v$ it contains, and check whether they belong to $\forall{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$, in the loop starting in line 3. If $v\in\forall{\sf Pre}\left(\uparrow\!\left(\mathcal{A}\right)\right)$ (line 3), $v$ is added to $\mathcal{B}$. Otherwise, another optimisation of the algorithm occurs: $v$ is discarded from $\mathrm{ToSearch}$, as well as all the nodes that are smaller than $v$ (line 10). This is correct by properties of the tba-simulation (see [GGS14]), and allows the algorithm to eliminate candidates from $\mathrm{ToSearch}$ much quicker.

To conclude the description of Algorithm 3, let us explain how to compute $\exists{\sf Pre}\left(\mathcal{A}\right)$ efficiently, when $\mathcal{A}\subseteq V_{\mathcal{T}}$, as needed in line 3. Let $(S,\mathcal{T})$ be a $\mathcal{T}$-node. Then, $(S^{\prime},\mathcal{S})\in\exists{\sf Pre}\left(S,\mathcal{T}\right)$ iff there is a set $\tau^{\prime}\subseteq\tau$ of scheduled tasks s.t. $|\tau^{\prime}|\leq m$ (at most $m$ tasks have been scheduled) and the following conditions hold for all $\tau_{i}\in\tau$:

(i) $\textsc{nat}_{S^{\prime}}(\tau_{i})=\min(\textsc{nat}_{S}(\tau_{i})+1,T_{i})$ (ii) $\textsc{rct}_{S}(\tau_{i})=C_{i}$implies $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})$

(iii) $\textsc{rct}_{S}(\tau_{i})<C_{i}$implies $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})$ if $\tau_{i}\not\in\tau^{\prime}$; and $\textsc{rct}_{S^{\prime}}(\tau_{i})=\textsc{rct}_{S}(\tau_{i})+1$ otherwise.

4.3 Further optimisation of the algorithm

We close our discussion of BW-TBA by describing the last optimisation that further enhances the performance of the algorithm. In Algorithm 2, the ${\sf UPre}^{\#}$ operator is applied, at each step of the main loop, to the whole ${\sf AntiLosing}_{i}$ set in order to compute ${\sf AntiLosing}_{i+1}$. While this makes the discussion of the algorithm easier, it incurs unnecessary computations: instead of computing the uncontrollable predecessors of all states in ${\sf AntiLosing}_{i}$, one should instead compute the uncontrollable predecessors of the node that have been inserted in ${\sf AntiLosing}_{i}$ at the previous iteration of the loop only. As an example, on the game in Figure 1, ${\sf AntiLosing}_{0}=\left\lfloor\{\mathcal{T}_{4},\ldots,\mathcal{T}_{10}\}\right\rfloor$; ${\sf AntiLosing}_{1}={\sf AntiLosing}_{0}\cup\{\mathcal{S}_{2}\}$ since $\mathcal{S}_{2}$ is incomparable to $\mathcal{T}_{4},\ldots,\mathcal{T}_{10}$. Then, to discover that $\mathcal{T}_{2}$ is a losing node too, we should only apply ${\sf UPre}^{\#}$ to $\mathcal{S}_{2}$, and not to $\mathcal{T}_{4},\ldots,\mathcal{T}_{10}$ again.

To formalise this idea, we introduce the notion of frontier. Intuitively, at each step $i$ of the algorithm, ${\sf Frontier}_{i}$ is an antichain that represents the newly discovered losing states, i.e. the states that have been declared losing at step $i$ but were not known to be losing at step $i-1$. To define formally the sequence $\left({\sf Frontier}_{i}\right)_{i\geq 0}$, we introduce the operator $\forall{\sf Pre}^{*}\left(\mathcal{A},\mathcal{C}\right)$ defined as $\forall{\sf Pre}^{*}\left(\mathcal{A},\mathcal{C}\right)=\break\uparrow\!\left(\exists{\sf Pre}\left(\mathcal{C}\right)\right)\cap\forall{\sf Pre}^{\#}\left(\mathcal{A}\right)$. That is, nodes in $\forall{\sf Pre}^{*}\left(\mathcal{A},\mathcal{C}\right)$ have all their successors in $\mathcal{A}$ and are larger than some predecessor of $\mathcal{C}$. Hence, $\forall{\sf Pre}^{*}\left(\mathcal{A},\mathcal{C}\right)$ can be computed by adapting Algorithm 3, substituting $\exists{\sf Pre}\left(\mathcal{C}\right)$ for $\exists{\sf Pre}\left(\mathcal{A}\right)$ in line 3. Clearly, if we manage to keep the size of $\mathcal{C}$ as small as possible, we will further decrease the size of $\mathrm{ToSearch}$, and Algorithm 3 will be even more efficient.

Now let us define the sequence of ${\sf Frontier}_{i}$ sets. We let ${\sf Frontier}_{0}=\left\lfloor{\sf Bad}\right\rfloor={\sf Bad}_{\sqsupseteq}$. For all $i>0$, we let:

[TABLE]

and:

[TABLE]

Observe that in this new definition of the uncontrollable predecessor operator, only predecessors of nodes in the frontier are considered for computation, which is the key of the optimisation. The next lemma and proposition justify the correctness of this new construction. In particular, Proposition 3 shows that the sequence $\left({\sf AntiLosing}_{i}\right)_{i\geq 0}$ (which is computed by BW-TBA) can be computed applying the operator we have just described, on elements from the frontier only.

To establish Proposition 3, we first need an ancillary lemma, showing that all the elements that occur in the frontier at some step $i$ are also in ${\sf AntiLosing}_{i}$:

Lemma 4**.**

For all $i\in\mathbb{N},{\sf Frontier}_{i}\subseteq{\sf AntiLosing}_{i}$.

Proof.

We prove the lemma by induction on $i$.

Base case: When $i=0$, ${\sf AntiLosing}_{0}={\sf Bad}_{\sqsupseteq}$ and ${\sf Frontier}_{0}$ = ${\sf Bad}_{\sqsupseteq}$. Hence the lemma is trivially correct.

**Inductive case: ** Given ${\sf Frontier}_{i}\subseteq{\sf AntiLosing}_{i}$, we will prove that:

[TABLE]

i.e. $\forall v\in{\sf Frontier}_{i+1}:v\in{\sf AntiLosing}_{i+1}$.

By the definition of the sequence ${\sf Frontier}$:

[TABLE]

By the definition of the sequence ${\sf AntiLosing}$, ${\sf AntiLosing}_{i+1}=\lfloor{\sf AntiLosing}_{i}\cup\exists{\sf Pre}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{S}}\right)\cup\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{T}}\right)\rfloor$. Hence, proving that the two following items are correct is sufficient.

1. (i)

$\exists{\sf Pre}\left({\sf Frontier}_{i}\cap V_{\mathcal{S}}\right)\subseteq\exists{\sf Pre}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{S}}\right)$ 2. (ii)

$\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i},{\sf Frontier}_{i}\cap V_{\mathcal{T}}\right)\subseteq\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{T}}\right)$.

We then prove these two items as follows:

• (i)

Given $v\in\exists{\sf Pre}\left({\sf Frontier}_{i}\cap V_{\mathcal{S}}\right)$, then $\exists v^{\prime}\in{\sf Succ}\left(v\right)$ where $v^{\prime}\in{\sf Frontier}_{i}\cap V_{\mathcal{S}}$ (see equation (1)). Since ${\sf Frontier}_{i}\subseteq{\sf AntiLosing}_{i}$ then $v^{\prime}\in{\sf AntiLosing}_{i}$ as well. Hence, $v\in\exists{\sf Pre}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{S}}\right)$.

• (i)

Given $v\in\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i},{\sf Frontier}_{i}\cap V_{\mathcal{T}}\right)$ then $v\in\exists{\sf Pre}\left({\sf Frontier}_{i}\cap V_{\mathcal{T}}\right)\cap\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{T}}\right)$. Therefore, $v\in\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i}\cap V_{\mathcal{T}}\right)$ as well.

Hence the lemma is successfully proved. ∎

We can now prove Proposition 3:

Proposition 3**.**

For all $i\in\mathbb{N}$:

[TABLE]

Proof of Proposition 3.

The proof is proved by induction on $i$.

**Base case: ** When $i=0$, ${\sf AntiLosing}_{0}={\sf Frontier}_{0}={\sf Bad}_{\sqsupseteq}$. By definition of the sequence ${\sf AntiLosing}$:

[TABLE]

On the other hand:

[TABLE]

Since ${\sf AntiLosing}_{0}={\sf Frontier}_{0}$, then:

[TABLE]

Hence, ${\sf UPre}^{\#}\left({\sf AntiLosing}_{0}\right)={\sf Frontier}_{1}$. Finally, ${\sf AntiLosing}_{1}=\lfloor{\sf AntiLosing}_{0}\cap{\sf Frontier}_{1}\rfloor$.

**Inductive case: ** For all $i>0$, given ${\sf AntiLosing}_{i+1}=\lfloor{\sf AntiLosing}_{i}\cup{\sf Frontier}_{i+1}\rfloor$, we need to prove ${\sf AntiLosing}_{i+2}=\lfloor{\sf AntiLosing}_{i+1}\cup{\sf Frontier}_{i+2}\rfloor$. In other words we need to prove that:

[TABLE]

We divide into two cases as follows.

For all states controlled by player $\mathcal{S}$, the proposition becomes:

[TABLE]

We need to prove that ${\sf AntiLosing}_{i+1}\cup\exists{\sf Pre}\left({\sf AntiLosing}_{i+1}\right)$ (abbreviated by $\mathcal{L}$) = ${\sf AntiLosing}_{i+1}\cup\exists{\sf Pre}\left({\sf Frontier}_{i+1}\right)$ (abbreviated by $\mathcal{R}$).

• •

Assume that $\exists v\in\mathcal{L}$ such that $v\not\in\mathcal{R}$ ($v\in V_{\mathcal{T}}$). Hence:

(i) $v\not\in{\sf AntiLosing}_{i+1}$; and

(ii) $v\in\exists{\sf Pre}\left({\sf AntiLosing}_{i+1}\right)$.

From 1i, there does not exist $v^{\prime}\in{\sf AntiLosing}_{i}$ such that $v\in\exists{\sf Pre}\left(\{v^{\prime}\}\right)$. From 1ii, there exists $v^{\prime}\in{\sf AntiLosing}_{i+1}$ such that $v\in\exists{\sf Pre}\left(\{v^{\prime}\}\right)$. Hence $v^{\prime}\in{\sf AntiLosing}_{i+1}\setminus{\sf AntiLosing}_{i}$, i.e. $v^{\prime}\in{\sf Frontier}_{i+1}$ (thanks to the hypothesis). In consequence, $v\in\exists{\sf Pre}\left({\sf Frontier}_{i+1}\right)$. In contradiction. Therefore $\mathcal{L}\subseteq\mathcal{R}$.

• •

Given $v\in\mathcal{R}$, if $v\in{\sf AntiLosing}_{i+1}$ then $v\in\mathcal{L}$. Otherwise, $v\in\exists{\sf Pre}\left({\sf Frontier}_{i+1}\right)$. Hence there exists $v^{\prime}\in{\sf Frontier}_{i+1}$ such that $v\in\exists{\sf Pre}\left(\{v^{\prime}\}\right)$. Since ${\sf Frontier}_{i+1}\subseteq{\sf AntiLosing}_{i+1}$ (see Lemma 4), $v^{\prime}\in{\sf AntiLosing}_{i+1}$. Thus by equation $\eqref{eq:pree2}$, $v\in\exists{\sf Pre}\left({\sf AntiLosing}_{i+1}\right)$, thus $v\in\mathcal{L}$. Hence, $\mathcal{L}\supseteq\mathcal{R}$. 2. 2.

For all states controlled by player $\mathcal{T}$, the proposition becomes:

[TABLE]

We need to prove ${\sf AntiLosing}_{i+1}\cup\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i+1}\right)={\sf AntiLosing}_{i+1}\cup\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i+1},{\sf Frontier}_{i+1}\right)$. For the sake of clarity let us denote:

[TABLE]

Hence, we need to show that $\mathcal{L}=\mathcal{R}$.

• •

Assume that there exists a state $v\in\mathcal{L}$ such that $v\not\in\mathcal{R}$. Therefore $v\not\in{\sf AntiLosing}_{i+1}$ (there exists $v^{\prime}\not\in{\sf AntiLosing}_{i}$ where $v\in\break\uparrow\!\left(\exists{\sf Pre}\left(v^{\prime}\right)\right)$ (a)) and $v\in\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i+1}\right)$, therefore ${\sf Succ}\left(v\right)\subseteq\break\uparrow\!\left({\sf AntiLosing}_{i+1}\right)$ (b), i.e. $v^{\prime}\in{\sf AntiLosing}_{i+1}$. Thanks to the hypothesis, $v^{\prime}\in{\sf AntiLosing}_{i+1}\setminus{\sf AntiLosing}_{i}$, i.e. $v^{\prime}\in{\sf Frontier}_{i+1}$ (c). By combining (a), (b) and (c), $v\in\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i+1},{\sf Frontier}_{i+1}\right)$. In consequence $v\in\mathcal{R}$. In contradiction. Hence, $\mathcal{L}\subseteq\mathcal{R}$.

• •

Given $v\in\mathcal{R}$, if $v\in{\sf AntiLosing}_{i+1}$ than $v\in\mathcal{L}$. Otherwise, $v\in\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i+1},{\sf Frontier}_{i+1}\right)$, therefore $v\in\forall{\sf Pre}^{\#}\left({\sf AntiLosing}_{i+1}\right)$ by definition of the operator $\forall{\sf Pre}^{*}\left(\mathcal{A},\mathcal{B}\right)$. Hence, $\mathcal{L}\supseteq\mathcal{R}$.

We conclude that ${\sf AntiLosing}_{i+1}=\lfloor{\sf AntiLosing}_{i}\cup{\sf Frontier}_{i+1}\rfloor$. ∎

Hence, the formula in line 5 of Algorithm 2 can be replaced by ${\sf AntiLosing}_{i+1}=\left\lfloor{\sf AntiLosing}_{i}\cup{\sf Frontier}_{i+1}\right\rfloor$ (see Proposition 3,), where ${\sf Frontier}_{i+1}$ is computed from ${\sf Frontier}_{i}$: ${\sf Frontier}_{i+1}=\lfloor\forall{\sf Pre}^{*}\left({\sf AntiLosing}_{i},{\sf Frontier}_{i}\cap V_{\mathcal{T}}\right)\cup{\sf AntiLosing}_{i}\cup$

$\exists{\sf Pre}\left({\sf Frontier}_{i}\cap V_{\mathcal{S}}\right)\rfloor$. Since all the computations are now performed on the frontier instead of the whole ${\sf AntiLosing}_{i}$ set, the performance of Algorithm 2 is improved. This is the algorithm we have implemented and that we report upon in the next section.

5 Experimental Results

Let us now report on a series of experiments that demonstrate the practical interest of our approach. Remember that our algorithm performs an exact test, i.e. given any real-time system of sporadic tasks, the algorithm always computes an online scheduler if one exists. Otherwise, the algorithm proves the absence of scheduler for the system.

Our implementations are made in C++ using the STL. We performed our experiments on a Mac Pro (mid 2010) server with OS X Yosemite, processor of 3.33 GHz, 6 core Intel Xeon and memory of 32 GB 1333 MHz DDR3 ECC. Our programs were compiled with Apple Inc.’s distribution of g++ version 4.2.1.

We compare the performance of our improved algorithm BW-TBA (Algorithm 2, implemented with the frontier optimisation described in Section 4.3) to three other approaches. The first one consists in scheduling the system with the classical EDF (Earliest Deadline First) scheduler. The second (called ES) consists in first building the portion of the game graph that contains all states that are reachable from $I$ (the initial state), then applying Algorithm 1 to compute ${\sf Lose}$, and finally testing whether $I\in{\sf Lose}$ or not. The third approach, called OTFUR-TBA has been introduced in [GGNS]. Contrary to BW-TBA and ES that are backward approaches (since we unfold the successor relation in a backward fashion, starting from the ${\sf Bad}$ states), OTFUR-TBA is a forward algorithm. It builds a portion of the game graph and looks for a winning strategy using on-the-fly computation. The idea has originally been introduced as a general algorithm called OTFUR for safety games [CDF*+*05], and OTFUR-TBA is essentially an improved version of OTFUR using antichain techniques (and the $\sqsupseteq$ partial order), just as BW-TBA is an improved version of ES. In [GGNS], we report on experiments showing OTFUR-TBA outperforms ES in practice.

EDF is known to be optimal for arbitrary collections of independent jobs scheduled upon uniprocessor platforms. This optimality result, however, is no longer true on multiprocessor platforms (that is, there are systems of sporadic tasks for which an online scheduler exists, but that will not be scheduled by EDF). The goal of our first experiment is to compare the number of systems that EDF and BW-TBA can schedule. To this aim, we have generated 2,000 sets of tasks, grouped by values of utilisation $U$. For all instances, we consider $m=2$ CPUs and $n=4$ tasks. For each $U\in[0.1,2]$ with a step of 0.1, 100 instances are randomly generated. The $T$ parameters of all tasks range in the interval $[5,15]$. The generation of this benchmark is based on the Uunifast algorithm [BB05].

Figure 3 depicts the ratio of systems scheduled by EDF and BW-TBA on the benchmark described above. All of the 2,000 randomly generated instances are feasible, hence BW-TBA always computes a scheduler, while the ratio of systems that are schedulable by EDF decreases sharply with the increase in the utilisation factor. This is a first strong point in favour of our approach.

Like BW-TBA, the ES algorithm performs an exact feasibility test, but we naively builds the whole graph of the game which is of exponential size. In order to compare the performance of ES and BW-TBA, we reuse the benchmark presented in [GGNS] (also based on Uunifast). It consists of 2,100 sets of tasks grouped by values of $T$, the interarrival time. For all instances, we consider $m=2$ CPUs and $n=3$ tasks. For each $i$ in $\{7,9,11,13,15,17,19\}$, a set called $\tau^{[i,i+2]}$ of 300 tasks is generated, with a $T$ parameter in the $[i,i+2]$ range. For each game instance in the benchmark, we run both BW-TBA and ES and collect two metrics: the number of explored states and the running time.

Figure 4 displays, for each set $\tau^{[i,i+2]}$, the average number of states explored and the average running time, of the two algorithms. Our improved algorithm BW-TBA outperforms ES both in terms of space and running time, by approximately one order of magnitude. These results definitely demonstrate the practical interest of antichain techniques for scheduling games.

Now, let us compare the performance of the forward and backward algorithms both enhanced with antichains. We performed another experiment on a benchmark where we let the number of tasks vary. We randomly generated 45 instances of systems with $n$ tasks for $n\in\{3,4,5,6\}$ (on a 2 CPUs platform). In all instances, we have $T\in[5,7]$, $U\in\{1,1.5,2\}$ and $D\in[C,T]$. Like the two previous benchmarks, this one is based on Uunifast too.

Our experiments show that, on all instances, BW-TBA explores less states than OTFUR-TBA. This phenomenon happens because BW-TBA computes only the losing states while OTFUR-TBA explores both losing and winning states during search. Table 2, presents the ratio of space explored by BW-TBA and OTFUR-TBA, for example, on systems with 6 tasks, BW-TBA consumes less than 10% of the memory needed by OTFUR-TBA on 64.64% of instances. Note that the memory performance of BW-TBA (vs OTFUR-TBA) improve when the number of tasks increase.

Table 3 presents the ratio of instances on which BW-TBA runs faster than OTFUR-TBA. Notice that the time taken for each instance (of a fixed number of tasks) is variable. For example, on 6-task systems, some are done within one minute; while others take hours to complete. The time taken depends on several hardly predictable characteristics of the system like the number of losing states. These experiments show no clear winner between BW-TBA and OTFUR-TBA, which are rather complementary approaches. In terms of memory, BW-TBA outperforms OTFUR-TBA but OTFUR-TBA might run faster on some systems.

6 Conclusion

Inspired by Bonifaci and Marchetti-Spaccamela, we have considered a game-based model for the online feasibility problem of sporadic tasks (on multiprocessor platforms), and we have developed an efficient algorithm to analyse these games, which takes into account the specific structure of the problem. Broadly speaking, we believe that the application of well-chosen formal methods techniques (together with specialised heuristics that exploit the structure of the problems), is a research direction that has a lot of potential and that should be further followed.