Library prosa.analysis.abstract.ideal_jlfp_rta

In this file we consider an ideal uni-processor ...
Require Import prosa.model.processor.ideal.

... and classic model of readiness without jitter and no self-suspensions, where pending jobs are always ready.
Require Import prosa.model.readiness.basic.

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

In this module we instantiate functions Interference and Interfering Workload for 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 arrival sequence with consistent arrivals.
Next, consider any ideal uni-processor schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
Assume we have sequential tasks, i.e., jobs of the same task execute in the order of their arrival.
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 in ts that is to be analyzed.
  Variable tsk : Task.

For simplicity, let's define some local names.

Interference and Interfering Workload

In this section, we introduce definitions of interference, interfering workload and a function that bounds cumulative interference.
For proper calculation of interference and interfering workload of a job, we need to distinguish interference received from other jobs of the same task and jobs of other tasks. In that regard, we introduce two additional relations. The first relation defines whether job j1 has a higher-than-or-equal-priority than job j2 and j1 is not equal to j2...
  Let another_hep_job: JLFP_policy Job :=
    fun j1 j2hep_job j1 j2 && (j1 != j2).

...and the second relation defines whether a job j1 has a higher-or-equal-priority than job j2 and the task of j1 is not equal to task of j2.
In order to introduce the interference, first we need to recall the definition of priority inversion introduced in module limited.fixed_priority.busy_interval: Definition is_priority_inversion t := if sched t is Some jlp then ~~ higher_eq_priority jlp j else false. I.e., 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.
  Let is_priority_inversion (j : Job) (t : instant) :=
    is_priority_inversion sched j t.

Next, we say that job j is incurring interference from another job with higher or equal priority at time t, if there exists job jhp (different from j) with a higher or equal priority that executes at time t.
  Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=
    if sched t is Some jhp then
      another_hep_job jhp j
    else false.

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.
  Definition is_interference_from_hep_job_from_another_task (j : Job) (t : instant) :=
    if sched t is Some jhp then
      hep_job_from_another_task jhp j
    else false.

Now, we define the notion of cumulative interference, called interfering_workload_of_jobs_with_hep_priority, that says how many units of workload are generated by jobs with higher or equal priority released at time t.
Instantiation of Interference 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 function and interfering workload of jobs with higher or equal priority.
For each of the concepts defined above, we introduce a corresponding cumulative function: (a) cumulative priority inversion...
  Definition cumulative_priority_inversion (j : Job) (t1 t2 : instant) :=
    \sum_(t1 t < t2) is_priority_inversion j t.

... (b) cumulative interference from other jobs with higher or equal priority...
... (c) and cumulative interference from jobs with higher or equal priority from other tasks...
... (d) cumulative interference...
... (e) cumulative workload from jobs with higher or equal priority...
... (f) and cumulative interfering workload.
Instantiated functions usually do not have 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.
  Let workload_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
    workload_of_jobs (fun jhpanother_hep_job jhp j) (arrivals_between t1 t2).

Similarly, we recall notions of service of higher or equal priority jobs from other tasks...
  Let service_of_hep_jobs_from_other_tasks (j : Job) (t1 t2 : instant) :=
    service_of_jobs sched (fun jhphep_job_from_another_task jhp j)
                    (arrivals_between t1 t2) t1 t2.

... and service of all other jobs with higher or equal priority.
  Let service_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
    service_of_jobs sched (fun jhpanother_hep_job jhp j) (arrivals_between t1 t2) t1 t2.

Equivalences

In this section we prove a few 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.

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 j t1 t2
          + cumulative_interference_from_other_hep_jobs j t1 t2.

Let j be any job of task tsk, and let upp_t be any time instant after job j's arrival. Then for any time interval lying before upp_t, 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.
    Lemma cumulative_task_interference_split:
       j t1 t2 upp_t,
        job_task j = tsk
        j \in arrivals_before arr_seq upp_t
        ~~ job_completed_by j t2
        cumulative_task_interference interference tsk upp_t t1 t2 =
        cumulative_priority_inversion j t1 t2 +
        cumulative_interference_from_hep_jobs_from_other_tasks j t1 t2.

In this section we prove that the (abstract) cumulative interfering workload is equivalent to 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 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.
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 : quiet_time_cl j t1.

Then for any 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.

Consider any job j of tsk.
        Variable j : Job.
        Hypothesis H_j_arrives : arrives_in arr_seq j.
        Hypothesis H_job_of_tsk : job_task j = tsk.
        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.

        Lemma quiet_time_cl_implies_quiet_time_ab:
           t, quiet_time_cl j t quiet_time_ab j t.

        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 obtained by instantiating the abstract definition of busy interval coincides with the conventional definition of busy interval.
        Lemma instantiated_busy_interval_equivalent_edf_busy_interval:
           t1 t2,
            busy_interval_cl j t1 t2 busy_interval_ab j t1 t2.

      End BusyIntervalEquivalence.

  End Equivalences.

End JLFPInstantiation.