A pre-order relation for exact schedulability test of sporadic tasks on multiprocessor Global Fixed-Priority scheduling

Youcheng Sun, Giuseppe Lipari

A Pre-Order Relation for Exact Schedulability Test of Sporadic Tasks on Multiprocessor Global Fixed-Priority Scheduling * Youcheng Sun Scuola Superiore Sant'Anna y.sun@sssup.it Giuseppe Lipari Univ. Lille, CNRS, Centrale Lille, UMR 9189 -CRIStAL -F-59000 Lille, France giuseppe.lipari@univ-lille1.fr December 9, 2015

Abstract

In this paper we present an exact schedulability test for sporadic realtime tasks scheduled by the Global Fixed Priority (G-FP) Fully Preemptive Scheduler on a multiprocessor system. The analysis consists in modeling the system as a Linear Hybrid Automaton (LHA), and in performing a reachability analysis for states representing deadline miss conditions. To mitigate the problem of state space explosion, we propose a pre-order relationship over the symbolic states of the model: states that are simulated by others can be safely eliminated from the state space.

We also formulate the concept of decidability interval with respect to a set of constrained-deadline sporadic tasks on multiprocessor. The decidability interval is a bounded time interval such that, if a deadline miss occurs in the schedule, then it is possible to find a configuration of arrival times for the tasks such that the deadline miss happens within the bounded interval. Vice versa, if no configuration of arrival times produces a deadline miss in the bounded interval, then no deadline miss is ever possible in the schedule. Hence we prove that the schedulability analysis problem is decidable, and we provide a formula for computing the decidability interval. To our knowledge, this is the first time such a time interval is proposed for sporadic tasks running on multiprocessor.

The proposed schedulability analysis has been implemented in a software tool. For the first time we assess the pessimism of the state-of-the-art approximate schedulability test through experiments. Moreover, we show

Introduction

A real-time system consists of a set of real-time tasks with timing constraints, executed on a single or multiprocessor platform. A real-time task is a piece of code that must be executed periodically or upon reception of an event. Each instance of the task is called a job and it is characterised by a worst-case execution time (i.e. an upper bound on the execution time of the corresponding piece of code), an arrival time (i.e. the instant at which the job is inserted in the ready queue of the operating system and could start executing) and a deadline (i.e. the instant in time within which it must completed). The response time of a job is the length of interval between its arrival and the time instant it finishes execution.

One fundamental problem for real-time systems is to assess the schedulability of a set of tasks on a platform by a certain scheduling algorithm: a task set is said to be schedulable if all jobs complete executions before their deadlines.

One of the most popular scheduling algorithms in the programming practice is the Fixed Priority Fully Preemptive scheduler: each task is assigned a fixed priority, and jobs are ordered in the ready queue by decreasing priority; if a lower priority task is executing and a higher priority task is activated, the latter can preempt the former and execute in its place.

Since the seminal work of [START_REF] Liu | Scheduling Algorithms for Multiprogramming in a Hard-Real-Time Environment[END_REF], the fixed-priority scheduling problem has been extensively studied. The problem has been solved exactly for single processor systems by using a well known property: the worst-case response time of a task happens when it is activated simultaneously with its higher priority tasks, and all jobs are activated at their maximum frequency. Therefore, it suffices to simulate the system starting from this critical instant and activating all subsequent jobs as soon as possible, until the first idle time.

In this paper, we consider the problem of checking the schedulability of a set of independent real-time sporadic tasks on a multiprocessor platform when the scheduling algorithm is the Global Fixed Priority (G-FP) Fully Preemptive scheduler. According to this scheduling algorithm, on a m-processor platform all jobs are ordered in one single ready queue by decreasing priority, and the m highest priority jobs are executed at every instant.

Unfortunately, there is no easy solution for checking the schedulability of a task set scheduled by G-FP. The difficulty comes from two facts:

• No single critical instant exists: the worst-case response time of a task can be found anywhere in the schedule. Also, it is not true that the worst-case response time happens when all jobs are activated as soon as possible. An example is presented in Section 3.

• On the other hand, the sporadic behaviour of the tasks increases the number of possible interleavings.

In order to find the exact combination of arrival times that leads to the worst-case response time of a task, it is then necessary to explore all possible legal combinations of arrivals, and this number is so large that a brute-force approach fails already for very small task sets.

Therefore, most of the research in the literature has been focused on finding upper bounds to the response times. However, to assess the pessimism of such approximate analyses, it is necessary to solve the problem exactly, i.e. to obtain necessary and sufficient conditions for the schedulability of a task set. Contributions In this paper, we address the problem of deriving an exact analysis for the schedulability of a set of sporadic real-time tasks scheduled by G-FP on a multiprocessor platform. We model the problem using the formalism of Linear Hybrid Automata ( [START_REF] Alur | Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems[END_REF][START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF]) to represent the tasks and the scheduler. In particular, deadline miss conditions are modeled as error locations in the automata. The analysis consists in performing a reachability analysis for such error states. Due to the non-deterministic sporadic task activations, the analysis complexity explodes for very small task sets. To defer the state explosion, we propose a weak simulation relation between symbolic states and prove its correctness. The relation allows us to eliminate those states that are not useful for our reachability analysis, thus reducing the size of the state space. Furthermore, we prove the decidability of the proposed analysis by demonstrating that the schedulability test of a set of sporadic tasks under G-FP scheduling policy can be done in a bounded time interval, called decidability interval. We present the implementation of our model in a software tool, and we show that it can handle more complex task sets with respect to state-of-the-art exact algorithms based on discrete time. Here, by "more complex" we mean that tasks' parameters can be generic values and, as we are going to see, this makes a critical difference between previous works on exact multiprocessor schedulability analysis and our solution. Also, we evaluate the pessimism of current state-of-the-art approximate schedulability analysis of G-FP scheduling over sporadic tasks. Through extensive experiments, we investigate the factors that could affect the runtime performance of the proposed schedulability analysis. Limitations. Unfortunately, as the number of sporadic tasks grows beyond 7, and for more than 4 processors, the complexity rises so much that all exact analysis techniques proposed so far can hardly terminate on current desktop computers, even when using our weak simulation relation. This is due to the exponential nature of the problem and it can only be mitigated by future improvements of the simulation relation. Thus, we will continue to work in this direction in the hope to further enhance the practicability of the method. Organisation. The remainder of this paper is organised as follows. In Section 2 we discuss previous works on the same problem. In Section 3 we formally introduce the problem. In Section 4 we describe the formalism of Linear Hybrid Automata. In Section 5 we present our model for the G-FP scheduling problem over sporadic tasks. The core of the paper is Section 6, in which we propose the pre-order relationship and prove its correctness as a weak simulation relation in our proposed LHA model; we also formalise the exact schedulability test, based on reachability analysis in LHA. In Section 7 we introduce the concept of decidability interval and demonstrate how to derive it for G-FP scheduling of sporadic tasks, then apply the obtained decidability interval result to prove the decidability of our exact test in case of constrained-deadline tasks. In Section 8 we report a set of experiments. Finally, in Section 9 we conclude the paper.

Related Work

Given the complexity of the problem, most of the work for G-FP scheduling is focused on obtaining an approximate schedulability test.

The general properties of multiprocessor scheduling have been discussed in many previous papers. [START_REF] Grolleau | On the periodic behavior of real-time schedulers on identical multiprocessor platforms[END_REF][START_REF] Cucu | Feasibility intervals for multiprocessor fixedpriority scheduling of arbitrary deadline periodic systems[END_REF] proposed upper bounds to the feasibility interval of a set of periodic tasks scheduled upon a multiprocessor (uniform or heterogeneous).

[3] developed sophisticated schedulability analysis techniques consisting in selecting a problem window, and in computing an upper bound to the maximum amount of workload and interference of each individual task in that window. Since then, reducing the pessimism in the estimation of workload and interference has been the main approach to improve analysis precision. [START_REF] Bertogna | Response-time analysis for globally scheduled symmetric multiprocessor platforms[END_REF] applied this technique to perform an iterative response time analysis of global scheduling. [START_REF] Guan | New response time bounds for fixed priority multiprocessor scheduling[END_REF] developed RTA-LC (Response Time Analysis with Limited Carry-in) schedulability analysis for G-FP scheduling by integrating the response time analysis in [START_REF] Bertogna | Response-time analysis for globally scheduled symmetric multiprocessor platforms[END_REF] and the technique in [START_REF] Baruah | Techniques for Multiprocessor Global Schedulability Analysis[END_REF] for Global Earliest Deadline First (G-EDF) scheduling of limiting the number of carry-in tasks.

[30] developed RTA-CE (RTA with Carry-in task sets Enumeration) that explicitly enumerates all possible carry-in task sets. Among approximate G-FP schedulability tests, RTA-CE achieves the best precision. In this paper, we also evaluate how much pessimism lies between the RTA-CE test and the exact analysis.

Regarding exact analysis, the first brute force approach to the problem was proposed in [START_REF] Baker | Brute-Force Determination of Multiprocessor Schedulability for Sets of Sporadic Hard-Deadline Tasks[END_REF]: the test assumes discrete time parameters, and it consists in building a finite state machine that represents all possible combinations of arrival times and execution sequences for a task set scheduled by G-EDF. Unfortunately, the problem is so complex that the authors could analyse only tasks whose period is in the range {3, 4, 5}; the tool produces an out-of-memory error for values of T = 6.

[15] proposed an exact schedulability test for a set of periodic tasks, but they did provide neither a tool, nor experiments with task sets. We believe that their algorithm is very complex and a naive implementation would not scale to a large number of tasks. [START_REF] Guan | Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking[END_REF] proposed a timed-automata model for schedulability analysis of periodic tasks. However, periodic tasks are simpler to analyse than sporadic tasks: we will provide a detailed comparison in Section 8.4.

Recently, [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF] improved over [START_REF] Baker | Brute-Force Determination of Multiprocessor Schedulability for Sets of Sporadic Hard-Deadline Tasks[END_REF] by using an antichain technique. In particular, they proposed a simulation relation between states of the underlying finite automaton. An informal definition of simulation relation is the following: Given two states s 1 and s 2 , we say that s 1 simulates s 2 (denoted as s 1 s 2 ) if and only if: 1) for every state s 2 successor of s 2 , there exists a state s 1 successor of s 1 and s 1 s 2 ; 2) if s 2 is an error state (i.e. it models a deadline miss), then also s 1 is an error state.

Thanks to this relation, when we find two states such that s 1 s 2 , we can avoid analysing all paths starting from state s 2 : in fact, if the error state is not reachable from s 1 , then it is not reachable from s 2 either. This produces a significant reduction on the number of states to be analysed in the reachability analysis. The simulation relation proposed in [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF] is valid for any fixed joblevel scheduling algorithm, including G-FP and G-EDF. Besides, [START_REF] Bonifaci | Feasibility analysis of sporadic real-time multiprocessor task systems[END_REF] studied the feasibility problem of sporadic tasks in multiprocessor by reducing it to a safety game, where the two players are the scheduler and the set of the tasks respectively. As shown in [START_REF] Geeraerts | Synthesising succinct strategies in safety and reachability games[END_REF], the antichain technique in [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF] can be applied to [START_REF] Bonifaci | Feasibility analysis of sporadic real-time multiprocessor task systems[END_REF] in order to improve the efficiency.

However, all such methods rely on explicit (discrete) techniques for time analysis and are limited to tasks with very small discrete parameters. For example, in their experiments [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF] could analyse task sets with maximum period equal to T = 8 on 2 processors.

In this paper we take a different approach. We model the system as a Linear Hybrid Automaton (LHA) and then we perform our analysis on the corresponding symbolic state space. As in [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF], we define a weak simulation relation over the symbolic states, and prove its correctness for G-FP scheduling. This allows us to considerably reduce the analysis time, and thus to analyse more complex task sets. Due to the different features between explicit and symbolic techniques for state space exploration, when tasks are with small parameters, it is possible that existing works on exact multiprocessor schedulability analysis are more efficient than our solution; however, our exact analysis is the only work that can handle task sets with general configurations.

System Model

We consider the problem of checking the schedulability of a set of n independent sporadic tasks, scheduled on m identical processors, with n > m, by G-FP, so that all timing constraints are respected.

A sporadic task τ i = (C i , D i , T i ) is characterised by a minimum interarrival time T i , a relative deadline D i and a worst-case execution time (WCET) C i (≤ min{D i , T i }). With an abuse of notation, T i is sometimes called period. The utilisation of a task is defined as U i = Ci Ti . The task emits jobs whose activation time is separated by at least T i units of time; each job executes for at most C i units of time and must complete within D i units of time from its activation. A task is said to have constrained-deadline if D i ≤ T i ; otherwise, it is called an unconstrained-deadline task. An arbitrary-deadline task has no requirement on the values of relative deadline D i and period T i , that is, D i could be less than, equal to or larger than T i . We assume that all jobs of the same task must be executed sequentially and cannot be parallelised. Each task is pre-assigned a fixed and unique priority, and we assume that a lower task index corresponds to a higher priority. We assume by convention that time 0 corresponds to the first arrival instant of any sporadic task in the system: in other words, no arrival event happens before time 0.

In this paper we consider global fixed-priority (G-FP) fully-preemptive scheduling: the execution of a job can be suspended at any time to execute another higher priority job (preemption); the same job can later resume execution on a possibly different processor (migration). G-FP scheduling is sustainable ( [START_REF] Baker | Sustainable multiprocessor scheduling of sporadic task systems[END_REF]), i.e. given a schedulable task set, by decreasing the WCET C i , increasing T i or enlarging D i of tasks, the task set remains schedulable.

As mentioned in Section 1, the main obstacle to perform an exact analysis is that there is no critical instant, and that the worst-case response time of a task may not correspond to a situation in which all jobs arrive as soon as possible.

To better understand the problem, consider the following example (from [START_REF] Baruah | Techniques for Multiprocessor Global Schedulability Analysis[END_REF]): the system consists of 3 tasks τ 1 = (1, 1, 2), τ 2 = (1, 3, 3) and τ 3 = (5, 6, 6), to be scheduled by G-FP on a 2-processor platform. Task τ 1 has the highest priority and τ 3 is the lowest priority task. The schedule obtained when all tasks start at time 0 and arrive as soon as possible is shown in Figure 1a, where all tasks meet their deadlines. However, if the second job of task τ 1 arrives at time instant 3 instead of 2, task τ 3 misses its deadline (Figure 1b).

In fact, we cannot make any worst-case assumption on the arrival times of the jobs, we need to analyse all legal combinations of arrival instants.

Linear Hybrid Automata

A hybrid automaton ( [START_REF] Alur | Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems[END_REF], [START_REF] Halbwachs | Verification of real-time systems using linear relation analysis[END_REF]) is a finite automaton associated with a finite set of variables continuously varying in dense time. In this section, we introduce the basic terminology and the definition of Linear Hybrid Automata.

Let Var = {x 1 , . . . , x n } be a set of continuous variables and V ar = { ẋ1 , . . . , ẋn } be the set of variables' derivatives over time. A linear constraint atom over Var is of the form n i=1 c i x i ∼ b, where c i (1 ≤ i ≤ n) and b are rational numbers and ∼∈ {<, ≤, =, ≥, >}. A linear constraint C is the conjunction of a finite number of constraint atoms. A valuation ν over Var is a function that assigns a real value to each element in Var. The set of all possible valuations over Var is denoted as V (Var). We write ν |= C to represent that ν satisfies C. The same notations can also be defined for V ar. Definition 1. A Linear Hybrid Automaton A = (Var, Loc, Init, Lab, Trans, D, Inv) consists of seven components:

• a finite set Var of variables;

• a finite set Loc of locations including an initial location l 0 ;

• a labeling function Init that specifies the initial linear constraint over variables;

• a finite set Lab of synchronisation labels including a stutter label ;

• a finite set Trans of transitions;

• a labeling function D which assigns to each location l a linear constraint over variables' derivatives;

• and a labeling function Inv which assigns each location l a constraint, called invariant, over variables.

The automaton can be in a location l as long as the current valuations of the variables satisfy Inv(l). A transition is a tuple (l, γ, a, α, l ) consisting of a source location l, a target location l , a guard γ that is a linear constraint over Var, a synchronisation label a ∈ Lab, and the transition relation α which is used to update the values of the variables in Var. We require that on each location, there is a stutter transition (l, true, , Id, l) where Id = {(ν, ν)|ν ∈ V (Var)} is the identical transition relation.

Let A 1 and A 2 be two LHA over a set of variables Var. Their parallel composition A 1 ×A 2 is the LHA (Var, Loc 1 ×Loc 2 , Init, Lab 1 ∪Lab 2 , Trans, D, Inv) such that:

• Init(l 1 , l 2 ) = Init 1 (l 1 ) ∧ Init 2 (l 2 ). • ((l 1 , l 2 ), γ, a, α, (l 1 , l 2 )) ∈ Trans iff 1. (l 1 , γ 1 , a 1 , α 1 , l 1 ) ∈ Trans 1 and (l 2 , γ 2 , a 2 , α 2 , l 2 ) ∈ Trans 2 . 2. γ = γ 1 ∧ γ 2 . 3. either a 1 = a 2 = a, or either a 1 = a ∈ (Lab 1 ∩ Lab 2 ) and a 2 = or a 1 = and a 2 = a ∈ (Lab 1 ∩ Lab 2 ). 4. α = α 1 ∧ α 2 . • D(l 1 , l 2 ) = D 1 (l 1 ) ∧ D 2 (l 2 ). • Inv(l 1 , l 2 ) = Inv 1 (l 1 ) ∧ Inv 2 (l 2 ).
A concrete state s of the LHA is in the form of (l, ν), where l is a location and ν ∈ V (Var). A state can change in two ways:

• A discrete step: (l, ν) a -→ (l , ν ) which means there exists a transition (l, γ, a, α, l ) and

ν |= γ ∧ ν = α(ν) ∧ ν |= Inv(l )
• A time step: (l, ν) t -→ (l, ν ) at which t is a real-value represents time elapsed, and

ν |= Inv(l) ∧ ν ∈ ν ↑ t D(l) ∧ν |= Inv(l) ∧ t ≥ 0
where ν ↑ t D(l) represents the set of valuations that can be reached by letting variables continuously evolve for t time units, according to derivatives constrained by D(l), and starting from the valuation ν.

We use → to represent a generic step, which could be either a discrete step or time step. We also define ⇒ to denote a sequence of steps, and t = ⇒ means that the accumulated time during the sequence of steps is t.

A symbolic state S of the LHA is a pair (l, C), where l is a location and C is a linear constraint over variables. We can define a step and a sequence of steps for symbolic states by lifting the definitions of step and sequence of steps for concrete states. When it comes to symbolic states, the corresponding operations are performed on convex regions instead of concrete valuations on variables.

For a concrete state s and a symbolic state S, we say s ∈ S if s.l = S.l and s.ν |= S.C. The concrete state space and symbolic state space of a LHA A are represented by space(A) and Space(A) respectively.

Multiprocessor Schedulability in LHA

In this section we describe the automaton used for modeling our scheduling problem. In particular, we use two different types of automata that synchronise with each other: the task automata and the scheduler automaton. Indeed, the LHA model we are going to propose can be also encoded by using Timed Automata with stopwatches ( [START_REF] Cassez | The Impressive Power of Stopwatches[END_REF]). As it will be clear in the next section, the only difference is that we allow some variables to decrease at unitary rate, whereas in Stopwatch Timed Automata all variables are either stopped or increasing at unitary rate. We think that using the LHA model is more straightforward to understand our analysis scheme in Section 6.

The task automata

We start by presenting the LHA that models one single sporadic task. Such a LHA model for the sporadic task is called task automaton. A concrete task Variable p represents the time passed since the latest activation of the task, and its rate is always 1. Every time a new job arrives, p is reset to 0. Variable c represents the remaining computation time of a task. Its rate can be 0, when the task does not execute, or -1 when the task executes.

Idle ṗ = 1, ċ = 0 Waiting ṗ = 1, ċ = 0 p ≤ D Running ṗ = 1, ċ = -1 c ≥ 0 ∧ p ≤ D Deadline Missed arrival p ≥ T p := 0 c := C dispatch p ≥ T p := 0 c := c + C p ≥ D preemption c > 0 c > 0∧ p ≥ D p ≥ T p := 0 c := c + C end c = 0
The automaton works as follows. Initially, it is in state Idle, where p ≥ 0 and c = 0; p ≥ 0 models the fact that the first job release of a task can happen at any time. From there, when the guard constraint p ≥ T is satisfied, i.e. at least T time units have been passed since latest activation of the task, it can move non-deterministically to location Waiting. Along with this new job arrival transition, p variable is reset to 0 and C is assigned to variable c. Also, it synchronises with the scheduler (see next section) on the task arrival label. Notice that every task always executes for its WCET: as mentioned in Section 3, G-FP is sustainable, thus if the system is schedulable when every task always executes for its WCET, it is also schedulable when a task is allowed to execute for less than its WCET.

While in Waiting, the rate of c will remain equal to 0. The automaton moves to location Running after synchronising with the scheduler on label dispatch, which notifies that some processor is available for the task to run. While a task is running, the rate of c is set to -1, so its remaining computation time decreases. Its execution can be preempted by the arrival of a higher priority task, at which point the task will move back to location Waiting after synchronising with the scheduler on label preemption.

We say a task is active if it is in location Waiting or Running. An active task must finish its computation time before reaching its deadline. This means the c variable must reach 0 no later than the time at which p reaches D. Otherwise, a task misses its deadline and goes (from Waiting or Running) to the Deadline-Missed location. If a task finishes its execution before deadline, i.e. c = 0 and p ≤ D, the task is forced to move to location Idle (transition from Running to Idle).

In case that a task has unconstrained deadline, there could be a new job arrival for an active task. This is modeled as a non-deterministic transition from Waiting or Running to itself. Since the new instance must wait for its precedence completes, variable c is incremented by C with the transition.

In the following we will denote as TA i the automaton corresponding to the i-th task in the system, with q i , c i , p i its location, left computation time and passed time, respectively, and with arrival i , end i , dispatch i , preemption i the corresponding synchronisation labels.

Scheduling automaton

Given a set of tasks T = {TA 1 , . . . , TA n }, set A is defined as the set of active tasks that are in locations Waiting or Running, and set R denotes the set of tasks that are in location Running.

Let Scheduler : 2 T → 2 T be a scheduling function that, given a set of active tasks, returns the set of executing tasks: R = Scheduler(A).

In this paper, we consider a G-FP Scheduler, which chooses the min{m, |A|} highest priority tasks to run.

The scheduling function can be modeled by a finite automaton synchronised with the task automata the system is composed of. More formally, the scheduling (or scheduler) automaton Sched = {m, Loc, Lab} is characterised by:

• m is the number of identical processors in the system;

• Loc is the set of locations of the scheduler;

• Lab = i Lab i with Lab i = {arrival i , end i , dispatch i , preemption i } is the set of synchronisation labels.
The responsibility of a scheduling automaton is to synchronise with the task automata, i.e. to decide which tasks to run (staying in location Running) and which tasks to wait (staying in location Waiting). Every time a task completes its execution or releases a new job, the active task set A changes to A and a new running task set R is computed according to the scheduling function R = Scheduler(A ). Then, for the task that is in R but was not in R , the scheduling automaton informs its preemption from the processor through synchronisation on the preemption i label; and for the task that was not in R but is now in R , the scheduling automaton synchronises on the dispatch i label with it.

An example of scheduling automaton for n = 3 tasks on m = 2 processors is shown in Figure 3. In the figure, nodes depict locations, and the name of the location encodes the state of the system queue, and in some cases the event that just happened. For example, location E1E2W3 corresponds to the execution of task τ 1 and τ 2 on the two processors, and the task τ 3 waiting to be executed; location E1 arr2 represents the fact that, while task τ 1 is executing on one processor, task τ 2 has just arrived. Also, please note that all locations with names containing arr are assumed to be committed locations1 . Finally, on the edges we show the synchronisation labels (in short form for graphical reasons), hence arr1 stands for arrival 1 , etc. For simplicity, when there is a preemption (for example τ 3 is preempted by the arrival of τ 1 ), we put the two synchronisation labels pre3 and dis1 in the same transition. This means between the two synchronisations, no time will elapse (as we assume no context switch cost). This can be realised by inserting a committed location in between the two. In the special case of one processor, a formal modeling of the fixed-priority scheduler can be found in [START_REF] Sun | Toward parametric timed interfaces for real-time components[END_REF].

The number of locations needed for representing the scheduler automaton is exponential in the number of tasks. Such locations can be automatically generated by using function Scheduler() for computing which task to execute and which task to suspend or preempt. Notice also that the location encodes the same information that is contained in the task automata presented above; in particular, executing tasks will be in location Running, whereas suspended tasks will be in location Waiting. Therefore, the scheduler automaton does not add additional complexity to the problem; on the contrary, it restricts the number of possible combinations of task locations: for example a lower priority task cannot be in the Running location if there are m higher priority tasks that are active. Finally, a system automaton SA = (T , Sched), is the parallel composition of n task automata and one scheduler automaton, where

• T = {TA 1 , . . . , TA n } is a set of n task automata;
• Sched is the scheduler automaton.

The following theorem shows that SA models the real-time scheduling of a set T of sporadic tasks with G-FP, including all legal task arrival and execution patterns.

Theorem 1. Given a task set T , all tasks in T are guaranteed to meet their deadlines if and only if DeadlineMissed locations are not reachable in the system automaton SA.

Proof. We must demonstrate that, if there is a deadline miss for the set of tasks under G-FP scheduling, there is a sequence of transitions in SA starting from the initial location until to the DeadlineMissed location. Vice versa, if some DeadlineMissed locations can be reached using a sequence of transitions, then there exists a configuration of arrival times for the sporadic instances such that one task will miss its deadline. Suppose that the task set is not schedulable under G-FP and the first deadline miss happens at time t. We now build a sequence of transitions (i.e. a trace) in the SA that reproduces the schedule.

Suppose that the first instance of a task τ i is released at time r i,1 . Then, the corresponding TA remains in the Idle location while p < r i,1 , and the transition to location Waiting is taken when p = r i,1 ; correspondingly p is reset to 0. The scheduling automaton Sched at each instant represents the state of the ready queue, so it mimics the state of the schedule. For example, upon arrival of a high priority task, a sequence of transitions synchronized by dispatch and/or preemption is triggered in zero time so that the TA corresponding to the high priority task is moved to location Running, whereas the TA corresponding to the preempted task is moved to location Waiting. If a task executes for ∆t units of time, the corresponding variable c is decreased by the same amount, so the value of the variable always represents the execution time.

Successive releases at r i,j are treated differently: if the task has already completed its execution, the corresponding automaton is in location Idle, so they are treated as in the first release.

If at time r i,j the previous instance of τ i has not yet completed, the TA may decide non-deterministically to update c and p to account for the new instance or decide to ignore the new arrival and analyse the previous one. In practice, in the analysis we need to consider both cases. If the instance that misses the deadline is the (j -1)-th instance of task τ i , we ignore the release of the j -th instance (which has no impact on the current schedule), and continue the analysis of the current instance until the DeadlineMissed location is reached.

If instead the deadline miss happens on a different instance of the same task or of another tasks, we update variable c ← c + C and variable p ← 0 to account for the new instance.

Then, it is clear that each task arrival, execution, preemption and completion corresponds to a transition in the task automaton TA. Therefore, a deadline miss for a task always corresponds to the corresponding TA going into the DeadlineMissed location.

Vice versa, if there exists a sequence of transitions in SA that finally reaches the DeadlineMissed location, following the same reasoning as above, we can find a corresponding task arrival and preemption pattern in the scheduling of tasks that causes a deadline miss.

In conclusion, the task set is schedulable if and only if the location Deadline-Missed is not reachable in the system automaton SA. Given a state s in SA, A(s) and R(s) represent the set of active and running tasks in the system respectively. We denote with q 0 the current location of the scheduler automaton, and with q i (1 ≤ i ≤ n) the location of the i-th task automaton. The same notions are also applied to a symbolic state S.

Weak Simulation Relation in SA

In the previous section we proved that analysing the schedulability of a task set is equivalent to performing a reachability analysis of DeadlineMissed locations in SA. Due to the non-deterministic and sporadic behaviour of task arrivals, the exploration of SA's (symbolic) state space will easily produce a "state explosion". To reduce the number of generated states, we propose a weak simulation relation for SA such that, given two states S 1 and S 2 , if S 1 simulates S 2 then S 2 can be eliminated from state space without interfering with the final schedulability analysis result.

Weak simulation in concrete state space

We first discuss the weak simulation relation in concrete state space of SA, then we will extend it for symbolic states. Definition 2. A weak simulation relation in the concrete state space of SA is a pre-order ⊆ space × space such that the following two conditions are satisfied:

1. ∀s 1 , s 2 , s 4 s.t. s 1 s 2 , s 2 → s 4 : there exists s 3 s.t. s 1 ⇒ s 3 and s 3 s 4 ; 2. ∀s 1 , s 2 s.t. s 1 s 2 : ∀i s 2 .q i = DeadlineMissed implies s 1 .q i = DeadlineMissed. If s 1 s 2 , we say that s 1 simulates s 2 . If s 1 s 2 but s 2 s 1 , we write s 1 s 2 .
Roughly speaking, s 1 s 2 means that the scenario in s 1 is worse than in s 2 for tasks to finish execution before their deadlines.

The first condition in Definition 2 says that, given s 1 s 2 and given s 2 that performs a (discrete or time) step to s 4 , there exists a state s 3 reachable from s 1 such that s 3 s 4 . The second condition says that if some task in the simulated state (s 2 ) misses its deadline, so does it in the simulating state (s 1 ). For these two reasons, during state space exploration, we can safely eliminate states that are simulated by others without violating the reachability analysis result. Note that for two states s 1 s 2 and s 2 s 1 , we only need to keep one of them. Now, we present a specific pre-order relation in space(SA) that satisfies the definition of a weak simulation relation, thus it can be used to simplify the state space exploration in SA. Definition 3 (Slack-time pre-order). For automaton SA, the slack-time preorder st ⊆ space × space is defined as follows: ∀s 1 , s 2 , s 1 st s 2 if and only if

∀τ i : s 1 .p i ≥ s 2 .p i ∧ s 1 .c i ≥ s 2 .c i
For an active task, the difference between the time left before its deadline and the remaining computation time is called the slack of the task. When the slack is less than 0, the task is doomed to miss its deadline. Intuitively, a smaller slack corresponds to a more urgent scenario. In a task automaton TA i , the slack can be computed by D i -p i -c i . Given two states s 1 , s 2 such that s 1 st s 2 , there is s 1 .p i ≥ s 2 .p i and s 1 .c i ≥ s 2 .c i . So, an active task's slack in s 1 is no larger than its slack (if in s 2 it is also active) in s 2 .

We now prove that st satisfies the two conditions for a weak simulation relation in Definition 2.

Theorem 2. The pre-order relation st is a weak simulation relation in space(SA).

Proof. To prove that st is indeed a weak simulation relation, we must demonstrate that it satisfies the two properties stated in Definition 2, where the second point trivially holds for st . Therefore, in this proof we address the first point: i.e. given s 1 st s 2 and s 2 → s 4 , we prove that there exists s 3 such that s 1 ⇒ s 3 and s 3 st s 4 . s 2 → s 4 in SA can be a time step or a discrete step. The latter could be further differentiated, depending on whether it is caused by a task arrival or by a task completion. In the following we will analyse these cases one by one.

.p i = s 1 .p i + t ≥ s 2 .p i + t = s 4 .p i . If a task τ i is not in A(s 2 )
, then s 2 .c i = s 4 .c i = 0; certainly, there will be s 3 .c i ≥ s 4 .c i . Otherwise, a key observation for the proof is that ∀i, s 1 .c i ≥ s 2 .c i implies A(s 2 ) ⊆ A(s 1 ); so task τ i in A(s 2 ) also belongs to A(s 1 ). Suppose from s 1 to s 3 (s 2 to s 4 ), the time that τ i stays in location Running is t 1 (t 2 ). Since the scheduler chooses tasks to run according to their fixed priority and A(s 2 ) ⊆ A(s 1 ), t 1 will be no larger than t 2 and s 3 .c i = s 1 .c i -t 1 ≥ s 2 .c i -t 2 = s 4 .c i . So, we proved that s 3 st s 4 .

2. s 2 → s 4 is a discrete step caused by the arrival of a task τ i . For such a step, only variables of the arriving task will change. Because that s 1 .p i ≥ s 2 .p i , there exists also a discrete step from s 1 to s 3 triggered by τ i 's new arrival job. We have s 3 .p i = s 4 .p i = 0 and s 3 .

c i = s 1 .c i + C i ≥ s 2 .c i + C i = s 4 .c i .
So, we proved s 3 st s 4 .

3. s 2 → s 4 is a discrete step caused by the completion of a task τ i . For such a step, only variables of the finishing task will change. Then, s 4 .p i = s 2 .p i ≤ s 1 .p i and s 4 .c i = 0 ≤ s 1 .c i . Remember that in the definition of LHA, there is always a stutter transition from a location to itself. So, there is s 1 → s 1 and s 1 st s 4 .

In conclusion, the pre-order st satisfies point one in Definition 2 also. Thus st is a weak simulation relation in SA.

Weak simulation in symbolic state space

As continuous variables in LHA vary in dense time domain, the weak simulation relation in concrete state space cannot be applied to reachability analysis directly. In this section, we extend the slack time weak simulation relation st to symbolic states.

We remind here the concepts in Section 4 that a symbolic state is defined as a pair S = (l, C), where l is a location and C is a linear constraint (or a convex region). A symbolic state abstracts a (possibly infinite) set of concrete states. We could define the weak simulation relation in symbolic state space (Space) by employing its counterpart in concrete state space (space).

Given symbolic states S 1 and S 2 , we say S 1 simulates S 2 if

∀s 2 ∈ S 2 , ∃s 1 ∈ S 1 s.t. s 1 s 2 (1)
Remember that a symbolic state is a pair (l, C) with a location l and a linear constraint C. The linear constraint C can be represented by a convex region. In the following we use C to denote both a linear constraint and its convex region. In the context of st for concrete state space, there is no need to consider location names. Clearly, given two states S 1 = (l 1 , C 1 ) and

S 2 = (l 2 , C 2 ), if C 1 includes C 2 (denoted as C 1 ⊇ C 2 ), then S 1 simulates S 2 .
In the following, we are going to explore a more general relationship between convex regions that could be used to judge the simulation relation between symbolic states.

Assume we are in a N-dimensional space. Given two valuations ν = (x 1 , x 2 , . . . , x N ) and ν = (y 1 , y 2 , . . . , y N ), we say ν prevails ν , denoted by ν ≥ ν , if for all i it holds x i ≥ y i . We say a valuation ν is prevailed by a convex region C if there exists some valuation ν |= C and ν ≥ ν. Given two convex regions C 1 and

C 2 , C 1 is said to prevail C 2 , denoted as C 1 ≥ C 2 if for all ν |= C 2 , ν is prevailed by C 1 .
We can see that the prevailing relation is transitive. The convex region inclusion is a sufficient (but not necessary) condition for prevailing relation.

Given two valuations ν and ν such that ν prevails ν , if we pair them with location names we can obtain two concrete states s = (l, ν) and s = (l , ν ). The prevailing relation between ν and ν implies that s st s . Similarly, the weak simulation relation between symbolic states can be decided by employing the prevailing relation between two convex regions.

We first extend the slack time pre-order from concrete state space to symbolic state space. Definition 4. For the SA automaton, the slack-time pre-order st ⊆ Space × Space is defined such that ∀S 1 , S 2 , S 1 st S 2 if and only if S 1 .C prevails S 2 .C. Theorem 3. The pre-order st ⊆ Space × Space is a weak simulation relation.

Proof. From the definition of convex region prevailing.

We now need an efficient method for checking if two convex regions are in a relationship of prevailing. To do this, we first define a widening operator ∇.

Given a convex region C, its widening ∇(C) is the convex region that can be obtained as follows: Finally, the prevailing relation between two convex regions, thus the simulation relation between two symbolic states, can be decided by the following lemma. Proof. We first prove that

• Construct linear constraints C in 2×N dimensional space (x 1 , . . . , x N , y 1 , . . . , y N ) such that (y 1 , . . . , y N ) |= C ∧ ∀i, x i ≤ y i x y x + y ≤ 4 x ≥ 1 y ≥ 1
C 1 ≥ C 2 ⇒ ∇(C 1 ) ⊇ ∇(C 2 ). Since C 1 ≥ C 2 ≥ ∇(C 2 )
and ∇(C 1 ) is the largest region prevailed by C 1 , we get ∇(C 1 ) ⊇ ∇(C 2 ).

Then we prove

∇(C 1 ) ⊇ ∇(C 2 ) ⇒ C 1 ≥ C 2 . From ∇(C 1 ) ⊇ ∇(C 2 ), we have C 1 ≥ ∇(C 1 ) ≥ ∇(C 2 ) ≥ C 2 . So, C 1 ≥ C 2 ⇔ ∇(C 1 ) ⊇ ∇(C 2
) and the lemma is proved.

Optimizing the slack-time pre-order relation

We now present another more efficient simulation relation as an extension of the slack-time pre-order relation st in case that tasks have constrained deadlines. Although a similar pre-order can also be defined for arbitrary-deadline sporadic tasks, for simplicity we restrict our extension only for tasks with deadlines less than or equivalent to their respective minimum interarrival times.

Let us first have a look at a simple example. Given two states s 1 and s 2 with s 1 .c i = s 2 .c i = 0, s 1 .p i = T i + 1, s 2 .p i = T i + 10000 and for any j = i, there is s 1 .c j ≥ s 2 .c j and s 1 .p j ≥ s 2 .p j . Following the definition of slack-time pre-order, we would see s 1 s 2 because of s 1 .p i < s 2 .p i . However, for a task with p i ≥ T i that is ready for releasing a new job, the exact valuation of p i does not really matter. In the following, we are going to extend the original slack-time pre-order given this observation.

Definition 5 (Extended slack-time pre-order). For automaton SA, the extended slack-time pre-order st space × space is defined as follows: ∀s 1 , s 2 , s 1 st s 2 if and only if for any τ i

s 1 .p i ≥ s 2 .p i ∧ s 1 .c i ≥ s 2 .c i or s 1 .p i > T i ∧ s 1 .c i ≥ s 2 .c i (C1)
The extension comes from the condition in (C1): s 1 .c i ≥ s 2 .c i is the same as in st ; s 1 .p i > T i says that τ i is eligible to release a new job in s 1 at any time. The extension part is meaningful when s 2 .p i > s 1 .p i > T i and in such a case the new job release of τ i in both s 1 and s 2 can happen at any time regardless of the exact values of s 1 .p i or s 2 .p i .

Theorem 4. The extended pre-order relation st is still a weak simulation relation in space(SA).

Proof. Let us say s 1 st s 2 . 2 .p i ≤ T i , then the original st pre-order relation simply holds. Otherwise, if there is s 1 .c i = 0, then for any job release of τ i from s 2 , τ i can trigger its job release also in s 1 ; given the structure of a Task Automaton and the constraint s 1 .p i > T i , there is no possibility that s 1 .c i > 0 (suppose that s 1 be not in a DeadlineMissed location). In the end, our proof for Theorem 2 still holds for the extended slack-time pre-order. Additionally, we can define the new pre-order for unconstrained-deadline tasks by modifying the condition in (C1) as:

s 1 .p i > D i ∧ s 1 .c i ≥ s 2 .c i .
The reasoning behind this is similar as in proof of Theorem 4 and we are not going into details of it.

As in the case of st , we are going to adapt st for symbolic state space of SA. We first extend the widening operator ∇. We define a new widening operator ∇ such that given a convex polyhedron C, ∇ (C) is constructed as follows.

• For each task τ i , let us say the dimension x i (in C) corresponds to its p i variable. If x i > T i , then we unconstrain x i ; that is, after the operation there is -∞ < x i < +∞.

• Suppose C be the resulted convex polyhedron after the first step; the original widening operator ∇ is then called on C . That is, the final widened convex region is ∇(C ). Now, let us define the extended slack-time pre-order in the symbolic state space Space(SA) and prove its validity. Definition 6. For the SA automaton, the extended slack-time pre-order st ⊆ Space × Space is defined such that ∀S 1 , S 2 , S 1 st S 2 if and only if ∇ (S 1 .C) includes ∇ (S 2 .C).

Theorem 5. The extended pre-order st ⊆ Space × is a weak simulation relation.

Proof. After the ∇ operation, -∞ < p i < +∞ notifies the existence of such tasks that are eligible to release new jobs at any time from then on. As in condition (1), the weak simulation relation between symbolic states can be derived from corresponding weak simulation relation in concrete state space. Given the definition of extended slack-time pre-order st in space(SA), the claim in this theorem is valid.

In the remainder of this work, we implicitly use the notation slack-time pre-order st to denote also the extended one.

Schedulability Analysis in SA

In this section, we formulate the algorithm to explore the state space of SA by using a breadth-first traversal for reachability analysis. The pseudo-code of the Schedulability Analysis algorithm in SA (SA-SA) is shown in Algorithm 1. S 0 is the initial state of SA, R denotes the set of reachable states in SA and F is the set of states representing deadline miss. The Post operation returns the set of states that can be reached in a single transition from states in R. If some state in F is reachable, then the task set encoded in SA is deemed not-schedulable.

Max (R ) is defined as

∀S ∈ Max (R ) : ∃S ∈ R s.t. S st S ∀S, S ∈ Max (R ) : S st S
At line 8 of the algorithm, Max operation eliminates from R the states that are simulated by others. When no new state is produced (line 9), the algorithm terminates and the task set is deemed schedulable. As long as it terminates, the correctness of Algorithm 1 can be proved following the same scheme as in [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF]. We skip the details here.

Moreover, we can also define Max ⊇ (R ) as

∀S ∈ Max ⊇ (R ) : ∃S ∈ R s.t. S .l = S.l ∧ S .C ⊃ S.C ∀S, S ∈ Max ⊇ (R ) : ¬(S .l = S.l ∧ S .C ⊇ S.C)
This is a common and very basic strategy to eliminate unnecessary states during state space exploration. If we replace Max (R ) with Max ⊇ (R ), we obtain a version of SA-SA that does not use the simulation relation, which is a normal reachability analysis procedure. In Section 8.1, we will compare the efficiency of these two versions of SA-SA, with and without simulation relation. As st does not require the equivalence of location names between two states such that s 1 st s 2 and convex region inclusion is a special case of convex region prevailing, there is Max (R ) ⊆ Max ⊇ (R ). We will investigate how much efficiency improvement the schedulability analysis can obtain through simulation relation enhancement.

Unlike previous exact analysis techniques in discrete time domain, SA-SA works in continuous domain, which makes it less sensitive to the values of task parameters. For example, given the task set T 1 = {(C 1 , D 1 , T 1 ), . . . , (C n , D n , T n )}, we enlarge every task parameter by multiplying by 10 and obtain

T 2 = {(C 1 • 10, D 1 • 10, T 1 • 10), . . . , (C n • 10, D n • 10, T n • 10)}.
When we apply SA-SA on T 1 and T 2 , the number of states generated at each step will be exactly the same for the two cases, whereas this may not be true for the method in [START_REF] Baker | Brute-Force Determination of Multiprocessor Schedulability for Sets of Sporadic Hard-Deadline Tasks[END_REF] and [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF].

We have implemented SA-SA in the software FOrmal Real-Time Scheduler (FORTS)( [START_REF] Sun | FOrmal Real-Time Scheduler (FORTS)[END_REF]). end if 14: end while In general the reachability analysis of LHAs is not decidable. However, specific LHAs may be analysable in a finite number of steps. We now prove that the problem under investigation is indeed decidable.

The Decidability Interval

In this section, we formulate the concept of decidability interval, a bounded time interval starting from time 0 (that is the beginning of the schedule) such that a set of sporadic tasks is schedulable if and only if there exists no configuration of release patterns that provokes a deadline miss inside this interval. In other words, we must check the schedules generated by all possible patterns of releases, but each one only inside the decidability interval.

We then propose a formula for computing the decidability interval for G-FP scheduling of sporadic tasks with constrained deadlines, and we show that this interval is indeed quite short. Note that the concept of decidability interval is applicable to scheduling of sporadic tasks and does not rely on the system automaton SA.

In the end, based on the decidability interval obtained G-FP scheduling, we prove the decidability of SA-SA algorithm with respect to constraineddeadline sporadic tasks. In the remainder of this paper, by default we assume that all tasks have constrained deadlines.

System statuses and the dominance relation

We first introduce some preliminary concepts and properties that will be used for defining and deriving the decidability interval.

The task status δ i (t) of a task τ i at time t is defined as a pair δ i (t) = (p i (t), c i (t)).

• p i (t) is the activation variable and records the time passed since τ i 's latest activation.

• c i (t) is the execution variable and represents the unfinished computation of τ i at time t.

Clearly, p i (t) and c i (t) here mimic their respective counterparts (p i variable and c i variable) in the task automaton TA. Please refer to Section 5.1 for a more detailed explanation on these variables. At any time t, there could be infinite possibilities of task statuses δ i (t), subject to different task release patterns.

The system status ∆(t) at time t for the task set T = {τ 1 , . . . , τ n } is defined as the composition of all its tasks' statuses, ∆(t) = (δ 1 (t), . . . , δ n (t)). A system status ∆(t) maps to a concrete state (l, ν) in SA, as all the values of p i (t) and c i (t) for each task: 1) on one hand represent the valuation ν in a state, and 2) on the other hand encode corresponding location information l.

Let T k , with k ≤ n, be the subset containing the first k tasks from T . We define ∆ k (t) as the partial system status of the tasks in T k .

We say that a task τ i is active under the system status ∆(t) if in the corresponding task status δ i (t) there is c i (t) > 0. A ∆(t) denotes the set of active tasks under system status ∆(t). If at time t there is p i (t) = D i and c i (t) > 0, then τ i misses its deadline.

If a task τ i is released at time t, then task statuses for τ i before and after the release are also different. Prior to the release, there is p i (t) ≥ T i and c i (t) = 0; after the release, we have p i (t) = 0 and c i (t) = C i . To make an explicit distinction between the two cases, we use p i (t) and c i (t) to denote the latter. Such a convention also applies for task status δ i (t) and system status ∆ (t). (The initial configuration) We assume ∆(0) is the initial status of the system. Tasks in the system are released asynchronously and we do not know when the first instance of a task is released. Thus, we configure the initial system status as ∀τ i ∈ T p i (0) ≥ 0 and c i (0) = 0 This means that the p i (0) could be an arbitrary non-negative value.

(The dominance relation) Given two task statuses δ i (t) and i (t ), at time t and t respectively, we say δ i (t) dominates δ i (t ), denoted as δ i (t) δ i (t ), if the following conditions hold.

• p i (t) ≥ p i (t ).

• c i (t) ≥ c i (t ).
The relationship can be lifted to system status: given two system statuses ∆(t) and ∆(t ), we say ∆(t) dominates ∆(t ), denoted as ∆(t) ∆(t ), if ∀τ i ∈ T there is δ i (t) δ i (t ). The dominance relation can naturally be applied between partial system statuses.

The dominance relation between system statuses mimics the slack-time preorder relation in system automaton SA but without the underlying LHA model. By understanding this, the following property is straightforward. Lemma 2. Assume there are two system statuses ∆(t) and ∆(t ) at t and t respectively and ∆(t) ∆(t ). Suppose be an arbitrary non-negative value and ∆(t + ) be a system status at (t + ) such that from ∆(t ) to ∆(t + )

• there is no task activation;

• or, there is exactly one task activation at time (t + ).

Then, there exists a system status ∆(t + ) such that ∆(t + ) ∆(t + ).

Proof. We first consider the case that from ∆(t ) to ∆(t + ) there is no new task release. As tasks are activated sporadically, there exists a system status ∆(t + ) such that from ∆(t) to ∆(t + ) there is also no new task arrival. In such a case, all activation variables continuously increase. For any task τ i there is p i (t + ) = p i (t) + and p i (t + ) = p i (t ) + . As ∆(t) ∆(t ), for any task τ i , there is p i (t) ≥ p i (t ) and c i (t) ≥ c i (t ); this further implies that p i (t + ) ≥ p i (t + ). Now, it is the turn to analyze the execution variables. If τ i is not an active task in ∆(t ), as there is no new task arrival, there will be c i (t ) = c i (t + ) = 0; thus, c i (t + ) ≥ c i (t + ) trivially holds. On the other hand, if τ i is indeed an active task in ∆(t ), then it is also an active task in ∆(t). Suppose π and π be the higher-priority interference that τ i suffers from t to (t + ) and from t to (t + ) respectively. Since ∆(t) ∆(t ), A ∆(t) ⊇ A ∆(t ) and for any task τ j ∈ ∆(t ) its unfinished execution in ∆(t) is no smaller than its unfinished execution in ∆(t ) as c i (t) ≥ c i (t ). According to the G-FP scheduling policy, π will not be smaller than π , i.e., π ≥ π . Suppose that c i (t + ) > 0 (otherwise, c i (t + ) ≥ c i (t + ) will trivially hold). There is actually c

i (t + ) = c i (t ) - ( -π ) = c i (t) + π -; on the other side, c i (t + ) = c i (t) + π -≥ c i (t + ).
As a result, we have ∆(t + ) ∆(t + ). Now, let us consider the second case, that is some task τ k is activated task at time (t + ). That is, before τ k is released, there is p k (t + ) ≥ T k ; after τ k is activated, there is p k (t + ) = 0 and c k (t + ) = C k . From t (t) to (t + ) ((t + )), tasks that are different from τ k can analysed in the same way as in the above discussion. Thus, We are going to concentrate on the task τ k .

As ∆(t) ∆(t ), there is p k (t) ≥ p k (t ). From t to (t + ), if τ k does not release a new task instance, there is p k (t + ) = p k (t) + ≥ p k (t ) + ≥ T k . So, at time (t + ), a new instance from τ k is eligible to be released, which will result in p k (t + ) = 0 = p k (t + ) and c k (t + ) = C k = c k (t + ). As a result, ∆ (t + ) ∆ (t + ).

Hence, the lemma is proved.

Then, we generalise the above Lemma 2 as follows.

Theorem 6. Suppose ∆(t) and ∆(t ) are two system statuses such that ∆(t) ∆(t ). Then, for any non-negative value Θ and for any system status ∆(t + Θ), there exists a system status ∆(t + Θ) such that ∆(t + Θ) ∆(t + Θ).

Proof. From ∆(t ) to ∆(t + Θ), the time interval [t , t + Θ] can be divided into a finite (let us say N ) of successive sub-intervals [t , t

+ 1 ], [t + 1 , t + 2 ], . . . , [t + N -1 , t + Θ]
such that in each such sub-interval there is no new task arrival or there is exact one new task arrival and it happens at the end of the sub-interval. Note that in case there are multiple task arrivals at a single time point, we can build multiple sub-intervals with length 0. Then, Lemma 2 can be applied successively to each sub-interval and the Theorem is proved.

The decidability interval for G-FP scheduling

First, we formally define the decidability interval for a set of sporadic tasks under G-FP scheduling as follows.

Definition 7. (Decidability Interval) The decidability interval is defined as a time interval [0, L] such that the schedulability of task set T on m processors under a G-FP scheduler can be decided inside it. That is, the task set T is schedulable if and only if no task will miss its deadline in the interval [0, L].

In order to compute the decidability interval for G-FP scheduling, we need to introduce another concept called dominant interval. Definition 8. (Level-k Dominant Interval) For the task subset T k ⊆ T , its level-k dominant interval is defined as a time interval [0, L k ] such that for any t and for any system status ∆ k (t ), there exists t ∈ [0, L k ] and there exists a system status ∆ k (t) such that ∆ k (t) ∆ k (t ).

A level-k dominant interval must be a decidability interval for T k . Suppose that a task τ i ∈ T k misses its deadline at time t under system status ∆ k (t ), i.e., p i (t ) = D i and c i (t ) > 0. Given the definition of a level-k dominant interval, there exists ∆ k (t) with t ∈ [0, L k ] such that ∆ k (t) ∆ k (t ). That is, p i (t) ≥ p i (t ) and c i (t) ≥ c i (t ); this implies that τ i also misses its deadline at time t. The decidability interval and level-k dominant interval can be bridged through the following two theorems.

Theorem 7. Let [0, L k ] be the level-k dominant interval for T k . Then, [0, L k + k+1 ]
is the decidability interval for T k+1 .

Proof. Task τ k+1 cannot interfere the execution of higher-priority ones from T k , and T k is schedulable if and only if no task from it misses a deadline in the interval [0,

L k ] ⊂ [0, L k + D k+1 ].
As for τ k+1 , we will show that if there is a deadline miss for it after the time point (L k + D k+1 ), there exists also a deadline miss for τ k+1 inside the interval [0,

L k + D k+1 ].
Since L k is the level-k dominant interval, for any time t > L k and for any ∆ k (t ), there exists time t ∈ [0, L k ] and there exists ∆ k (t) such that ∆ k (t) ∆ k (t ). Suppose that task τ k+1 is released at an arbitrary time t > L k , after which there is p k+1 (t ) = 0 and c k+1 (t ) = C k+1 . If we consider the time

t ∈ [0, L k ] with ∆ k (t)
∆ k (t ), as tasks are sporadically activated and at the initial time the activation variable can have any value, then there exists a situation in which p k+1 (t) ≥ T k+1 ; this means the task τ k+1 can also be activated at time t. After τ k+1 is released, there will be also p k+1 (t) = 0 and c k+1 (t) = C k+1 .

Thus, for any release of τ k+1 at any t > L k , there also exists the release for τ k+1 at some time t ∈ [0, L k ] such that after the release ∆ k+1 (t) ∆ k+1 (t ). Suppose that there exists ∆(t + D m+1 ) such that τ k+1 misses its deadline, i.e., p k+1 (t + D k+1 ) = D k+1 and c k+1 (t + D k+1 ) > 0; according to Theorem 6, there also exists ∆ k+1 (t+D k+1 ) with ∆ k+1 (t+D k+1 ) ∆ k+1 (t +D k+1 ), which implies p k+1 (t + D k+1 ) = D k+1 and c k+1 (t + D k+1 ) ≥ c k+1 (t + D k+1 ) > 0, i.e., τ k+1 also misses its deadline at time (t + D k+1 ).

For any release of τ k at time [0, L k ], its absolute deadline is bounded by (L k + D k+1 ). That is, the task τ k+1 is schedulable if and only if there is no deadline miss in the interval [0, L k + D k+1 ]. In conclusion, [0, L k + D k+1 ] is the decidability interval for T k+1 .

The above Theorem 7 demonstrates how to derive a decidability interval from a dominant interval. On the contrary, the next theorem shows that a decidability interval can itself be also a dominant interval as long as the following property is verified.

Theorem 8. The decidability interval [0, L k + D k+1 ] in Theorem 7 is a level- (k + 1) dominant interval if τ k+1 is schedulable.
Proof. We are going to discuss two cases given the task status δ k+1 (t ) of τ k+1 at time t > L k + D k+1 : c k+1 (t ) = 0 or c k+1 (t ) > 0.

(Case 1: c k+1 (t ) = 0) Because that L k is the level-k dominant interval, there exists t ∈ [0, L k ] and ∆ k (t) such that ∆ k (t) ∆ k (t ). As for τ k+1 , given the initial configuration and the sporadic activation behaviour, there exists task status such that p k+1 (t) ≥ p k+1 (t ) and c k+1 (t) = 0 = c k+1 (t ). As a result, ∆(t) k+1 ∆ k+1 (t ).

(Case 2: c k+1 (t ) > 0) For such a system status ∆ k+1 (t ) with c k+1 (t ) > 0, the corresponding τ k+1 is released at time (t -p k+1 (t )), denoted as t 0 . Before the release, there must be p k+1 (t 0 ) ≥ T k+1 ; and after the release, there is p k+1 (t 0 ) = 0 and c k+1 (t 0 ) = C k+1 Then, there exists t 0 ∈ [0, L k ] such that ∆ k (t 0 ) ∆ k (t 0 ) and p k+1 (t 0 ) ≥ p k+1 (t 0 ) and c k+1 (t 0 ) = 0; this implies, by triggering the release of τ k+1 , ∆ k+1 (t 0 ) ∆ k+1 (t 0 ). According to the Theorem 6, after p k+1 (t ) time elapsing, there must exist system status ∆ k+1 (t 0 + p k+1 (t )) ≥ ∆ k+1 (t ). Let us denote with t = t 0 + p k+1 (t ). As τ k+1 is schedulable and c k+1 > 0, there is p k+1 (t ) < D k+1 ; together with

t 0 ∈ [0, L k ], we have t ∈ [0, L k + D k+1 ).
In conclusion, ∀t > L k + D k+1 ∀∆ k+1 (t ), there exists t ∈ [0,

L k + D k+1 ] and ∆ k+1 (t) such that ∆ k+1 (t) ∆ k+1 (t ). That is, [0, L k + D k+1 ] is a level-(k + 1) dominant interval.
Theorem 7 and Theorem 8 provide a recursive way to construct the decidability interval for a given task set T . However, the starting point of such a procedure is still missing. The following theorem fills in the gap.

Lemma 3. The level-m dominant interval is [0, L m ] with L m = max τi∈Tm {C i }.
Proof. Suppose that m = 2 and T 2 = {τ 1 , τ 2 }.

Given any time point t > L 2 , the system status ∆(t ) is in one of the following situations.

• Both τ 1 and τ 2 are active such that 0

≤ p 1 (t ) < C 1 , c 1 (t ) = C 1 -p 1 (t ) and 0 ≤ p 2 (t ) < C 2 , c 2 (t ) = C 2 -p 2 (t ).
• τ 1 is active and τ 2 is not active such that 0 ≤ p 1 (t ) < C 1 , c 1 (t ) = C 1 -p 1 (t ) and p 2 (t ) ≥ 0, c 2 (t ) = 0.

• τ 1 is not active and τ 2 is active such that p 1 (t ) ≥ 0, c 1 (t ) = 0 and 0 ≤ p 2 (t ) < C 2 , c 2 (t ) = C 2 -p 2 (t ).

• Both τ 1 and τ 2 are not active such that p 1 (t ) ≥ 0, c 1 (t ) = 0 and p 2 (t ) ≥ 0, c 2 (t ) = 0.

For any of the cases listed above, it is not difficult to find a time point t ∈ [0, L m ] with a configuration ∆(t) such that ∆(t) ∆(t ). For example, in case both τ 1 and τ 2 are active, the corresponding scenario is depicted in Figure 5, where τ 1 and τ 2 are released at time r 1 and r 2 respectively. At time t , there is c

1 (t ) = C 1 -t + r 1 , p 1 (t ) = t -r 1 , c 2 (t ) = C 2 -t + r 2 , p 2 (t ) = t -r 2 . Note that p 1 (t ) = t -r 1 and p 2 (t ) = t -r 2 are upper bounded by L m = max τi∈Tm {C i }.
Then, let us consider the time t ∈ [0, L m ] such that t = max{t -r 1 , t -r 2 }. There exists the task release of τ 1 at time (t-p 1 (t )) and the task release of τ 2 at (t -p 2 (t )) such that at time t we will see p 1 (t) = p 1 (t ) and p 2 (t) = p 2 (t ). This implies that c

1 (t) = C 1 -p 1 (t) = C 1 -p 1 (t ) = c 1 (t ) and c 1 (t) = C 1 -p 1 (t) = C 1 -p 1 (t ) = c 1 (t ). As a result ∆(t) ∆(t ).
In case there is an active task (let us say τ 1 ) and an inactive task (let us say τ 2 , i.e., p 2 (t ) ≥ 0 and c 2 (t ) = 0) at time t , for the active task the above analysis still can be applied, and the time t ∈ [0, L m ] can be found such that c 1 (t) = c 1 (t ) and p 1 (t) = p 1 (t ). For the inactive task τ 2 , we remind that, at t r1 r2 Figure 5: Both τ 1 and τ 2 are active time 0, c 2 (0) = 0 and 2 (0) can be any non-negative value; when there is no new task arrival, an activation variable will monotonically increase. This means that at time t, there must exist a task status δ 2 (t) for τ 2 with p 2 (t) ≥ p 2 (t ) and c 2 (t) = 0. As a result, ∆(t) ∆(t ).

In the last case, both tasks are inactive. There exists ∆(0) such that ∆(0) ∆(t ). Moreover, if we consider a general m ≥ 2, it is simply a matter of expanding the list for combinations of active and inactive tasks.

Starting from the level-m dominant interval and by repeatedly applying Theorems 7 and 8, we are able to compute the decidability interval for any task set T . Proof. Suppose that T is not schedulable. Let us say τ k is the highest-priority task among all non-schedulable tasks. According to Theorem 7, Theorem 8 and Lemma 3, the decidability interval for T k is [0,

1≤i≤m C i + m<i≤k D i ], which is contained in [0, L]
. This implies that if T is not schedulable, then there exists necessarily a configuration of releases such that a deadline miss happens in the interval [0, L]. Thus, [0, L] is the decidability interval for T .

Given the fact that a task will never have its job run for more than its WCRT, we could refine the formulation of a decidability interval. Lemma 4. For a task set T = {τ 1 , . . . , τ n } with n tasks running on m processors, its decidability interval can be further refined as

[0, L] with L = 1≤i≤m C i + m<i≤n min{R i , D i }.
Proof. By replacing D i with min{R i , D i }, the proofs for Theorem 7 and Theorem 8 still hold. In the end, the new decidability interval length is valid.

Discussion A concept called feasibility interval has been extensively studied in [START_REF] Cucu | Feasibility intervals for fixed-priority real-time scheduling on uniform multiprocessors[END_REF], [START_REF] Cucu | Feasibility intervals for multiprocessor fixedpriority scheduling of arbitrary deadline periodic systems[END_REF], and [START_REF] Cucu-Grosjean | Exact schedulability tests for real-time scheduling of periodic tasks on unrelated multiprocessor platforms[END_REF] for multiprocessor scheduling of periodic tasks. For a set of periodic tasks, its feasibility interval is a finite interval such that if all jobs released within it can meet their deadlines, then the system is schedulable. Such a result from the determinism of tasks' periodic activations and its complexity is sensitive to the tasks' hyperperiod. The hyperperiod for a task set is defined as the least common multiple among all tasks' periods.

On the other hand, the concept of feasibility interval cannot be applied to multiprocessor scheduling of sporadic tasks. In fact, we are not aware of any work for bounding a time interval for exact multiprocessor schedulability analysis of sporadic tasks.

The decidability interval proposed in this work is the first result that proposes a small bounded interval to check the schedulability of a set of sporadic tasks in global multiprocessor scheduling. Moreover, as shown in Theorem 9, the computed decidability interval for a task set could be much shorter than its counterpart for multiprocessor periodic tasks, as it does not rely on the value of hyperperiod.

Decidability for SA-SA algorithm

Now, we are going to answer the decidability question (in the end of Section 6.4) for the SA-SA algorithm. Thanks to the decidability interval computed by Theorem 9, we know that in case of a set of constrained-deadline tasks, it is enough to perform the reachability analysis of DeadlinMissed location in the bounded time interval [0, L].

The reachability analysis of a generic LHA is undecidable ( [START_REF] Alur | Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems[END_REF]), even in bounded time ( [START_REF] Brihaye | On reachability for hybrid automata over bounded time[END_REF]). However, [START_REF] Brihaye | On reachability for hybrid automata over bounded time[END_REF] proposed a subclass of LHA, subject to well defined language restrictions, for which the reachability problem in bounded time is decidable. More specifically, clock variables must all be monotonically increasing or stopped. The class of Stopwatch Timed Automata falls in this category.

Since our model is equivalent to a Stopwatch Timed Automaton (with an appropriate transformation of variables), it can be seen that the reachability problem of SA in bounded time is also decidable.

Theorem 10. The termination of Algorithm 1 (SA-SA) is guaranteed in case of sporadic tasks with constrained deadlines.

Proof. It follows from Theorem 9 in our work and from Theorem 1 in [START_REF] Brihaye | On reachability for hybrid automata over bounded time[END_REF].

Experiments

In this section we evaluate the runtime performance of SA-SA by applying the algorithm to randomly generated schedulability problems. Each task set in the experiment is characterised by a tuple (m, n, U ), where m = 2 is the number of processors, n ∈ {5, 6} is the number of tasks in the task set and U is the total utilisation of the task set (i.e. U = n i=1 Ci Ti ). Given the number of tasks n and the total task set utilisation U , the utilisation of each task is generated according to Randfixedsum algorithm ( [START_REF] Emberson | Techniques for the synthesis of multiprocessor tasksets[END_REF]). Task periods are distributed in After selecting a task period T i , the WCET is computed as C i = T i • U i ; the relative deadline is then randomly sampled from C i to T i , After a task set is randomly generated, priorities are assigned to its tasks by the Deadline Monotonic strategy; that is, a task with shorter deadline is assigned higher priority.

Discussion It is important to underline the advantages of our methodology with respect to the methods proposed in [START_REF] Baker | Brute-Force Determination of Multiprocessor Schedulability for Sets of Sporadic Hard-Deadline Tasks[END_REF], [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF], [START_REF] Bonifaci | Feasibility analysis of sporadic real-time multiprocessor task systems[END_REF]. These methods typically assume task parameters such as WCETs, deadlines and periods to be rather small integers. For example, for testing their method, [START_REF] Geeraerts | Multiprocessor schedulability of arbitrary-deadline sporadic tasks: complexity and antichain algorithm[END_REF] restricted tasks to have period no larger than 8. This is mainly due to the fact that they use discrete time model checking, with integer time values. Thus, these methods are sensitive to the absolute values of task parameters. On the other hand, relying on the formalism of LHA in continuous time domain, we are able to apply exact schedulability test on more general task configurations.

SA-SA algorithm with and without slack-time preorder relation

First, we demonstrate how much the slack-time pre-order ( st ) can benefit the reachability analysis in system automaton SA, by comparing the SA-SA algorithm and the SA-SA Without weak Simulation (SA-SA-WoS). We randomly generate 100 task sets with m = 2, n = 5 and utilisation randomly chosen in [0.5, 2.0]. Then we apply SA-SA and SA-SA-WoS to each task set, and we respectively record state space size for the two to decide the schedulability of every task set. Without the enhancement of slack-time pre-order, SA-SA-WoS faces the danger of going out of memory for some task sets. So, we put an upper threshold of 40000 for the symbolic state space size during the test of a task set by SA-SA-WoS. When the number of generated states exceeds this threshold, we stop the analysis and return with error. Results are reported in Figure 6. Each point in the graphic represents a task set: the x-axis value records the number of states generated by SA-SA-WoS for checking the and the y-axis is the state space size generated by SA-SA. As shown in the figure, by employing the slack-time weak simulation relation st , the size of state space for schedulability check is reduced significantly. In most cases, state space sizes resulted by SA-SA and SA-SA-WoS can differ by an order of magnitude.

Runtime complexity of SA-SA algorithm

In Theorem 10, we have proved the termination of schedulability analysis by SA-SA. In this part, we will evaluate the factors that could affect SA-SA's runtime performance.

All simulations are conducted in a MacBook with 2.5 GHz Intel Core i5 and 8 GB memory. At first, we consider 2 processors (n = 2) and 5 tasks (m = 5). More specifically, we randomly generate a series of task sets with U uniformly distributed within [0. [START_REF] Baker | Brute-Force Determination of Multiprocessor Schedulability for Sets of Sporadic Hard-Deadline Tasks[END_REF][START_REF] Alur | The algorithmic analysis of hybrid systems[END_REF].

By applying SA-SA on these task sets, we record the time consumed and final state space size for each test.

The results are shown in Figure 7a that displays the state space size of all tests by SA-SA. Each point in the figure is a task set, which is further distinguished by being schedulable and not schedulable. The x-axis denotes the utilisation of the task set and the y-axis counts the final state space size by SA-SA to decide its schedulability. Similarly, Figure 7b reports the time cost (in minutes) to decide a task set's schedulability and Figure 7c shows the relation between state space size and time cost.

As we can observe, most tests terminate in a short time with a relatively small state space size. However, with an increase of the task set utilisation, we may experience cases with a rather high runtime cost, with respect to states generated and time spent. This is due to the fact that a higher task set utilisation has a larger chance to result in a longer decidability interval (Lemma 4), within which there could be more complex task execution interleavings, thus complicating SA-SA's reachability analysis.

Furthermore, we run simulations with m = 2 and n = 6. This time, we fix several different utilisation levels for generating task sets. The time spent and state space size on each task set by SA-SA are plotted in Figure 8. Note that we manually stop the procedure when analysis time exceeds 7 hours (upper bound on the maximum time cost we experienced for 5 tasks running on 2 processors), and we use black colors to denote these cases in Figure 8a. In the same figure, we use red colors and blue colors for schedulable and unschedulable task sets respectively. Still, a task set with higher utilisation tends to complicate the analysis by SA-SA, and this is compatible with our observation from m = 2 and n = 5. On other side, we must understand that for the unschedulable task set, SA-SA may terminate without exploring the complete state space, as long as the corresponding deadline miss condition is encountered. Thus, the schedulability check of an unschedulable task set may finish very soon. When it comes to the simulation results, as the total utilisation keeps increasing, there will more unschedulable task sets. In fact, the average runtime performance (time cost and state space size) of SA-SA improves in the high utilisation end of our simulations, as shown in Figure 8b and Figure 8c.

Comparison with state-of-the-art over-approximate approach

In this part, we assess the pessimism of state-of-the-art over-approximate schedulability test for sporadic tasks under G-FP policy. We pick up the task set utilisation U from the set {0.5, 0.6 . . . , 1.5, 1.6} with m = 2 and n = 5. Then, for each U we generate 100 task sets, for which RTA-CE and SA-SA are applied. The number of schedulable tasks discovered by RTA-CE and SA-SA on each utilisation level are recorded respectively. Results are plotted in Figure 9. The x-axis shows the utilisation and the y-axis represents the percentage of schedulable tasks over the total number of randomly sampled tasks (at each utilisation level).

As shown in Figure 9, there is still a considerable number of schedulable task sets that RTA-CE failed to find. Such a gap could be seen as a motivation to further develop more precise approximate schedulability analysis.

Exact schedulability analysis for periodic tasks in G-FP

Finally, we would like to discuss the difference in complexity between exact analysis of periodic tasks and sporadic tasks.

In the case of single processor, for the fixed-priority scheduling, the schedulability analyses of sporadic tasks and synchronous periodic tasks are not really different, as they share the same worst-case scenario. When it comes to multiprocessor, no worst-case scenario has even been found for sporadic or periodic tasks under G-FP. Therefore, to perform an exact analysis we need to analyse all possible task activations and interleavings, for both sporadic and periodic tasks.

As we proved in Theorem 9, the exact analysis of sporadic tasks can be done in a decidability interval, which is relatively small. Therefore, the complexity of analysing sporadic tasks comes from the non-deterministic which produce many different arrival patterns that need to be analysed. As for periodic tasks, they have deterministic activation patterns, and the complexity of an exact analysis is affected by the length of the feasibility interval, which is directly related to the hyperperiod of the tasks.

In this section, we refer to [START_REF] Guan | Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking[END_REF] and [START_REF] Guan | Schedulability analysis of global fixed-priority or EDF multiprocessor scheduling with symbolic model-checking[END_REF] for the exact test for periodic tasks. Both works adopt the discrete approach to model the schedule of a set of periodic tasks running on multiprocessor. Even though [START_REF] Guan | Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking[END_REF] builds the model by Timed Automata, the continuous time is discretised by using a global clock. Thus, they restrict the absolute values of task parameters to small integers. Actually, in both cases the authors choose task periods in a range [START_REF] Bertogna | Response-time analysis for globally scheduled symmetric multiprocessor platforms[END_REF][START_REF] Guan | Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking[END_REF] for their experiments.

In principle, the analysis scheme for periodic tasks considers all possible combinations of tasks' initial offsets; for an arbitrary combination of initial offsets, tasks' periodic activations are fixed, the system is simulated and any deadline miss is checked.

In the following, we replicate the experiment in [START_REF] Guan | Schedulability analysis of global fixed-priority or EDF multiprocessor scheduling with symbolic model-checking[END_REF], where there are 8 tasks running on 4 processors. Our goal here is not to solve the exact schedulability analysis of periodic tasks, but rather to demonstrate the different runtime complexity. Therefore, we consider all offsets to be equal to 0, so all tasks arrive at the same time.

We randomly generate 1000 periodic task sets. The system automaton for schedulability check for periodic tasks can be generated similarly as the SA for sporadic tasks: in Figure 2, the guard on the transition from Idle to Waiting is set to p = T . We also restrict ourselves to tasks with constrained deadline (i.e. Figure 10: The exact analysis for periodic tasks D ≤ T ), so we remove all guards and actions from the transitions from Waiting to itself, and from Running to itself. Finally, we do not use our simulation relation, because it is only valid for sporadic tasks and cannot be easily extended to periodic tasks.

In the end, we use FORTS to check the schedulability of each task set and records the time cost for deciding the schedulability. Results are reported in Figure 10. The x-axis denotes the length of the hyperperiod of a task set and the y-axis denotes the size of the state space when schedulability check is completed for the task set. As we anticipated, the number of states to explore increases with the length of hyperperiod. The maximum time we experienced for deciding a task set's schedulability is less than 3 minutes. It follows that, deciding the schedulability of a set of periodic tasks is in average easier than checking the schedulability of a set of sporadic tasks.

Conclusions and future work

In this paper, we formally model the exact G-FP scheduling on a multiprocessor platform; we propose a weak simulation relation for reducing the complexity of state space exploration. Then, we formulate SA-SA algorithm for the exact schedulability test. Even though the reachability problem in LHA is undecidable, we prove the correctness and termination condition for SA-SA. Compared to previous works on exact analysis, our methodology allows more complex task sets: we are able to analyse tasks with arbitrary values of parameters. On the other hand, our simulation relation work can be regarded as a general approach to mitigate the complexity brought by sporadic events when modeling real-time systems with a formalism like Stopwatch Timed Automata.

However, as task set size increases, the complexity of exact analysis is still too high even with our approach. We are working on other ways of reducing the complexity: first, we would like to use a different representation for the symbolic states (e.g. Octagons ( [START_REF] Miné | The octagon abstract domain[END_REF]) or Difference Bound Matrices ( [START_REF] Miné | A New Numerical Abstract Domain Based on Difference-Bound Matrices[END_REF])), which requires an approximate analysis similar to the ones used for Stopwatch Timed Automata and Time Petri Nets ( [START_REF] Bucci | Timed state space analysis of real-time preemptive systems[END_REF]). Second, we are investigating the possibility to enhance and extend our simulation relation, so to further reduce the state space.

Furthermore, although exact critical instants for G-FP scheduling are not known, [30] proved a class of release patterns that could lead to worst-case response time. By exploring the advanced study in scheduling theory, we may achieve simpler models or even faster state space analysis methods.

Finally, we proved that the schedulability analysis of a sporadic task set could be done in bounded time. To our knowledge, this is the first paper to demonstrate the decidability of the problem and to formulate such an upper bound. It will be interesting to see if we can apply this result to further enhance the approximate schedulability analysis methods.

Figure 1 :

 1 Figure 1: Example of schedule of sporadic tasks (a) jobs arrive as soon as possible (b) second job of τ 1 is delayed.

Figure 2 :

 2 Figure 2: Task Automaton

Figure 3 :

 3 Figure 3: Scheduler for 3 tasks on 2 processors

Figure 4 :

 4 Figure 4: A convex region C and its windening ∇(C)

Lemma 1 .

 1 Given two convex regions C 1 and C 2 , C 1 ≥ C 2 if and only if ∇(C 1 ) includes ∇(C 2 ).

Algorithm 1 :

 1 Schedulability Analysis in SA (SA-SA) 1: R ← {S 0 } 2: while true do 3:P ← Post(R) 4: if P ∩ F = ∅ then 5:

Theorem 9 .

 9 For a task set T = {τ 1 , . . . , τ n } with n tasks running on m processors, its decidability interval is [0, L] with L = 1≤i≤m C i + m<i≤n D i .

Figure 6 :

 6 Figure 6: SA-SA v.s. SA-SA-WoS

Figure 9 :

 9 Figure 9: Comparison between RTA-CE and SA-SA

  1. s 2 → s 4 is a time step with elapsed time t: s 2 = ⇒ s 3 with the same t as accumulated time; and let us assume that there is no new task arrival during this time interval. For any task τ i , s 3

		t -→ s 4 . Let us consider a
	timed step sequence s 1	t

  The analytic test we use is the Response Time Analysis with Carry-in Enumeration (RTA-CE) proposed in[30]. Although being the most accurate over-approximate schedulability test for G-FP scheduling problem to date, RTA-CE is still pessimistic. That is, RTA-CE may judge a schedulable task set as not-schedulable. It is interesting and meaningful to see how much gap there is between the approximate result of RTA-CE and the exact result of SA-SA.

A committed location is a location where time is not allowed to elapse; more details can be found in[START_REF] Bengtsson | Timed Automata: Semantics, Algorithms and Tools[END_REF].