# Library prosa.analysis.abstract.run_to_completion

Require Export prosa.analysis.facts.model.service_of_jobs.

Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.

Require Export prosa.analysis.abstract.definitions.

Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.

Require Export prosa.analysis.abstract.definitions.

# 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 jobs.

In addition, we assume existence of a function
mapping jobs to their preemption points.

Consider any kind of uni-service ideal processor state model.

Context {PState : ProcessorState Job}.

Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.

Hypothesis H_unit_service_proc_model : unit_service_proc_model 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 ...

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

... and any schedule of this arrival sequence.

Assume we are provided with abstract functions for interference and interfering workload.

Variable interference : Job → instant → bool.

Variable interfering_workload : Job → instant → duration.

Variable interfering_workload : Job → instant → duration.

For simplicity, let's define some local names.

Let work_conserving := work_conserving arr_seq sched.

Let cumul_interference := cumul_interference interference.

Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.

Let busy_interval := busy_interval sched interference interfering_workload.

Let cumul_interference := cumul_interference interference.

Let cumul_interfering_workload := cumul_interfering_workload interfering_workload.

Let busy_interval := busy_interval sched interference interfering_workload.

We assume that the schedule is work-conserving.

Variable j : Job.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_cost_positive : job_cost_positive j.

Hypothesis H_j_arrives : arrives_in arr_seq j.

Hypothesis H_job_cost_positive : job_cost_positive j.

Next, consider any busy interval

`[t1, t2)`

of job j.
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.

Variables (t : instant) (delta : duration).

Hypothesis H_greater_than_or_equal : t1 ≤ t.

Hypothesis H_less_or_equal: t + delta ≤ t2.

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.
Lemma interference_is_complement_to_schedule:

service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.

End InterferenceIsComplement.

service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.

End InterferenceIsComplement.

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.

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.

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.

Theorem j_receives_at_least_run_to_completion_threshold:

service sched j (t1 + delta) ≥ progress_of_job.

End InterferenceBoundedImpliesEnoughService.

service sched j (t1 + delta) ≥ progress_of_job.

End InterferenceBoundedImpliesEnoughService.

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.