Require Export rt.restructuring.analysis.definitions.no_carry_in.
Require Export rt.restructuring.analysis.facts.busy_interval_exists.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import rt.restructuring.model.processor.ideal.
(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
Require Import rt.restructuring.model.readiness.basic.
(** * Existence of No Carry-In Instant *)
(** 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 high-priority workload) generated by the task set to be bounded. *)
(** Next, we derive a sufficient condition for existence of
no carry-in instant for uniprocessor for JLFP schedulers *)
Section ExistsNoCarryIn.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
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.
(** 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.
(** ... 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.
(** Assume a given JLFP policy. *)
Variable higher_eq_priority : JLFP_policy Job.
(** 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 higher_eq_priority.
(** 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 :
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 the schedule is work-conserving, ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
(** ... and there are no duplicate job arrivals. *)
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_uniq arr_seq.
(** 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_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 :
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_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. *)
Hypothesis H_priority_is_reflexive: reflexive_priorities.
(** Recall the notion of workload of all jobs released in a given interval [t1, t2)... *)
Let total_workload t1 t2 :=
workload_of_jobs predT (arrivals_between t1 t2).
(** ... and total service of jobs within some time interval [t1, t2). *)
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between 0 t2) 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 Δ: duration.
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 upper-bounded by the supply the processor encounters
no carry-in instants at least every Δ time units. *)
Section ProcessorIsNotTooBusy.
(** 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.
(** 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'. *)
Section ProcessorIsNotTooBusyInduction.
(** Consider an arbitrary time instant t... *)
Variable t: duration.
(** ...such that the processor has no carry-in 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_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 + Δ) < Δ ->
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.
move: LT => [t_idle [/andP [LEt GTe] IDLE]].
move: LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
{ 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 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.
(** Finally, we show that any interval of length Δ contains a time instant with no carry-in. *)
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 δ) => [Z|POS]; 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 j.
(** We show that there must exist 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 arr_seq sched higher_eq_priority 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 higher_eq_priority j ARR H_priority_is_reflexive (job_arrival j))
as [t1 [PREFIX GE]].
apply job_pending_at_arrival; auto.
move: GE => /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 arr_seq sched higher_eq_priority 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 ExistsNoCarryIn.