Skip to content

GitLab

Commit 11a82d9b authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Clean up EDF theory and add separate file for EDF bound

parent f88c28db
Hide whitespace changes
Inline Side-by-side
bertogna_edf_comp.v
View file @ 11a82d9b
Require Import Vbase schedule bertogna_edf_theory util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path
workload_bound.
Require Import Vbase task job task_arrival schedule platform interference
workload workload_bound schedulability priority response_time
bertogna_fp_theory bertogna_edf_theory interference_bound_edf util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeIterationEDF.
Import Schedule ResponseTimeAnalysisEDF WorkloadBound.
Import Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound EDFSpecificBound ResponseTimeAnalysisFP
ResponseTimeAnalysisEDF.
Section Analysis.
......@@ -112,7 +115,7 @@ Module ResponseTimeIterationEDF.
interference_bound_edf task_cost task_period task_deadline tsk x2 (tsk_other, R').
Proof.
intros tsk x1 x2 tsk_other R R' LEx LEr GEperiod LEcost.
unfold interference_bound_edf, interference_bound.
unfold interference_bound_edf, interference_bound_fp.
rewrite leq_min; apply/andP; split.
{
rewrite leq_min; apply/andP; split.
......@@ -134,9 +137,9 @@ Module ResponseTimeIterationEDF.
}
}
{
apply leq_trans with (n := edf_specific_bound task_cost task_period task_deadline tsk (tsk_other, R));
apply leq_trans with (n := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R);
first by apply geq_minr.
unfold edf_specific_bound; simpl.
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));
......
bertogna_edf_theory.v
View file @ 11a82d9b
Require Import Vbase task job task_arrival schedule platform interference
workload workload_bound schedulability priority response_time
bertogna_fp_theory util_divround util_lemmas
bertogna_fp_theory interference_bound_edf util_divround util_lemmas
ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module ResponseTimeAnalysisEDF.
Export Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound ResponseTimeAnalysisFP.
Import Job SporadicTaskset ScheduleOfSporadicTask Workload Schedulability ResponseTime
Priority SporadicTaskArrival WorkloadBound EDFSpecificBound ResponseTimeAnalysisFP.
Section InterferenceBoundEDF.
(* In the following section, we define Bertogna and Cirinei's
interference bound for EDF scheduling. *)
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task -> nat.
......@@ -34,18 +36,11 @@ Module ResponseTimeAnalysisEDF.
(* By combining Bertogna's interference bound for a work-conserving
scheduler ... *)
Let basic_interference_bound := interference_bound task_cost task_period tsk delta tsk_R.
Let basic_interference_bound := interference_bound_fp task_cost task_period tsk delta tsk_R.
(* ... with and EDF-specific interference bound, ... *)
Definition edf_specific_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
(div_floor d_tsk p_other) * e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other)).
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
(* Bertogna and Cirinei define the following interference bound
under EDF scheduling. *)
Definition interference_bound_edf :=
......@@ -57,15 +52,18 @@ Module ResponseTimeAnalysisEDF.
Let interferes_with_tsk := is_interfering_task_jlfp tsk.
(* The total interference incurred by tsk is thus bounded by: *)
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences. *)
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | interferes_with_tsk tsk_other)
interference_bound_edf (tsk_other, R_other).
End AllTasks.
End InterferenceBoundEDF.
End TotalInterferenceBoundEDF.
(* In this section, we prove that Bertogna and Cirinei's RTA yields
safe response-time bounds. *)
Section ResponseTimeBound.
Context {sporadic_task: eqType}.
......@@ -111,11 +109,11 @@ Module ResponseTimeAnalysisEDF.
(* In order not to overcount job interference, we assume that
jobs of the same task do not execute in parallel.
Our proof requires a definition of interference based on
the sum of the individual contributions of each job:
I_total = I_j1 + I_j2 + ...
Note that under EDF, this is equivalent to task precedence
constraints. *)
constraints.
This is required because our proof uses a definition of
interference based on the sum of the individual contributions
of each job: I_total = I_j1 + I_j2 + ... *)
Hypothesis H_no_intra_task_parallelism:
jobs_of_same_task_dont_execute_in_parallel job_task sched.
......@@ -131,18 +129,17 @@ Module ResponseTimeAnalysisEDF.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task rate sched tsk.
Let response_time_bounded_by (j: JobIn arr_seq) (R: time) :=
completed job_cost rate sched j (job_arrival j + R).
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk rate sched.
(* Assume a known response-time bound R is known... *)
Let task_with_response_time := (sporadic_task * time)%type.
Variable rt_bounds: seq task_with_response_time.
(* ...for any task in the task set, ...*)
Hypothesis H_rt_bounds_contains_all_tasks:
unzip1 rt_bounds = ts.
(* ...for any task in the task set. *)
Hypothesis H_rt_bounds_contains_all_tasks: unzip1 rt_bounds = ts.
(* ..., R is a fixed-point of the response-time recurrence, ... *)
(* Also, assume that R is a fixed-point of the response-time recurrence, ... *)
Let I (tsk: sporadic_task) (delta: time) :=
total_interference_bound_edf task_cost task_period task_deadline tsk rt_bounds delta.
Hypothesis H_response_time_is_fixed_point :
......@@ -150,1044 +147,520 @@ Module ResponseTimeAnalysisEDF.
(tsk, R) \in rt_bounds ->
R = task_cost tsk + div_floor (I tsk R) num_cpus.
(* ..., R is as larger as the task cost, ... *)
(*Hypothesis H_response_time_bounds_ge_cost:
forall tsk_other R,
(tsk_other, R) \in rt_bounds -> R >= task_cost tsk_other.*)
(* ..., and R is no larger than the deadline. *)
Hypothesis H_interfering_tasks_miss_no_deadlines:
Hypothesis H_tasks_miss_no_deadlines:
forall tsk_other R,
(tsk_other, R) \in rt_bounds -> R <= task_deadline tsk_other.
(* Assume that the schedule satisfies the global scheduling
invariant with EDF priority, i.e., if any job of tsk is
backlogged, every processor must be busy with jobs with
no greater absolute deadline. *)
Let higher_eq_priority :=
@EDF Job arr_seq job_deadline. (* TODO: implicit params seems broken *)
(* Assume that the schedule satisfies the global scheduling invariant
for EDF, i.e., if any job of tsk is backlogged, every processor
must be busy with jobs with no larger absolute deadline. *)
Let higher_eq_priority := @EDF Job arr_seq job_deadline. (* TODO: implicit params broken *)
Hypothesis H_global_scheduling_invariant:
JLFP_JLDP_scheduling_invariant_holds job_cost num_cpus rate sched higher_eq_priority.
(* Next, we define Bertogna and Cirinei's response-time bound recurrence *)
Variable tsk: sporadic_task.
Variable R: time.
Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.
(* In order to prove that R is a response-time bound, we first present some lemmas. *)
Section Lemmas.
Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk.
(* Let (tsk, R) be any task to be analyzed, with its response-time bound R. *)
Variable tsk: sporadic_task.
Variable R: time.
Hypothesis H_tsk_R_in_rt_bounds: (tsk, R) \in rt_bounds.
(* Now, we prove that R bounds the response time of tsk in any schedule. *)
Theorem bertogna_cirinei_response_time_bound_edf :
response_time_bounded_by j R.
Proof.
unfold response_time_bounded_by, completed, completed_jobs_dont_execute,
valid_sporadic_job in *.
rename H_completed_jobs_dont_execute into COMP,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_rt_bounds_contains_all_tasks into HASTASKS,
H_interfering_tasks_miss_no_deadlines into NOMISS,
H_rate_equals_one into RATE,
H_global_scheduling_invariant into INVARIANT,
(*H_response_time_bounds_ge_cost into GE_COST,*)
H_response_time_is_fixed_point into FIX,
H_tsk_R_in_rt_bounds into INbounds,
H_job_of_tsk into JOBtsk.
(* Let's prove some basic facts about the tasks. *)
assert (INts: forall tsk R, (tsk, R) \in rt_bounds -> tsk \in ts).
{
by intros tsk0 R0 IN0; rewrite -HASTASKS; apply/mapP; exists (tsk0, R0).
}
(* Consider any job j of tsk. *)
Variable j: JobIn arr_seq.
Hypothesis H_job_of_tsk: job_task j = tsk.
assert (GE_COST: forall tsk R, (tsk, R) \in rt_bounds -> task_cost tsk <= R).
{
by intros tsk0 R0 IN0; rewrite [R0](FIX tsk0); first apply leq_addr.
}
(* Assume that job j did not complete on time, ... *)
Hypothesis H_j_not_completed: ~~ completed job_cost rate sched j (job_arrival j + R).
(* First, rewrite the claim in terms of the *absolute* response-time bound (arrival + R) *)
remember (job_arrival j + R) as ctime.
generalize dependent R.
generalize dependent tsk.
generalize dependent j.
clear R tsk j.
(* and that it is the first job not to satisfy its response-time bound. *)
Hypothesis H_all_previous_jobs_completed_on_time :
forall (j_other: JobIn arr_seq) tsk_other R_other,
job_task j_other = tsk_other ->
(tsk_other, R_other) \in rt_bounds ->
job_arrival j_other + R_other < job_arrival j + R ->
completed job_cost rate sched j_other (job_arrival j_other + R_other).
(* Now, we apply strong induction on the absolute response-time bound. *)
induction ctime as [ctime IH] using strong_ind_lt.
(* Let's call x the interference incurred by job j due to tsk_other, ...*)
Let x (tsk_other: sporadic_task) :=
task_interference job_cost job_task rate sched j
tsk_other (job_arrival j) (job_arrival j + R).
intros j' tsk' JOBtsk R' INbounds EQc; subst ctime.
assert (BEFOREok: forall (j0: JobIn arr_seq) tsk R0,
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j' + R' ->
service rate sched j0 (job_arrival j0 + R0) == job_cost j0).
{
by ins; apply IH with (tsk := tsk) (R := R0).
} clear IH.
(* According to the IH, all jobs with absolute response-time bound t < (job_arrival j + R)
have correct response-time bounds.
Now, we prove the same result for job j by contradiction.
Assume that (job_arrival j + R) is not a response-time bound for job j. *)
destruct (completed job_cost rate sched j' (job_arrival j' + R')) eqn:COMPLETED;
first by move: COMPLETED => /eqP COMPLETED; rewrite COMPLETED eq_refl.
apply negbT in COMPLETED; exfalso.
(* Let x be the cumulative time during [job_arrival j, job_arrival j + R)
where a job j is interfered with by tsk_k, ... *)
set x := fun tsk_other =>
if (tsk_other \in ts) && is_interfering_task_jlfp tsk' tsk_other then
task_interference job_cost job_task rate sched j'
tsk_other (job_arrival j') (job_arrival j' + R')
else 0.
(* ..., and let X be the cumulative time in the same interval where j is interfered
with by any task. *)
set X :=
total_interference job_cost rate sched j' (job_arrival j') (job_arrival j' + R').
(* Let's recall the interference bound under EDF scheduling. *)
set I_edf := fun (tup: task_with_response_time) =>
let (tsk_k, R_k) := tup in
if is_interfering_task_jlfp tsk' tsk_k then
interference_bound_edf task_cost task_period task_deadline tsk' R' (tsk_k, R_k)
else 0.
(* Since j has not completed, recall the time when it is not
executing is the total interference. *)
exploit (complement_of_interf_equals_service job_cost rate sched j' (job_arrival j')
(job_arrival j' + R'));
last intro EQinterf; ins; unfold has_arrived;
first by apply leqnn.
rewrite {2}[_ + R']addnC -addnBA // subnn addn0 in EQinterf.
(* and X the total interference incurred by job j due to any task. *)
Let X := total_interference job_cost rate sched j (job_arrival j) (job_arrival j + R).
(* Recall Bertogna and Cirinei's workload bound ... *)
Let workload_bound (tsk_other: sporadic_task) (R_other: time) :=
W task_cost task_period tsk_other R_other R.
(*... and the EDF-specific bound, ... *)
Let edf_specific_bound (tsk_other: sporadic_task) (R_other: time) :=
edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
(* ... which combined form the interference bound. *)
Let interference_bound (tsk_other: sporadic_task) (R_other: time) :=
interference_bound_edf task_cost task_period task_deadline tsk R (tsk_other, R_other).
(* Also, let ts_interf be the subset of tasks that interfere with tsk. *)
Let ts_interf := [seq tsk_other <- ts | is_interfering_task_jlfp tsk tsk_other].
Section LemmasAboutInterferingTasks.
(* In order to derive a contradiction, we first show that per-task
interference x_k is no larger than the basic interference bound (based on W). *)
assert (BASICBOUND:
forall tsk_k R_k,
(tsk_k, R_k) \in rt_bounds ->
x tsk_k <= W task_cost task_period tsk_k R_k R').
{
intros tsk_k R_k INBOUNDSk.
unfold x.
destruct ((tsk_k \in ts) && is_interfering_task_jlfp tsk' tsk_k) eqn:INTERFk;
last by done.
move: INTERFk => /andP [INk INTERFk].
unfold task_interference.
apply leq_trans with (n := workload job_task rate sched tsk_k
(job_arrival j') (job_arrival j' + R'));
(* Let (tsk_other, R_other) be any pair of higher-priority task and
response-time bound computed in previous iterations. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
Hypothesis H_response_time_of_tsk_other: (tsk_other, R_other) \in rt_bounds.
(* Note that tsk_other is in task set ts ...*)
Lemma bertogna_edf_tsk_other_in_ts: tsk_other \in ts.
Proof.
by rewrite -H_rt_bounds_contains_all_tasks; apply/mapP; exists (tsk_other, R_other).
Qed.
(* Also, R_other is larger than the cost of tsk_other. *)
Lemma bertogna_edf_R_other_ge_cost :
R_other >= task_cost tsk_other.
Proof.
by rewrite [R_other](H_response_time_is_fixed_point tsk_other);
first by apply leq_addr.
Qed.
(* Since tsk_other cannot interfere more than it executes, we show that
the interference caused by tsk_other is no larger than workload bound W. *)
Lemma bertogna_edf_workload_bounds_interference :
x tsk_other <= workload_bound tsk_other R_other.
Proof.
unfold valid_sporadic_job in *.
rename H_rate_equals_one into RATE,
H_all_previous_jobs_completed_on_time into BEFOREok,
H_valid_job_parameters into PARAMS,
H_valid_task_parameters into TASK_PARAMS,
H_restricted_deadlines into RESTR,
H_tasks_miss_no_deadlines into NOMISS.
unfold x, task_interference.
have INts := bertogna_edf_tsk_other_in_ts.
apply leq_trans with (n := workload job_task rate sched tsk_other
(job_arrival j) (job_arrival j + R));
first by apply task_interference_le_workload; ins; rewrite RATE.
apply workload_bounded_by_W with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline); try (by ins); last 2 first;
[ by apply GE_COST
| by ins; apply BEFOREok with (tsk := tsk_k); ins; rewrite RATE
[ by apply bertogna_edf_R_other_ge_cost
| by ins; apply BEFOREok with (tsk_other := tsk_other); ins; rewrite RATE
| by ins; rewrite RATE
| by ins; apply TASK_PARAMS
| by ins; apply RESTR |].
red; move => j'' JOBtsk' LEdl; unfold job_misses_no_deadline.
assert (PARAMS' := PARAMS j''); des; rewrite PARAMS'1 JOBtsk'.
apply completion_monotonic with (t := job_arrival j'' + (R_k)); ins;
red; move => j' JOBtsk' LEdl; unfold job_misses_no_deadline.
assert (PARAMS' := PARAMS j'); des; rewrite PARAMS'1 JOBtsk'.
apply completion_monotonic with (t := job_arrival j' + (R_other)); ins;
first by rewrite leq_add2l; apply NOMISS.
apply BEFOREok with (tsk := tsk_k); ins.
apply leq_ltn_trans with (n := job_arrival j'' + job_deadline j''); last by done.
by specialize (PARAMS j''); des; rewrite leq_add2l PARAMS1 JOBtsk'; apply NOMISS.
}
assert (EDFBOUND:
forall tsk_k R_k,
(tsk_k, R_k) \in rt_bounds ->
x tsk_k <= edf_specific_bound task_cost task_period task_deadline tsk' (tsk_k, R_k)).
{
unfold valid_sporadic_taskset, is_valid_sporadic_task, valid_sporadic_job in *.
intros tsk_k R_k INBOUNDSk.
rename R' into R_i.
unfold x; destruct ((tsk_k \in ts) && is_interfering_task_jlfp tsk' tsk_k) eqn:INTERFk;
last by done.
move: INTERFk => /andP [INk INTERFk].
unfold edf_specific_bound; simpl.
rename j' into j_i, tsk' into tsk_i.
set t1 := job_arrival j_i.
set t2 := job_arrival j_i + R_i.
set D_i := task_deadline tsk_i; set D_k := task_deadline tsk_k;
set p_k := task_period tsk_k.
rewrite interference_eq_interference_joblist; last by done.
unfold task_interference_joblist.
(* Simplify names *)
set n_k := div_floor D_i p_k.
(* Identify the subset of jobs that actually cause interference *)
set interfering_jobs :=
filter (fun (x: JobIn arr_seq) =>
(job_task x == tsk_k) && (job_interference job_cost rate sched j_i x t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
(* Remove the elements that we don't care about from the sum *)
assert (SIMPL:
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
job_interference job_cost rate sched j_i j t1 t2 =
\sum_(j <- interfering_jobs) job_interference job_cost rate sched j_i j t1 t2).
{
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 (job_interference job_cost rate sched j_i i t1 t2 != 0) eqn:DIFF; first by done.
by apply negbT in DIFF; rewrite negbK in DIFF; apply/eqP.
} rewrite SIMPL; clear SIMPL.
(* Remember that for any job of tsk, service <= task_cost tsk *)
assert (LTserv: forall j (INi: j \in interfering_jobs),
job_interference job_cost rate sched j_i j t1 t2 <= task_cost tsk_k).
{
intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _].
specialize (PARAMS j); des.
apply leq_trans with (n := service_during rate sched j t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
by apply cumulative_service_le_task_cost with (job_task0 := job_task) (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline).
}
(* Order the sequence of interfering jobs by arrival time, so that
we can identify the first and last jobs. *)
set order := fun (x y: JobIn arr_seq) => job_arrival x <= job_arrival y.
set sorted_jobs := (sort order interfering_jobs).
assert (SORT: sorted order sorted_jobs);
first by apply sort_sorted; unfold total, order; ins; apply leq_total.
rewrite (eq_big_perm sorted_jobs) /=; last by rewrite -(perm_sort order).
(* Remember that both sequences have the same set of elements *)
assert (INboth: forall x, (x \in interfering_jobs) = (x \in sorted_jobs)).
by apply perm_eq_mem; rewrite -(perm_sort order).
assert (PRIOinterf:
forall (j j': JobIn arr_seq) t1 t2,
job_interference job_cost rate sched j' j t1 t2 != 0 ->
job_arrival j + job_deadline j <= job_arrival j' + job_deadline j').
{
clear - t1 t2 INVARIANT; clear t1 t2.
intros j j' t1 t2 INTERF.
unfold job_interference in INTERF.
destruct ([exists t': 'I_t2, (t' >= t1) && backlogged job_cost rate sched j' t' && scheduled sched j t']) eqn:EX.
{
move: EX => /existsP EX; destruct EX as [t' EX];move: EX => /andP [/andP [LE BACK] SCHED].
eapply interfering_job_has_higher_eq_prio in BACK;
[ | by apply INVARIANT | by apply SCHED].
by apply BACK.
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
rewrite big_nat_cond (eq_bigr (fun x => 0)) in INTERF;
first by rewrite -big_nat_cond big_const_nat iter_addn mul0n addn0 eq_refl in INTERF.
intros i; rewrite andbT; move => /andP [GT LT].
specialize (ALL (Ordinal LT)); simpl in ALL.
rewrite -andbA negb_and -implybE in ALL; move: ALL => /implyP ALL.
by specialize (ALL GT); apply/eqP; rewrite eqb0.
}
}
(* Find some dummy element to use in the nth function *)
destruct (size sorted_jobs == 0) eqn:SIZE0;
first by move: SIZE0 =>/eqP SIZE0; rewrite (size0nil SIZE0) big_nil.
apply negbT in SIZE0; rewrite -lt0n in SIZE0.
assert (EX: exists elem: JobIn arr_seq, True); des.
destruct sorted_jobs; [by rewrite ltn0 in SIZE0 | by exists s].
clear EX SIZE0.
(* Remember that the jobs are ordered by arrival. *)
assert (ALL: forall i (LTsort: i < (size sorted_jobs).-1),
order (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1)).
by destruct sorted_jobs; [by ins| by apply/pathP; apply SORT].
apply BEFOREok with (tsk_other := tsk_other); ins.
apply leq_ltn_trans with (n := job_arrival j' + job_deadline j'); last by done.
by specialize (PARAMS j'); des; rewrite leq_add2l PARAMS1 JOBtsk'; apply NOMISS.
Qed.
(* Recall that the edf-specific interference bound also holds. *)
Lemma bertogna_edf_specific_bound_holds :
x tsk_other <= edf_specific_bound tsk_other R_other.
Proof.
apply interference_bound_edf_bounds_interference.
Qed.
(* Now we start the proof. First, we show that the workload bound
holds if n_k is no larger than the number of interferings jobs. *)
destruct (size sorted_jobs <= n_k) eqn:NUM.
{
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_(_ <- _) job_interference _ _ _ _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
by apply leq_sum; intros j; rewrite andbT; intros INj; apply LTserv; rewrite INboth.
}
}
apply negbT in NUM; rewrite -ltnNge in NUM.
(* Now we index the sum to access the first and last elements. *)
rewrite (big_nth elem).
(* First and last only exist if there are at least 2 jobs. Thus, we must show
that the bound holds for the empty list. *)
destruct (size sorted_jobs) eqn:SIZE; first by rewrite big_geq.
rewrite SIZE.
(* Let's derive some properties about the first element. *)
exploit (mem_nth elem); last intros FST.
by instantiate (1:= sorted_jobs); instantiate (1 := 0); rewrite SIZE.
move: FST; rewrite -INboth mem_filter; move => /andP FST; des.
move: FST => /andP FST; des; move: FST => /eqP FST.
rename FST0 into FSTin, FST into FSTtask, FST1 into FSTserv.
(* Now we show that the bound holds for a singleton set of interfering jobs. *)
set j_fst := (nth elem sorted_jobs 0).
set a_fst := job_arrival j_fst.
assert (DLfst: job_deadline j_fst = task_deadline tsk_k).
{
by specialize (PARAMS j_fst); des; rewrite PARAMS1 FSTtask.
}
End LemmasAboutInterferingTasks.
assert (DLi: job_deadline j_i = task_deadline tsk_i).
{
by specialize (PARAMS j_i); des; rewrite PARAMS1 JOBtsk.
}
(* Next we prove some lemmas that help to derive a contradiction.*)
Section DerivingContradiction.
assert (AFTERt1: completed job_cost rate sched j_fst (a_fst + R_k) -> t1 <= a_fst + R_k).
{
intros RBOUND.
rewrite leqNgt; apply/negP; unfold not; intro BUG.
move: FSTserv => /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during rate sched j_fst t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k); try (by done); apply ltnW.
}
(* 1) Since job j did not complete by its response time bound, it follows that
the total interference X >= R - e_k + 1. *)
Lemma bertogna_edf_too_much_interference : X >= R - task_cost tsk + 1.
Proof.
rename H_completed_jobs_dont_execute into COMP,
H_valid_job_parameters into PARAMS,