Library prosa.analysis.abstract.lower_bound_on_service

Lower Bound On Job Service

In this section we prove that if the cumulative interference inside a busy interval is bounded by a certain constant then a job executes long enough to reach a specified amount of service.
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}.

In addition, we assume existence of a function mapping jobs to their preemption points.
  Context `{JobPreemptable Job}.

Consider any kind of processor state model.
  Context {PState : ProcessorState Job}.

Consider any arrival sequence with consistent arrivals ...
... and any schedule of this arrival sequence.
  Variable sched : schedule PState.

Assume that the job costs are no larger than the task costs.
Let tsk be any task that is to be analyzed.
  Variable tsk : Task.

Assume we are provided with abstract functions for interference and interfering workload.
  Context `{Interference Job}.
  Context `{InterferingWorkload Job}.

We assume that the schedule is work-conserving.
Let j be any job of task tsk with positive cost.
  Variable j : Job.
  Hypothesis H_j_arrives : arrives_in arr_seq j.
  Hypothesis H_job_of_tsk : job_of_task tsk j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

In this section, we show that the cumulative interference is a complement to the total time where job j is scheduled inside a busy interval prefix.
Consider any busy interval prefix [t1, t2) of job j.
    Variable t1 t2 : instant.
    Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.

Consider any sub-interval [t, t + δ) inside the busy interval [t1, t2).
    Variables (t : instant) (δ : duration).
    Hypothesis H_t1_le_t : t1 t.
    Hypothesis H_tδ_le_t2 : t + δ t2.

We prove that sum of cumulative service and cumulative interference in the interval [t, t + δ) is equal to δ.
Also, note that under the unit-service processor model assumption, the sum of service within the interval [t, t + δ) and the cumulative interference within the same interval is bounded by the length of the interval (i.e., δ).
In this section, we prove a sufficient condition under which job j receives enough service.
Consider any busy interval [t1, t2) of job j.
    Variable t1 t2 : instant.
    Hypothesis H_busy_interval : busy_interval sched j t1 t2.

Let progress_of_job be the desired service of job j.
    Variable progress_of_job : duration.
    Hypothesis H_progress_le_job_cost : progress_of_job job_cost j.

Assume that for some δ the sum of desired progress and cumulative interference is bounded by δ.
    Variable δ : duration.
    Hypothesis H_total_workload_is_bounded :
      progress_of_job + cumulative_interference j t1 (t1 + δ) δ.

Then, it must be the case that the job has received no less service than progress_of_job.