Bound on Higher-or-Equal Priority Workload under ELF Scheduling is Valid

In this file, we prove that the upper bound on interference incurred by a job from jobs with higher-or-equal priority that come from other tasks under ELF scheduling (defined in prosa.analysis.definitions.workload.elf_athep_bound) is valid.

Consider any type of tasks, each characterized by a WCET task_cost, a relative deadline task_deadline, an arrival curve max_arrivals, and a relative priority point, ...

... and any type of jobs associated with these tasks, where each job has a task job_task, a cost job_cost, and an arrival time job_arrival.

Consider any kind of processor model.

Consider any valid arrival sequence arr_seq ...

... with valid job costs.

We consider an arbitrary task set ts ...

... and assume that all jobs stem from tasks in this task set.

We assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is an arrival bound of tsk.

Let tsk be any task to be analyzed.

Consider any schedule.

Consider any fixed-priority scheduling policy.

Before we prove the main result, we establish some auxiliary lemmas.

Consider an arbitrary job j of tsk.

Consider the busy interval [t1, t2) of job j.

Let's define A as a relative arrival time of job j (with respect to time t1).

Consider an arbitrary shift delta inside the busy interval ...

... and the set of all arrivals between t1 and t1 + delta.

Now, we define a predicate to identify jobs from a given task that have priority higher than or equal to j.

Consider an arbitrary task tsk_o ≠ tsk from ts.

And assume that ep_task_interfering_interval_length tsk tsk_o A is bounded by delta.

Then we prove that the total workload of jobs with higher-or-equal priority from task tsk_o over the interval [t1, t1 + Δ] is bounded by the workload over the interval [t1, t1 + ep_task_interfering_interval_length tsk tsk_o A]. The intuition behind this inequality is that jobs that arrive after time instant t1 + ep_task_interfering_interval_length tsk tsk_o A have lower priority than job j.

Consider the jobs that have priority higher than or equal to j released by any task in the same priority band as tsk (excluding tsk). We prove that the workload of these jobs is at most bound_on_ep_task_workload.

Next, consider a workload of all jobs with priority higher than j released by any task in higher priority band. we establish that this workload is at most bound_on_hp_task_workload.

To help with further analysis, we establish a useful lemma on partitioning higher-or-equal priority workloads.

Finally, we establish that the workload of jobs with priority higher than or equal to j is at most bound_on_athep_workload.

The validity of bound_on_athep_workload then easily follows from lemma sum_of_workloads_is_at_most_bound_on_total_hep_workload.