# 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 + δ) ≥ δ.
Proof.
rewrite /service_during /cumulative_interference /cumul_cond_interference /service_at.
rewrite -big_split //= -{1}(sum_of_ones t δ) big_nat [in X in _ ≤ X]big_nat leq_sum // ⇒ x /andP[Lo Hi].
move: (H_work_conserving j t1 t2 x) ⇒ Workj.
feed_n 4 Workj ⇒ //; first by lia.
rewrite /cond_interference //=.
case INT: interference; first by lia.
by rewrite // addn0; apply Workj; rewrite INT.
Qed.
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 + δ) ≤ δ.
Proof.
move ⇒ UNIT.
rewrite /service_during /cumulative_interference/service_at -big_split //=.
rewrite -{2}(sum_of_ones t δ).
rewrite big_nat [in X in _ ≤ X]big_nat; apply leq_sum ⇒ x /andP[Lo Hi].
move: (H_work_conserving j t1 t2 x) ⇒ Workj.
feed_n 4 Workj ⇒ //.
{ by apply/andP; split; lia. }
rewrite /cond_interference //=.
destruct (interference j x).
- rewrite addn1 ltnS.
by move_neq_up NE; apply Workj.
- by rewrite addn0; apply UNIT.
Qed.
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.
Proof.
destruct (leqP (t1 + δ) t2) as [NEQ|NEQ]; last first.
{ move: (job_completes_within_busy_interval _ _ _ _ H_busy_interval) ⇒ COMPL.
apply leq_trans with (job_cost j) ⇒ [//|].
rewrite /service -(service_during_cat _ _ _ t2); last by apply/andP; split; last apply ltnW.
by apply leq_trans with (service_during sched j 0 t2); [| rewrite leq_addr].
}
{ move: H_total_workload_is_bounded ⇒ BOUND.
rewrite addnC in BOUND; apply leq_subRL_impl in BOUND.
apply leq_trans with (δ - cumulative_interference j t1 (t1 + δ)) ⇒ [//|].
apply leq_trans with (service_during sched j t1 (t1 + δ)).
- eapply leq_trans.
+ by apply leq_sub2r, (interference_is_complement_to_schedule t1 t2);
[apply H_busy_interval | apply leqnn | apply NEQ].
+ by rewrite -addnBA // subnn addn0 //.
- rewrite /service -[X in _ ≤ X](service_during_cat _ _ _ t1); first by rewrite leq_addl //.
by apply/andP; split; last rewrite leq_addr.
}
Qed.
End InterferenceBoundedImpliesEnoughService.
End LowerBoundOnService.