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

... and any type of jobs associated with these tasks.
Context {Job : JobType}.
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 arrival sequence with consistent arrivals...
Next, consider any ideal uni-processor schedule of this arrival sequence.
Assume that the job costs are no larger than the task costs.
Let tsk be any task that is to be analyzed.

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.
Lemma job_completes_within_busy_interval:
completed_by sched j t2.
Proof.
move: (H_busy_interval) ⇒ [[/andP [_ LT] [_ _]] [_ QT2]].
unfold pending, has_arrived in QT2.
move: QT2; rewrite /pending negb_and; move ⇒ /orP [QT2|QT2].
{ by move: QT2 ⇒ /negP QT2; exfalso; apply QT2, ltnW. }
by rewrite Bool.negb_involutive in QT2.
Qed.

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.
Lemma interference_is_complement_to_schedule:
service_during sched j t (t + delta) + cumul_interference j t (t + delta) = delta.
Proof.
rewrite /service_during /cumul_interference/service_at.
rewrite -big_split //=.
rewrite -{2}(sum_of_ones t delta).
rewrite big_nat [in RHS]big_nat.
apply: eq_bigrx /andP[Lo Hi].
move: (H_work_conserving j t1 t2 x) ⇒ Workj.
feed_n 5 Workj; try done.
{ by apply/andP; split; eapply leq_trans; eauto 2. }
rewrite -/(service_at sched j x) service_at_is_scheduled_at.
have->: scheduled_at sched j x = ~~ interference j x.
{ by apply/idP/negP; intuition. }
Qed.

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.

Assume that for some delta, the sum of desired progress and cumulative interference is bounded by delta (i.e., the supply).
Variable delta : duration.
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.
service sched j (t1 + delta) progress_of_job.
Proof.
case NEQ: (t1 + delta t2); last first.
{ intros.
have L8 := job_completes_within_busy_interval.
apply leq_trans with (job_cost j); first by done.
rewrite /service.
rewrite -(service_during_cat _ _ _ t2).
apply leq_trans with (service_during sched j 0 t2); [by done | by rewrite leq_addr].
by apply/andP; split; last (apply negbT in NEQ; apply ltnW; rewrite ltnNge).
}
apply subh3 in BOUND.
apply leq_trans with (delta - cumul_interference j t1 (t1 + delta)); first by done.
apply leq_trans with (service_during sched j t1 (t1 + delta)).
{ rewrite -{1}[delta](interference_is_complement_to_schedule t1) //.
}
{ rewrite /service -[X in _ X](service_during_cat _ _ _ t1).
by apply/andP; split; last rewrite leq_addr.
}
}
Qed.

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.
Then, job j must complete in job_cost j - job_run_to_completion_threshold j time units after it reaches run-to-completion threshold.
Lemma job_completes_after_reaching_run_to_completion_threshold:
t,
job_run_to_completion_threshold j service sched j t
completed_by sched j (t + (job_cost j - job_run_to_completion_threshold j)).
Proof.
movet ES.
set (job_cost j - job_run_to_completion_threshold j) as job_last.
have LSNP := @job_nonpreemptive_after_run_to_completion_threshold
Job H2 H3 _ _ arr_seq sched _ j _ t.
apply negbNE; apply/negP; intros CONTR.
have SCHED: t', t t' t + job_last scheduled_at sched j t'.
{ movet' /andP [GE LT].
rewrite -[t'](@subnKC t) //.
eapply LSNP; eauto 2; first by rewrite leq_addr.
rewrite subnKC //.
apply/negP; intros COMPL.
move: CONTR ⇒ /negP Temp; apply: Temp.
apply completion_monotonic with (t0 := t'); try done.
}
have SERV: job_last + 1 \sum_(t t' < t + (job_last + 1)) service_at sched j t'.
rewrite big_nat_cond [in X in _ X]big_nat_cond.
rewrite leq_sum //.
movet' /andP [NEQ _].
rewrite service_at_is_scheduled_at.
}
eapply service_at_most_cost with (j0 := j) (t0 := t + job_last.+1) in H_completed_jobs_dont_execute; last first.
{ by apply ideal_proc_model_provides_unit_service. }
move: H_completed_jobs_dont_execute; rewrite leqNgt; move ⇒ /negP T; apply: T.
rewrite /service -(service_during_cat _ _ _ t); last by (apply/andP; split; last rewrite leq_addr).
apply leq_trans with (job_run_to_completion_threshold j + service_during sched j t (t + job_last.+1));