# Library prosa.results.rta.ovh.edf.limited_preemptive

Require Export prosa.model.job.properties.
Require Export prosa.model.composite.valid_task_arrival_sequence.
Require Export prosa.analysis.facts.readiness.sequential.
Require Export prosa.analysis.facts.model.overheads.schedule.
Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
Require Export prosa.analysis.abstract.restricted_supply.task_intra_interference_bound.
Require Export prosa.analysis.abstract.restricted_supply.bounded_bi.edf.
Require Export prosa.analysis.abstract.restricted_supply.search_space.edf.
Require Export prosa.analysis.facts.model.task_cost.
Require Export prosa.analysis.facts.priority.edf.
Require Export prosa.analysis.facts.blocking_bound.edf.
Require Export prosa.analysis.facts.workload.edf_athep_bound.
Require Export prosa.analysis.facts.model.overheads.sbf.jlfp.

# RTA for EDF Scheduling with Fixed Preemption Points on Uniprocessors with Overheads

In the following, we derive a response-time analysis for EDF schedulers, assuming a workload of sporadic real-time tasks with fixed preemption points, characterized by arbitrary arrival curves, executing upon a uniprocessor subject to scheduling overheads. To this end, we instantiate the sequential variant of abstract Restricted-Supply Analysis (aRSA) as provided in the prosa.analysis.abstract.restricted_supply module.
Section RTAforLimitedPreemptiveEDFModelwithArrivalCurves.

## Defining the System Model

Before any formal claims can be stated, an initial setup is needed to define the system model under consideration. To this end, we next introduce and define the following notions using Prosa's standard definitions and behavioral semantics:

- the processor model,
- tasks, jobs, and their parameters,
- the task set and the task under analysis,
- the sequence of job arrivals,
- the absence of self-suspensions,
- an arbitrary schedule of the task set, and finally,
- an upper bound on overhead-induced delays.

### Processor Model

Consider a unit-speed uniprocessor subject to scheduling overheads.
#[local] Existing Instance overheads.processor_state.

### Tasks and Jobs

Consider tasks characterized by a WCET task_cost, relative deadline task_deadline, an arrival curve max_arrivals, and a list of preemption points task_preemption_points, ...
Context {Task : TaskType} `{TaskCost Task} `{TaskDeadline Task}
`{MaxArrivals Task} `{TaskPreemptionPoints Task}.
... and their associated jobs, where each job has a corresponding task job_task, an execution time job_cost, an arrival time job_arrival, and a list of job's preemption points job_preemptive_points.
Context {Job : JobType} `{JobTask Job Task} `{JobCost Job} `{JobArrival Job}
`{JobPreemptionPoints Job}.
We assume that jobs are limited-preemptive.
#[local] Existing Instance limited_preemptive_job_model.

### The Task Set and the Task Under Analysis

Consider an arbitrary task set ts, and ...
Variable ts : seq Task.
... let tsk be any task in ts that is to be analyzed.
Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

### The Job Arrival Sequence

Allow for any possible arrival sequence arr_seq consistent with the parameters of the task set ts. That is, arr_seq is a valid arrival sequence in which each job's cost is upper-bounded by its task's WCET, every job stems from a task in ts, and the number of arrivals respects each task's max_arrivals bound.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_task_arrival_sequence : valid_task_arrival_sequence ts arr_seq.
We assume a model with fixed preemption points. I.e., each task is divided into a number of non-preemptive segments by inserting statically predefined preemption points.
Hypothesis H_valid_model_with_fixed_preemption_points :
valid_fixed_preemption_points_model arr_seq ts.
Additionally, we assume that all jobs in arr_seq have positive execution costs. This requirement is not fundamental to the analysis approach itself but reflects an artifact of the current proof structure specific to upper bounds on the total duration of overheads.
Hypothesis H_arrivals_have_positive_job_costs :
arrivals_have_positive_job_costs arr_seq.

### Absence of Self-Suspensions

We assume the classic (i.e., Liu & Layland) model of readiness without jitter or self-suspensions, wherein pending jobs are always ready.
Context {RM : JobReady Job (overheads.processor_state Job)}.
Hypothesis H_basic_readiness : basic_readiness RM.

### The Schedule

Consider a work-conserving, valid uniprocessor schedule with limited preemptions and explicit overheads that corresponds to the given arrival sequence arr_seq (and hence the given task set ts).
Variable sched : schedule (overheads.processor_state Job).
Hypothesis H_valid_schedule : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_schedule_with_limited_preemptions :
schedule_respects_preemption_model arr_seq sched.
We assume that the schedule respects the EDF policy.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_policy_is_EDF : policy_is_EDF JLFP.
Hypothesis H_respects_policy :
respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
Furthermore, we require that the schedule has no superfluous preemptions; that is, preemptions occur only when strictly required by the scheduling policy (specifically, a job is never preempted by another job of equal priority).
Hypothesis H_no_superfluous_preemptions : no_superfluous_preemptions sched.

### Bounding the Total Overhead Duration

We assume that the scheduling overheads encountered in the schedule sched are bounded by the following upper bounds:

- the maximum dispatch overhead is bounded by DB,
- the maximum context-switch overhead is bounded by CSB, and
- the maximum cache-related preemption delay is bounded by CRPDB.

Variable DB CSB CRPDB : duration.
Hypothesis H_valid_overheads_model : overhead_resource_model sched DB CSB CRPDB.
To conservatively account for the maximum cumulative delay that task tsk may experience due to scheduling overheads, we introduce an overhead bound. This term upper-bounds the maximum cumulative duration during which processor cycles are "lost" to dispatch, context-switch, and preemption-related delays in a given interval.
For EDF scheduling, we use a generic JLFP bound, where the bound in an interval of length Δ is determined by the total number of arrivals in the system. In this case, up to n such arrivals can lead to at most 1 + 2n segments without a schedule change, each potentially incurring dispatch, context-switch, and preemption-related overhead.
Let overhead_bound Δ :=
(DB + CSB + CRPDB) × (1 + 2 × \sum_(tsk_o <- ts) max_arrivals tsk_o Δ).

## Maximum Length of a Busy Interval

In order to apply aRSA, we require a bound on the maximum busy-window length. To this end, let L be any positive solution of the busy-interval "recurrence" (i.e., inequality) overhead_bound L + total_request_bound_function ts L ≤ L, as defined below.
As the lemma busy_intervals_are_bounded_rs_edf shows, under EDF scheduling, this condition is sufficient to guarantee that the maximum busy-window length is at most L, i.e., the length of any busy interval is bounded by L.
Definition busy_window_recurrence_solution (L : duration) :=
L > 0
∧ L ≥ overhead_bound L + total_request_bound_function ts L.

## Response-Time Bound

Having established all necessary preliminaries, it is finally time to state the claimed response-time bound R.
A value R is a response-time bound for task tsk if, for any given offset A in the search space (w.r.t. the busy-window bound L), the response-time bound "recurrence" (i.e., inequality) has a solution F not exceeding R.
Definition rta_recurrence_solution L R :=
∀ (A : duration),
is_in_search_space ts tsk L A →
∃ (F : duration),
F ≥ overhead_bound F
+ blocking_bound ts tsk A
+ (task_request_bound_function tsk (A + ε) - (task_last_nonpr_segment tsk - ε))
+ bound_on_athep_workload ts tsk A F
∧ A + R ≥ F + (overhead_bound (A + R) - overhead_bound F)
+ (task_last_nonpr_segment tsk - ε).
Finally, using the sequential variant of abstract restricted-supply analysis, we establish that, given a bound on the maximum busy-window length L, any such R is indeed a sound response-time bound for task tsk under EDF scheduling with limited preemptions on a unit-speed uniprocessor subject to scheduling overheads.
Theorem uniprocessor_response_time_bound_limited_edf :
∀ (L : duration),
busy_window_recurrence_solution L →
∀ (R : duration),
rta_recurrence_solution L R →
task_response_time_bound arr_seq sched tsk R.
End RTAforLimitedPreemptiveEDFModelwithArrivalCurves.