Library prosa.analysis.abstract.run_to_completion

Run-to-Completion Threshold of a job

In this module, we provide a sufficient condition under which a job receives enough service to become non-preemptive. Previously we defined the notion of run-to-completion threshold (see file abstract.run_to_completion_threshold.v). Run-to-completion threshold is the amount of service after which a job cannot be preempted until its completion. In this section we prove that if cumulative interference inside a busy interval is bounded by a certain constant then a job executes long enough to reach its run-to-completion threshold and become non-preemptive.
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 uni-service ideal processor state model.
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.
  Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
  Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.

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.
For simplicity, let's define some local names.
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_task j = tsk.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Next, consider any busy interval [t1, t2) of job j.
  Variable t1 t2 : instant.
  Hypothesis H_busy_interval : busy_interval j t1 t2.

First, we prove that job j completes by the end of the busy interval. Note that the busy interval contains the execution of job j, in addition time instant t2 is a quiet time. Thus by the definition of a quiet time the job should be completed before time t2.
In this section we show that the cumulative interference is a complement to the total time where job j is scheduled inside the busy interval.
Consider any sub-interval [t, t + delta) inside the busy interval t1, t2).
    Variables (t : instant) (delta : duration).
    Hypothesis H_greater_than_or_equal : t1 t.
    Hypothesis H_less_or_equal: t + delta t2.

We prove that sum of cumulative service and cumulative interference in the interval [t, t + delta) is equal to delta.
In this section, we prove a sufficient condition under which job j receives enough service.
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 delta, the sum of desired progress and cumulative interference is bounded by delta (i.e., the supply).
    Variable delta : duration.
    Hypothesis H_total_workload_is_bounded:
      progress_of_job + cumul_interference j t1 (t1 + delta) delta.

Then, it must be the case that the job has received no less service than progress_of_job.
In this section we prove a simple lemma about completion of a job after is reaches run-to-completion threshold.
Assume that completed jobs do not execute ...
.. and the preemption model is valid.
Then, job j must complete in job_cost j - job_run_to_completion_threshold j time units after it reaches run-to-completion threshold.