Throughout this file, we assume ideal uni-processor schedules.

JLFP instantiation of Interference and Interfering Workload for ideal uni-processor.

In this module we instantiate functions Interference and Interfering Workload for ideal uni-processor schedulers with an arbitrary JLFP-policy that satisfies the sequential-tasks hypothesis. We also prove equivalence of Interference and Interfering Workload to the more conventional notions of service or workload.

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Consider any valid arrival sequence with consistent arrivals ...

... and any ideal uni-processor schedule of this arrival sequence ...

... where jobs do not execute before their arrival or after completion.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.

We also assume that the policy respects sequential tasks, meaning that later-arrived jobs of a task don't have higher priority than earlier-arrived jobs of the same task.

Let tsk be any task.

Interference and Interfering Workload

In the following, we introduce definitions of interference, interfering workload and a function that bounds cumulative interference.

Instantiation of Interference

Before we define the notion of interference, we need to recall the definition of priority inversion. We say that job j is incurring a priority inversion at time t if there exists a job with lower priority that executes at time t. In order to simplify things, we ignore the fact that according to this definition a job can incur priority inversion even before its release (or after completion). All such (potentially bad) cases do not cause problems, as each job is analyzed only within the corresponding busy interval where the priority inversion behaves in the expected way. We say that job j incurs interference at time t iff it cannot execute due to a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion.

Instantiation of Interfering Workload

The interfering workload, in turn, is defined as the sum of the priority inversion predicate and interfering workload of jobs with higher or equal priority.

Equivalences

In this section we prove useful equivalences between the definitions obtained by instantiation of definitions from the Abstract RTA module (interference and interfering workload) and definitions corresponding to the conventional concepts. Instantiated functions of interference and interfering workload usually do not have any useful lemmas about them. However, it is possible to prove their equivalence to the more conventional notions like service or workload. Next, we prove the equivalence between the instantiations and conventional notions as well as a few useful rewrite rules.

In the following subsection, we prove properties of the introduced functions under the assumption that the schedule is idle.

Consider a time instant t ...

... and assume that the schedule is idle at t.

We prove that in this case: ... ... there is no interference, ...

... as well as no interference for tsk.

Next, we prove properties of the introduced functions under the assumption that the scheduler is not idle.

Consider a job j of task tsk. In this subsection, job j is deemed to be the main job with respect to which the functions are computed.

Consider a time instant t.

In the next subsection, we consider a case when a job j' from the same task (as job j) is scheduled.

Consider a job j' that comes from task tsk and is scheduled at time instant t.

Similarly, there is no task interference, since in order to incur the task interference, a job from a distinct task must be scheduled.

In the next subsection, we consider a case when a job j' from a task other than j's task is scheduled.

Consider a job j' that does _not comes from task tsk and is scheduled at time instant t.

Hence, if we assume that j' has higher-or-equal priority, ...

Moreover, in this case, task tsk also incurs interference.

We prove that we can split cumulative interference into two parts: (1) cumulative priority inversion and (2) cumulative interference from jobs with higher or equal priority.

Similarly, we prove that we can split cumulative interfering workload into two parts: (1) cumulative priority inversion and (2) cumulative interfering workload from jobs with higher or equal priority.

Let j be any job of task tsk. Then the cumulative task interference received by job j is bounded to the sum of the cumulative priority inversion of job j and the cumulative interference incurred by job j due to higher-or-equal priority jobs from other tasks.

In this section, we prove that the (abstract) cumulative interfering workload is equivalent to the conventional workload, i.e., the one defined with concrete schedule parameters.

Let [t1,t2) be any time interval.

Consider any job j of tsk.

Then for any job j, the cumulative interfering workload is equal to the conventional workload.

In this section we prove that the abstract definition of busy interval is equivalent to the conventional, concrete definition of busy interval for JLFP scheduling.

In order to avoid confusion, we denote the notion of a quiet time in the classical sense as quiet_time_cl, and the notion of quiet time in the abstract sense as quiet_time_ab.

Same for the two notions of a busy interval prefix ...

... and the two notions of a busy interval.

Consider any job j of tsk.

To show the equivalence of the notions of busy intervals, we first show that the notions of quiet time are also equivalent. First, we show that the classical notion of quiet time implies the abstract notion of quiet time.

And vice versa, the abstract notion of quiet time implies the classical notion of quiet time.

The equivalence trivially follows from the lemmas above.

Based on that, we prove that the concept of busy interval prefix obtained by instantiating the abstract definition of busy interval prefix coincides with the conventional definition of busy interval prefix.

Similarly, we prove that the concept of busy interval obtained by instantiating the abstract definition of busy interval coincides with the conventional definition of busy interval.

For the sake of proof automation, we note the frequently needed special case of an abstract busy window implying the existence of a classic quiet time.

Also for automation, we note a similar fact about classic busy-window prefixes.

In this section we prove some properties about the interference and interfering workload as defined in this file.

Consider work-bearing readiness.

Assume that the schedule is valid and work-conserving.

Note that we differentiate between abstract and classical notions of work-conserving schedule.

We assume that the schedule is a work-conserving schedule in the classical sense, and later prove that the hypothesis about abstract work-conservation also holds.

Assume the scheduling policy under consideration is reflexive.

In this section, we prove the correctness of interference inside the busy interval, i.e., we prove that if interference for a job is false then the job is scheduled and vice versa. This property is referred to as abstract work conservation.

Consider a job j that is in the arrival sequence and has a positive job cost.

Let the busy interval of the job be [t1,t2).

Consider a time t inside the busy interval of the job.

First, we prove that if interference is false at a time t then the job is scheduled.

Conversely, if the job is scheduled at t then interference is false.

Using the above two lemmas, we can prove that abstract work conservation always holds for these instantiations of I and IW.

Next, in order to prove that these definitions of I and IW are consistent with sequential tasks, we need to assume that the policy under consideration respects sequential tasks.

We prove that these definitions of I and IW are consistent with sequential tasks.

Since interfering and interfering workload are sufficient to define the busy window, next, we reason about the bound on the length of the busy window.

Consider an arrival curve.

Consider a set of tasks that respects the arrival curve.

Assume that all jobs come from this task set.

Consider a constant L such that...

... L is greater than 0, and...

L is the fixed point of the following equation.

Assume all jobs have a valid job cost.

Then, we prove that L is a bound on the length of the busy window.

To preserve modularity and hide the implementation details of a technical definition presented in this file, we make the definition opaque. This way, we ensure that the system will treat each of these definitions as a single entity.

We add some facts into the "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically where needed.