Library prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_service
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.arrival.jitter.job.
Require Import prosa.classic.model.schedule.uni.schedulability prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule
prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
prosa.classic.model.schedule.uni.susp.schedule
prosa.classic.model.schedule.uni.susp.platform
prosa.classic.model.schedule.uni.susp.valid_schedule.
Require Import prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule
prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Module JitterScheduleService.
Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
UniprocessorScheduleWithJitter Schedulability ResponseTime TaskArrival
ScheduleConstruction ValidSuspensionAwareSchedule.
Module basic := schedule.UniprocessorSchedule.
Module susp := ScheduleWithSuspensions.
Module jitter_aware := Platform.
Module susp_aware := PlatformWithSuspensions.
Module job_jitter := JobWithJitter.
Module reduction := JitterScheduleConstruction.
Module reduction_prop := JitterScheduleProperties.
Section ProvingScheduleProperties.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
Require Import prosa.classic.model.priority prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.task_arrival
prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.arrival.jitter.job.
Require Import prosa.classic.model.schedule.uni.schedulability prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule
prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals
prosa.classic.model.schedule.uni.susp.schedule
prosa.classic.model.schedule.uni.susp.platform
prosa.classic.model.schedule.uni.susp.valid_schedule.
Require Import prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule
prosa.classic.analysis.uni.susp.dynamic.jitter.jitter_schedule_properties.
Require Import prosa.classic.model.schedule.uni.transformation.construction.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
Module JitterScheduleService.
Import Job SporadicTaskset Suspension Priority SuspensionIntervals Workload Service
UniprocessorScheduleWithJitter Schedulability ResponseTime TaskArrival
ScheduleConstruction ValidSuspensionAwareSchedule.
Module basic := schedule.UniprocessorSchedule.
Module susp := ScheduleWithSuspensions.
Module jitter_aware := Platform.
Module susp_aware := PlatformWithSuspensions.
Module job_jitter := JobWithJitter.
Module reduction := JitterScheduleConstruction.
Module reduction_prop := JitterScheduleProperties.
Section ProvingScheduleProperties.
Context {Task: eqType}.
Variable task_cost: Task → time.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → Task.
1) Basic Setup & Setting
Variable ts: seq Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent:
arrival_times_are_consistent job_arrival arr_seq.
Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.
Hypothesis H_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_job_deadlines_equal_task_deadlines:
∀ j, arrives_in arr_seq j → job_deadline j = task_deadline (job_task j).
Hypothesis H_constrained_deadlines:
constrained_deadline_model task_period task_deadline ts.
Hypothesis H_sporadic_arrivals:
sporadic_task_model task_period job_arrival job_task arr_seq.
Variable higher_eq_priority: FP_policy Task.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.
Hypothesis H_priority_is_total: FP_is_total_over_task_set higher_eq_priority ts.
Let job_higher_eq_priority := FP_to_JLDP job_task higher_eq_priority.
Variable job_suspension_duration: job_suspension Job.
Variable sched_susp: schedule Job.
Hypothesis H_valid_schedule:
valid_suspension_aware_schedule job_arrival arr_seq job_higher_eq_priority
job_suspension_duration job_cost sched_susp.
Let job_response_time_in_sched_susp_bounded_by :=
is_response_time_bound_of_job job_arrival job_cost sched_susp.
Let job_misses_no_deadline_in_sched_susp :=
job_misses_no_deadline job_arrival job_cost job_deadline sched_susp.
2) Analysis Setup
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Let arr_j := job_arrival j.
Variable R_j: time.
Let other_hep_task tsk_other :=
higher_eq_priority tsk_other (job_task j) && (tsk_other != job_task j).
Variable R_hp: Job → time.
Hypothesis H_bounded_response_time_of_hp_jobs:
∀ j_hp,
arrives_in arr_seq j_hp →
other_hep_task (job_task j_hp) →
job_response_time_in_sched_susp_bounded_by j_hp (R_hp j_hp).
Hypothesis H_no_deadline_misses_for_previous_jobs:
∀ j0,
arrives_in arr_seq j0 →
job_arrival j0 < job_arrival j →
job_task j0 = job_task j →
job_misses_no_deadline_in_sched_susp j0.
3) Instantiation of the Reduction
Let sched_jitter := reduction.sched_jitter job_arrival job_task arr_seq higher_eq_priority
job_cost job_suspension_duration j R_hp.
Let inflated_job_cost := reduction.inflated_job_cost job_cost job_suspension_duration j.
Let job_jitter := reduction.job_jitter job_arrival job_task higher_eq_priority job_cost j R_hp.
4) Setup for Next Sections
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let job_arrived_before := arrived_before job_arrival.
Let job_has_arrived := has_arrived job_arrival.
Let job_has_actually_arrived := jitter_has_passed job_arrival job_jitter.
Let job_completed_in_sched_jitter := completed_by inflated_job_cost sched_jitter.
Let job_suspended_at :=
suspended_at job_arrival job_cost job_suspension_duration sched_susp.
Let job_cumulative_suspension :=
cumulative_suspension_during job_arrival job_cost job_suspension_duration sched_susp.
Let job_completed_in_sched_susp := completed_by job_cost sched_susp.
Let backlogged_in_sched_susp := susp.backlogged job_arrival job_cost
job_suspension_duration sched_susp.
Let arrivals := jobs_arrived_between arr_seq.
Let actual_arrivals := actual_arrivals_between job_arrival job_jitter arr_seq.
Let arrivals_before_end_of_interval := arrivals 0 (arr_j + R_j).
Let actual_arrivals_before_end_of_interval := actual_arrivals 0 (arr_j + R_j).
Let other_higher_eq_priority_job j_hp :=
higher_eq_priority (job_task j_hp) (job_task j) && (j_hp != j).
Definition workload_of_other_hep_jobs_in_sched_susp t1 t2 :=
workload_of_jobs job_cost (arrivals t1 t2) other_higher_eq_priority_job.
Definition workload_of_other_hep_jobs_in_sched_jitter t1 t2 :=
workload_of_jobs inflated_job_cost (actual_arrivals t1 t2) other_higher_eq_priority_job.
Definition service_of_other_hep_jobs_in_sched_susp t1 t2 :=
service_of_jobs sched_susp arrivals_before_end_of_interval other_higher_eq_priority_job t1 t2.
Definition service_of_other_hep_jobs_in_sched_jitter t1 t2 :=
service_of_jobs sched_jitter actual_arrivals_before_end_of_interval
other_higher_eq_priority_job t1 t2.
5) Auxiliary Lemmas
Section AuxiliaryLemmas.
Section ServiceEqualsWorkload.
Variable t: time.
Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.
Hypothesis H_workload_has_finished:
∀ j_hp,
arrives_in arr_seq j_hp →
actual_arrival_before job_arrival job_jitter j_hp t →
other_higher_eq_priority_job j_hp →
job_completed_in_sched_jitter j_hp t.
Lemma jitter_reduction_service_equals_workload_in_jitter:
service_of_other_hep_jobs_in_sched_jitter 0 t ≥
workload_of_other_hep_jobs_in_sched_jitter 0 t.
Proof.
rename H_workload_has_finished into WORK.
rewrite /workload_of_other_hep_jobs_in_sched_jitter
/workload_of_jobs /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
set act := actual_arrivals.
set t1 := arr_j; set t2 := arr_j + R_j.
set hep := other_higher_eq_priority_job.
set Sj := service_during sched_jitter.
apply leq_trans with (n := \sum_(j0 <- act 0 t | hep j0) Sj j0 0 t); last first.
{
rewrite big_mkcond [X in _ ≤ X]big_mkcond.
apply leq_sum_sub_uniq; first by apply actual_arrivals_uniq.
intros j0 IN0.
try ( by apply actual_arrivals_between_sub with (t3 := 0) (t4 := t) ) ||
by apply actual_arrivals_between_sub with (t1 := 0) (t2 := t).
}
apply leq_sum_seq; rewrite /act /actual_arrivals; intros j0 IN0 HP0.
apply WORK; try done.
- by apply in_actual_arrivals_between_implies_arrived in IN0.
- by apply in_actual_arrivals_implies_arrived_before in IN0.
Qed.
End ServiceEqualsWorkload.
Section ServiceBoundedByWorkload.
Variable t: time.
Hypothesis H_before_end_of_interval: t ≤ arr_j + R_j.
Lemma jitter_reduction_service_in_sched_susp_le_workload:
service_of_other_hep_jobs_in_sched_susp 0 t ≤
workload_of_other_hep_jobs_in_sched_susp 0 t.
Proof.
move: (H_valid_schedule) ⇒ [FROMarr [MUSTARRs [COMPs _]]].
rename H_before_end_of_interval into LTt.
rewrite /workload_of_other_hep_jobs_in_sched_susp /workload_of_jobs
/service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals.
set t1 := arr_j; set t2 := arr_j + R_j.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
apply leq_trans with (n := \sum_(j0 <- all 0 t | hep j0) Ss j0 0 t);
last by apply leq_sum; intros j0 _; apply cumulative_service_le_job_cost.
rewrite exchange_big [X in _ ≤ X]exchange_big /=.
apply leq_sum_nat; move ⇒ t' /= LT' _.
apply leq_trans with (n := \sum_(j0 <- all 0 t2 | hep j0 &&
(scheduled_at sched_susp j0 t')) 1).
{
rewrite big_mkcond [X in _ ≤ X]big_mkcond.
rewrite /service_at; apply leq_sum; intros j0 _.
by case: hep; case SCHED': scheduled_at.
}
apply leq_trans with (n := \sum_(j0 <- all 0 t | hep j0 &&
(scheduled_at sched_susp j0 t')) 1); last first.
{
rewrite big_mkcond [X in _ ≤ X]big_mkcond.
rewrite /service_at; apply leq_sum; intros j0 _.
by case: hep; case SCHED': scheduled_at.
}
rewrite -big_filter -[X in _ ≤ X]big_filter.
apply leq_sum_sub_uniq; first by rewrite filter_uniq //; eapply arrivals_uniq; eauto 1.
intros j0; rewrite 2!mem_filter; move ⇒ /andP [/andP [HP0 SCHED0] IN0].
rewrite HP0 SCHED0 /=.
have ARRin0: arrives_in arr_seq j0 by apply FROMarr in SCHED0.
have ARR0: job_arrival j0 ≤ t' by apply MUSTARRs.
try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_ltn_trans _ LT').
Qed.
End ServiceBoundedByWorkload.
End AuxiliaryLemmas.
Section LessServiceBeforeArrival.
Section LessServiceForEachJob.
Variable j_hp: Job.
Hypothesis H_arrives: arrives_in arr_seq j_hp.
Hypothesis H_higher_or_equal_priority: other_higher_eq_priority_job j_hp.
Let arr_hp := job_arrival j_hp.
Let cost_hp := job_cost j_hp.
Let Rhp := R_hp j_hp.
Section Case1.
Hypothesis H_same_task: job_task j_hp = job_task j.
Lemma jitter_reduction_less_job_service_before_interval_case1:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
move: (H_valid_schedule) ⇒ [_ [MUSTARRs [COMPs _]]].
rename H_no_deadline_misses_for_previous_jobs into NOMISS,
H_constrained_deadlines into DL, H_jobs_from_taskset into FROM,
H_sporadic_arrivals into SPO.
move: H_higher_or_equal_priority ⇒ /andP [HP NEQ].
case (ltnP arr_hp arr_j) ⇒ [BEFORE | AFTER]; last first.
{
rewrite /service /service_during.
rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
move: H_same_task ⇒ /eqP SAMEtsk; apply negbF in SAMEtsk.
by rewrite /actual_arrival /job_jitter /reduction.job_jitter HP SAMEtsk /= addn0.
}
apply leq_trans with (n := inflated_job_cost j_hp).
{
apply cumulative_service_le_job_cost.
by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
}
rewrite /inflated_job_cost /reduction.inflated_job_cost.
apply negbTE in NEQ; rewrite NEQ.
apply completion_monotonic with (t := arr_hp + job_deadline j_hp); last by apply NOMISS.
rewrite H_job_deadlines_equal_task_deadlines //.
apply leq_trans with (n := arr_hp + task_period (job_task j_hp));
first by rewrite leq_add2l DL // FROM.
apply SPO; try (by done); last by apply ltnW.
by intros SAME; subst; rewrite eq_refl in NEQ.
Qed.
End Case1.
Section Case2.
Hypothesis H_different_task: job_task j_hp != job_task j.
Hypothesis H_released_no_earlier: arr_j ≤ actual_job_arrival j_hp.
Lemma jitter_reduction_less_job_service_before_interval_case2:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
rename H_different_task into DIFFtask.
move: H_higher_or_equal_priority ⇒ /andP [HP NEQ].
rewrite /service /service_during.
by rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
Qed.
End Case2.
Section Case3.
Hypothesis H_different_task: job_task j_hp != job_task j.
Hypothesis H_distance_is_smaller:
arr_j - arr_hp < Rhp - cost_hp.
Lemma jitter_reduction_less_job_service_before_interval_case3:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
rename H_higher_or_equal_priority into HEP, H_distance_is_smaller into MIN.
move: (HEP) ⇒ /andP [HP NEQ].
rewrite /service /service_during.
rewrite (cumulative_service_before_jitter_is_zero job_arrival job_jitter) //;
first by eapply reduction_prop.sched_jitter_jobs_execute_after_jitter; eauto 1.
rewrite /actual_arrival /job_jitter /reduction.job_jitter HP H_different_task /=.
rewrite /minn MIN.
case (leqP (job_arrival j) (job_arrival j_hp)) ⇒ [AFTER | BEFORE];
first by apply: (leq_trans AFTER); apply leq_addr.
by rewrite subnKC; last by apply ltnW.
Qed.
End Case3.
Section Case4.
Hypothesis H_different_task: job_task j_hp != job_task j.
Hypothesis H_completes_before_j_arrives: arr_hp + Rhp ≤ arr_j.
Lemma jitter_reduction_less_job_service_before_interval_case4:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
rename H_higher_or_equal_priority into HEP,
H_bounded_response_time_of_hp_jobs into RESPhp.
move: (HEP) ⇒ /andP [HP NEQ].
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
last by apply extend_sum.
apply leq_trans with (n := cost_hp);
last by apply RESPhp; last by apply/andP; split.
apply leq_trans with (n := inflated_job_cost j_hp);
last by rewrite /inflated_job_cost /reduction.inflated_job_cost -[_==_]negbK NEQ.
apply cumulative_service_le_job_cost.
by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
Qed.
End Case4.
Section Case5.
Hypothesis H_different_task: job_task j_hp != job_task j.
Hypothesis H_released_before: actual_job_arrival j_hp < arr_j.
Hypothesis H_j_hp_completes_after_j_arrives: arr_j < arr_hp + Rhp.
Hypothesis H_distance_is_not_smaller: Rhp - cost_hp ≤ arr_j - arr_hp.
Remark jitter_reduction_jitter_equals_R_minus_cost:
job_jitter j_hp = Rhp - cost_hp.
Proof.
rename H_higher_or_equal_priority into HEP, H_different_task into DIFFtask.
move: (HEP) ⇒ /andP [HP NEQ].
rewrite /job_jitter /reduction.job_jitter HP DIFFtask /= /minn.
by rewrite ltnNge H_distance_is_not_smaller /=.
Qed.
Lemma jitter_reduction_less_job_service_before_interval_case5:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
move: (H_valid_schedule) ⇒ [_ [MUSTARRs [COMPs _]]].
have JITdef := jitter_reduction_jitter_equals_R_minus_cost.
rename H_higher_or_equal_priority into HEP,
H_bounded_response_time_of_hp_jobs into RESPhp.
move: (HEP) ⇒ /andP [HP NEQ].
set arr_hp' := actual_job_arrival j_hp.
set cost_hp' := inflated_job_cost j_hp.
have JIT: job_jitter j_hp = Rhp - cost_hp by apply JITdef.
apply leq_trans with (n := cost_hp - (arr_hp + Rhp - arr_j)); last first.
{
rewrite /cost_hp leq_subLR.
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
first by apply RESPhp; last by apply/andP; split.
rewrite /service /service_during.
apply leq_trans with (n := \sum_(arr_j ≤ t' < arr_hp+Rhp)
1 + service sched_susp j_hp arr_j);
last by apply leq_add; first by simpl_sum_const.
rewrite → big_cat_nat with (n := arr_j); [simpl | by done | by apply ltnW].
by rewrite addnC; apply leq_add; first by apply leq_sum; intros t0 _; apply leq_b1.
}
{
have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival
job_task arr_seq higher_eq_priority job_cost job_suspension_duration.
rewrite /service /service_during.
rewrite (ignore_service_before_jitter job_arrival job_jitter) //;
[| by eapply AFTERj; eauto 1 | by apply ltnW].
apply leq_trans with (n := \sum_(arr_hp' ≤ t0 < arr_j) 1);
first by apply leq_sum; intros t0 _; apply leq_b1.
simpl_sum_const; rewrite /arr_hp' /actual_job_arrival /actual_arrival JIT.
have LEcost: cost_hp ≤ Rhp.
{
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
first by apply RESPhp; last by apply/andP;split.
apply leq_trans with (n := \sum_(arr_hp ≤ t' < arr_hp + Rhp) 1);
last by simpl_sum_const; rewrite addKn.
rewrite /service /service_during.
rewrite (ignore_service_before_arrival job_arrival) //; last by apply leq_addr.
by apply leq_sum; intros t0 _; apply leq_b1.
}
rewrite addnBA; last by done.
rewrite subnBA; last by apply: (leq_trans LEcost); apply leq_addl.
rewrite subnBA; last by apply ltnW.
by apply leq_sub2r; rewrite addnC.
}
Qed.
End Case5.
Lemma jitter_reduction_less_job_service_before_interval:
service sched_jitter j_hp arr_j ≤ service sched_susp j_hp arr_j.
Proof.
have CASE1 := jitter_reduction_less_job_service_before_interval_case1.
have CASE2 := jitter_reduction_less_job_service_before_interval_case2.
have CASE3 := jitter_reduction_less_job_service_before_interval_case3.
have CASE4 := jitter_reduction_less_job_service_before_interval_case4.
have CASE5 := jitter_reduction_less_job_service_before_interval_case5.
have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
feed AFTERj; try (by done).
case (boolP (job_task j_hp == job_task j)) ⇒ [/eqP SAME | DIFFtsk]; first by apply CASE1.
case (leqP arr_j (actual_job_arrival j_hp)) ⇒ [LEarr | GTarr]; first by apply CASE2.
case (ltnP (arr_j - arr_hp) (Rhp - cost_hp)) ⇒ [LTdiff | GEdiff]; first by apply CASE3.
case (leqP (arr_hp + Rhp) arr_j) ⇒ [LEarrj | GTarrj]; first by apply CASE4.
by apply CASE5.
Qed.
End LessServiceForEachJob.
Corollary jitter_reduction_less_service_before_the_interval:
service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
service_of_other_hep_jobs_in_sched_susp 0 arr_j.
Proof.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/service_of_other_hep_jobs_in_sched_susp
/actual_arrivals_before_end_of_interval /arrivals_before_end_of_interval
/actual_arrivals_before /jobs_arrived_before.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set t2 := arr_j + R_j.
apply leq_trans with (n := \sum_(j_hp <- actual_arrivals 0 t2 | hep j_hp) Ss j_hp 0 arr_j).
{
apply leq_sum_seq; rewrite /actual_arrivals; intros j0 IN0 HEP0.
apply jitter_reduction_less_job_service_before_interval; try (by done).
by apply in_actual_arrivals_between_implies_arrived in IN0.
}
{
rewrite big_mkcond [X in _ ≤ X]big_mkcond /actual_arrivals /=.
apply leq_sum_sub_uniq; first by apply actual_arrivals_uniq.
by intros j0; rewrite !mem_filter /=; move ⇒ /andP [_ IN0].
}
Qed.
End LessServiceBeforeArrival.
Section MoreServiceAfterArrival.
Section Conservation.
Variable t: time.
Hypothesis H_no_earlier_than_j: t ≥ arr_j.
Lemma jitter_reduction_actual_arrival_before_end_of_interval:
∀ j_hp,
other_higher_eq_priority_job j_hp →
job_arrival j_hp ≤ t →
actual_job_arrival j_hp ≤ t.
Proof.
move ⇒ j_hp /andP [HP NEQ] ARRhp.
set arr_hp := job_arrival j_hp.
set cost_hp := job_cost j_hp.
rewrite /actual_job_arrival /actual_arrival /job_jitter /reduction.job_jitter HP /=.
case: ifP ⇒ [NEQtsk | /eqP SAMEtsk]; last by rewrite addn0.
case (ltnP (arr_j - arr_hp) (R_hp j_hp - cost_hp)) ⇒ [MINl | MINr].
{
rewrite /minn MINl.
case (leqP arr_hp arr_j) ⇒ [BEFORE | AFTER]; first by rewrite subnKC //.
by apply leq_trans with (n := arr_hp + (arr_hp - arr_hp));
[by rewrite leq_add2l leq_sub2r // ltnW | by rewrite subnn addn0].
}
{
rewrite /minn ltnNge MINr /=.
apply leq_trans with (n := arr_hp + (arr_j - arr_hp)); first by rewrite leq_add2l.
case (leqP arr_hp arr_j) ⇒ [BEFORE | AFTER]; first by rewrite subnKC //.
by apply leq_trans with (n := arr_hp + (arr_hp - arr_hp));
[by rewrite leq_add2l leq_sub2r // ltnW | by rewrite subnn addn0].
}
Qed.
Lemma jitter_reduction_workload_conservation_inside_interval:
workload_of_other_hep_jobs_in_sched_susp 0 t.+1 ≤
workload_of_other_hep_jobs_in_sched_jitter 0 t.+1.
Proof.
rewrite /workload_of_other_hep_jobs_in_sched_susp
/workload_of_other_hep_jobs_in_sched_jitter /workload_of_jobs.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
apply leq_trans with (n := \sum_(j0 <- all 0 t.+1 | hep j0) inflated_job_cost j0).
{
apply leq_sum_seq; rewrite /all /arrivals; move ⇒ j0 IN0 /andP [_ NEQ].
by apply negbTE in NEQ; rewrite /inflated_job_cost /reduction.inflated_job_cost NEQ //.
}
apply leq_trans with (n := \sum_(j0 <- all 0 t.+1 | hep j0 &&
(actual_job_arrival j0 < t.+1)) inflated_job_cost j0); last first.
{
rewrite -big_filter -[X in _ ≤ X]big_filter.
apply leq_sum_sub_uniq;
first by rewrite filter_uniq //; eapply arrivals_uniq; eauto 1.
intros j0; rewrite !mem_filter /=.
by move ⇒ /andP [/andP [HP LT] IN]; rewrite HP LT IN.
}
rewrite big_mkcond [X in _ ≤ X]big_mkcond /=.
apply leq_sum_seq; intros j0 IN0 _.
case HP: hep; simpl; last by done.
case: (leqP _ _); last by done.
intros BUG; exfalso; rewrite leqNgt in BUG; move: BUG ⇒ /negP BUG; apply: BUG.
apply jitter_reduction_actual_arrival_before_end_of_interval; try (by done).
by eapply in_arrivals_implies_arrived_before in IN0; eauto 1.
Qed.
End Conservation.
Section MoreServiceInsideTheInterval.
Section InductiveStep.
Variable d: time.
Hypothesis H_d_lt_R: d < R_j.
Hypothesis H_induction_hypothesis:
service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).
Section NoPendingJobs.
Hypothesis H_all_jobs_completed_in_sched_jitter:
∀ j_hp,
arrives_in arr_seq j_hp →
other_higher_eq_priority_job j_hp →
job_has_actually_arrived j_hp (arr_j + d) →
job_completed_in_sched_jitter j_hp (arr_j + d).
Lemma jitter_reduction_convert_service_to_workload:
service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
- service_of_other_hep_jobs_in_sched_susp 0 arr_j.
Proof.
have LEWORKs := jitter_reduction_service_in_sched_susp_le_workload.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set Sj := service_during sched_jitter.
set SCHs := scheduled_at sched_susp.
set SCHj := scheduled_at sched_jitter.
set SUSP := job_cumulative_suspension.
set Wj := workload_of_other_hep_jobs_in_sched_jitter.
set Ws := workload_of_other_hep_jobs_in_sched_susp.
set t1 := arr_j.
set t2 := arr_j + R_j.
rewrite exchange_big [X in _ ≤ _ - X]exchange_big /= /service_at.
rewrite -/SCHs -/SCHj addnS addn0.
set TSs := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
set TSj := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
rewrite leq_subRL_impl //.
rewrite addnC -big_cat_nat //=;
last by apply leq_trans with (n := t1 + d); first by apply leq_addr.
by rewrite exchange_big; apply LEWORKs; rewrite ltn_add2l.
Qed.
Lemma jitter_reduction_compare_workload:
workload_of_other_hep_jobs_in_sched_susp 0 (arr_j + d + 1)
- service_of_other_hep_jobs_in_sched_susp 0 arr_j
≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
- service_of_other_hep_jobs_in_sched_susp 0 arr_j.
Proof.
have CONS := jitter_reduction_workload_conservation_inside_interval.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set Sj := service_during sched_jitter.
set SCHs := scheduled_at sched_susp.
set SCHj := scheduled_at sched_jitter.
set SUSP := job_cumulative_suspension.
set Wj := workload_of_other_hep_jobs_in_sched_jitter.
set Ws := workload_of_other_hep_jobs_in_sched_susp.
set t1 := arr_j.
set t2 := arr_j + R_j.
rewrite exchange_big /= /service_at.
rewrite -/SCHs -/SCHj addnS addn0.
set TSs := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
set TSj := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
apply leq_trans with (n := Ws 0 (t1 + d).+1 - TSs 0 t1); first by done.
by rewrite leq_sub2r //; apply CONS, leq_addr.
Qed.
Lemma jitter_reduction_compare_service:
workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
- service_of_other_hep_jobs_in_sched_susp 0 arr_j
≤ workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1)
- service_of_other_hep_jobs_in_sched_jitter 0 arr_j.
Proof.
have LEserv := jitter_reduction_less_service_before_the_interval.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set Sj := service_during sched_jitter.
set SCHs := scheduled_at sched_susp.
set SCHj := scheduled_at sched_jitter.
set SUSP := job_cumulative_suspension.
set Wj := workload_of_other_hep_jobs_in_sched_jitter.
set Ws := workload_of_other_hep_jobs_in_sched_susp.
set t1 := arr_j.
set t2 := arr_j + R_j.
rewrite exchange_big [X in _ ≤ _ - X]exchange_big /= /service_at.
rewrite -/SCHs -/SCHj addnS addn0.
set TSs := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
set TSj := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
rewrite -/(TSs t1 (t1 + d).+1) -/(TSs 0 t1).
rewrite leq_sub2l //.
rewrite /TSj /TSs exchange_big [X in _ ≤ X]exchange_big /=.
by apply LEserv.
Qed.
Lemma jitter_reduction_convert_workload_to_service:
workload_of_other_hep_jobs_in_sched_jitter 0 (arr_j + d + 1) -
service_of_other_hep_jobs_in_sched_jitter 0 arr_j ≤
service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
Proof.
have EQWORKj := jitter_reduction_service_equals_workload_in_jitter.
rename H_all_jobs_completed_in_sched_jitter into ALL.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set Sj := service_during sched_jitter.
set SCHs := scheduled_at sched_susp.
set SCHj := scheduled_at sched_jitter.
set SUSP := job_cumulative_suspension.
set Wj := workload_of_other_hep_jobs_in_sched_jitter.
set Ws := workload_of_other_hep_jobs_in_sched_susp.
set t1 := arr_j.
set t2 := arr_j + R_j.
rewrite exchange_big [X in _ ≤ X]exchange_big /= /service_at.
rewrite -/SCHs -/SCHj addnS addn0.
set TSs := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- all 0 t2 | hep j_hp) SCHs j_hp t0.
set TSj := fun a b ⇒ \sum_(a ≤ t0 < b)
\sum_(j_hp <- act 0 t2 | hep j_hp) SCHj j_hp t0.
rewrite -/(TSj t1 (t1 + d).+1) -/(TSj 0 t1).
rewrite leq_subLR -big_cat_nat //=;
last by apply leq_trans with (n := t1 + d); first by apply leq_addr.
rewrite exchange_big /=.
feed (EQWORKj (t1 + d).+1); first by rewrite ltn_add2l.
apply EQWORKj.
intros j0 ARRin0 ARR0 HEP0; specialize (ALL j0 ARRin0 HEP0 ARR0).
by apply completion_monotonic with (t := t1 + d).
Qed.
Lemma jitter_reduction_inductive_step_case1:
service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
Proof.
apply: (leq_trans jitter_reduction_convert_service_to_workload).
apply: (leq_trans jitter_reduction_compare_workload).
apply: (leq_trans jitter_reduction_compare_service).
by apply: (leq_trans jitter_reduction_convert_workload_to_service).
Qed.
End NoPendingJobs.
Section ThereArePendingJobs.
Hypothesis H_there_are_pending_jobs_in_sched_jitter:
∃ j_hp,
arrives_in arr_seq j_hp ∧
other_higher_eq_priority_job j_hp ∧
job_has_actually_arrived j_hp (arr_j + d) ∧
~~ job_completed_in_sched_jitter j_hp (arr_j + d).
Lemma jitter_reduction_inductive_step_case2:
service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d + 1) ≤
service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d + 1).
Proof.
have RESPj := reduction_prop.sched_jitter_respects_policy job_arrival job_task ts
arr_seq _ _ higher_eq_priority _ _ _ job_cost job_suspension_duration j _ R_hp.
feed_n 6 RESPj; try (by done).
unfold reduction_prop.jitter_aware.respects_FP_policy in RESPj.
have NOTj := reduction_prop.sched_jitter_does_not_pick_j job_arrival job_task ts arr_seq
_ _ higher_eq_priority _ _ job_cost job_suspension_duration j R_hp.
feed_n 4 NOTj; try (by done).
have WORKj := reduction_prop.sched_jitter_work_conserving job_arrival job_task arr_seq _
higher_eq_priority job_cost job_suspension_duration j R_hp.
feed WORKj; first by done.
have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
feed AFTERj; try (by done).
set sched_j := reduction_prop.reduction.sched_jitter _ _ _ _ _ _ _ _ in AFTERj NOTj
WORKj RESPj.
set inf_cost := reduction_prop.reduction.inflated_job_cost _ _ _ in NOTj WORKj
AFTERj RESPj.
set job_jit := reduction_prop.reduction.job_jitter _ _ _ _ _ _ in AFTERj NOTj
WORKj RESPj.
rename H_priority_is_transitive into TRANS, H_induction_hypothesis into IH,
H_there_are_pending_jobs_in_sched_jitter into HASj.
rewrite /service_of_other_hep_jobs_in_sched_jitter
/actual_arrivals_before_end_of_interval /actual_arrivals_before.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs
/arrivals_before_end_of_interval /jobs_arrived_before.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
set Ss := service_during sched_susp.
set Sj := service_during sched_jitter.
set SCHs := scheduled_at sched_susp.
set SCHj := scheduled_at sched_jitter.
set SUSP := job_cumulative_suspension.
set Wj := workload_of_other_hep_jobs_in_sched_jitter.
set Ws := workload_of_other_hep_jobs_in_sched_susp.
set t1 := arr_j.
set t2 := arr_j + R_j.
rewrite exchange_big [X in _ ≤ X]exchange_big /=.
rewrite addnS /service_at addn0.
rewrite big_nat_recr ?leq_addr // big_nat_recr ?leq_addr //=.
apply leq_add;
first by rewrite exchange_big [X in _ ≤ X]exchange_big; apply IH.
case (boolP (has (fun j0 ⇒ hep j0 && scheduled_at sched_susp j0 (t1 + d))
(all 0 t2))) ⇒ [HASs | ALLs]; last first.
{
rewrite -all_predC in ALLs; move: ALLs ⇒ /allP ALLs.
rewrite big_seq_cond big1 //.
move ⇒ j0 /andP [IN0 HP0]; apply/eqP; rewrite eqb0.
by specialize (ALLs j0 IN0); rewrite /= HP0 /= in ALLs.
}
move: HASs ⇒ /hasP [j0 IN0 /andP [HP0 SCHED0]].
rewrite big_mkcond (bigD1_seq j0) /=; [| by done | by eapply arrivals_uniq; eauto 1].
rewrite HP0 SCHED0 big1 //; last first.
{
intros j1 NEQ; case: (hep j1); last by done.
apply/eqP; rewrite eqb0; apply/negP; intro SCHED1.
apply (only_one_job_scheduled _ j1) in SCHED0; last by done.
by rewrite SCHED0 eq_refl in NEQ.
}
rewrite addn0.
move: HASj ⇒ [j1 [ARRin1 [HEP1 [IN1 NOTCOMP1]]]].
move: (HEP1) ⇒ /andP [HP1 NEQ1].
rewrite /act /actual_arrivals in IN1.
case (boolP (scheduled_at sched_jitter j1 (t1+d))) ⇒ [SCHED1 | NOTSCHED1].
{
rewrite (big_rem j1) /=; first by rewrite /hep HEP1 SCHED1.
apply arrived_between_implies_in_actual_arrivals; try (by done).
rewrite /actual_arrival_between /=.
by apply leq_ltn_trans with (n := arr_j + d); last by rewrite ltn_add2l.
}
have BACK1: backlogged job_arrival inflated_job_cost job_jitter sched_jitter j1 (t1+d).
by repeat (apply/andP; split); try (by done).
move: (BACK1) (BACK1) ⇒ SCHED2 PRIO2.
apply WORKj in SCHED2; try (by done).
move: SCHED2 ⇒ [j2 SCHED2].
apply RESPj with (j_hp := j2) in PRIO2; try (by done).
have ARRin2: arrives_in arr_seq j2.
{
rewrite /sched_j in SCHED2.
try ( by apply reduction_prop.sched_jitter_jobs_come_from_arrival_sequence with
(sched_susp0 := sched_susp) in SCHED2 ) ||
by apply reduction_prop.sched_jitter_jobs_come_from_arrival_sequence with
(sched_susp := sched_susp) in SCHED2.
}
have HP2: hep j2.
{
apply/andP; split; first by apply (TRANS (job_task j1)).
apply/eqP; intro SAME; subst j2.
move: BACK1 ⇒ /andP [PEND1 _].
by specialize (NOTj j1 (t1+d) ARRin1 NEQ1 PEND1 HP1); rewrite SCHED2 in NOTj.
}
have IN2: j2 \in act 0 t2.
{
apply arrived_between_implies_in_actual_arrivals; try (by done).
rewrite /actual_arrival_between /=.
apply leq_ltn_trans with (n := t1+d); last by rewrite ltn_add2l.
by apply AFTERj.
}
by rewrite (big_rem j2) //= HP2 SCHED2.
Qed.
End ThereArePendingJobs.
End InductiveStep.
Lemma jitter_reduction_more_service_inside_the_interval:
∀ d,
d ≤ R_j →
service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + d) ≤
service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + d).
Proof.
have CASE1 := jitter_reduction_inductive_step_case1.
have CASE2 := jitter_reduction_inductive_step_case2.
set all := arrivals; set act := actual_arrivals.
set hep := other_higher_eq_priority_job.
rename H_priority_is_transitive into TRANS.
induction d.
{
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs.
by intros _; rewrite exchange_big /= addn0 big_geq.
}
intros LTR; feed (IHd); first by apply ltnW.
rewrite -addn1 addnA.
case (boolP (has (fun j0 ⇒ hep j0 && job_has_actually_arrived j0 (arr_j + d)
&& ~~ completed_by inflated_job_cost sched_jitter j0 (arr_j + d))
(act 0 (arr_j + R_j)))) ⇒ [HASj | ALLj]; last first.
{
apply CASE1; try (by done).
rewrite -all_predC in ALLj; move: ALLj ⇒ /allP ALLj.
intros j0 ARRin0 HEP0 ARR0.
feed (ALLj j0).
{
apply arrived_between_implies_in_actual_arrivals; try (by done).
rewrite /actual_arrival_between /=.
by apply leq_ltn_trans with (n := arr_j + d); last by rewrite ltn_add2l.
}
by rewrite /= /hep HEP0 ARR0 /= negbK in ALLj.
}
{
apply (CASE2 _ LTR IHd).
move: HASj ⇒ /hasP [j0 IN0 /andP [/andP [HP0 ARR0] NOTCOMP0]].
∃ j0; repeat (split); try (by done).
rewrite /act /actual_arrivals in IN0.
by apply in_actual_arrivals_between_implies_arrived in IN0.
}
Qed.
End MoreServiceInsideTheInterval.
End MoreServiceAfterArrival.
Section JitterAwareScheduleIsWorse.
Let job_response_time_in_sched_jitter_bounded_by :=
is_response_time_bound_of_job job_arrival inflated_job_cost sched_jitter.
Lemma jitter_reduction_service_jitter:
service_during sched_jitter j arr_j (arr_j + R_j) ≤
R_j - service_of_other_hep_jobs_in_sched_jitter arr_j (arr_j + R_j).
Proof.
have ARRj := reduction_prop.sched_jitter_jobs_come_from_arrival_sequence job_arrival job_task
arr_seq higher_eq_priority job_cost job_suspension_duration sched_susp _ j _ R_hp.
feed_n 2 ARRj; try done.
have AFTERj := reduction_prop.sched_jitter_jobs_execute_after_jitter job_arrival job_task
arr_seq higher_eq_priority job_cost job_suspension_duration j _ R_hp.
feed AFTERj; try done.
set Sj := service_during sched_jitter j arr_j.
set Shp := service_of_other_hep_jobs_in_sched_jitter arr_j.
rewrite leq_subRL_impl //.
apply leq_trans with (n := \sum_(arr_j ≤ t < arr_j + R_j) 1);
last by simpl_sum_const; rewrite addKn.
rewrite /Sj /Shp /service_of_other_hep_jobs_in_sched_jitter /service_of_jobs
/service_during.
rewrite exchange_big -big_split /=.
apply leq_sum_nat; move ⇒ i /andP [GEi LTi] _.
destruct (sched_jitter i) as [j'|] eqn:SCHED;
last by rewrite /service_at /scheduled_at SCHED /= add0n; simpl_sum_const.
case (boolP ((j' == j) || ~~ higher_eq_priority (job_task j') (job_task j))).
{
intros OR; rewrite big1; first by rewrite addn0 leq_b1.
intros j_hp HP; rewrite /other_higher_eq_priority_job in HP.
apply/eqP; rewrite eqb0; apply contraT; rewrite negbK; move ⇒ /eqP SCHED'.
rewrite SCHED in SCHED'; case: SCHED' ⇒ SAME; subst j_hp.
move: OR ⇒ /orP [/eqP EQ | NOTHP]; subst; first by rewrite eq_refl andbF in HP.
by apply negbTE in NOTHP; rewrite NOTHP /= in HP.
}
{
rewrite negb_or negbK; move ⇒ /andP [NEQ HP].
rewrite -[1]add0n; apply leq_add.
{
rewrite leqn0 eqb0; apply/negP; intro SCHED'.
apply only_one_job_scheduled with (j1 := j') in SCHED'; [subst | by apply/eqP].
by rewrite eq_refl in NEQ.
}
{
move: SCHED ⇒ /eqP SCHED.
have IN: arrives_in arr_seq j' by apply ARRj in SCHED.
have ARR: actual_arrival_before job_arrival job_jitter j' (arr_j + R_j).
by apply AFTERj in SCHED; apply: (leq_ltn_trans _ LTi).
rewrite big_mkcond (bigD1_seq j') /=; first last.
- by eapply actual_arrivals_uniq; eauto 1.
- by eapply arrived_between_implies_in_actual_arrivals.
rewrite /other_higher_eq_priority_job HP NEQ /=.
move: SCHED ⇒ /eqP SCHED.
rewrite /service_at /scheduled_at SCHED eq_refl.
rewrite big1 //; intros j_other NEQother.
case: ifP ⇒ HPother; last by done.
apply/eqP; rewrite eqb0; apply/eqP; case ⇒ SAME; subst j_other.
by rewrite eq_refl in NEQother.
}
}
Qed.
Section JobNotCompleted.
Hypothesis H_j_not_completed:
~~ job_completed_in_sched_susp j (arr_j + R_j).
Lemma jitter_reduction_service_susp:
R_j - service_of_other_hep_jobs_in_sched_susp arr_j (arr_j + R_j) ≤
service_during sched_susp j arr_j (arr_j + R_j) +
job_cumulative_suspension j arr_j (arr_j + R_j).
Proof.
move: (H_valid_schedule) ⇒ [FROM [ARRIVE [COMPs [WORK [PRIO _]]]]].
rename H_j_not_completed into NOTCOMP.
rewrite leq_subLR -big_split /=.
rewrite /service_of_other_hep_jobs_in_sched_susp /service_of_jobs.
rewrite exchange_big -big_split /=.
apply leq_trans with (n := \sum_(arr_j ≤ t < arr_j + R_j) 1);
first by simpl_sum_const; rewrite addKn.
apply leq_sum_nat; move ⇒ i /andP [GEi LTi] _.
rewrite -/job_suspended_at /service_at.
case: (boolP (job_suspended_at _ _)) ⇒ [SUSP | NOTSUSP];
[by rewrite addnA leq_addl | rewrite addn0].
case: (boolP (scheduled_at _ _ _)) ⇒ [SCHED | NOTSCHED];
[by rewrite leq_addl | rewrite addn0].
have BACK: susp.backlogged job_arrival job_cost job_suspension_duration sched_susp j i.
{
repeat (apply/andP; split); try (by done).
apply/negP; intro COMP.
move: NOTCOMP ⇒ /negP NOTCOMP; apply: NOTCOMP.
by apply completion_monotonic with (t := i); try (by done); apply ltnW.
}
move: (BACK) ⇒ SCHED; apply WORK in SCHED; last by done.
move: SCHED ⇒ [j_hp SCHEDhp].
have NEQ: j_hp != j by apply/eqP ⇒ SAME; subst; rewrite SCHEDhp in NOTSCHED.
have HP: higher_eq_priority (job_task j_hp) (job_task j) by apply PRIO with (t := i).
rewrite (big_rem j_hp) /other_higher_eq_priority_job /=; last first.
{
have IN: arrives_in arr_seq j_hp by apply FROM in SCHEDhp.
try ( apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival);
try (by done) ) ||
apply arrived_between_implies_in_arrivals with (job_arrival := job_arrival);
try (by done).
by apply: (leq_trans _ LTi); apply ARRIVE.
}
by rewrite HP NEQ SCHEDhp /=.
Qed.
Lemma jitter_reduction_less_service_for_job_j:
service_during sched_jitter j arr_j (arr_j + R_j) ≤
service_during sched_susp j arr_j (arr_j + R_j)
+ job_cumulative_suspension j arr_j (arr_j + R_j).
Proof.
apply: (leq_trans jitter_reduction_service_jitter).
apply: (leq_trans _ jitter_reduction_service_susp).
by apply leq_sub2l, jitter_reduction_more_service_inside_the_interval.
Qed.
End JobNotCompleted.
Hypothesis H_response_time_of_j_in_sched_jitter:
job_response_time_in_sched_jitter_bounded_by j R_j.
Corollary jitter_reduction_job_j_completes_no_later:
job_response_time_in_sched_susp_bounded_by j R_j.
Proof.
move: (H_valid_schedule) ⇒ [_ [MUSTARRs [COMPs [WORK [PRIO SELF]]]]].
rename H_response_time_of_j_in_sched_jitter into COMPj.
apply contraT; intro NOTCOMPs.
suff NOTCOMPj: ~~ job_response_time_in_sched_jitter_bounded_by j R_j;
[by rewrite COMPj in NOTCOMPj | clear COMPj].
have LESS := jitter_reduction_less_service_for_job_j NOTCOMPs.
rewrite -ltnNge.
rewrite /inflated_job_cost /reduction.inflated_job_cost eq_refl.
apply leq_ltn_trans with (n := service_during sched_jitter j arr_j (arr_j + R_j)).
{ rewrite /service /service_during.
rewrite (ignore_service_before_arrival job_arrival) ?leq_addr //.
try ( apply jobs_with_jitter_must_arrive_to_execute with (job_jitter0 := job_jitter) ) ||
apply jobs_with_jitter_must_arrive_to_execute with (job_jitter := job_jitter).
by apply reduction_prop.sched_jitter_jobs_execute_after_jitter.
}
apply: (leq_ltn_trans LESS).
rewrite -addn1 -addnA [_ + 1]addnC addnA; apply leq_add.
{ rewrite addn1; apply contraT; rewrite -leqNgt; intro LE.
exfalso; move: NOTCOMPs ⇒ /negP NOTCOMPs; apply: NOTCOMPs.
rewrite /job_response_time_in_sched_susp_bounded_by /is_response_time_bound_of_job.
rewrite /completed_by.
apply: (leq_trans LE).
rewrite /service /service_during.
by rewrite [X in _ ≤ X](ignore_service_before_arrival job_arrival) ?leq_addr.
}
by apply cumulative_suspension_le_total_suspension.
Qed.
End JitterAwareScheduleIsWorse.
End ProvingScheduleProperties.
End JitterScheduleService.