From d6cdcfe124b496b49db4da5c1d6ddd79526e7556 Mon Sep 17 00:00:00 2001
From: Sergey Bozhko
Date: Tue, 20 Aug 2019 14:50:57 +0200
Subject: [PATCH] tighten responsetime recurrence for EDF
When we were writing the paper on Abstract RTA, we noticed that the responsetime recurrence for EDF does not match the known bound.
This merge request tightens the analysis in Prosa to match the known bound.

model/schedule/uni/limited/busy_interval.v  582 ++++++++++++
.../concrete_models/response_time_bound.v  25 +
.../edf/nonpr_reg/response_time_bound.v  2 +
.../uni/limited/edf/response_time_bound.v  20 +
model/schedule/uni/service.v  90 +++
util/sum.v  22 +
6 files changed, 523 insertions(+), 218 deletions()
diff git a/model/schedule/uni/limited/busy_interval.v b/model/schedule/uni/limited/busy_interval.v
index 9f31e9cb..2980f961 100644
 a/model/schedule/uni/limited/busy_interval.v
+++ b/model/schedule/uni/limited/busy_interval.v
@@ 42,6 +42,7 @@ Module BusyIntervalJLFP.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Let job_remaining_cost j t := remaining_cost job_cost sched j t.
+ Let arrivals_between := jobs_arrived_between arr_seq.
(* In this section, we define the notion of a busy interval. *)
Section BusyInterval.
@@ 132,6 +133,40 @@ Module BusyIntervalJLFP.
priority_inversion_of_job_is_bounded_by j B.
End TaskPriorityInversionBound.
+
+ (* In this section we define the computational
+ version of the notion of quiet time. *)
+ Section DecidableQuietTime.
+
+ (* We say that t is a quiet time for j iff every higherpriority job from
+ the arrival sequence that arrived before t has completed by that time. *)
+ Definition quiet_time_dec (j : Job) (t : time) :=
+ all
+ (fun j_hp => higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
+ (jobs_arrived_before arr_seq t).
+
+ (* We also show that the computational and propositional definitions are equivalent. *)
+ Lemma quiet_time_P :
+ forall j t, reflect (quiet_time j t) (quiet_time_dec j t).
+ Proof.
+ intros; apply/introP.
+ { intros QT s ARRs HPs BEFs.
+ move: QT => /allP QT.
+ specialize (QT s); feed QT.
+ eapply arrived_between_implies_in_arrivals; eauto 2.
+ by move: QT => /implyP Q; apply Q in HPs.
+ }
+ { move => /negP DEC; intros QT; apply: DEC.
+ apply/allP; intros s ARRs.
+ apply/implyP; intros HPs.
+ apply QT; try done.
+  by apply in_arrivals_implies_arrived in ARRs.
+  eapply in_arrivals_implies_arrived_between in ARRs; eauto 2.
+ by move: ARRs => /andP [_ HP].
+ }
+ Qed.
+
+ End DecidableQuietTime.
(* Now we prove some lemmas about busy intervals. *)
Section Lemmas.
@@ 146,7 +181,6 @@ Module BusyIntervalJLFP.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
(* Recall the list of jobs that arrive in any interval. *)
 Let arrivals_between := jobs_arrived_between arr_seq.
Let quiet_time t1 := quiet_time j t1.
Let busy_interval_prefix t1 t2 := busy_interval_prefix j t1 t2.
Let busy_interval t1 t2 := busy_interval j t1 t2.
@@ 385,22 +419,28 @@ Module BusyIntervalJLFP.
(* Let t1 be a quiet time. *)
Variable t1: time.
Hypothesis H_quiet_time: quiet_time t1.
+
+ (* Assume that there is no quiet time in the interval (t1, t1 + Δ]. *)
+ Variable Δ: time.
+ Hypothesis H_no_quiet_time: forall t, t1 < t <= t1 + Δ > ~ quiet_time t.
+
+ (* For clarity, we introduce a notion of the total service of jobs released in
+ time interval [t_beg, t_end) during the time interval [t1, t1 + Δ). *)
+ Let service_received_by_hep_jobs_released_during t_beg t_end :=
+ service_of_higher_or_equal_priority_jobs
+ sched (arrivals_between t_beg t_end) higher_eq_priority j t1 (t1 + Δ).
(* We prove that jobs with higherthanorequal priority that
 arrived before time instant t1 receive no service after
+ released before time instant t1 receive no service after
time instant t1. *)
 Lemma jobs_receive_no_service_after_quiet_time:
 forall (Δ: time),
 let arrivals_after_t1 := arrivals_between t1 (t1 + Δ) in
 let all_arrivals := arrivals_between 0 (t1 + Δ) in

 \sum_(j_hp < arrivals_after_t1  higher_eq_priority j_hp j)
 service_during sched j_hp t1 (t1 + Δ) =
 \sum_(j_hp < all_arrivals  higher_eq_priority j_hp j)
 service_during sched j_hp t1 (t1 + Δ).
+ Lemma hep_jobs_receive_no_service_before_quiet_time:
+ service_received_by_hep_jobs_released_during t1 (t1 + Δ) =
+ service_received_by_hep_jobs_released_during 0 (t1 + Δ).
Proof.
intros.
 rewrite /arrivals_after_t1 /all_arrivals /arrivals_between.
+ rewrite /service_received_by_hep_jobs_released_during
+ /service_of_higher_or_equal_priority_jobs
+ /service_of_jobs /arrivals_between.
rewrite [in X in _ = X](job_arrived_between_cat _ _ t1);
[   rewrite leq_addr]; try done.
rewrite big_cat //=.
@@ 419,52 +459,16 @@ Module BusyIntervalJLFP.
 by eapply in_arrivals_implies_arrived_before; eauto 2.
Qed.
 (* Assume that there is no quiet time in the interval (t1, t1 + Δ]. *)
 Variable Δ: time.
 Hypothesis H_no_quiet_time: forall t, t1 < t <= t1 + Δ > ~ quiet_time t.

(* Next we prove that the total service within a "nonquiet"
 time interval (t1, t1 + Δ] is exactly Δ. *)
+ time interval [t1, t1 + Δ) is exactly Δ. *)
Lemma no_idle_time_within_non_quiet_time_interval:
 \sum_(j < arrivals_between 0 (t1 + Δ)) service_during sched j t1 (t1 + Δ) = Δ.
+ service_of_jobs sched (arrivals_between 0 (t1 + Δ)) predT t1 (t1 + Δ) = Δ.
Proof.
 intros.
 have EQ: \sum_(t1 <= x < t1 + Δ) 1 = Δ.
 { by rewrite big_const_nat iter_addn mul1n addn0 {2}[t1]addn0 subnDl subn0. }
 rewrite {3}EQ exchange_big //=. clear EQ.
+ intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
+ rewrite {3}[Δ](sum_of_ones t1) exchange_big //=.
apply/eqP; rewrite eqn_leq; apply/andP; split.
 { rewrite leq_sum //.
 move => t' _.
 case SCHED: (sched t') => [j1  ]; simpl.
 { case ARR: (j1 \in arrivals_between 0 (t1 + Δ)).
 { rewrite (big_rem j1) //=; simpl.
 rewrite /service_at /scheduled_at SCHED; simpl.
 rewrite [1]addn0 leq_add //.
  by case (Some j1 == Some j1).
  rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 apply/eqP; rewrite eqb0.
 apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
 inversion CONTR; subst j2; clear CONTR.
 rewrite rem_filter in ARRj2; last first.
 eapply arrivals_uniq; eauto 2.
 move: ARRj2; rewrite mem_filter; move => /andP [/negP CONTR _].
 by apply: CONTR. }
 { apply leq_trans with 0; last by done.
 rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 apply/eqP; rewrite eqb0.
 rewrite /scheduled_at SCHED.
 apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
 inversion CONTR; clear CONTR.
 by subst j2; rewrite ARR in ARRj2. } }
 { apply leq_trans with 0; last by done.
 rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 by rewrite /service_at /scheduled_at SCHED. }
 }
 { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=.
 rewrite leq_sum //.
+ { rewrite leq_sum //; move => t' _; eapply service_of_jobs_le_1; eauto. }
+ { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=; rewrite leq_sum //.
move => t' /andP [/andP [LT GT] _].
apply/sum_seq_gt0P.
case SCHED: (sched t') => [j1  ]; last first.
@@ 476,7 +480,7 @@ Module BusyIntervalJLFP.
apply: H_no_quiet_time.
by apply idle_time_implies_quiet_time_at_the_next_time_instant.
}
 { feed (H_no_quiet_time t'). by apply/andP; split; last rewrite ltnW.
+ { feed (H_no_quiet_time t'); first by apply/andP; split; last rewrite ltnW.
apply: H_no_quiet_time.
intros j_hp IN HP ARR.
apply contraT; intros NOTCOMP.
@@ 490,21 +494,15 @@ Module BusyIntervalJLFP.
}
}
{ exists j1; split.
  unfold arrivals_between.
 apply arrived_between_implies_in_arrivals with job_arrival; try done.
 unfold jobs_come_from_arrival_sequence in *.
+  apply arrived_between_implies_in_arrivals with job_arrival; try done.
apply H_jobs_come_from_arrival_sequence with t'.
 unfold scheduled_at . rewrite SCHED. by done.
 unfold arrived_between; apply/andP; split; first by done.
 unfold jobs_must_arrive_to_execute in *.
 move: SCHED => /eqP SCHED.
 apply H_jobs_must_arrive_to_execute in SCHED.
 unfold has_arrived in SCHED.
+ rewrite /scheduled_at SCHED; by done.
+ apply/andP; split; first by done.
+ move: SCHED => /eqP SCHED; apply H_jobs_must_arrive_to_execute in SCHED.
by apply leq_ltn_trans with t'.
 
 by rewrite /service_at /scheduled_at SCHED lt0b. }
+  by rewrite /service_at /scheduled_at SCHED lt0b. }
}
 Qed.
+ Qed.
End QuietTimeAndServiceOfJobs.
@@ 563,27 +561,20 @@ Module BusyIntervalJLFP.
rename H_j_is_pending into PEND,
H_work_conserving into WORK, H_priority_is_reflexive into REFL.
unfold busy_interval_prefix.
 set dec_quiet :=
 fun t => all (fun j_hp =>
 higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
 (jobs_arrived_before arr_seq t).
 destruct ([exists t:'I_t_busy.+1, dec_quiet t]) eqn:EX.
 {
 set last := \max_(t < t_busy.+1  dec_quiet t) t.
+ destruct ([exists t:'I_t_busy.+1, quiet_time_dec j t]) eqn:EX.
+ { set last := \max_(t < t_busy.+1  quiet_time_dec j t) t.
move: EX => /existsP [t EX].
 have PRED: dec_quiet last by apply (bigmax_pred t_busy.+1 dec_quiet t).
+ have PRED: quiet_time_dec j last by apply (bigmax_pred t_busy.+1 (quiet_time_dec j) t).
have QUIET: quiet_time last.
 {
 move: PRED => /allP PRED.
+ { move: PRED => /allP PRED.
intros j_hp IN HP ARR.
feed (PRED j_hp).
 by apply arrived_between_implies_in_arrivals with (job_arrival0 := job_arrival).
 by rewrite HP implyTb in PRED.
+ { by eapply arrived_between_implies_in_arrivals; eauto. }
+ by rewrite HP implyTb in PRED.
}
exists last.
have JAIN: last <= job_arrival j <= t_busy.
 {
 apply/andP; split; last by move: PEND => /andP [ARR _].
+ { apply/andP; split; last by move: PEND => /andP [ARR _].
apply contraT; rewrite ltnNge; intros BEFORE.
feed (QUIET j FROM); first by apply REFL.
specialize (QUIET BEFORE).
@@ 592,29 +583,23 @@ Module BusyIntervalJLFP.
[by rewrite QUIET in NOTCOMP ].
by apply bigmax_ltn_ord with (i0 := t).
}
 split; last by done.
 repeat split.
+ repeat split; try done.
 by apply bigmax_ltn_ord with (i0 := t).
  by done.
 
 move => t0 /andP [GTlast LTbusy] QUIET0.
 have PRED0: dec_quiet t0.
 {
 apply/allP; intros j_hp ARR; apply/implyP; intros HP.
+  move => t0 /andP [GTlast LTbusy] QUIET0.
+ have PRED0: quiet_time_dec j t0.
+ { apply/allP; intros j_hp ARR; apply/implyP; intros HP.
apply QUIET0.
 by eapply in_arrivals_implies_arrived; eauto.
 by done.
 by eapply in_arrivals_implies_arrived_before; eauto.
}
have BUG: t0 <= last.
 {
 have LE := @leq_bigmax_cond _ (fun (x: 'I_t_busy.+1) => dec_quiet x)
 (fun x => x) (Ordinal LTbusy) PRED0.
 by apply LE.
+ { intros.
+ have LE := @leq_bigmax_cond _ (fun (x: 'I_t_busy.+1) => quiet_time_dec j x) (fun x => x) (Ordinal LTbusy) PRED0.
+ by apply LE.
}
apply leq_trans with (p := last) in GTlast; last by done.
by rewrite ltnn in GTlast.
  by rewrite ltnS.
}
{
apply negbT in EX; rewrite negb_exists in EX; move: EX => /forallP ALL.
@@ 676,93 +661,47 @@ Module BusyIntervalJLFP.
and priority inversion equals delta. *)
Lemma busy_interval_has_uninterrupted_service:
delta <= priority_inversion_bound + hp_service t1 (t1 + delta).
 Proof.
+ Proof.
move: H_is_busy_prefix => [H_strictly_larger [H_quiet [_ EXj]]].
destruct (delta <= priority_inversion_bound) eqn:KLEΔ.
{ by apply leq_trans with priority_inversion_bound; last rewrite leq_addr. }
apply negbT in KLEΔ; rewrite ltnNge in KLEΔ.
 apply leq_trans with (cumulative_priority_inversion j t1 (t1 + delta) + hp_service t1 (t1 + delta)); last first.
 { rewrite leq_add2r.
 destruct (t1 + delta <= t_busy.+1) eqn:NEQ.
 { apply H_priority_inversion_is_bounded in H_is_busy_prefix.
 apply leq_trans with (cumulative_priority_inversion j t1 t_busy.+1); last by done.
 unfold cumulative_priority_inversion.
 rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + delta)) //=.
 rewrite leq_addr //.
 by rewrite leq_addr.
 }
 { apply H_priority_inversion_is_bounded.
 apply negbT in NEQ. rewrite ltnNge in NEQ.
 repeat split; try done.
  by rewrite addn1 leq_add2l.
  move => t' /andP [LT GT]; apply H_no_quiet_time.
 by apply/andP; split; [  rewrite ltnW ].
  move: EXj => /andP [T1 T2].
 apply/andP; split; first by done.
 by apply ltn_trans with (t_busy.+1).
 }
 }
 unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs.
 rewrite jobs_receive_no_service_after_quiet_time //.
 rewrite sum_pred_diff.
 rewrite addnBA; last first.
 { rewrite big_mkcond //= leq_sum //.
 by intros j' _; case (higher_eq_priority j' j). }
 rewrite addnC.
 rewrite addnBA; last first.
 rewrite exchange_big //=.
 unfold cumulative_priority_inversion.
 unfold is_priority_inversion.
 apply leq_sum_seq.
 move => t II _.
 rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
 rewrite big_mkcond //=.
 case SCHED: (sched t) => [j1  ]; simpl.
 { case PRIO1: (higher_eq_priority j1 j); simpl.
 { rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 case PRIO2: (higher_eq_priority j2 j); simpl; first by done.
 rewrite /service_at /scheduled_at SCHED.
 case EQ: (j1 == j2).
 { move: EQ => /eqP EQ; subst j2.
 by rewrite PRIO1 in PRIO2. }
 { apply/eqP; rewrite eqb0.
 apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
 inversion CONTR; clear CONTR.
 by subst j2; rewrite PRIO1 in PRIO2. } }
 { case ARR: (j1 \in arrivals_between 0 (t1 + delta)).
 { rewrite (big_rem j1) //= PRIO1; simpl.
 rewrite /service_at /scheduled_at SCHED; simpl.
 rewrite [1]addn0 leq_add //.
  by case (Some j1 == Some j1).
+ apply leq_trans with (cumulative_priority_inversion j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
+ { rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time //.
+ rewrite /service_of_higher_or_equal_priority_jobs /service_of_jobs sum_pred_diff.
+ rewrite addnBA; last first.
+ { by rewrite big_mkcond //= leq_sum //; intros j' _; case (higher_eq_priority j' j). }
+ rewrite addnC addnBA.
+ { intros. have H := no_idle_time_within_non_quiet_time_interval; unfold service_of_jobs in H.
+ by rewrite H // leq_addr.
+ }
+ { rewrite /cumulative_priority_inversion /is_priority_inversion exchange_big //=.
+ apply leq_sum_seq; move => t II _.
+ rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
+ case SCHED: (sched t) => [j1  ]; simpl; first last.
+ { by rewrite leqn0 big1_seq; last (move => j1 _; rewrite /service_at /scheduled_at SCHED). }
+ { case PRIO1: (higher_eq_priority j1 j); simpl; first last.
+  by eapply service_of_jobs_le_1; eauto 2.
 rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 case (higher_eq_priority j2 j); simpl; first by done.
 apply/eqP; rewrite eqb0.
 apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
 inversion CONTR; subst j2; clear CONTR.
 rewrite rem_filter in ARRj2; last first.
 eapply arrivals_uniq; eauto 2.
 move: ARRj2; rewrite mem_filter; move => /andP [/negP CONTR _].
 by apply: CONTR. }
 { apply leq_trans with 0; last by done.
 rewrite leqn0 big1_seq; first by done.
 move => j2 /andP [_ ARRj2].
 case (higher_eq_priority j2 j); simpl; first by done.
 apply/eqP; rewrite eqb0.
 rewrite /scheduled_at SCHED.
 apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
 inversion CONTR; clear CONTR.
 by subst j2; rewrite ARR in ARRj2. } } }
 { simpl.
 rewrite leqn0 big1_seq; first by done.
 move => j1 /andP [_ ARRj1].
 rewrite /service_at /scheduled_at SCHED.
 by case (higher_eq_priority j1 j).
+ move => j2 /andP [PRIO2 ARRj2].
+ rewrite /service_at /scheduled_at SCHED.
+ case EQ: (j1 == j2).
+ + by move: EQ => /eqP EQ; subst j2; rewrite PRIO1 in PRIO2.
+ + apply/eqP; rewrite eqb0; apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
+ by inversion CONTR; clear CONTR; subst j2; rewrite PRIO1 in PRIO2. } } }
+ { rewrite leq_add2r.
+ destruct (t1 + delta <= t_busy.+1) eqn:NEQ; [  apply negbT in NEQ; rewrite ltnNge in NEQ].
+  apply leq_trans with (cumulative_priority_inversion j t1 t_busy.+1); last eauto 2.
+ by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + delta)) //=; rewrite leq_addr.
+  apply H_priority_inversion_is_bounded; repeat split; try done.
+ + by rewrite addn1 leq_add2l.
+ + move => t' /andP [LT GT]; apply H_no_quiet_time.
+ by apply/andP; split; [  rewrite ltnW ].
+ + move: EXj => /andP [T1 T2].
+ by apply/andP; split; [done  apply ltn_trans with (t_busy.+1)].
}
 by rewrite no_idle_time_within_non_quiet_time_interval // leq_addr.
Qed.

+
(* Moreover, the fact that the interval is not quiet also implies
that there's more workload requested than service received. *)
Lemma busy_interval_too_much_workload:
@@ 799,8 +738,6 @@ Module BusyIntervalJLFP.
destruct (higher_eq_priority j1 j); last by done.
by apply cumulative_service_le_job_cost.
}


unfold service_during.
rewrite (ignore_service_before_arrival job_arrival); rewrite //; [ by apply ltnW].
rewrite < ignore_service_before_arrival with (t2:=0); rewrite //; [by apply ltnW].
@@ 829,16 +766,10 @@ Module BusyIntervalJLFP.
Proof.
have TOOMUCH := busy_interval_workload_larger_than_interval.
have BOUNDED := H_workload_is_bounded.
 rename H_is_busy_prefix into PREFIX.
 set dec_quiet :=
 fun t =>
 all (fun j_hp => higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
 (jobs_arrived_before arr_seq t).
 destruct ([exists t2:'I_(t1 + delta).+1, (t2 > t1) && dec_quiet t2]) eqn:EX.
 {
 have EX': exists (t2: nat), ((t1 < t2 <= t1 + delta) && dec_quiet t2).
 {
 move: EX => /existsP [t2 /andP [LE QUIET]].
+ rename H_is_busy_prefix into PREFIX.
+ destruct ([exists t2:'I_(t1 + delta).+1, (t2 > t1) && quiet_time_dec j t2]) eqn:EX.
+ { have EX': exists (t2: nat), ((t1 < t2 <= t1 + delta) && quiet_time_dec j t2).
+ { move: EX => /existsP [t2 /andP [LE QUIET]].
exists t2; apply/andP; split; last by done.
by apply/andP; split; last by rewrite ltnS; apply ltn_ord.
}
@@ 876,7 +807,7 @@ Module BusyIntervalJLFP.
rewrite ltnNge; apply/negP; intros CONTR.
feed (NQ t2); first by apply/andP; split; last rewrite ltnS.
apply NQ.
 unfold dec_quiet in *.
+ unfold quiet_time_dec in *.
intros jhp ARR HP AB.
move: QUIET => /allP QUIET.
feed (QUIET jhp).
@@ 913,7 +844,6 @@ Module BusyIntervalJLFP.
End UpperBound.
End BoundingBusyInterval.

(* In this section, we show that from a workload bound we can infer
the existence of a busy interval. *)
@@ 1006,6 +936,282 @@ Module BusyIntervalJLFP.
End Lemmas.
+ (* In this section, we derive an alternative condition for the existence of
+ a busy interval. The new condition requires the total workload (instead
+ of the highpriority workload) generated by the task set to be bounded. *)
+ Section NonOverloadedProcessor.
+
+ (* The processor has no carryin at time t iff every job (regardless of priority)
+ from the arrival sequence released before t has completed by that time. *)
+ Definition no_carry_in (t: time) :=
+ forall j_o,
+ arrives_in arr_seq j_o >
+ arrived_before job_arrival j_o t >
+ job_completed_by j_o t.
+
+ (* The fact that there is no carryin at time instant t
+ trivially implies that t is a quiet time. *)
+ Lemma no_carry_in_implies_quiet_time :
+ forall j t,
+ no_carry_in t >
+ quiet_time j t.
+ Proof.
+ by intros j t FQT j_hp ARR HP BEF; apply FQT.
+ Qed.
+
+ (* Assume that there are no duplicate job arrivals. *)
+ Hypothesis H_arrival_sequence_is_a_set:
+ arrival_sequence_is_a_set arr_seq.
+
+ (* We also assume that the schedule is workconserving and that jobs
+ do not execute before their arrival nor after completion. *)
+ Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+ Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+ Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+
+ (* Next we show that an idle time implies no carry in at this time instant. *)
+ Lemma idle_instant_implies_no_carry_in_at_t :
+ forall t,
+ is_idle sched t >
+ no_carry_in t.
+ Proof.
+ intros ? IDLE j ARR HA.
+ apply/negPn/negP; intros NCOMPL.
+ move: IDLE => /eqP IDLE.
+ move: (H_work_conserving j t ARR) => NIDLE.
+ feed NIDLE.
+ { apply/andP; split; last first.
+ { by rewrite /scheduled_at IDLE. }
+ { by apply/andP; split; [apply ltnW  done]. }
+ }
+ move: NIDLE => [j' SCHED].
+ by rewrite /scheduled_at IDLE in SCHED.
+ Qed.
+
+ (* Moreover, an idle time implies no carry in at the next time instant. *)
+ Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
+ forall t,
+ is_idle sched t >
+ no_carry_in t.+1.
+ Proof.
+ intros ? IDLE j ARR HA.
+ apply/negPn/negP; intros NCOMPL.
+ move: IDLE => /eqP IDLE.
+ move: (H_work_conserving j t ARR) => NIDLE.
+ feed NIDLE.
+ { apply/andP; split; last first.
+ { by rewrite /scheduled_at IDLE. }
+ { apply/andP; split; first by done.
+ move: NCOMPL => /negP NC1; apply/negP; intros NC2; apply: NC1.
+ by apply completion_monotonic with t.
+ }
+ }
+ move: NIDLE => [j' SCHED].
+ by rewrite /scheduled_at IDLE in SCHED.
+ Qed.
+
+ (* Let the priority relation be reflexive. *)
+ Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
+
+ (* Next, we recall the notion of workload of all jobs released in a given interval [t1, t2)... *)
+ Let total_workload t1 t2 :=
+ workload_of_jobs job_cost (arrivals_between t1 t2) predT.
+
+ (* ... and total service of jobs within some time interval [t1, t2). *)
+ Let total_service t1 t2 :=
+ service_of_jobs sched (arrivals_between 0 t2) predT t1 t2.
+
+ (* Assume that for some positive Δ, the sum of requested workload
+ at time (t + Δ) is bounded by delta (i.e., the supply).
+ Note that this assumption bounds the total workload of
+ jobs released in a time interval [t, t + Δ) regardless of
+ their priorities. *)
+ Variable Δ: time.
+ Hypothesis H_delta_positive: Δ > 0.
+ Hypothesis H_workload_is_bounded: forall t, total_workload t (t + Δ) <= Δ.
+
+ (* Next we prove that since for any time instant t there is a point where
+ the total workload is upperbounded by the supply the processor encounters
+ no carryin instants at least every Δ time units. *)
+ Section ProcessorIsNotTooBusy.
+
+ (* We start by proving that the processor has no carryin at
+ the beginning (i.e., has no carryin at time instant 0). *)
+ Lemma no_carry_in_at_the_beginning :
+ no_carry_in 0.
+ Proof.
+ intros s ARR AB; exfalso.
+ by rewrite /arrived_before ltn0 in AB.
+ Qed.
+
+ (* In this section, we prove that for any time instant t there
+ exists another time instant t' ∈ (t, t + Δ] such that the
+ processor has no carryin at time t'. *)
+ Section ProcessorIsNotTooBusyInduction.
+
+ (* Consider an arbitrary time instant t... *)
+ Variable t: time.
+
+ (* ...such that the processor has no carryin at time t. *)
+ Hypothesis H_no_carry_in: no_carry_in t.
+
+ (* First, recall that the total service is bounded by the total workload. Therefore
+ the total service of jobs in the interval [t, t + Δ) is bounded by Δ. *)
+ Lemma total_service_is_bounded_by_Δ :
+ total_service t (t + Δ) <= Δ.
+ Proof.
+ unfold total_service.
+ rewrite {3}[Δ]addn0 {2}(subnn t) addnBA // [in X in _ <= X]addnC.
+ apply service_of_jobs_le_delta.
+ by eapply arrivals_uniq; eauto 2.
+ Qed.
+
+ (* Next we consider two cases:
+ (1) The case when the total service is strictly less than Δ,
+ (2) And when the total service is equal to Δ. *)
+
+ (* In the first case, we use the pigeonhole principle to conclude
+ that there is an idle time instant; which in turn implies existence
+ of a time instant with no carryin. *)
+ Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
+ total_service t (t + Δ) < Δ >
+ exists δ, δ < Δ /\ no_carry_in (t.+1 + δ).
+ Proof.
+ unfold total_service; intros LT.
+ rewrite {3}[Δ]addn0 {2}(subnn t) addnBA // [Δ + t]addnC in LT.
+ eapply low_service_implies_existence_of_idle_time in LT; eauto; [  by rewrite leq_addr].
+ move: LT => [t_idle [/andP [LEt GTe] IDLE]].
+ move: LEt; rewrite leq_eqVlt; move => /orP [/eqP EQLT].
+ { exists 0; split; first done.
+ rewrite addn0; subst t_idle.
+ intros s ARR BEF.
+ apply idle_instant_implies_no_carry_in_at_t_pl_1 in IDLE; try done.
+ by apply IDLE.
+ }
+ have EX: exists γ, t_idle = t + γ.
+ { by exists (t_idle  t); rewrite subnKC // ltnW. }
+ move: EX => [γ EQ]; subst t_idle; rewrite ltn_add2l in GTe.
+ rewrite {1}[t]addn0 ltn_add2l in LT.
+ exists (γ.1); split.
+  apply leq_trans with γ. by rewrite prednK. by rewrite ltnW.
+  rewrite subn1 addn1 addnA subnKC //.
+ intros s ARR BEF.
+ by apply idle_instant_implies_no_carry_in_at_t.
+ Qed.
+
+ (* In the second case, the total service within the time interval [t, t + Δ) is equal to Δ.
+ On the other hand, we know that the total workload is lowerbounded by the total service
+ and upperbounded by Δ. Therefore, the total workload is equal to total service this
+ implies completion of all jobs by time [t + Δ] and hence no carryin at time [t + Δ]. *)
+ Lemma completion_of_all_jobs_implies_no_carry_in :
+ total_service t (t + Δ) = Δ >
+ no_carry_in (t + Δ).
+ Proof.
+ unfold total_service; intros EQserv.
+ move: (H_workload_is_bounded t); move => WORK.
+ have EQ: total_workload 0 (t + Δ) = service_of_jobs sched (arrivals_between 0 (t + Δ)) predT 0 (t + Δ).
+ { intros.
+ have COMPL := all_jobs_have_completed_impl_workload_eq_service
+ job_arrival job_cost arr_seq _ sched _ _ predT 0 t t.
+ feed_n 4 COMPL; try done.
+ { intros; apply H_no_carry_in.
+  eapply in_arrivals_implies_arrived; eauto 2.
+  eapply in_arrivals_implies_arrived_between in H; eauto 2.
+ by move: H => /andP [_ H].
+ }
+ apply/eqP; rewrite eqn_leq; apply/andP; split; last by apply service_of_jobs_le_workload.
+ rewrite /total_workload (workload_of_jobs_cat job_cost arr_seq (t)); last first.
+ apply/andP; split; [by done  by rewrite leq_addr].
+ rewrite (service_of_jobs_cat_scheduling_interval job_arrival _ _ _ _ _ _ _ t); try done; first last.
+ { by apply/andP; split; [by done  by rewrite leq_addr]. }
+ rewrite COMPL addnA leq_add2l.
+ rewrite service_of_jobs_cat_arrival_interval; last first.
+ apply/andP; split; [by done by rewrite leq_addr].
+ rewrite EQserv.
+ by apply H_workload_is_bounded.
+ }
+ intros s ARR BEF.
+ eapply workload_eq_service_impl_all_jobs_have_completed; eauto 2; try done.
+ by eapply arrived_between_implies_in_arrivals; eauto 2.
+ Qed.
+
+ End ProcessorIsNotTooBusyInduction.
+
+ (* Finally, we show that any interval of length Δ contains a time instant with no carryin. *)
+ Lemma processor_is_not_too_busy :
+ forall t, exists δ, δ < Δ /\ no_carry_in (t + δ).
+ Proof.
+ induction t.
+ { by exists 0; split; [  rewrite addn0; apply no_carry_in_at_the_beginning]. }
+ { move: IHt => [δ [LE FQT]].
+ move: (posnP δ) => [ZPOS]; last first.
+ { exists (δ.1); split.
+  by apply leq_trans with δ; [rewrite prednK  apply ltnW].
+  by rewrite subn1 addn1 addnA subnKC //.
+ } subst δ; rewrite addn0 in FQT; clear LE.
+ move: (total_service_is_bounded_by_Δ t); rewrite leq_eqVlt; move => /orP [/eqP EQ  LT].
+  exists (Δ.1); split.
+ + by rewrite prednK.
+ + by rewrite addSn subn1 addn1 addnA subnK; first apply completion_of_all_jobs_implies_no_carry_in.
+  by apply low_total_service_implies_existence_of_time_with_no_carry_in.
+ }
+ Qed.
+
+ End ProcessorIsNotTooBusy.
+
+ (* Consider an arbitrary job j with positive cost. *)
+ Variable j: Job.
+ Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
+ Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
+
+ (* We show that there must exists a busy interval [t1, t2) that
+ contains the arrival time of j. *)
+ Corollary exists_busy_interval_from_total_workload_bound :
+ exists t1 t2,
+ t1 <= job_arrival j < t2 /\
+ t2 <= t1 + Δ /\
+ busy_interval j t1 t2.
+ Proof.
+ have PREFIX := exists_busy_interval_prefix j _ _ (job_arrival j).
+ feed_n 3 PREFIX; try done.
+ { apply/andP; split; first by apply leqnn.
+ rewrite /completed_by /service /service_during.
+ rewrite (ignore_service_before_arrival job_arrival) //.
+ rewrite big_geq; last by apply leqnn.
+ move: H_job_cost_positive; rewrite /job_cost_positive; move => POS.
+ by rewrite ltnNge.
+ } move: PREFIX => [t1 [PREFIX /andP [GE1 _]]].
+ exists t1; move: (processor_is_not_too_busy t1.+1) => [δ [LE QT]].
+ apply no_carry_in_implies_quiet_time with (j := j) in QT.
+ have EX: exists t2, ((t1 < t2 <= t1.+1 + δ) && quiet_time_dec j t2).
+ { exists (t1.+1 + δ); apply/andP; split.
+  by apply/andP; split; first rewrite addSn ltnS leq_addr.
+  by apply/quiet_time_P. }
+ move: (ex_minnP EX) => [t2 /andP [/andP [GTt2 LEt2] QUIET] MIN]; clear EX.
+ have NEQ: t1 <= job_arrival j < t2.
+ { apply/andP; split; first by done.
+ rewrite ltnNge; apply/negP; intros CONTR.
+ move: (PREFIX) => [_ [_ [NQT _]]].
+ move: (NQT t2); clear NQT; move => NQT.
+ feed NQT; first by (apply/andP; split; [rewrite ltnS]).
+ by apply: NQT; apply/quiet_time_P.
+ }
+ exists t2; split; last split; first by done.
+ { apply leq_trans with (t1.+1 + δ); [by done  by rewrite addSn ltn_add2l]. }
+ { move: PREFIX => [_ [QTt1 [NQT _]]]; repeat split; try done.
+  move => t /andP [GEt LTt] QTt.
+ feed (MIN t).
+ { apply/andP; split.
+ + by apply/andP; split; last (apply leq_trans with t2; [apply ltnW  ]).
+ + by apply/quiet_time_P.
+ }
+ by move: LTt; rewrite ltnNge; move => /negP LTt; apply: LTt.
+  by apply/quiet_time_P.
+ }
+ Qed.
+
+ End NonOverloadedProcessor.
+
End Definitions.
End BusyIntervalJLFP.
diff git a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
index 418cba72..ac20dd71 100644
 a/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v
@@ 129,8 +129,7 @@ Module RTAforConcreteModels.
job_arrival job_cost arr_seq sched
can_be_preempted_for_fully_preemptive_model higher_eq_priority.
 (* Let L be any positive fixed point of the busy interval recurrence,
 determined by the higherorequalpriority workload. *)
+ (* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
Hypothesis H_fixed_point: L = total_rbf L.
@@ 173,7 +172,6 @@ Module RTAforConcreteModels.
rewrite /task_lock_in_service_le_task_cost. by done.
unfold task_lock_in_service_bounds_job_lock_in_service.
by intros ? ARR TSK; rewrite TSK; apply H_job_cost_le_task_cost.
  by rewrite BLOCK add0n.
 move => A /andP [LT NEQ].
specialize (H_R_is_maximum A); feed H_R_is_maximum.
{ by apply/andP; split. }
@@ 204,11 +202,10 @@ Module RTAforConcreteModels.
\max_(tsk_other < ts  (tsk_other != tsk) && (D tsk_other > D tsk))
(task_cost tsk_other  ε).
 (* Let L be any positive fixed point of the busy interval recurrence, determined by
 the sum of blocking and higherorequalpriority workload. *)
+ (* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
 Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+ Hypothesis H_fixed_point: L = total_rbf L.
(* To reduce the time complexity of the analysis, recall the notion of search space. *)
Let is_in_search_space A :=
@@ 294,11 +291,10 @@ Module RTAforConcreteModels.
\max_(tsk_other < ts  (tsk_other != tsk) && (D tsk_other > D tsk))
(task_max_nps tsk_other  ε).
 (* Let L be any positive fixed point of the busy interval recurrence, determined by
 the sum of blocking and higherorequalpriority workload. *)
+ (* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
 Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+ Hypothesis H_fixed_point: L = total_rbf L.
(* To reduce the time complexity of the analysis, recall the notion of search space. *)
Let is_in_search_space A :=
@@ 365,8 +361,7 @@ Module RTAforConcreteModels.
eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments
with (task_lock_in_service := fun tsk => (task_cost tsk  (task_last_nps tsk  ε)))
(job_lock_in_service := fun job => (job_cost job  (job_last_nps job  ε)))
 (L0 := L) (job_max_nps0 := job_max_nps)
 (job_cost0 := job_cost )
+ (L0 := L)(job_cost0 := job_cost) (task_max_nps0 := task_max_nps)
; eauto 2.
{ by apply model_with_fixed_preemption_points_is_correct. }
{ eapply model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions; eauto 2.
@@ 425,8 +420,7 @@ Module RTAforConcreteModels.
eapply number_of_preemption_points_at_least_two with (job_cost0 := job_cost); eauto 2.
eapply list_of_preemption_point_is_not_empty with (job_cost0 := job_cost); eauto 2.
}
 by done.

+ by done.
rewrite ENDj; last by done.
apply leq_trans with (job_max_nps j).
 by apply NondecreasingSequence.last_of_seq_le_max_of_seq.
@@ 525,11 +519,10 @@ Module RTAforConcreteModels.
\max_(tsk_other < ts  (tsk_other != tsk) && (D tsk_other > D tsk))
(task_max_nps tsk_other  ε).
 (* Let L be any positive fixed point of the busy interval recurrence, determined by
 the sum of blocking and higherorequalpriority workload. *)
+ (* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
 Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+ Hypothesis H_fixed_point: L = total_rbf L.
(* To reduce the time complexity of the analysis, recall the notion of search space. *)
Let is_in_search_space A :=
diff git a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
index 4e59075b..a23e31d5 100644
 a/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v
@@ 306,7 +306,7 @@ Module RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
(* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
 Hypothesis H_fixed_point: L = blocking_bound + total_rbf L.
+ Hypothesis H_fixed_point: L = total_rbf L.
(* To reduce the time complexity of the analysis, recall the notion of search space. *)
Let is_in_search_space A :=
diff git a/model/schedule/uni/limited/edf/response_time_bound.v b/model/schedule/uni/limited/edf/response_time_bound.v
index 840d5e82..be685691 100644
 a/model/schedule/uni/limited/edf/response_time_bound.v
+++ b/model/schedule/uni/limited/edf/response_time_bound.v
@@ 147,7 +147,7 @@ Module AbstractRTAforEDFwithArrivalCurves.
(* Let L be any positive fixed point of the busy interval recurrence. *)
Variable L: time.
Hypothesis H_L_positive: L > 0.
 Hypothesis H_fixed_point: L = priority_inversion_bound + total_rbf L.
+ Hypothesis H_fixed_point: L = total_rbf L.
(* Next, we define an upper bound on interfering workload received from jobs
of other tasks with higherthanorequal priority. *)
@@ 297,21 +297,15 @@ Module AbstractRTAforEDFwithArrivalCurves.
job_arrival job_cost job_task arr_seq sched tsk interference interfering_workload L.
Proof.
intros j ARR TSK POS.
 have EX := exists_busy_interval
+ have EX := exists_busy_interval_from_total_workload_bound
job_arrival job_cost arr_seq _ sched _
 EDF j _ _ _ _ _ _ priority_inversion_bound _ L.
 feed_n 12 EX; try eauto 2.
+ EDF _ _ _ _ _ L _ _ j ARR POS.
+ feed_n 9 EX; try eauto 2.
{ by unfold JLFP_is_reflexive, reflexive, EDF, Priority.EDF. }
{ intros.
 rewrite {2}H_fixed_point leq_add //.
 apply leq_trans with (workload_of_jobs job_cost (jobs_arrived_between arr_seq t (t + L)) predT).
  rewrite /workload_of_higher_or_equal_priority_jobs /workload_of_jobs
 big_mkcond [X in _ <= X]big_mkcond leq_sum //=.
 intros s _.
 by case (EDF s j).
  apply total_workload_le_total_rbf'' with job_task; try done.
 intros tsk0 IN0.
 by move: (H_family_of_proper_arrival_curves tsk0 IN0) => [ARRB _].
+ rewrite {2}H_fixed_point.
+ apply total_workload_le_total_rbf'' with job_task; try done.
+ by intros tsk0 IN0; move: (H_family_of_proper_arrival_curves tsk0 IN0) => [ARRB _].
}
move: EX => [t1 [t2 [H1 [H2 GGG]]]].
exists t1, t2; split; first by done.
diff git a/model/schedule/uni/service.v b/model/schedule/uni/service.v
index e85763d7..3abcb64b 100644
 a/model/schedule/uni/service.v
+++ b/model/schedule/uni/service.v
@@ 203,6 +203,7 @@ Module Service.
(* ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+ Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
(* For simplicity, let's define some local names. *)
Let job_completed_by := completed_by job_cost sched.
@@ 365,6 +366,95 @@ Module Service.
move => t' _.
by apply service_of_jobs_le_1.
Qed.
+
+ (* Next we prove that total service that is lower than the
+ range implies the existence of an idle time instant. *)
+ Lemma low_service_implies_existence_of_idle_time :
+ forall t1 t2,
+ t1 <= t2 >
+ service_of_jobs sched (arrivals_between 0 t2) predT t1 t2 < t2  t1 >
+ exists t, t1 <= t < t2 /\ is_idle sched t.
+ Proof.
+ intros ? ? LE SERV.
+ have EX: exists δ, t2 = t1 + δ.
+ { by exists (t2  t1); rewrite subnKC // ltnW. }
+ move: EX => [δ EQ]; subst t2; clear LE.
+ rewrite {3}[t1 + δ]addnC addnBA // subnn addn0 in SERV.
+ rewrite /service_of_jobs exchange_big //= in SERV.
+ apply sum_le_summation_range in SERV.
+ move: SERV => [x [/andP [GEx LEx] L]].
+ exists x; split; first by apply/andP; split.
+ apply/negPn; apply/negP; intros NIDLE.
+ unfold is_idle in NIDLE.
+ destruct(sched x) eqn:SCHED; last by done.
+ move: SCHED => /eqP SCHED; clear NIDLE.
+ move: L => /eqP; rewrite sum_nat_eq0_nat; move => /allP L.
+ specialize (L s); feed L.
+ { unfold arrivals_between.
+ eapply arrived_between_implies_in_arrivals; eauto 2.
+ apply/andP; split; first by done.
+ apply H_jobs_must_arrive_to_execute in SCHED.
+ by apply leq_ltn_trans with x.
+ }
+ by move: L; simpl; rewrite /service_at /scheduled_at SCHED eqb0; move => /eqP EQ.
+ Qed.
+
+ (* In this section we prove a few facts about splitting
+ the total service of a set of jobs. *)
+ Section ServiceCat.
+
+ (* We show that the total service of jobs released in a time interval [t1,t2) during [t1,t2)
+ is equal to the sum of:
+ (1) the total service of jobs released in time interval [t1, t) during time [t1, t)
+ (2) the total service of jobs released in time interval [t1, t) during time [t, t2)
+ and (3) the total service of jobs released in time interval [t, t2) during time [t, t2). *)
+ Lemma service_of_jobs_cat_scheduling_interval :
+ forall P t1 t2 t,
+ t1 <= t <= t2 >
+ service_of_jobs sched (arrivals_between t1 t2) P t1 t2
+ = service_of_jobs sched (arrivals_between t1 t) P t1 t
+ + service_of_jobs sched (arrivals_between t1 t) P t t2
+ + service_of_jobs sched (arrivals_between t t2) P t t2.
+ Proof.
+ move => P t1 t2 t /andP [GEt LEt].
+ rewrite /arrivals_between (job_arrived_between_cat _ _ t) //.
+ rewrite {1}/service_of_jobs big_cat //=.
+ rewrite exchange_big //= (@big_cat_nat _ _ _ t) //=;
+ rewrite [in X in X + _ + _]exchange_big //= [in X in _ + X + _]exchange_big //=.
+ apply/eqP; rewrite !addnA eqn_add2l eqn_add2l.
+ rewrite exchange_big //= (@big_cat_nat _ _ _ t) //= [in X in _ + X]exchange_big //=.
+ rewrite [service_of_jobs _ _ _ _ _]add0n /service_of_jobs eqn_add2r.
+ rewrite big_nat_cond big1 //.
+ move => x /andP [/andP [GEi LTi] _].
+ rewrite big_seq_cond big1 //.
+ move => s /andP [ARR Ps].
+ rewrite /service_at /scheduled_at.
+ apply/eqP; rewrite eqb0; apply/negP; intros SCHED.
+ apply H_jobs_must_arrive_to_execute in SCHED.
+ eapply in_arrivals_implies_arrived_between in ARR; eauto 2.
+ move: SCHED; rewrite /has_arrived leqNgt; move => /negP CONTR; apply: CONTR.
+ move: ARR => /andP [ARR1 ARR2].
+ by apply leq_trans with t.
+ Qed.
+
+ (* We show that the total service of jobs released in a time interval [t1,t2) during [t,t2)
+ is equal to the sum of:
+ (1) the total service of jobs released in a time interval [t1,t) during [t,t2)
+ and (2) the total service of jobs released in a time interval [t,t2) during [t,t2). *)
+ Lemma service_of_jobs_cat_arrival_interval :
+ forall P t1 t2 t,
+ t1 <= t <= t2 >
+ service_of_jobs sched (arrivals_between t1 t2) P t t2 =
+ service_of_jobs sched (arrivals_between t1 t) P t t2 +
+ service_of_jobs sched (arrivals_between t t2) P t t2.
+ Proof.
+ move => P t1 t2 t /andP [GEt LEt].
+ apply/eqP;rewrite eq_sym; apply/eqP.
+ rewrite /arrivals_between [in X in _ = X](job_arrived_between_cat _ _ t) //.
+ by rewrite {3}/service_of_jobs big_cat //=.
+ Qed.
+
+ End ServiceCat.
(* In this section, we introduce a connection between the cumulative
service, cumulative workload, and completion of jobs. *)
diff git a/util/sum.v b/util/sum.v
index 5e54b774..106e8900 100644
 a/util/sum.v
+++ b/util/sum.v
@@ 261,6 +261,28 @@ Section ExtraLemmas.
rewrite addnC addnBA; last by done.
by rewrite subnn addn0.
Qed.
+
+ (* We show that the fact that the sum is smaller than the range
+ of the summation implies the existence of a zero element. *)
+ Lemma sum_le_summation_range :
+ forall f t Δ,
+ \sum_(t <= x < t + Δ) f x < Δ >
+ exists x, t <= x < t + Δ /\ f x = 0.
+ Proof.
+ induction Δ; intros; first by rewrite ltn0 in H.
+ destruct (f (t + Δ)) eqn: EQ.
+ { exists (t + Δ); split; last by done.
+ by apply/andP; split; [rewrite leq_addr  rewrite addnS ltnS].
+ }
+ { move: H; rewrite addnS big_nat_recr //= ?leq_addr // EQ addnS ltnS; move => H.
+ feed IHΔ.
+ { by apply leq_ltn_trans with (\sum_(t <= i < t + Δ) f i + n); first rewrite leq_addr. }
+ move: IHΔ => [z [/andP [LE GE] ZERO]].
+ exists z; split; last by done.
+ apply/andP; split; first by done.
+ by rewrite ltnS ltnW.
+ }
+ Qed.
End ExtraLemmas.

GitLab