Library prosa.analysis.abstract.restricted_supply.iw_readiness

Readiness-Aware JLFP Instantiation of Interference and Interfering Workload Functions for Restricted-Supply Uniprocessors

Here we instantiate the interference and interfering workload functions, as required by abstract restricted-supply analysis (aRSA).
Section IWInstantiation.

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}.

Assume a fully supply-consuming, unit-supply uniprocessor model.
Allow for any notion of job readiness.
  Context `{!JobReady Job PState}.

Consider any valid arrival sequence ...
... and any valid schedule of this arrival sequence.
  Variable sched : schedule PState.
  Hypothesis H_valid_schedule : valid_schedule sched arr_seq.

Consider any JLFP policy and assume that the priority relation is reflexive and transitive.

Interference and Interfering Workload

In the following, we introduce definitions of interference and interfering workload.

Instantiation of Interference

We say that job j incurs interference at time t iff it cannot execute due to (1) the lack of supply at time t, (2) due to service inversion (i.e., a lower-priority job receiving service at t), (3) due to another higher-or-equal-priority job receiving service, (4) due to j and all other higher-or-equal-priority jobs becoming non-ready.
  #[local] Instance rs_readiness_jlfp_interference : Interference Job :=
    {
      interference (j : Job) (t : instant) :=
        is_blackout sched t
        || another_hep_job_interference arr_seq sched j t
        || service_inversion arr_seq sched j t
        || (has_supply sched t && ~~ some_hep_job_ready arr_seq sched j t)
    }.

Instantiation of Interfering Workload

The interfering workload, in turn, is defined as the sum of the indicator values of the predicates in the definition of interference.

  #[local] Instance rs_readiness_jlfp_interfering_workload : InterferingWorkload Job :=
    {
      interfering_workload (j : Job) (t : instant) :=
        is_blackout sched t
        + other_hep_jobs_interfering_workload arr_seq j t
        + service_inversion arr_seq sched j t
        + has_supply sched t && ~~ some_hep_job_ready arr_seq sched j t
    }.

To simplify our proof, we define a notion of cumulative_readiness_interference that is disjoint from is_blackout. This will help us to split cumulative_interference and cumulative_interfering_workload into disjoint parts.

Equivalences

We prove that we can split cumulative interference into disjoint parts.
Similarly, we prove that we can split cumulative interfering workload into disjoint parts.
Now, let tsk be any given task.
  Variable tsk : Task.

Let [t1, t2) be a time interval and let j be any job of task tsk that is not completed by time t2. Then we prove a bound on the cumulative interference received due to jobs of other tasks executing.
Next, consider cumulative intra-supply interference, which accounts for any interference that occurs while the processor offers supply.
To this end, let's first define a predicate to express intra-supply interference.
  Let intra_supply (_j : Job) (t : instant) := has_supply sched t.

The cumulative interference conditioned on intra_supply can be split into three disjoint parts.
In this section, we prove that the (abstract) cumulative interfering workload due to other higher-or-equal priority jobs is equal to the conventional workload (from other higher-or-equal priority jobs).
Let [t1, t2) be any time interval.
    Variables t1 t2 : instant.

Consider any job j of tsk in the given arrival sequence.
    Variable j : Job.
    Hypothesis H_j_arrives : arrives_in arr_seq j.
    Hypothesis H_job_of_tsk : job_of_task tsk j.

The cumulative interfering workload (w.r.t. j) due to other higher-or-equal priority jobs is equal to the conventional workload from other higher-or-equal priority jobs.
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.
We similarly define local names 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.

To prove that the two notions of busy intervals are equivalent, we first show that the respective notions of quiet times 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.
    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 a 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.
Next, we prove that abstract busy window implies the existence of a classic quiet time.
    Fact abstract_busy_interval_classic_quiet_time :
       t1 t2,
        busy_interval_ab j t1 t2 quiet_time_cl j t1.

Also, 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.
  Section I_IW_correctness.

Note that we differentiate between abstract and classical notions of work-conserving schedules.
Recall the notion of an abstract busy-interval prefix.
We assume that the schedule is a work-conserving schedule in the classical sense, and later prove that this implies that abstract work-conservation also holds.
    Hypothesis H_work_conserving : work_conserving_cl.

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 an arriving job j with positive cost.
      Variable j : Job.
      Hypothesis H_arrives : arrives_in arr_seq j.
      Hypothesis H_job_cost_positive : 0 < job_cost j.

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

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

We first prove that, inside the busy interval, there always exists a pending higher-or-equal-priority job. To prove this, we make use of the obtained result that, for the given interference and interfering workload functions, the notions of abstract and classical busy intervals are equivalent.
      Lemma pending_hep_job_exists_inside_busy_interval :
         jhp,
          arrives_in arr_seq jhp
           pending sched jhp t
           hep_job jhp j.

We now prove that, if interference is false at a time t, then the job is scheduled at time t.
Conversely, if the job is scheduled at time t, then interference is false.
Using the above two lemmas, we can prove that abstract work conservation always holds for these instantiations of interference (I) and interfering workload (W).
Next, in order to prove that these definitions of interference and interfering workload are consistent with sequential tasks, we need to assume that the policy under consideration respects sequential tasks.
We prove that these definitions of interference and interfering workload are consistent with sequential tasks.
Finally, we show that cumulative interference (I) never exceeds the cumulative interfering workload (W).