Library prosa.analysis.abstract.ideal.iw_instantiation

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 ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

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.
Let tsk be any task.
  Variable tsk : Task.

Assume we have sequential tasks, i.e., jobs of the same task execute in the order of their arrival.
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.

Interference and Interfering Workload

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

Instantiation of Interference

We say that job j is incurring interference from another job with higher-or-equal priority at time t if there exists a job jhp (different from j) with a higher-or-equal priority that executes at time t.
  Definition another_hep_job_interference (j : Job) (t : instant) :=
     jhp,
      (jhp \in arrivals_up_to arr_seq t)
       another_hep_job jhp j
       receives_service_at sched jhp t.

In order to use the above definition in aRTA, we need to define its computational version.
Notice that the computational and propositional definitions are equivalent; ...
... for convenience, we prove that their negated counterparts are equivalent as well.
Similarly, we say that job j is incurring interference from a job with higher-or-equal priority of another task at time t if there exists a job jhp (of a different task) with higher-or-equal priority that executes at time t.
In order to use the above definition in aRTA, we need to define its computational version.
We also show that the computational and propositional definitions are equivalent.
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.
  #[local,program] Instance ideal_jlfp_interference : Interference Job :=
    {
      interference (j : Job) (t : instant) :=
        priority_inversion_dec arr_seq sched j t || another_hep_job_interference_dec j t
    }.

Instantiation of Interfering Workload

Now, we define the notion of cumulative interfering workload, called other_hep_jobs_interfering_workload, that says how many units of workload are generated by jobs with higher-or-equal priority released at time t.
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.
  #[local,program] Instance ideal_jlfp_interfering_workload : InterferingWorkload Job :=
    {
      interfering_workload (j : Job) (t : instant) :=
        priority_inversion_dec arr_seq sched j t + other_hep_jobs_interfering_workload j t
    }.

Auxiliary definitions

For each of the concepts defined above, we introduce a corresponding cumulative function:
(a) cumulative interference from other jobs with higher-or-equal priority ...
... (b) and cumulative interference from jobs with higher or equal priority from other tasks, ...
... and (c) cumulative workload from jobs with higher or equal priority.
Instantiated functions usually do not come with any useful lemmas about them. In order to reuse existing lemmas, we need to prove equivalence of the instantiated functions to some conventional notions. The instantiations given in this file are equivalent to service and workload. Further, we prove these equivalences formally.
Before we present the formal proofs of the equivalences, we recall the notion of workload of higher or equal priority jobs.
... and service of all other jobs with higher or equal priority.
Similarly, we recall notions of service of higher or equal priority jobs from other tasks.

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.
As it was mentioned previously, 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.
  Section Equivalences.

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

Consider a time instant t ...
      Variable t : instant.

... and assume that the schedule is idle at t.
      Hypothesis H_idle : is_idle sched t.

We prove that in this case: ...
... there is no interference from higher-or-equal priority jobs, ...
      Lemma idle_implies_no_hep_job_interference :
         j, ¬ another_hep_job_interference j t.

... there is no interference from higher-or-equal priority jobs from another task, ...
... there is no interference, ...
      Lemma idle_implies_no_interference :
         j, ¬ interference j t.

... as well as no interference for tsk. Recall that the additional argument upper_bound is an artificial horizon needed needed to make task interference function constructive. For more details, refer to the original description of the function.
Next, we prove properties of the introduced functions under the assumption that the scheduler is not idle.
    Section ScheduledJob.

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.
      Variable j : Job.
      Hypothesis H_j_tsk : job_of_task tsk j.

Consider a time instant t.
      Variable t : instant.

First, consider a case when some jobs is scheduled at time t.
      Section SomeJobIsScheduled.

Consider a job j' (not necessarily distinct from job j) that is scheduled at time t.
        Variable j' : Job.
        Hypothesis H_sched : scheduled_at sched j' t.

Under the stated assumptions, we show that the interference from another higher-or-equal priority job is equivalent to the relation another_hep_job.
        Lemma interference_ahep_equiv_ahep :
          another_hep_job_interference j t another_hep_job j' j.

      End SomeJobIsScheduled.

Next, consider a case when j itself is scheduled at t.
      Section JIsScheduled.

Assume that j is scheduled at time t.
        Hypothesis H_j_sched : scheduled_at sched j t.

Then there is no interference from higher-or-equal priority jobs at time t.
        Lemma interference_ahep_job_eq_false :
          ¬ another_hep_job_interference j t.

      End JIsScheduled.

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

Consider a job j' that comes from task tsk and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_tsk : job_of_task tsk j'.
        Hypothesis H_j'_sched : scheduled_at sched j' t.

Then we show that interference from higher-or-equal priority jobs from another task is false.
        Lemma interference_athep_eq_false :
          ¬ another_task_hep_job_interference j t.

Similarly, there is no task interference, since in order to incur the task interference, a job from a distinct task must be scheduled.
        Lemma task_interference_eq_false :
           upper_bound, ¬ task_interference_received_before arr_seq sched tsk upper_bound t.

      End FromSameTask.

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

Consider a job j' that does _not comes from task tsk and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.
        Hypothesis H_j'_sched : scheduled_at sched j' t.

We prove that then j incurs higher-or-equal priority interference from another task iff j' has higher-or-equal priority than j.
Hence, if we assume that j' has higher-or-equal priority, ...
        Hypothesis H_j'_hep : hep_job j' j.

... we are able to show that j incurs higher-or-equal priority interference from another task.
        Lemma sched_athep_implies_interference_athep :
          another_task_hep_job_interference j t.

Moreover, in this case, task tsk also incurs interference.
        Lemma sched_athep_implies_task_interference :
           upper_bound,
            (j \in arrivals_between arr_seq 0 upper_bound)
            task_interference_received_before arr_seq sched tsk upper_bound t.

      End FromDifferentTask.

In the last subsection, we consider a case when the scheduled job j' has lower priority than job j.
      Section LowerPriority.

Consider a job j' that has lower priority than job j and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_sched : scheduled_at sched j' t.
        Hypothesis H_j'_lp : ~~ hep_job j' j.

        Lemma sched_alp_implies_interference_ahep_false :
          ¬ another_hep_job_interference j t.

      End LowerPriority.

    End ScheduledJob.

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.
    Lemma cumulative_interference_split :
       j t1 t2,
        cumulative_interference j t1 t2
        = cumulative_priority_inversion arr_seq sched j t1 t2
          + cumulative_another_hep_job_interference j t1 t2.

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.
Before we prove a lemma about the task's interference split, we show that any job j of task tsk experiences either priority inversion or task interference if two properties are satisfied: (1) task tsk is not scheduled at a time instant t and (2) there is a job jo that experiences interference at a time t.
Let j be any job of task tsk, and let upper_bound be any time instant after job j's arrival. Then for any time interval lying before upper_bound, the cumulative interference received by tsk is equal to the sum of the cumulative priority inversion of job j and the cumulative interference incurred by task tsk due to 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.
      Variables t1 t2 : instant.

Consider any job j of tsk.
      Variable j : Job.
      Hypothesis H_j_arrives : arrives_in arr_seq j.
      Hypothesis H_job_of_tsk : job_of_task tsk j.

Then for any job j, the cumulative interfering workload is equal to the conventional workload.
In this section, we prove that the (abstract) cumulative interference of jobs with higher or equal priority is equal to total service of jobs with higher or equal priority.
Consider any job j of tsk.
      Variable j : Job.
      Hypothesis H_j_arrives : arrives_in arr_seq j.
      Hypothesis H_job_of_tsk : job_of_task tsk j.

We consider an arbitrary time interval [t1, t) that starts with a quiet time.
      Variable t1 t : instant.
      Hypothesis H_quiet_time : busy_interval.quiet_time arr_seq sched j t1.

Then for job j, the (abstract) instantiated function of interference is equal to the total service of jobs with higher or equal priority.
The same applies to the alternative definition of interference.
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.
    Section BusyIntervalEquivalence.

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.
      Variable j : Job.
      Hypothesis H_j_arrives : arrives_in arr_seq j.
      Hypothesis H_job_cost_positive : job_cost_positive j.

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.
      Lemma quiet_time_cl_implies_quiet_time_ab :
         t, quiet_time_cl j t quiet_time_ab j t.

And vice versa, the abstract notion of quiet time implies the classical notion of quiet time.
      Lemma quiet_time_ab_implies_quiet_time_cl :
         t, quiet_time_ab j t quiet_time_cl j t.

The equivalence trivially follows from the lemmas above.
      Corollary instantiated_quiet_time_equivalent_quiet_time :
         t,
          quiet_time_cl j t quiet_time_ab j t.

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.
In this section we prove some properties about the interference and interfering workload as defined in this file.
  Section I_IW_correctness.

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.
    Hypothesis H_work_conserving : work_conserving_cl.

Assume the scheduling policy under consideration is reflexive.
    Hypothesis policy_reflexive : reflexive_priorities.

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.

    Section Abstract_Work_Conservation.

Consider a job j that is in the arrival sequence and has a positive job cost.
      Variable j : Job.
      Hypothesis H_arrives : arrives_in arr_seq j.
      Hypothesis H_job_cost_positive : 0 < job_cost j.

Let the busy interval of the job be [t1,t2).
      Variable t1 t2 : instant.
      Hypothesis H_busy_interval_prefix : busy_interval_prefix_ab j t1 t2.

Consider a time t inside the busy interval of the job.
      Variable t : instant.
      Hypothesis H_t_in_busy_interval : t1 t < t2.

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.
    Section BusyWindowBound.

Consider an arrival curve.
      Context `{MaxArrivals Task}.

Consider a set of tasks that respects the arrival curve.
      Variable ts : list Task.
      Hypothesis H_taskset_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.

Assume that all jobs come from this task set.
Consider a constant L such that...
      Variable L : duration.
... L is greater than 0, and...
      Hypothesis H_L_positive : L > 0.

L is the fixed point of the following equation.
      Hypothesis H_fixed_point : L = total_request_bound_function ts L.

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.