diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index 7f7b0151adc4aa5e035bcba30bff02d044a4973e..cad93d2d939ef9a318d91b0bedbfa486f6fabd63 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -697,7 +697,11 @@ Section JLFPInstantiation.
move => j ARR TSK POS.
edestruct busy_interval_from_total_workload_bound
with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]] => //.
- { by move => t; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
+ { move => t _; rewrite {3}H_fixed_point.
+ have ->: blackout_during sched t (t + L) = 0.
+ { apply/eqP; rewrite /blackout_during big1 // => l _.
+ by rewrite /is_blackout ideal_proc_has_supply. }
+ by rewrite add0n; apply total_workload_le_total_rbf. }
exists t1, t2; split=> [//|]; split=> [//|].
by apply instantiated_busy_interval_equivalent_busy_interval.
Qed.
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index a4a055750046a5de03ea97ec80feaa6be15097b6..4eccd7890dcfe492dc0a91026767448c07e40eaf 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -21,17 +21,17 @@ Section BusyIntervalExistence.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
- Context {Arrival: JobArrival Job}.
- Context {Cost : JobCost Job}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
(** Consider any valid arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
- (** Allow for any uniprocessor model that ensures ideal progress. *)
+ (** Allow for any fully-consuming uniprocessor model. *)
Context {PState : ProcessorState Job}.
- Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_uniproc : uniprocessor_model PState.
+ Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.
(** Next, consider any schedule of the arrival sequence ... *)
Variable sched : schedule PState.
@@ -47,7 +47,7 @@ Section BusyIntervalExistence.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
(** Further, allow for any work-bearing notion of job readiness ... *)
- Context `{@JobReady Job PState Cost Arrival}.
+ Context `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
(** ... and assume that the schedule is work-conserving. *)
@@ -74,10 +74,8 @@ Section BusyIntervalExistence.
~ is_idle arr_seq sched t.
Proof.
move=> j t ARR PEND IDLE.
- have [jhp [ARRhp [READYhp _]]] : exists j_hp : Job,
- arrives_in arr_seq j_hp
- /\ job_ready sched j_hp t
- /\ hep_job j_hp j
+ have [jhp [ARRhp [READYhp _]]] :
+ exists j_hp : Job, arrives_in arr_seq j_hp /\ job_ready sched j_hp t /\ hep_job j_hp j
by apply: H_job_ready.
move: IDLE; rewrite is_idle_iff => /eqP; rewrite scheduled_job_at_none => // IDLE.
have [j_other SCHED]: exists j_other : Job, scheduled_at sched j_other t
@@ -124,14 +122,18 @@ Section BusyIntervalExistence.
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2.
- (** We assume that, for some positive [Δ], the total workload generated in any
- interval of length [Δ] is bounded by [Δ] (i.e., the supply provided by an
- ideal-progress unit-speed processor). Note that this assumption bounds the
- total workload of jobs released in a time interval <<[t, t + Δ)>>
- regardless of their priorities. *)
+ (** We assume that, for some positive [Δ], the sum of the total
+ blackout and the total workload generated in any interval of
+ length [Δ] starting with no carry-in is bounded by [Δ]. 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 + Δ) <= Δ.
+ Hypothesis H_workload_is_bounded :
+ forall t,
+ no_carry_in arr_seq sched t ->
+ blackout_during sched t (t + Δ) + total_workload t (t + Δ) <= Δ.
(** In the following, we also require a unit-speed processor. *)
Hypothesis H_unit_service_proc_model : unit_service_proc_model PState.
@@ -155,31 +157,46 @@ Section BusyIntervalExistence.
Hypothesis H_no_carry_in : no_carry_in arr_seq sched 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 [Δ]. *)
+ workload. Therefore the sum of the total blackout and the
+ total service of jobs in the interval <<[t, t + Δ)>> is
+ bounded by [Δ]. *)
Lemma total_service_is_bounded_by_Δ :
- total_service t (t + Δ) <= Δ.
+ blackout_during sched t (t + Δ) + total_service t (t + Δ) <= Δ.
Proof.
- rewrite /total_service -{3}[Δ]addn0 -{2}(subnn t) addnBA // [in X in _ <= X]addnC.
- by apply: service_of_jobs_le_length_of_interval'.
+ have EQ: \sum_(t <= x < t + Δ) 1 = Δ.
+ { by rewrite big_const_nat iter_addn mul1n addn0 -{2}[t]addn0 subnDl subn0. }
+ rewrite -{3}EQ {EQ}.
+ rewrite /total_service /blackout_during /supply.blackout_during.
+ rewrite /service_of_jobs/service_during/service_at exchange_big //=.
+ rewrite -big_split //= leq_sum //; move => t' _.
+ have [BL|SUP] := blackout_or_supply sched t'.
+ { rewrite -[1]addn0; apply leq_add; first by case: (is_blackout).
+ rewrite leqn0; apply/eqP; apply big1 => j _.
+ eapply no_service_during_blackout in BL.
+ by apply: BL. }
+ { rewrite /is_blackout SUP add0n.
+ exact: service_of_jobs_le_1. }
Qed.
(** Next we consider two cases:
- (1) The case when the total service is strictly less than [Δ], and
- (2) the case when the total service is equal to [Δ]. *)
+ (1) The case when the sum of blackout and service is strictly less than [Δ], and
+ (2) the case when the sum of blackout and 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 arr_seq sched (t.+1 + δ).
+ blackout_during sched t (t + Δ) + total_service t (t + Δ) < Δ ->
+ exists δ,
+ δ < Δ /\ no_carry_in arr_seq sched (t.+1 + δ).
Proof.
- rewrite /total_service-{3}[Δ]addn0 -{2}(subnn t) addnBA // [Δ + t]addnC => ?.
+ rewrite /total_service-{3}[Δ]addn0 -{2}(subnn t) addnBA // [Δ + t]addnC => LTS.
have [t_idle [/andP [LEt GTe] IDLE]]: exists t0 : nat,
t <= t0 < t + Δ
- /\ is_idle arr_seq sched t0
- by apply: low_service_implies_existence_of_idle_time =>//.
+ /\ is_idle arr_seq sched t0.
+ { apply: low_service_implies_existence_of_idle_time_rs =>//.
+ rewrite !subnKC in LTS; try by apply leq_addr.
+ by rewrite addKn. }
move: LEt; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
{ exists 0; split => //.
rewrite addn0 EQ => s ARR BEF.
@@ -196,14 +213,15 @@ Section BusyIntervalExistence.
exact: idle_instant_no_carry_in.
Qed.
- (** In the second case, the total service within the time interval
- <<[t, t + Δ)>> is equal to [Δ]. We also know that the total
- workload is lower-bounded by the total service and upper-bounded
- by [Δ]. Therefore, the total workload is equal to the total service,
- which implies completion of all jobs by time [t + Δ] and hence no
- carry-in at time [t + Δ]. *)
+ (** In the second case, the sum of blackout and service within
+ the time interval <<[t, t + Δ)>> is equal to [Δ]. We also
+ know that the total workload is lower-bounded by the total
+ service and upper-bounded by [Δ]. Therefore, the total
+ workload is equal to the total service, which 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 + Δ) = Δ ->
+ blackout_during sched t (t + Δ) + total_service t (t + Δ) = Δ ->
no_carry_in arr_seq sched (t + Δ).
Proof.
rewrite /total_service => EQserv s ARR BEF.
@@ -231,7 +249,7 @@ Section BusyIntervalExistence.
+ rewrite COMPL -addnA leq_add2l.
rewrite -service_of_jobs_cat_arrival_interval;
last by apply/andP; split; [|rewrite leq_addr].
- by rewrite EQserv.
+ by evar (b : nat); rewrite -(leq_add2l b) EQserv.
Qed.
End ProcessorIsNotTooBusyInduction.
@@ -260,10 +278,6 @@ Section BusyIntervalExistence.
(** ** Busy Interval Existence *)
- (** We now derive the existence of a busy interval from the preceding lemma,
- under the strengthened assumption of an ideal-progress processor. *)
- Hypothesis H_progress : ideal_progress_proc_model PState.
-
(** Consider an arbitrary job [j] with positive cost. *)
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
@@ -311,4 +325,3 @@ Section BusyIntervalExistence.
Qed.
End BusyIntervalExistence.
-
diff --git a/analysis/facts/model/ideal/service_of_jobs.v b/analysis/facts/model/ideal/service_of_jobs.v
index e2d9ff4ab71a631a11488afd1102fd62572b8ea6..602e54577ce090697a548043ab814769f5113b2c 100644
--- a/analysis/facts/model/ideal/service_of_jobs.v
+++ b/analysis/facts/model/ideal/service_of_jobs.v
@@ -1,17 +1,87 @@
-Require Export prosa.model.schedule.scheduled.
-Require Export prosa.model.aggregate.workload.
+Require Export prosa.model.priority.classes.
Require Export prosa.model.aggregate.service_of_jobs.
-Require Export prosa.analysis.facts.model.service_of_jobs.
-Require Export prosa.analysis.facts.behavior.completion.
-Require Export prosa.analysis.facts.model.scheduled.
+Require Export prosa.analysis.facts.behavior.service.
+(** * Service Received by Sets of Jobs in Uniprocessor Schedules *)
+
+(** In this section, we establish a fact about the service received by
+ _sets_ of jobs in the presence of idle times on a fully-consuming
+ uniprocessor model. *)
+Section FullyConsumingModelLemmas.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** Allow for any fully-consuming uniprocessor model. *)
+ Context {PState : ProcessorState Job}.
+ Hypothesis H_uniproc : uniprocessor_model PState.
+ Hypothesis H_fully_consuming_proc_model : fully_consuming_proc_model PState.
+
+ (** Consider any arrival sequence with consistent arrivals. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** Next, consider any schedule of this arrival sequence ... *)
+ Variable sched : schedule PState.
+ 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.
+
+ (** Let [P] be any predicate over jobs. *)
+ Variable P : pred Job.
+
+ (** We prove that, if the sum of the total blackout and the total
+ service within some time interval <<[t1,t2)>> is smaller than
+ [t2 - t1], then there is an idle time instant <<t ∈ [t1,t2)>>. *)
+ Lemma low_service_implies_existence_of_idle_time_rs :
+ forall t1 t2,
+ blackout_during sched t1 t2
+ + service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
+ exists t,
+ t1 <= t < t2 /\ is_idle arr_seq sched t.
+ Proof.
+ move=> t1 t2 SERV.
+ destruct (t1 <= t2) eqn:LE; last first.
+ { move: LE => /negP/negP; rewrite -ltnNge.
+ move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.
+ by move: LT => /eqP -> in SERV; rewrite ltn0 in SERV.
+ }
+ interval_to_duration t1 t2 δ.
+ rewrite {4}[t1 + δ]addnC -addnBA // subnn addn0 in SERV.
+ rewrite /service_of_jobs exchange_big //= in SERV.
+ rewrite -big_split //= in SERV.
+ apply sum_le_summation_range in SERV.
+ move: SERV => [x [/andP [GEx LEx] L]].
+ exists x; split; first by apply/andP; split.
+ move: L => /eqP; rewrite addn_eq0 eqb0 sum_nat_eq0_nat filter_predT => /andP [SUP /allP L].
+ apply/negPn/negP; rewrite is_nonidle_iff //= => [[j SCHED]].
+ have /eqP: service_at sched j x == 0.
+ { apply/L/arrived_between_implies_in_arrivals => //.
+ rewrite /arrived_between; apply/andP; split => //.
+ have: job_arrival j <= x by apply: H_jobs_must_arrive_to_execute.
+ lia. }
+ move: SUP; rewrite negbK => SUP SERV.
+ eapply ideal_progress_inside_supplies in SUP => //.
+ by move: SUP; rewrite /receives_service_at SERV.
+ Qed.
+
+End FullyConsumingModelLemmas.
(** * Service Received by Sets of Jobs in Uniprocessor Ideal-Progress Schedules *)
-(** In this file, we establish a fact about the service received by _sets_ of
+(** Next, we establish a fact about the service received by sets of
jobs in the presence of idle times on a uniprocessor under the
- ideal-progress assumption (i.e., that a scheduled job necessarily receives
- nonzero service). *)
+ ideal-progress assumption (i.e., that a scheduled job necessarily
+ receives nonzero service). *)
Section IdealModelLemmas.
(** Consider any type of tasks ... *)
@@ -29,8 +99,8 @@ Section IdealModelLemmas.
(** Allow for any uniprocessor model that ensures ideal progress. *)
Context {PState : ProcessorState Job}.
- Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_uniproc : uniprocessor_model PState.
+ Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
(** Next, consider any ideal uni-processor schedule of this arrival sequence ... *)
Variable sched : schedule PState.
@@ -45,11 +115,12 @@ Section IdealModelLemmas.
Variable P : pred Job.
(** We prove that if the total service within some time interval <<[t1,t2)>>
- is smaller than <<t2 - t1>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
+ is smaller than <<[t2 - t1]>>, then there is an idle time instant [t ∈ [t1,t2)]. *)
Lemma low_service_implies_existence_of_idle_time :
forall t1 t2,
service_of_jobs sched predT (arrivals_between arr_seq 0 t2) t1 t2 < t2 - t1 ->
- exists t, t1 <= t < t2 /\ is_idle arr_seq sched t.
+ exists t,
+ t1 <= t < t2 /\ is_idle arr_seq sched t.
Proof.
move=> t1 t2 SERV.
destruct (t1 <= t2) eqn:LE; last first.
@@ -57,9 +128,7 @@ Section IdealModelLemmas.
move => LT; apply ltnW in LT; rewrite -subn_eq0 in LT.
by move: LT => /eqP -> in SERV; rewrite ltn0 in SERV.
}
- have EX: exists δ, t2 = t1 + δ.
- { by exists (t2 - t1); rewrite subnKC // ltnW. }
- move: EX => [δ EQ]; subst t2; clear LE.
+ interval_to_duration t1 t2 δ.
rewrite {3}[t1 + δ]addnC -addnBA // subnn addn0 in SERV.
rewrite /service_of_jobs exchange_big //= in SERV.
apply sum_le_summation_range in SERV.