Library prosa.classic.analysis.global.jitter.interference_bound_edf
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.response_time prosa.classic.model.schedule.global.workload
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.platform prosa.classic.model.schedule.global.jitter.interference
prosa.classic.model.schedule.global.jitter.interference_edf.
Require Import prosa.classic.analysis.global.jitter.workload_bound prosa.classic.analysis.global.jitter.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDFJitter.
Import JobWithJitter SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask Schedulability
ResponseTime WorkloadBoundJitter Priority TaskArrival Interference InterferenceEDF.
Export InterferenceBoundJitter.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk: sporadic_task.
Variable delta: time.
Variable tsk_other: sporadic_task.
Variable R_other: time.
Definition edf_specific_interference_bound :=
let d_tsk := task_deadline tsk in
let e_other := task_cost tsk_other in
let p_other := task_period tsk_other in
let d_other := task_deadline tsk_other in
let j_other := task_jitter tsk_other in
(div_floor d_tsk p_other) × e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other - j_other)).
End SpecificBoundDef.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
Variable R_prev: seq task_with_response_time.
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
Let basic_interference_bound := interference_bound_generic task_cost task_period task_jitter tsk delta tsk_R.
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk tsk_other R_other.
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
Section TotalInterference.
Let other_task := different_task tsk.
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
Section ProofSpecificBound.
Import ScheduleWithJitter Interference Platform SporadicTaskset.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
Context {arr_seq: arrival_sequence Job}.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
Variable num_cpus: nat.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_edf_policy: respects_JLFP_policy job_arrival job_cost job_jitter arr_seq
sched (EDF job_arrival job_deadline).
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
Variable j_i: Job.
Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
Variable R_k: time.
Hypothesis H_R_k_le_deadline: task_jitter tsk_k + R_k ≤ task_deadline tsk_k.
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
Hypothesis H_all_previous_jobs_completed_on_time :
∀ j_k,
arrives_in arr_seq j_k →
job_task j_k = tsk_k →
job_arrival j_k + task_jitter tsk_k + R_k < job_arrival j_i + task_jitter tsk_i + delta →
completed job_cost sched j_k (job_arrival j_k + task_jitter tsk_k + R_k).
Section MainProof.
Let t1 := job_arrival j_i + job_jitter j_i.
Let t2 := t1 + delta.
Let x :=
task_interference job_arrival job_cost job_task job_jitter sched j_i tsk_k t1 t2.
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk_i tsk_k R_k.
Let a_i := job_arrival j_i.
Let D_i := task_deadline tsk_i.
Let D_k := task_deadline tsk_k.
Let p_k := task_period tsk_k.
Let J_i := task_jitter tsk_i.
Let J_k := task_jitter tsk_k.
Let n_k := div_floor D_i p_k.
Let interference_caused_by := job_interference job_arrival job_cost job_jitter sched j_i.
Let interfering_jobs :=
filter (fun j' ⇒
(job_task j' == tsk_k) && (interference_caused_by j' t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival interfering_jobs).
Section SimplifyJobSequence.
Lemma interference_bound_edf_use_another_definition :
x ≤ \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Proof.
apply interference_le_interference_joblist.
Qed.
Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2 =
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2.
Proof.
unfold interfering_jobs; rewrite big_filter.
rewrite big_mkcond; rewrite [\sum_(_ <- _ | _) _]big_mkcond /=.
apply eq_bigr; intros i _; clear -i.
destruct (job_task i == tsk_k); rewrite ?andTb ?andFb; last by done.
destruct (interference_caused_by i t1 t2 != 0) eqn:DIFF; first by done.
by apply negbT in DIFF; rewrite negbK in DIFF; apply/eqP.
Qed.
Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j \in sorted_jobs →
arrives_in arr_seq j ∧
job_task j = tsk_k ∧
interference_caused_by j t1 t2 != 0 ∧
j \in jobs_scheduled_between sched t1 t2.
Proof.
intros j LT.
rewrite -interference_bound_edf_job_in_same_sequence mem_filter in LT.
move: LT ⇒ /andP [/andP [/eqP JOBi SERVi] INi]; repeat split; try (by done).
unfold jobs_scheduled_between in *; rewrite mem_undup in INi.
apply mem_bigcat_nat_exists in INi; des.
rewrite mem_scheduled_jobs_eq_scheduled in INi.
by apply (H_jobs_come_from_arrival_sequence j i).
Qed.
Lemma interference_bound_edf_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Proof.
intros i elem LT.
assert (SORT: sorted earlier_arrival sorted_jobs).
by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j \in interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
Proof.
rename H_valid_job_parameters into PARAMS.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
intros j IN.
feed (interference_bound_edf_all_jobs_from_tsk_k j);
first by rewrite -interference_bound_edf_job_in_same_sequence.
move ⇒ [ARRj [TSKj [_ SCHEDj]]].
specialize (PARAMS j ARRj); des.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
try ( by apply cumulative_service_le_task_cost with (job_task0 := job_task)
(task_deadline0 := task_deadline) (job_cost0 := job_cost)
(job_deadline0 := job_deadline); try (by done) ) ||
by apply cumulative_service_le_task_cost with (job_task := job_task)
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline); try (by done).
Qed.
End SimplifyJobSequence.
Section InterferenceFewJobs.
Hypothesis H_few_jobs: size sorted_jobs ≤ n_k.
Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2 ≤
interference_bound.
Proof.
rewrite -[\sum_(_ <- _ | _) _]addn0 leq_add //.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk_k);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
{
rewrite [\sum_(_ <- _) interference_caused_by _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
apply leq_sum; intros i; move/andP ⇒ [INi _].
rewrite -interference_bound_edf_job_in_same_sequence in INi.
by apply interference_bound_edf_interference_le_task_cost.
}
Qed.
End InterferenceFewJobs.
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
Proof.
by apply leq_ltn_trans with (n := n_k).
Qed.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
Section FactsAboutFirstJob.
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Proof.
by apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth,
interference_bound_edf_at_least_one_job.
Qed.
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
by specialize (PARAMS j_fst FSTarr); des; rewrite PARAMS2 FSTtask.
Qed.
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS,
H_job_of_tsk_i into JOBtsk.
by specialize (PARAMS j_i H_j_i_arrives); des; rewrite PARAMS2 JOBtsk.
Qed.
Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
completed job_cost sched j_fst (a_fst + J_k + R_k) →
t1 ≤ a_fst + J_k + R_k.
Proof.
intros RBOUND.
rewrite leqNgt; apply/negP; unfold not; intro BUG.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [_ [_ [FSTserv _]]].
move: FSTserv ⇒ /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
unfold service_during.
by ( try ( apply cumulative_service_after_job_rt_zero with
(job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k) ) ||
apply cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k) );
try (by done); rewrite addnA; last by apply ltnW.
Qed.
End FactsAboutFirstJob.
Section InterferenceSingleJob.
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_simpl_when_there's_one_job :
D_i %% p_k - (D_k - R_k - J_k) = D_i - (D_k - R_k - J_k).
Proof.
rename H_many_jobs into NUM,
H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in ×.
rewrite H_only_one_job in NUM.
rewrite ltnS leqn0 in NUM; move: NUM ⇒ /eqP EQnk.
move: EQnk ⇒ /eqP EQnk; unfold n_k, div_floor in EQnk.
rewrite -leqn0 leqNgt divn_gt0 in EQnk;
last by specialize (TASK_PARAMS tsk_k INk); des.
by rewrite -ltnNge in EQnk; rewrite modn_small //.
Qed.
Section ResponseTimeOfSingleJobBounded.
Hypothesis H_j_fst_completed_by_rt_bound :
completed job_cost sched j_fst (a_fst + J_k + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
job_interference job_arrival job_cost job_jitter sched j_i j_fst t1 t2
≤ D_i - (D_k - R_k - J_k).
Proof.
rename H_j_fst_completed_by_rt_bound into RBOUND.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval RBOUND.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [ARRfst [_ [LEdl _]]].
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k - J_k ≤ D_i) eqn:LEdk; last first.
{
apply negbT in LEdk; rewrite -ltnNge in LEdk.
apply leq_trans with (n := 0); last by done.
apply leq_trans with (n := job_interference job_arrival job_cost
job_jitter sched j_i j_fst (a_fst + J_k + R_k) t2); last first.
{
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
try ( by apply cumulative_service_after_job_rt_zero with
(job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k);
try (by done); rewrite addnA // leqnn ) ||
by apply cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k);
try (by done); rewrite addnA // leqnn.
}
{
apply extend_sum; last by apply leqnn.
rewrite -(leq_add2r D_i).
rewrite interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline in LEdl.
apply leq_trans with (n := a_fst + D_k); last first.
{
apply leq_trans with (n := job_arrival j_i + D_i); first by done.
by rewrite leq_add2r leq_addr.
}
rewrite -2!addnA leq_add2l.
rewrite addnA.
by apply ltnW; rewrite -ltn_subRL addnC subnDA.
}
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i t2);
first by apply extend_sum; [by apply leq_addr | by apply leqnn].
rewrite -(leq_add2r (D_k - R_k - J_k)) addnBAC // -addnBA // subnn addn0.
assert (SUBST: D_k - R_k - J_k = \sum_(a_fst + J_k + R_k ≤ i < a_fst + D_k) 1).
{
rewrite big_const_nat iter_addn mul1n addn0.
rewrite [_ + D_k]addnC.
rewrite -subnBA; last by rewrite -addnA leq_addr.
rewrite [a_fst + _]addnC -addnA [a_fst + R_k]addnC addnA.
rewrite -addnBA // subnn addn0.
by rewrite [_ + R_k]addnC subnDA.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst a_i (a_fst + D_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r.
destruct (t2 ≤ a_fst + J_k + R_k) eqn:LEt2.
{
apply extend_sum; first by apply leqnn.
apply leq_trans with (n := a_fst + J_k + R_k); first by done.
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
{
unfold job_interference.
apply negbT in LEt2; rewrite -ltnNge in LEt2.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | | by apply ltnW]; last first.
{
by apply leq_trans with (n := t1); first by apply leq_addr.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i
(a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) t2).
{
rewrite leq_add2l.
by apply job_interference_le_service.
}
unfold service_during.
( try ( rewrite → cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
(job_arrival0 := job_arrival) (R := J_k + R_k) ) ||
rewrite → cumulative_service_after_job_rt_zero with (job_cost := job_cost)
(job_arrival := job_arrival) (R := J_k + R_k));
rewrite ?addnA //.
rewrite addn0; apply extend_sum; first by done.
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
}
unfold job_interference.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | | ]; last first.
{
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
{
by apply leq_trans with (n := t1); first by apply leq_addr.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i
(a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) (a_fst + D_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r leq_add2l.
by apply job_interference_le_service.
}
unfold service_during.
( try ( rewrite → cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
(job_cost0 := job_cost) (R:=J_k + R_k) ) ||
rewrite → cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
(job_cost := job_cost) (R:=J_k + R_k));
rewrite ?addnA //.
rewrite addn0.
apply leq_trans with (n := (\sum_(a_i ≤ t < a_fst + J_k + R_k) 1) +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1).
{
apply leq_add; last by rewrite SUBST.
simpl_sum_const; rewrite -{1}[_ + R_k](addKn a_i) -addnBA //;
last by apply leq_trans with (n := t1); first by apply leq_addr.
by apply job_interference_le_delta.
}
rewrite -big_cat_nat; simpl; last by rewrite -addnA leq_add2l H_R_k_le_deadline.
{
simpl_sum_const; rewrite leq_subLR; unfold D_i, D_k, t1, a_fst.
by rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
}
by apply leq_trans with (n := t1); first by apply leq_addr.
Qed.
End ResponseTimeOfSingleJobBounded.
Section ResponseTimeOfSingleJobNotBounded.
Hypothesis H_j_fst_not_complete_by_rt_bound :
~~ completed job_cost sched j_fst (a_fst + J_k + R_k).
Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
job_arrival j_fst + J_k + R_k ≥ job_arrival j_i + J_i + delta.
Proof.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
rewrite leqNgt; apply/negP; intro LT.
move: H_j_fst_not_complete_by_rt_bound ⇒ /negP BUG; apply BUG.
by apply H_all_previous_jobs_completed_on_time.
Qed.
Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
D_i < D_k - R_k - J_k →
interference_caused_by j_fst t1 t2 = 0.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives; des.
intro LTdk.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
rewrite 2!ltn_subRL addnA [R_k + _]addnC in LTdk.
rewrite -(ltn_add2l a_fst) 2!addnA in LTdk.
apply leq_ltn_trans with (m := t1 + D_i) in LTdk; last first.
{
rewrite leq_add2r.
apply leq_trans with (n := t1 + delta); first by apply leq_addr.
apply leq_trans with (n := job_arrival j_i + J_i + delta).
{
unfold J_i;rewrite leq_add2r leq_add2l.
rewrite -H_job_of_tsk_i; apply PARAMS0.
}
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in BUG; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline in BUG.
apply leq_ltn_trans with (m := job_arrival j_i + D_i) in LTdk;
last by rewrite leq_add2r leq_addr.
by apply (leq_trans LTdk) in BUG; rewrite ltnn in BUG.
Qed.
Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
D_i ≥ D_k - R_k - J_k →
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k - J_k).
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives; des.
intro LEdk.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTtask [_ [LEdl _]]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply leq_subRL_impl.
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst t1 (job_arrival j_fst + J_k + R_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r; apply extend_sum; first by apply leqnn.
apply leq_trans with (n := job_arrival j_i + J_i + delta);
last by done.
rewrite leq_add2r leq_add2l.
by unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k)1).
{
apply leq_add; unfold job_interference.
{
simpl_sum_const.
rewrite -{1}[job_arrival j_fst + J_k + R_k](addKn t1) -addnBA;
first by apply job_interference_le_delta.
apply leq_trans with (n := a_i + J_i + delta); last by done.
apply leq_trans with (n := a_i + J_i); last by apply leq_addr.
by rewrite leq_add2l /J_i -H_job_of_tsk_i; apply PARAMS0.
}
simpl_sum_const; rewrite addnC.
rewrite -subnBA; last by rewrite -addnA leq_addr.
rewrite [a_fst + _]addnC -addnA [a_fst + _]addnC addnA.
rewrite -addnBA // subnn addn0.
by rewrite addnC subnDA.
}
rewrite -big_cat_nat; simpl; last 2 first.
{
apply leq_trans with (n := t1 + delta); first by apply leq_addr.
apply leq_trans with (n := job_arrival j_i + J_i + delta).
{
rewrite leq_add2r leq_add2l.
unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
}
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
{
by rewrite -addnA leq_add2l; apply H_R_k_le_deadline.
}
rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
unfold D_i, D_k, t1, a_fst.
rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite leq_add2r leq_addr.
try ( by apply interference_under_edf_implies_shorter_deadlines with (arr_seq0 := arr_seq)
(job_arrival0 := job_arrival) (job_deadline0 := job_deadline) in LEdl ) ||
by apply interference_under_edf_implies_shorter_deadlines with (arr_seq := arr_seq)
(job_arrival := job_arrival) (job_deadline := job_deadline) in LEdl.
Qed.
End ResponseTimeOfSingleJobNotBounded.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k - J_k).
Proof.
destruct (completed job_cost sched j_fst (a_fst + J_k + R_k)) eqn:COMP;
first by apply interference_bound_edf_holds_for_single_job_that_completes_on_time.
apply negbT in COMP.
destruct (ltnP D_i (D_k - R_k - J_k)) as [LEdk | LTdk].
by rewrite interference_bound_edf_holds_for_single_job_with_big_slack.
by apply interference_bound_edf_holds_for_single_job_with_small_slack.
Qed.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
Proof.
have ONE := interference_bound_edf_simpl_when_there's_one_job.
have SLACK := interference_bound_edf_interference_of_j_fst_limited_by_slack.
rename H_many_jobs into NUM, H_only_one_job into SIZE.
unfold interference_caused_by, interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
rewrite SIZE ltnS leqn0 in NUM; move: NUM ⇒ /eqP EQnk.
rewrite EQnk mul0n add0n.
rewrite leq_min; apply/andP; split.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite SIZE.
}
by rewrite ONE; apply SLACK.
Qed.
End InterferenceSingleJob.
Section InterferenceTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
Section FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Proof.
apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth.
by rewrite H_at_least_two_jobs.
Qed.
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [LSTtask _]].
by specialize (PARAMS j_lst LSTarr); des; rewrite PARAMS2 LSTtask.
Qed.
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
Proof.
rename H_at_least_two_jobs into SIZE.
unfold j_fst, j_lst; rewrite -[num_mid_jobs.+1]add0n.
apply prev_le_next; last by rewrite SIZE leqnn.
by intros i LT; apply interference_bound_edf_jobs_ordered_by_arrival.
Qed.
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Proof.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
feed (interference_bound_edf_all_jobs_from_tsk_k j_lst).
by apply mem_nth; rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
move ⇒ [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
apply LSTserv; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
rewrite (cumulative_service_before_job_arrival_zero job_arrival) //.
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
Qed.
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + J_k + R_k).
Proof.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *; des.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k; des.
set j_snd := nth elem sorted_jobs 1.
exploit interference_bound_edf_all_jobs_from_tsk_k.
{
by apply mem_nth; instantiate (1 := 1); rewrite H_at_least_two_jobs.
}
instantiate (1 := elem); move ⇒ [SNDarr [SNDtsk [/eqP SNDserv _]]].
apply H_all_previous_jobs_completed_on_time; try (by done).
apply leq_ltn_trans with (n := job_arrival j_snd); last first.
{
apply leq_trans with (n := t2); last first.
{
unfold t2, t1; rewrite leq_add2r leq_add2l.
by rewrite -H_job_of_tsk_i; apply PARAMS0.
}
rewrite ltnNge; apply/negP; red; intro BUG; apply SNDserv.
apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
( try ( apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival));
try (by done).
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
}
apply leq_trans with (n := a_fst + p_k).
{
apply leq_trans with (n := job_arrival j_fst + D_k);
first by rewrite -addnA leq_add2l.
by rewrite leq_add2l; apply H_constrained_deadlines.
}
unfold p_k; rewrite -FST0.
apply H_sporadic_tasks; [| by done | by done | by rewrite SNDtsk | ]; last first.
{
apply interference_bound_edf_jobs_ordered_by_arrival.
by rewrite H_at_least_two_jobs.
}
red; move ⇒ /eqP BUG.
by rewrite nth_uniq in BUG; rewrite ?SIZE //;
[ by apply interference_bound_edf_at_least_one_job
| by rewrite H_at_least_two_jobs
| by rewrite sort_uniq; apply filter_uniq, undup_uniq].
Qed.
End FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Proof.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
rewrite EQnk telescoping_sum;
last by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
rewrite -[_ × _ tsk_k]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat.
rewrite big_nat_cond [\sum_(0 ≤ i < _)(_-_)]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.
assert (ARRle: job_arrival cur ≤ job_arrival next).
by unfold cur, next; apply interference_bound_edf_jobs_ordered_by_arrival.
assert (INnth: cur \in interfering_jobs ∧ next \in interfering_jobs).
{
rewrite 2!interference_bound_edf_job_in_same_sequence; split.
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
by apply mem_nth; destruct sorted_jobs; ins.
}
rewrite 2?mem_filter in INnth; des.
feed (interference_bound_edf_all_jobs_from_tsk_k cur).
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].
feed (interference_bound_edf_all_jobs_from_tsk_k next).
by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].
assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) ≤ job_arrival next).
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ ⇒ /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ ⇒ /eqP EQ; ssrlia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
by rewrite leq_subRL_impl // addnC /p_k -INnth.
Qed.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k ≥ num_mid_jobs.+1.
Proof.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
interference_bound_edf_j_fst_completed_on_time.
rename H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in ×.
have DIST := interference_bound_edf_many_periods_in_between.
rewrite leqNgt; apply/negP; unfold not; intro LTnk; unfold n_k in LTnk.
rewrite ltn_divLR in LTnk; last by specialize (TASK_PARAMS tsk_k INk); des.
apply (leq_trans LTnk) in DIST; rewrite ltn_subRL in DIST.
rewrite -(ltn_add2r (J_k + R_k)) -addnA [D_i + _]addnC addnA in DIST.
unfold t1 in ×.
apply leq_ltn_trans with (m := job_arrival j_i + D_i) in DIST; last first.
{
rewrite addnA leq_add2r.
by apply leq_trans with (n := job_arrival j_i + job_jitter j_i);
first by apply leq_addr.
}
apply leq_trans with (p := a_lst + D_k) in DIST;
last by rewrite leq_add2l.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [LEdl _]]].
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
interference_bound_edf_j_i_deadline in LEdl.
by apply (leq_trans DIST) in LEdl; rewrite ltnn in LEdl.
Qed.
Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
interference_caused_by j_lst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
≤ n_k × task_cost tsk_k.
Proof.
apply leq_trans with (n := num_mid_jobs.+1 × task_cost tsk_k); last first.
{
rewrite leq_mul2r; apply/orP; right.
by apply interference_bound_edf_n_k_covers_middle_jobs_plus_one.
}
rewrite mulSn; apply leq_add.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite H_at_least_two_jobs.
}
{
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs) task_cost tsk_k);
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 ≤ i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
Qed.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Proof.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
move: NK; rewrite leq_eqVlt orbC; move ⇒ /orP NK; des;
first by rewrite SIZE ltnS leqNgt NK in NUM.
by rewrite NK.
Qed.
Section InterferenceOfFirstJob.
Lemma interference_bound_edf_remainder_ge_slack :
D_k - R_k - J_k ≤ D_i %% p_k.
Proof.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
interference_bound_edf_j_fst_completed_on_time.
have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
have DIST := interference_bound_edf_many_periods_in_between.
rewrite -NK in DIST.
rewrite 2!leq_subLR addnA [R_k + _]addnC -subndiv_eq_mod.
fold (div_floor D_i p_k) n_k.
rewrite addnBA; last by apply leq_trunc_div.
apply leq_trans with (n := J_k + R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
rewrite -(leq_add2r a_lst) addnBAC; last first.
{
apply leq_trans with (n := t2);
[by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
rewrite addnC addnA.
apply leq_trans with (n := t1 + D_i).
unfold t2; rewrite leq_add2l; apply H_delta_le_deadline.
by rewrite leq_add2r addnA; apply AFTERt1.
}
rewrite -addnBA // subnn addn0 [D_k + _]addnC.
apply leq_trans with (n := job_arrival j_i + D_i); last first.
{
rewrite [_ + a_fst]addnC 2!addnA leq_add2r.
by apply leq_trans with (n := t1); first by apply leq_addr.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
try ( by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
Lemma interference_bound_edf_simpl_by_moving_to_left_side :
interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k × p_k ≤ D_i →
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k - J_k).
Proof.
intro LE.
apply leq_subRL_impl.
by rewrite -subndiv_eq_mod; apply leq_subRL_impl.
Qed.
Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
interference_caused_by j_fst t1 t2 ≤ \sum_(t1 ≤ t < a_fst + J_k + R_k) 1.
Proof.
assert (AFTERt1: t1 ≤ a_fst + J_k + R_k).
{
apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
by apply interference_bound_edf_j_fst_completed_on_time.
}
destruct (leqP t2 (a_fst + J_k + R_k)) as [LEt2 | GTt2].
{
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst t1 (a_fst + J_k + R_k));
first by apply extend_sum; rewrite ?leqnn.
simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
by apply job_interference_le_delta.
}
{
unfold interference_caused_by, job_interference.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
rewrite -[\sum_(_ ≤ _ < _) 1]addn0; apply leq_add.
{
simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
by apply job_interference_le_delta.
}
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
( try ( apply cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
(job_cost0 := job_cost) (R := J_k + R_k) ) ||
apply cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
(job_cost := job_cost) (R := J_k + R_k));
[ by done | rewrite addnA | by rewrite addnA leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
Qed.
Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k × p_k ≤
\sum_(t1 ≤ t < a_fst + J_k + R_k) 1
+ \sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1.
Proof.
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
D_i %/ p_k × p_k).
{
rewrite 2!leq_add2r.
apply interference_bound_edf_interference_of_j_fst_bounded_by_response_time.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
(a_lst - a_fst)).
{
rewrite leq_add2l; fold (div_floor D_i p_k) n_k.
rewrite interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
by apply interference_bound_edf_many_periods_in_between.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1 + \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1).
{
rewrite -3!addnA leq_add2l; apply leq_add;
rewrite big_const_nat iter_addn mul1n addn0;
[by rewrite subnDl addnC subnDA | by rewrite subnDr leqnn].
}
by apply leqnn.
Qed.
Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
\sum_(t1 ≤ t < a_fst + J_k + R_k) 1
+ \sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
Proof.
assert (AFTERt1: t1 ≤ a_fst + J_k + R_k).
{
apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
by apply interference_bound_edf_j_fst_completed_on_time.
}
rewrite -big_cat_nat;
[simpl | by apply AFTERt1 | by rewrite -addnA leq_add2l; apply H_R_k_le_deadline].
rewrite -big_cat_nat; simpl; last 2 first.
{
by apply (leq_trans AFTERt1); rewrite -addnA leq_add2l.
}
{
rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
last by rewrite add0n H_at_least_two_jobs ltnSn.
by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
}
by rewrite big_const_nat iter_addn mul1n addn0.
Qed.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k - J_k).
Proof.
apply interference_bound_edf_simpl_by_moving_to_left_side.
apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite -addnA leq_add2l leq_addl.
try ( by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
End InterferenceOfFirstJob.
Lemma interference_bound_edf_holds_for_multiple_jobs :
\sum_(0 ≤ i < num_mid_jobs.+2)
interference_caused_by (nth elem sorted_jobs i) t1 t2 ≤ interference_bound.
Proof.
rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
rewrite addnA addnC addnA.
have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
unfold interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
rewrite addnC addnA; apply leq_add;
first by rewrite addnC interference_bound_edf_holds_for_middle_and_last_jobs.
rewrite leq_min; apply/andP; split.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite H_at_least_two_jobs.
}
by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack.
Qed.
End InterferenceTwoOrMoreJobs.
End InterferenceManyJobs.
Theorem interference_bound_edf_bounds_interference :
x ≤ interference_bound.
Proof.
apply (leq_trans interference_bound_edf_use_another_definition).
rewrite interference_bound_edf_simpl_by_filtering_interfering_jobs.
rewrite interference_bound_edf_simpl_by_sorting_interfering_jobs.
destruct (size sorted_jobs ≤ n_k) eqn:NUM;
first by apply interference_bound_edf_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.
assert (EX: ∃ elem: Job, True).
destruct sorted_jobs as [| j]; [by rewrite ltn0 in NUM | by ∃ j].
destruct EX as [elem _].
rewrite (big_nth elem).
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.
destruct n as [| num_mid_jobs].
{
rewrite big_nat_recr // big_geq //.
rewrite [nth]lock /= -lock add0n.
by apply interference_bound_edf_holds_for_a_single_job; rewrite SIZE.
}
{
by apply interference_bound_edf_holds_for_multiple_jobs; first by rewrite SIZE.
}
Qed.
End MainProof.
End ProofSpecificBound.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
Variable delta delta' R R': time.
Hypothesis H_delta_monotonic: delta ≤ delta'.
Hypothesis H_response_time_monotonic: R ≤ R'.
Hypothesis H_cost_le_rt_bound: task_cost tsk_other ≤ R.
Lemma interference_bound_edf_monotonic :
interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta (tsk_other, R) ≤
interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta' (tsk_other, R').
Proof.
rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
unfold interference_bound_edf, interference_bound_generic.
rewrite leq_min; apply/andP; split.
{
rewrite leq_min; apply/andP; split.
apply leq_trans with (n := (minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
(snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
first by apply geq_minl.
apply leq_trans with (n := W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
(snd (tsk_other, R)) delta);
[by apply geq_minl | by apply W_monotonic].
apply leq_trans with (n := minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
first by apply geq_minl.
apply leq_trans with (n := delta - task_cost tsk + 1);
first by apply geq_minr.
by rewrite leq_add2r leq_sub2r.
}
{
apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
task_deadline task_jitter tsk tsk_other R);
first by apply geq_minr.
unfold edf_specific_interference_bound; simpl.
rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
(task_deadline tsk_other - R - task_jitter tsk_other));
[by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
}
Qed.
End MonotonicitySpecificBound.
End InterferenceBoundEDFJitter.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.response_time prosa.classic.model.schedule.global.workload
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule
prosa.classic.model.schedule.global.jitter.platform prosa.classic.model.schedule.global.jitter.interference
prosa.classic.model.schedule.global.jitter.interference_edf.
Require Import prosa.classic.analysis.global.jitter.workload_bound prosa.classic.analysis.global.jitter.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDFJitter.
Import JobWithJitter SporadicTaskset ScheduleWithJitter ScheduleOfSporadicTask Schedulability
ResponseTime WorkloadBoundJitter Priority TaskArrival Interference InterferenceEDF.
Export InterferenceBoundJitter.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk: sporadic_task.
Variable delta: time.
Variable tsk_other: sporadic_task.
Variable R_other: time.
Definition edf_specific_interference_bound :=
let d_tsk := task_deadline tsk in
let e_other := task_cost tsk_other in
let p_other := task_period tsk_other in
let d_other := task_deadline tsk_other in
let j_other := task_jitter tsk_other in
(div_floor d_tsk p_other) × e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other - j_other)).
End SpecificBoundDef.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
Variable R_prev: seq task_with_response_time.
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
Let basic_interference_bound := interference_bound_generic task_cost task_period task_jitter tsk delta tsk_R.
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk tsk_other R_other.
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
Section TotalInterference.
Let other_task := different_task tsk.
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
Section ProofSpecificBound.
Import ScheduleWithJitter Interference Platform SporadicTaskset.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_jitter: Job → time.
Context {arr_seq: arrival_sequence Job}.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job_with_jitter task_cost task_deadline task_jitter job_cost job_deadline job_task job_jitter j.
Variable num_cpus: nat.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ j,
arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_edf_policy: respects_JLFP_policy job_arrival job_cost job_jitter arr_seq
sched (EDF job_arrival job_deadline).
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
Variable j_i: Job.
Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
Variable R_k: time.
Hypothesis H_R_k_le_deadline: task_jitter tsk_k + R_k ≤ task_deadline tsk_k.
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
Hypothesis H_all_previous_jobs_completed_on_time :
∀ j_k,
arrives_in arr_seq j_k →
job_task j_k = tsk_k →
job_arrival j_k + task_jitter tsk_k + R_k < job_arrival j_i + task_jitter tsk_i + delta →
completed job_cost sched j_k (job_arrival j_k + task_jitter tsk_k + R_k).
Section MainProof.
Let t1 := job_arrival j_i + job_jitter j_i.
Let t2 := t1 + delta.
Let x :=
task_interference job_arrival job_cost job_task job_jitter sched j_i tsk_k t1 t2.
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline task_jitter tsk_i tsk_k R_k.
Let a_i := job_arrival j_i.
Let D_i := task_deadline tsk_i.
Let D_k := task_deadline tsk_k.
Let p_k := task_period tsk_k.
Let J_i := task_jitter tsk_i.
Let J_k := task_jitter tsk_k.
Let n_k := div_floor D_i p_k.
Let interference_caused_by := job_interference job_arrival job_cost job_jitter sched j_i.
Let interfering_jobs :=
filter (fun j' ⇒
(job_task j' == tsk_k) && (interference_caused_by j' t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival interfering_jobs).
Section SimplifyJobSequence.
Lemma interference_bound_edf_use_another_definition :
x ≤ \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Proof.
apply interference_le_interference_joblist.
Qed.
Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2 =
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2.
Proof.
unfold interfering_jobs; rewrite big_filter.
rewrite big_mkcond; rewrite [\sum_(_ <- _ | _) _]big_mkcond /=.
apply eq_bigr; intros i _; clear -i.
destruct (job_task i == tsk_k); rewrite ?andTb ?andFb; last by done.
destruct (interference_caused_by i t1 t2 != 0) eqn:DIFF; first by done.
by apply negbT in DIFF; rewrite negbK in DIFF; apply/eqP.
Qed.
Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Proof.
by rewrite (perm_big sorted_jobs) /=; last by rewrite -(perm_sort earlier_arrival).
Qed.
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j \in sorted_jobs →
arrives_in arr_seq j ∧
job_task j = tsk_k ∧
interference_caused_by j t1 t2 != 0 ∧
j \in jobs_scheduled_between sched t1 t2.
Proof.
intros j LT.
rewrite -interference_bound_edf_job_in_same_sequence mem_filter in LT.
move: LT ⇒ /andP [/andP [/eqP JOBi SERVi] INi]; repeat split; try (by done).
unfold jobs_scheduled_between in *; rewrite mem_undup in INi.
apply mem_bigcat_nat_exists in INi; des.
rewrite mem_scheduled_jobs_eq_scheduled in INi.
by apply (H_jobs_come_from_arrival_sequence j i).
Qed.
Lemma interference_bound_edf_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Proof.
intros i elem LT.
assert (SORT: sorted earlier_arrival sorted_jobs).
by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j \in interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
Proof.
rename H_valid_job_parameters into PARAMS.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
intros j IN.
feed (interference_bound_edf_all_jobs_from_tsk_k j);
first by rewrite -interference_bound_edf_job_in_same_sequence.
move ⇒ [ARRj [TSKj [_ SCHEDj]]].
specialize (PARAMS j ARRj); des.
apply leq_trans with (n := service_during sched j t1 t2);
first by apply job_interference_le_service.
try ( by apply cumulative_service_le_task_cost with (job_task0 := job_task)
(task_deadline0 := task_deadline) (job_cost0 := job_cost)
(job_deadline0 := job_deadline); try (by done) ) ||
by apply cumulative_service_le_task_cost with (job_task := job_task)
(task_deadline := task_deadline) (job_cost := job_cost)
(job_deadline := job_deadline); try (by done).
Qed.
End SimplifyJobSequence.
Section InterferenceFewJobs.
Hypothesis H_few_jobs: size sorted_jobs ≤ n_k.
Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2 ≤
interference_bound.
Proof.
rewrite -[\sum_(_ <- _ | _) _]addn0 leq_add //.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk_k);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
{
rewrite [\sum_(_ <- _) interference_caused_by _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
apply leq_sum; intros i; move/andP ⇒ [INi _].
rewrite -interference_bound_edf_job_in_same_sequence in INi.
by apply interference_bound_edf_interference_le_task_cost.
}
Qed.
End InterferenceFewJobs.
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
Proof.
by apply leq_ltn_trans with (n := n_k).
Qed.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
Section FactsAboutFirstJob.
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Proof.
by apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth,
interference_bound_edf_at_least_one_job.
Qed.
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
by specialize (PARAMS j_fst FSTarr); des; rewrite PARAMS2 FSTtask.
Qed.
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS,
H_job_of_tsk_i into JOBtsk.
by specialize (PARAMS j_i H_j_i_arrives); des; rewrite PARAMS2 JOBtsk.
Qed.
Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
completed job_cost sched j_fst (a_fst + J_k + R_k) →
t1 ≤ a_fst + J_k + R_k.
Proof.
intros RBOUND.
rewrite leqNgt; apply/negP; unfold not; intro BUG.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [_ [_ [FSTserv _]]].
move: FSTserv ⇒ /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during sched j_fst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
unfold service_during.
by ( try ( apply cumulative_service_after_job_rt_zero with
(job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k) ) ||
apply cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k) );
try (by done); rewrite addnA; last by apply ltnW.
Qed.
End FactsAboutFirstJob.
Section InterferenceSingleJob.
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_simpl_when_there's_one_job :
D_i %% p_k - (D_k - R_k - J_k) = D_i - (D_k - R_k - J_k).
Proof.
rename H_many_jobs into NUM,
H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in ×.
rewrite H_only_one_job in NUM.
rewrite ltnS leqn0 in NUM; move: NUM ⇒ /eqP EQnk.
move: EQnk ⇒ /eqP EQnk; unfold n_k, div_floor in EQnk.
rewrite -leqn0 leqNgt divn_gt0 in EQnk;
last by specialize (TASK_PARAMS tsk_k INk); des.
by rewrite -ltnNge in EQnk; rewrite modn_small //.
Qed.
Section ResponseTimeOfSingleJobBounded.
Hypothesis H_j_fst_completed_by_rt_bound :
completed job_cost sched j_fst (a_fst + J_k + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
job_interference job_arrival job_cost job_jitter sched j_i j_fst t1 t2
≤ D_i - (D_k - R_k - J_k).
Proof.
rename H_j_fst_completed_by_rt_bound into RBOUND.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval RBOUND.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [ARRfst [_ [LEdl _]]].
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
destruct (D_k - R_k - J_k ≤ D_i) eqn:LEdk; last first.
{
apply negbT in LEdk; rewrite -ltnNge in LEdk.
apply leq_trans with (n := 0); last by done.
apply leq_trans with (n := job_interference job_arrival job_cost
job_jitter sched j_i j_fst (a_fst + J_k + R_k) t2); last first.
{
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
unfold service_during; rewrite leqn0; apply/eqP.
try ( by apply cumulative_service_after_job_rt_zero with
(job_arrival0 := job_arrival) (job_cost0 := job_cost) (R := J_k + R_k);
try (by done); rewrite addnA // leqnn ) ||
by apply cumulative_service_after_job_rt_zero with
(job_arrival := job_arrival) (job_cost := job_cost) (R := J_k + R_k);
try (by done); rewrite addnA // leqnn.
}
{
apply extend_sum; last by apply leqnn.
rewrite -(leq_add2r D_i).
rewrite interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline in LEdl.
apply leq_trans with (n := a_fst + D_k); last first.
{
apply leq_trans with (n := job_arrival j_i + D_i); first by done.
by rewrite leq_add2r leq_addr.
}
rewrite -2!addnA leq_add2l.
rewrite addnA.
by apply ltnW; rewrite -ltn_subRL addnC subnDA.
}
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i t2);
first by apply extend_sum; [by apply leq_addr | by apply leqnn].
rewrite -(leq_add2r (D_k - R_k - J_k)) addnBAC // -addnBA // subnn addn0.
assert (SUBST: D_k - R_k - J_k = \sum_(a_fst + J_k + R_k ≤ i < a_fst + D_k) 1).
{
rewrite big_const_nat iter_addn mul1n addn0.
rewrite [_ + D_k]addnC.
rewrite -subnBA; last by rewrite -addnA leq_addr.
rewrite [a_fst + _]addnC -addnA [a_fst + R_k]addnC addnA.
rewrite -addnBA // subnn addn0.
by rewrite [_ + R_k]addnC subnDA.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst a_i (a_fst + D_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r.
destruct (t2 ≤ a_fst + J_k + R_k) eqn:LEt2.
{
apply extend_sum; first by apply leqnn.
apply leq_trans with (n := a_fst + J_k + R_k); first by done.
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
{
unfold job_interference.
apply negbT in LEt2; rewrite -ltnNge in LEt2.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | | by apply ltnW]; last first.
{
by apply leq_trans with (n := t1); first by apply leq_addr.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i
(a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) t2).
{
rewrite leq_add2l.
by apply job_interference_le_service.
}
unfold service_during.
( try ( rewrite → cumulative_service_after_job_rt_zero with (job_cost0 := job_cost)
(job_arrival0 := job_arrival) (R := J_k + R_k) ) ||
rewrite → cumulative_service_after_job_rt_zero with (job_cost := job_cost)
(job_arrival := job_arrival) (R := J_k + R_k));
rewrite ?addnA //.
rewrite addn0; apply extend_sum; first by done.
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
}
unfold job_interference.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | | ]; last first.
{
rewrite -addnA leq_add2l.
by apply H_R_k_le_deadline.
}
{
by apply leq_trans with (n := t1); first by apply leq_addr.
}
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i j_fst a_i
(a_fst + J_k + R_k) + service_during sched j_fst (a_fst + J_k + R_k) (a_fst + D_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r leq_add2l.
by apply job_interference_le_service.
}
unfold service_during.
( try ( rewrite → cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
(job_cost0 := job_cost) (R:=J_k + R_k) ) ||
rewrite → cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
(job_cost := job_cost) (R:=J_k + R_k));
rewrite ?addnA //.
rewrite addn0.
apply leq_trans with (n := (\sum_(a_i ≤ t < a_fst + J_k + R_k) 1) +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1).
{
apply leq_add; last by rewrite SUBST.
simpl_sum_const; rewrite -{1}[_ + R_k](addKn a_i) -addnBA //;
last by apply leq_trans with (n := t1); first by apply leq_addr.
by apply job_interference_le_delta.
}
rewrite -big_cat_nat; simpl; last by rewrite -addnA leq_add2l H_R_k_le_deadline.
{
simpl_sum_const; rewrite leq_subLR; unfold D_i, D_k, t1, a_fst.
by rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
}
by apply leq_trans with (n := t1); first by apply leq_addr.
Qed.
End ResponseTimeOfSingleJobBounded.
Section ResponseTimeOfSingleJobNotBounded.
Hypothesis H_j_fst_not_complete_by_rt_bound :
~~ completed job_cost sched j_fst (a_fst + J_k + R_k).
Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
job_arrival j_fst + J_k + R_k ≥ job_arrival j_i + J_i + delta.
Proof.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
rewrite leqNgt; apply/negP; intro LT.
move: H_j_fst_not_complete_by_rt_bound ⇒ /negP BUG; apply BUG.
by apply H_all_previous_jobs_completed_on_time.
Qed.
Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
D_i < D_k - R_k - J_k →
interference_caused_by j_fst t1 t2 = 0.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives; des.
intro LTdk.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTarr [FSTtask _]].
rewrite 2!ltn_subRL addnA [R_k + _]addnC in LTdk.
rewrite -(ltn_add2l a_fst) 2!addnA in LTdk.
apply leq_ltn_trans with (m := t1 + D_i) in LTdk; last first.
{
rewrite leq_add2r.
apply leq_trans with (n := t1 + delta); first by apply leq_addr.
apply leq_trans with (n := job_arrival j_i + J_i + delta).
{
unfold J_i;rewrite leq_add2r leq_add2l.
rewrite -H_job_of_tsk_i; apply PARAMS0.
}
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
apply/eqP; rewrite -[_ _ _ _ == 0]negbK; apply/negP; red; intro BUG.
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in BUG; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in BUG; try (by done).
rewrite interference_bound_edf_j_fst_deadline
interference_bound_edf_j_i_deadline in BUG.
apply leq_ltn_trans with (m := job_arrival j_i + D_i) in LTdk;
last by rewrite leq_add2r leq_addr.
by apply (leq_trans LTdk) in BUG; rewrite ltnn in BUG.
Qed.
Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
D_i ≥ D_k - R_k - J_k →
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k - J_k).
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives; des.
intro LEdk.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k.
destruct FST as [FSTtask [_ [LEdl _]]].
have LTr := interference_bound_edf_response_time_bound_of_j_fst_after_interval.
apply leq_subRL_impl.
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst t1 (job_arrival j_fst + J_k + R_k) + (D_k - R_k - J_k)).
{
rewrite leq_add2r; apply extend_sum; first by apply leqnn.
apply leq_trans with (n := job_arrival j_i + J_i + delta);
last by done.
rewrite leq_add2r leq_add2l.
by unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k)1).
{
apply leq_add; unfold job_interference.
{
simpl_sum_const.
rewrite -{1}[job_arrival j_fst + J_k + R_k](addKn t1) -addnBA;
first by apply job_interference_le_delta.
apply leq_trans with (n := a_i + J_i + delta); last by done.
apply leq_trans with (n := a_i + J_i); last by apply leq_addr.
by rewrite leq_add2l /J_i -H_job_of_tsk_i; apply PARAMS0.
}
simpl_sum_const; rewrite addnC.
rewrite -subnBA; last by rewrite -addnA leq_addr.
rewrite [a_fst + _]addnC -addnA [a_fst + _]addnC addnA.
rewrite -addnBA // subnn addn0.
by rewrite addnC subnDA.
}
rewrite -big_cat_nat; simpl; last 2 first.
{
apply leq_trans with (n := t1 + delta); first by apply leq_addr.
apply leq_trans with (n := job_arrival j_i + J_i + delta).
{
rewrite leq_add2r leq_add2l.
unfold J_i; rewrite -H_job_of_tsk_i; apply PARAMS0.
}
by apply interference_bound_edf_response_time_bound_of_j_fst_after_interval.
}
{
by rewrite -addnA leq_add2l; apply H_R_k_le_deadline.
}
rewrite big_const_nat iter_addn mul1n addn0 leq_subLR.
unfold D_i, D_k, t1, a_fst.
rewrite -interference_bound_edf_j_fst_deadline
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite leq_add2r leq_addr.
try ( by apply interference_under_edf_implies_shorter_deadlines with (arr_seq0 := arr_seq)
(job_arrival0 := job_arrival) (job_deadline0 := job_deadline) in LEdl ) ||
by apply interference_under_edf_implies_shorter_deadlines with (arr_seq := arr_seq)
(job_arrival := job_arrival) (job_deadline := job_deadline) in LEdl.
Qed.
End ResponseTimeOfSingleJobNotBounded.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k - J_k).
Proof.
destruct (completed job_cost sched j_fst (a_fst + J_k + R_k)) eqn:COMP;
first by apply interference_bound_edf_holds_for_single_job_that_completes_on_time.
apply negbT in COMP.
destruct (ltnP D_i (D_k - R_k - J_k)) as [LEdk | LTdk].
by rewrite interference_bound_edf_holds_for_single_job_with_big_slack.
by apply interference_bound_edf_holds_for_single_job_with_small_slack.
Qed.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
Proof.
have ONE := interference_bound_edf_simpl_when_there's_one_job.
have SLACK := interference_bound_edf_interference_of_j_fst_limited_by_slack.
rename H_many_jobs into NUM, H_only_one_job into SIZE.
unfold interference_caused_by, interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
rewrite SIZE ltnS leqn0 in NUM; move: NUM ⇒ /eqP EQnk.
rewrite EQnk mul0n add0n.
rewrite leq_min; apply/andP; split.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite SIZE.
}
by rewrite ONE; apply SLACK.
Qed.
End InterferenceSingleJob.
Section InterferenceTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
Section FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Proof.
apply interference_bound_edf_all_jobs_from_tsk_k, mem_nth.
by rewrite H_at_least_two_jobs.
Qed.
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
Proof.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in ×.
rename H_valid_job_parameters into PARAMS.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [LSTtask _]].
by specialize (PARAMS j_lst LSTarr); des; rewrite PARAMS2 LSTtask.
Qed.
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
Proof.
rename H_at_least_two_jobs into SIZE.
unfold j_fst, j_lst; rewrite -[num_mid_jobs.+1]add0n.
apply prev_le_next; last by rewrite SIZE leqnn.
by intros i LT; apply interference_bound_edf_jobs_ordered_by_arrival.
Qed.
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Proof.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
feed (interference_bound_edf_all_jobs_from_tsk_k j_lst).
by apply mem_nth; rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
move ⇒ [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
apply LSTserv; apply/eqP; rewrite -leqn0.
apply leq_trans with (n := service_during sched j_lst t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP; unfold service_during.
rewrite (cumulative_service_before_job_arrival_zero job_arrival) //.
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
Qed.
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + J_k + R_k).
Proof.
have PARAMS := H_valid_job_parameters j_i H_j_i_arrives.
unfold valid_sporadic_job_with_jitter, valid_sporadic_job in *; des.
have FST := interference_bound_edf_j_fst_is_job_of_tsk_k; des.
set j_snd := nth elem sorted_jobs 1.
exploit interference_bound_edf_all_jobs_from_tsk_k.
{
by apply mem_nth; instantiate (1 := 1); rewrite H_at_least_two_jobs.
}
instantiate (1 := elem); move ⇒ [SNDarr [SNDtsk [/eqP SNDserv _]]].
apply H_all_previous_jobs_completed_on_time; try (by done).
apply leq_ltn_trans with (n := job_arrival j_snd); last first.
{
apply leq_trans with (n := t2); last first.
{
unfold t2, t1; rewrite leq_add2r leq_add2l.
by rewrite -H_job_of_tsk_i; apply PARAMS0.
}
rewrite ltnNge; apply/negP; red; intro BUG; apply SNDserv.
apply/eqP; rewrite -leqn0; apply leq_trans with (n := service_during
sched j_snd t1 t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
( try ( apply cumulative_service_before_job_arrival_zero with (job_arrival0 := job_arrival) ) ||
apply cumulative_service_before_job_arrival_zero with (job_arrival := job_arrival));
try (by done).
try ( by apply arrival_before_jitter with (job_jitter0 := job_jitter) ) ||
by apply arrival_before_jitter with (job_jitter := job_jitter).
}
apply leq_trans with (n := a_fst + p_k).
{
apply leq_trans with (n := job_arrival j_fst + D_k);
first by rewrite -addnA leq_add2l.
by rewrite leq_add2l; apply H_constrained_deadlines.
}
unfold p_k; rewrite -FST0.
apply H_sporadic_tasks; [| by done | by done | by rewrite SNDtsk | ]; last first.
{
apply interference_bound_edf_jobs_ordered_by_arrival.
by rewrite H_at_least_two_jobs.
}
red; move ⇒ /eqP BUG.
by rewrite nth_uniq in BUG; rewrite ?SIZE //;
[ by apply interference_bound_edf_at_least_one_job
| by rewrite H_at_least_two_jobs
| by rewrite sort_uniq; apply filter_uniq, undup_uniq].
Qed.
End FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Proof.
unfold a_fst, a_lst, j_fst, j_lst.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
rewrite EQnk telescoping_sum;
last by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
rewrite -[_ × _ tsk_k]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat.
rewrite big_nat_cond [\sum_(0 ≤ i < _)(_-_)]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.
assert (ARRle: job_arrival cur ≤ job_arrival next).
by unfold cur, next; apply interference_bound_edf_jobs_ordered_by_arrival.
assert (INnth: cur \in interfering_jobs ∧ next \in interfering_jobs).
{
rewrite 2!interference_bound_edf_job_in_same_sequence; split.
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs; ins.
by apply mem_nth; destruct sorted_jobs; ins.
}
rewrite 2?mem_filter in INnth; des.
feed (interference_bound_edf_all_jobs_from_tsk_k cur).
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].
feed (interference_bound_edf_all_jobs_from_tsk_k next).
by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].
assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) ≤ job_arrival next).
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ ⇒ /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ ⇒ /eqP EQ; ssrlia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/interfering_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
by rewrite leq_subRL_impl // addnC /p_k -INnth.
Qed.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k ≥ num_mid_jobs.+1.
Proof.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
interference_bound_edf_j_fst_completed_on_time.
rename H_valid_task_parameters into TASK_PARAMS,
H_tsk_k_in_task_set into INk.
unfold valid_sporadic_taskset, is_valid_sporadic_task,
interference_bound, edf_specific_interference_bound in ×.
have DIST := interference_bound_edf_many_periods_in_between.
rewrite leqNgt; apply/negP; unfold not; intro LTnk; unfold n_k in LTnk.
rewrite ltn_divLR in LTnk; last by specialize (TASK_PARAMS tsk_k INk); des.
apply (leq_trans LTnk) in DIST; rewrite ltn_subRL in DIST.
rewrite -(ltn_add2r (J_k + R_k)) -addnA [D_i + _]addnC addnA in DIST.
unfold t1 in ×.
apply leq_ltn_trans with (m := job_arrival j_i + D_i) in DIST; last first.
{
rewrite addnA leq_add2r.
by apply leq_trans with (n := job_arrival j_i + job_jitter j_i);
first by apply leq_addr.
}
apply leq_trans with (p := a_lst + D_k) in DIST;
last by rewrite leq_add2l.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [LEdl _]]].
try ( apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LEdl; try (by done) ) ||
apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LEdl; try (by done).
unfold D_i, D_k in DIST; rewrite interference_bound_edf_j_lst_deadline
interference_bound_edf_j_i_deadline in LEdl.
by apply (leq_trans DIST) in LEdl; rewrite ltnn in LEdl.
Qed.
Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
interference_caused_by j_lst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
≤ n_k × task_cost tsk_k.
Proof.
apply leq_trans with (n := num_mid_jobs.+1 × task_cost tsk_k); last first.
{
rewrite leq_mul2r; apply/orP; right.
by apply interference_bound_edf_n_k_covers_middle_jobs_plus_one.
}
rewrite mulSn; apply leq_add.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite H_at_least_two_jobs.
}
{
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs) task_cost tsk_k);
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 ≤ i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
Qed.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Proof.
have NK := interference_bound_edf_n_k_covers_middle_jobs_plus_one.
rename H_many_jobs into NUM, H_at_least_two_jobs into SIZE.
move: NK; rewrite leq_eqVlt orbC; move ⇒ /orP NK; des;
first by rewrite SIZE ltnS leqNgt NK in NUM.
by rewrite NK.
Qed.
Section InterferenceOfFirstJob.
Lemma interference_bound_edf_remainder_ge_slack :
D_k - R_k - J_k ≤ D_i %% p_k.
Proof.
have AFTERt1 :=
interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval
interference_bound_edf_j_fst_completed_on_time.
have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
have DIST := interference_bound_edf_many_periods_in_between.
rewrite -NK in DIST.
rewrite 2!leq_subLR addnA [R_k + _]addnC -subndiv_eq_mod.
fold (div_floor D_i p_k) n_k.
rewrite addnBA; last by apply leq_trunc_div.
apply leq_trans with (n := J_k + R_k + D_i - (a_lst - a_fst)); last by apply leq_sub2l.
rewrite subnBA; last by apply interference_bound_edf_j_fst_before_j_lst.
rewrite -(leq_add2r a_lst) addnBAC; last first.
{
apply leq_trans with (n := t2);
[by apply ltnW, interference_bound_edf_last_job_arrives_before_end_of_interval|].
rewrite addnC addnA.
apply leq_trans with (n := t1 + D_i).
unfold t2; rewrite leq_add2l; apply H_delta_le_deadline.
by rewrite leq_add2r addnA; apply AFTERt1.
}
rewrite -addnBA // subnn addn0 [D_k + _]addnC.
apply leq_trans with (n := job_arrival j_i + D_i); last first.
{
rewrite [_ + a_fst]addnC 2!addnA leq_add2r.
by apply leq_trans with (n := t1); first by apply leq_addr.
}
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [ LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
try ( by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines with
(arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
Lemma interference_bound_edf_simpl_by_moving_to_left_side :
interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k × p_k ≤ D_i →
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k - J_k).
Proof.
intro LE.
apply leq_subRL_impl.
by rewrite -subndiv_eq_mod; apply leq_subRL_impl.
Qed.
Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
interference_caused_by j_fst t1 t2 ≤ \sum_(t1 ≤ t < a_fst + J_k + R_k) 1.
Proof.
assert (AFTERt1: t1 ≤ a_fst + J_k + R_k).
{
apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
by apply interference_bound_edf_j_fst_completed_on_time.
}
destruct (leqP t2 (a_fst + J_k + R_k)) as [LEt2 | GTt2].
{
apply leq_trans with (n := job_interference job_arrival job_cost job_jitter sched j_i
j_fst t1 (a_fst + J_k + R_k));
first by apply extend_sum; rewrite ?leqnn.
simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
by apply job_interference_le_delta.
}
{
unfold interference_caused_by, job_interference.
rewrite → big_cat_nat with (n := a_fst + J_k + R_k);
[simpl | by apply AFTERt1 | by apply ltnW].
rewrite -[\sum_(_ ≤ _ < _) 1]addn0; apply leq_add.
{
simpl_sum_const; rewrite -{1}[_ + _ + R_k](addKn t1) -addnBA //.
by apply job_interference_le_delta.
}
apply leq_trans with (n := service_during sched j_fst (a_fst + J_k + R_k) t2);
first by apply job_interference_le_service.
rewrite leqn0; apply/eqP.
( try ( apply cumulative_service_after_job_rt_zero with (job_arrival0 := job_arrival)
(job_cost0 := job_cost) (R := J_k + R_k) ) ||
apply cumulative_service_after_job_rt_zero with (job_arrival := job_arrival)
(job_cost := job_cost) (R := J_k + R_k));
[ by done | rewrite addnA | by rewrite addnA leqnn].
by apply interference_bound_edf_j_fst_completed_on_time.
}
Qed.
Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
interference_caused_by j_fst t1 t2 + (D_k - R_k - J_k) + D_i %/ p_k × p_k ≤
\sum_(t1 ≤ t < a_fst + J_k + R_k) 1
+ \sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1.
Proof.
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
D_i %/ p_k × p_k).
{
rewrite 2!leq_add2r.
apply interference_bound_edf_interference_of_j_fst_bounded_by_response_time.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 + (D_k - R_k - J_k) +
(a_lst - a_fst)).
{
rewrite leq_add2l; fold (div_floor D_i p_k) n_k.
rewrite interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
by apply interference_bound_edf_many_periods_in_between.
}
apply leq_trans with (n := \sum_(t1 ≤ t < a_fst + J_k + R_k) 1 +
\sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1 + \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1).
{
rewrite -3!addnA leq_add2l; apply leq_add;
rewrite big_const_nat iter_addn mul1n addn0;
[by rewrite subnDl addnC subnDA | by rewrite subnDr leqnn].
}
by apply leqnn.
Qed.
Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
\sum_(t1 ≤ t < a_fst + J_k + R_k) 1
+ \sum_(a_fst + J_k + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
Proof.
assert (AFTERt1: t1 ≤ a_fst + J_k + R_k).
{
apply interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval.
by apply interference_bound_edf_j_fst_completed_on_time.
}
rewrite -big_cat_nat;
[simpl | by apply AFTERt1 | by rewrite -addnA leq_add2l; apply H_R_k_le_deadline].
rewrite -big_cat_nat; simpl; last 2 first.
{
by apply (leq_trans AFTERt1); rewrite -addnA leq_add2l.
}
{
rewrite leq_add2r; unfold a_fst, a_lst, j_fst, j_lst.
rewrite -[num_mid_jobs.+1]add0n; apply prev_le_next;
last by rewrite add0n H_at_least_two_jobs ltnSn.
by ins; apply interference_bound_edf_jobs_ordered_by_arrival.
}
by rewrite big_const_nat iter_addn mul1n addn0.
Qed.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k - J_k).
Proof.
apply interference_bound_edf_simpl_by_moving_to_left_side.
apply (leq_trans interference_bound_edf_bounding_interference_with_interval_lengths).
rewrite interference_bound_edf_simpl_by_concatenation_of_intervals leq_subLR.
have LST := interference_bound_edf_j_lst_is_job_of_tsk_k.
destruct LST as [LSTarr [_ [LSTserv _]]].
unfold D_i, D_k, a_lst, t1; rewrite -interference_bound_edf_j_lst_deadline
-interference_bound_edf_j_i_deadline.
apply leq_trans with (n := a_i + job_deadline j_i);
last by rewrite -addnA leq_add2l leq_addl.
try ( by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq0 := arr_seq) (job_deadline0 := job_deadline) in LSTserv ) ||
by apply interference_under_edf_implies_shorter_deadlines
with (arr_seq := arr_seq) (job_deadline := job_deadline) in LSTserv.
Qed.
End InterferenceOfFirstJob.
Lemma interference_bound_edf_holds_for_multiple_jobs :
\sum_(0 ≤ i < num_mid_jobs.+2)
interference_caused_by (nth elem sorted_jobs i) t1 t2 ≤ interference_bound.
Proof.
rewrite [nth]lock big_nat_recl // big_nat_recr // /= -lock.
rewrite addnA addnC addnA.
have NK := interference_bound_edf_n_k_equals_num_mid_jobs_plus_one.
unfold interference_bound, edf_specific_interference_bound.
fold D_i D_k p_k n_k.
rewrite addnC addnA; apply leq_add;
first by rewrite addnC interference_bound_edf_holds_for_middle_and_last_jobs.
rewrite leq_min; apply/andP; split.
{
apply interference_bound_edf_interference_le_task_cost.
rewrite interference_bound_edf_job_in_same_sequence.
by apply mem_nth; rewrite H_at_least_two_jobs.
}
by apply interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack.
Qed.
End InterferenceTwoOrMoreJobs.
End InterferenceManyJobs.
Theorem interference_bound_edf_bounds_interference :
x ≤ interference_bound.
Proof.
apply (leq_trans interference_bound_edf_use_another_definition).
rewrite interference_bound_edf_simpl_by_filtering_interfering_jobs.
rewrite interference_bound_edf_simpl_by_sorting_interfering_jobs.
destruct (size sorted_jobs ≤ n_k) eqn:NUM;
first by apply interference_bound_edf_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.
assert (EX: ∃ elem: Job, True).
destruct sorted_jobs as [| j]; [by rewrite ltn0 in NUM | by ∃ j].
destruct EX as [elem _].
rewrite (big_nth elem).
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.
destruct n as [| num_mid_jobs].
{
rewrite big_nat_recr // big_geq //.
rewrite [nth]lock /= -lock add0n.
by apply interference_bound_edf_holds_for_a_single_job; rewrite SIZE.
}
{
by apply interference_bound_edf_holds_for_multiple_jobs; first by rewrite SIZE.
}
Qed.
End MainProof.
End ProofSpecificBound.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable task_jitter: sporadic_task → time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
Variable delta delta' R R': time.
Hypothesis H_delta_monotonic: delta ≤ delta'.
Hypothesis H_response_time_monotonic: R ≤ R'.
Hypothesis H_cost_le_rt_bound: task_cost tsk_other ≤ R.
Lemma interference_bound_edf_monotonic :
interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta (tsk_other, R) ≤
interference_bound_edf task_cost task_period task_deadline task_jitter tsk delta' (tsk_other, R').
Proof.
rename H_response_time_monotonic into LEr, H_delta_monotonic into LEx,
H_cost_le_rt_bound into LEcost, H_period_positive into GEperiod.
unfold interference_bound_edf, interference_bound_generic.
rewrite leq_min; apply/andP; split.
{
rewrite leq_min; apply/andP; split.
apply leq_trans with (n := (minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
(snd (tsk_other, R)) delta) (delta - task_cost tsk + 1)));
first by apply geq_minl.
apply leq_trans with (n := W_jitter task_cost task_period task_jitter (fst (tsk_other, R))
(snd (tsk_other, R)) delta);
[by apply geq_minl | by apply W_monotonic].
apply leq_trans with (n := minn (W_jitter task_cost task_period task_jitter (fst (tsk_other, R)) (snd (tsk_other, R)) delta) (delta - task_cost tsk + 1));
first by apply geq_minl.
apply leq_trans with (n := delta - task_cost tsk + 1);
first by apply geq_minr.
by rewrite leq_add2r leq_sub2r.
}
{
apply leq_trans with (n := edf_specific_interference_bound task_cost task_period
task_deadline task_jitter tsk tsk_other R);
first by apply geq_minr.
unfold edf_specific_interference_bound; simpl.
rewrite leq_add2l leq_min; apply/andP; split; first by apply geq_minl.
apply leq_trans with (n := task_deadline tsk %% task_period tsk_other -
(task_deadline tsk_other - R - task_jitter tsk_other));
[by apply geq_minr | by rewrite 2?leq_sub2l 2?leq_sub2r // leq_sub2l].
}
Qed.
End MonotonicitySpecificBound.
End InterferenceBoundEDFJitter.