Library prosa.analysis.facts.busy_interval.carry_in
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.carry_in.
Require Export prosa.analysis.facts.busy_interval.busy_interval.
Require Export prosa.analysis.definitions.carry_in.
Require Export prosa.analysis.facts.busy_interval.busy_interval.
Throughout this file, we assume ideal uniprocessor schedules.
Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model.
Existence of No Carry-In Instant
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any arrival sequence with consistent arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Next, consider any ideal uniprocessor schedule of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Assume a given JLFP policy.
For simplicity, let's define some local names.
Let job_pending_at := pending sched.
Let job_completed_by := completed_by sched.
Let arrivals_between := arrivals_between arr_seq.
Let no_carry_in := no_carry_in arr_seq sched.
Let quiet_time := quiet_time arr_seq sched.
Let job_completed_by := completed_by sched.
Let arrivals_between := arrivals_between arr_seq.
Let no_carry_in := no_carry_in arr_seq sched.
Let quiet_time := quiet_time arr_seq sched.
The fact that there is no carry-in at time instant t
trivially implies that t is a quiet time.
Lemma no_carry_in_implies_quiet_time :
∀ j t,
no_carry_in t →
quiet_time j t.
Proof.
by intros j t FQT j_hp ARR HP BEF; apply FQT.
Qed.
∀ 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 the schedule is work-conserving, ...
... and there are no duplicate job arrivals.
We show that an idle time implies no carry in at this time instant.
Lemma idle_instant_implies_no_carry_in_at_t :
∀ 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_def IDLE. }
{ by apply/andP; split; [apply ltnW | done]. }
}
move: NIDLE ⇒ [j' SCHED].
by rewrite scheduled_at_def IDLE in SCHED.
Qed.
∀ 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_def IDLE. }
{ by apply/andP; split; [apply ltnW | done]. }
}
move: NIDLE ⇒ [j' SCHED].
by rewrite scheduled_at_def 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 :
∀ 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_def 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_def IDLE in SCHED.
Qed.
∀ 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_def 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_def IDLE in SCHED.
Qed.
Let the priority relation be reflexive.
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 Δ: duration.
Hypothesis H_delta_positive: Δ > 0.
Hypothesis H_workload_is_bounded: ∀ t, total_workload t (t + Δ) ≤ Δ.
Hypothesis H_delta_positive: Δ > 0.
Hypothesis H_workload_is_bounded: ∀ t, total_workload t (t + Δ) ≤ Δ.
Next we prove that since for any time instant t there is a point where
the total workload is upper-bounded by the supply the processor encounters
no carry-in instants at least every Δ time units.
We start by proving that the processor has no carry-in at
the beginning (i.e., has no carry-in 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.
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 carry-in at time t'.
Consider an arbitrary time instant t...
...such that the processor has no carry-in at time 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_length_of_interval'.
by eapply arrivals_uniq; eauto 2.
Qed.
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_length_of_interval'.
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 carry-in.
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ 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.
move: LT ⇒ [t_idle [/andP [LEt GTe] IDLE]].
move: LEt; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ|LT].
{ ∃ 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: ∃ γ, t_idle = t + γ.
{ by ∃ (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.
∃ (γ.-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.
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ 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.
move: LT ⇒ [t_idle [/andP [LEt GTe] IDLE]].
move: LEt; rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ|LT].
{ ∃ 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: ∃ γ, t_idle = t + γ.
{ by ∃ (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.
∃ (γ.-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 lower-bounded by the total service
and upper-bounded by Δ. Therefore, the total workload is equal to total service this
implies completion of all jobs by time [t + Δ] and hence no carry-in 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 predT (arrivals_between 0 (t + Δ)) 0 (t + Δ).
{ intros.
have COMPL := all_jobs_have_completed_impl_workload_eq_service
arr_seq H_arrival_times_are_consistent sched
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.
feed COMPL; try done.
{ intros j A B; apply H_no_carry_in.
- eapply in_arrivals_implies_arrived; eauto 2.
- eapply in_arrivals_implies_arrived_between in A; eauto 2.
}
apply/eqP; rewrite eqn_leq; apply/andP; split;
last by apply service_of_jobs_le_workload;
auto using ideal_proc_model_provides_unit_service.
rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first.
apply/andP; split; [by done | by rewrite leq_addr].
rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ 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.
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 predT (arrivals_between 0 (t + Δ)) 0 (t + Δ).
{ intros.
have COMPL := all_jobs_have_completed_impl_workload_eq_service
arr_seq H_arrival_times_are_consistent sched
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.
feed COMPL; try done.
{ intros j A B; apply H_no_carry_in.
- eapply in_arrivals_implies_arrived; eauto 2.
- eapply in_arrivals_implies_arrived_between in A; eauto 2.
}
apply/eqP; rewrite eqn_leq; apply/andP; split;
last by apply service_of_jobs_le_workload;
auto using ideal_proc_model_provides_unit_service.
rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first.
apply/andP; split; [by done | by rewrite leq_addr].
rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ 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 carry-in.
Lemma processor_is_not_too_busy :
∀ t, ∃ δ, δ < Δ ∧ no_carry_in (t + δ).
Proof.
induction t.
{ by ∃ 0; split; [ | rewrite addn0; apply no_carry_in_at_the_beginning]. }
{ move: IHt ⇒ [δ [LE FQT]].
move: (posnP δ) ⇒ [Z|POS]; last first.
{ ∃ (δ.-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].
- ∃ (Δ.-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.
∀ t, ∃ δ, δ < Δ ∧ no_carry_in (t + δ).
Proof.
induction t.
{ by ∃ 0; split; [ | rewrite addn0; apply no_carry_in_at_the_beginning]. }
{ move: IHt ⇒ [δ [LE FQT]].
move: (posnP δ) ⇒ [Z|POS]; last first.
{ ∃ (δ.-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].
- ∃ (Δ.-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 j.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Corollary exists_busy_interval_from_total_workload_bound :
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + Δ ∧
busy_interval arr_seq sched j t1 t2.
Proof.
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
edestruct (exists_busy_interval_prefix
arr_seq H_arrival_times_are_consistent sched j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]].
apply job_pending_at_arrival; auto.
move: GE ⇒ /andP [GE1 _].
∃ 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: ∃ t2, ((t1 < t2 ≤ t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).
{ ∃ (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.
}
∃ 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 ExistsNoCarryIn.
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + Δ ∧
busy_interval arr_seq sched j t1 t2.
Proof.
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
edestruct (exists_busy_interval_prefix
arr_seq H_arrival_times_are_consistent sched j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]].
apply job_pending_at_arrival; auto.
move: GE ⇒ /andP [GE1 _].
∃ 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: ∃ t2, ((t1 < t2 ≤ t1.+1 + δ) && quiet_time_dec arr_seq sched j t2).
{ ∃ (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.
}
∃ 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 ExistsNoCarryIn.