# Library prosa.analysis.abstract.lower_bound_on_service

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.abstract.busy_interval.

# 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.
Section LowerBoundOnService.
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 ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
... and any schedule of this arrival sequence.
Variable sched : schedule PState.
Assume that the job costs are no larger than the task costs.
Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
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.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
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.
Section InterferenceIsComplement.
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 δ.
Lemma interference_is_complement_to_schedule :
service_during sched j t (t + δ) + cumulative_interference j t (t + δ) ≥ δ.
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., δ).
Remark service_and_interference_bounded :
unit_service_proc_model PState →
service_during sched j t (t + δ) + cumulative_interference j t (t + δ) ≤ δ.
End InterferenceIsComplement.
In this section, we prove a sufficient condition under which job j receives enough service.
Section InterferenceBoundedImpliesEnoughService.
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.
Theorem j_receives_enough_service :
service sched j (t1 + δ) ≥ progress_of_job.
End InterferenceBoundedImpliesEnoughService.
End LowerBoundOnService.