diff --git a/analysis/abstract/busy_interval.v b/analysis/abstract/busy_interval.v
index 8743a4a027902e0cbc6d2843cc4b43d745bdbb7e..17fd72fae8a7adafd7d74b5f62ca0a2c151b97b7 100644
--- a/analysis/abstract/busy_interval.v
+++ b/analysis/abstract/busy_interval.v
@@ -1,5 +1,6 @@
Require Export prosa.analysis.abstract.iw_auxiliary.
Require Export prosa.analysis.facts.model.workload.
+Require Export prosa.analysis.abstract.definitions.
(** * Lemmas About Abstract Busy Intervals *)
diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index 73f0c97ec7c05e87da86f0e3805aaf30c25c0cd2..b8c121db3162156dce8695b419a9cf878db55b02 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -344,42 +344,6 @@ Section JLFPInstantiation.
End InstantiatedWorkloadEquivalence.
- (** In this section, we prove that the (abstract) cumulative
- interference of jobs with higher or equal priority is equal to
- total service of jobs with higher or equal priority. *)
- Section InstantiatedServiceEquivalences.
-
- (** Consider any job [j] of [tsk]. *)
- Variable j : Job.
- Hypothesis H_j_arrives : arrives_in arr_seq j.
- Hypothesis H_job_of_tsk : job_of_task tsk j.
-
- (** We consider an arbitrary time interval <<[t1, t)>> that
- starts with a quiet time. *)
- Variable t1 t : instant.
- Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
-
- (** As follows from lemma [cumulative_pred_served_eq_service],
- the (abstract) instantiated function of interference is
- equal to the total service of any subset of jobs with higher
- or equal priority. *)
-
- (** The above is in particular true for the jobs other
- than [j] with higher or equal priority... *)
- Lemma cumulative_i_ohep_eq_service_of_ohep :
- cumulative_another_hep_job_interference arr_seq sched j t1 t
- = service_of_other_hep_jobs arr_seq sched j t1 t.
- Proof. by apply: cumulative_pred_served_eq_service => // => ? /andP[]. Qed.
-
- (** ...and for jobs from other tasks than [j] with higher
- or equal priority. *)
- Lemma cumulative_i_thep_eq_service_of_othep :
- cumulative_another_task_hep_job_interference arr_seq sched j t1 t
- = service_of_other_task_hep_jobs arr_seq sched j t1 t.
- Proof. by apply: cumulative_pred_served_eq_service => // => ? /andP[]. Qed.
-
- End InstantiatedServiceEquivalences.
-
(** In this section we prove that the abstract definition of busy
interval is equivalent to the conventional, concrete
definition of busy interval for JLFP scheduling. *)
@@ -390,15 +354,15 @@ Section JLFPInstantiation.
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
Let quiet_time_cl := classical.quiet_time arr_seq sched.
- Let quiet_time_ab := definitions.quiet_time sched.
+ Let quiet_time_ab := abstract.definitions.quiet_time sched.
(** Same for the two notions of a busy interval prefix ... *)
Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
- Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
+ Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
(** ... and the two notions of a busy interval. *)
Let busy_interval_cl := classical.busy_interval arr_seq sched.
- Let busy_interval_ab := definitions.busy_interval sched.
+ Let busy_interval_ab := abstract.definitions.busy_interval sched.
(** Consider any job j of [tsk]. *)
Variable j : Job.
@@ -445,8 +409,7 @@ Section JLFPInstantiation.
erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
- rewrite -/(service_of_other_hep_jobs arr_seq _ j 0 t) -cumulative_i_ohep_eq_service_of_ohep; eauto;
- last by move => ? _ _ ; unfold arrived_before; lia.
+ rewrite -/(service_of_other_hep_jobs arr_seq _ j 0 t) -cumulative_i_ohep_eq_service_of_ohep => //.
rewrite -/(workload_of_other_hep_jobs _ j 0 t) -cumulative_iw_hep_eq_workload_of_ohep; eauto.
move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
{ have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
diff --git a/analysis/abstract/iw_auxiliary.v b/analysis/abstract/iw_auxiliary.v
index fb17f86922faf22325535fa79ed7a02d7566577e..2aa1dbc6b74af9b09b3dec1225bb9c7f8d70ee16 100644
--- a/analysis/abstract/iw_auxiliary.v
+++ b/analysis/abstract/iw_auxiliary.v
@@ -2,6 +2,9 @@ Require Export prosa.analysis.definitions.interference.
Require Export prosa.analysis.definitions.task_schedule.
Require Export prosa.analysis.facts.priority.classes.
Require Export prosa.analysis.abstract.restricted_supply.busy_prefix.
+Require Export prosa.model.aggregate.service_of_jobs.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+
(** * Auxiliary Lemmas About Interference and Interfering Workload. *)
@@ -416,6 +419,53 @@ Section InterferenceAndInterferingWorkloadAuxiliary.
End SupplyAndScheduledJob.
+ (** In this section, we prove that the (abstract) cumulative
+ interference of jobs with higher or equal priority is equal to
+ total service of jobs with higher or equal priority. *)
+ Section InstantiatedServiceEquivalences.
+
+ (** First, let us assume that the introduced processor model is
+ unit-service. *)
+ Hypothesis H_unit_service : unit_service_proc_model PState.
+
+ (** Consider any job [j] of [tsk]. *)
+ Variable j : Job.
+ Hypothesis H_j_arrives : arrives_in arr_seq j.
+ Hypothesis H_job_of_tsk : job_of_task tsk j.
+
+ (** We consider an arbitrary time interval <<[t1, t)>> that
+ starts with a (classic) quiet time. *)
+ Variable t1 t : instant.
+ Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
+
+ (** As follows from lemma [cumulative_pred_served_eq_service],
+ the (abstract) instantiated function of interference is
+ equal to the total service of any subset of jobs with higher
+ or equal priority. *)
+
+ (** The above is in particular true for the jobs other
+ than [j] with higher or equal priority... *)
+ Lemma cumulative_i_ohep_eq_service_of_ohep :
+ cumulative_another_hep_job_interference arr_seq sched j t1 t
+ = service_of_other_hep_jobs arr_seq sched j t1 t.
+ Proof.
+ apply: cumulative_pred_served_eq_service => //.
+ - by move => ? /andP[].
+ Qed.
+
+ (** ...and for jobs from other tasks than [j] with higher
+ or equal priority. *)
+ Lemma cumulative_i_thep_eq_service_of_othep :
+ cumulative_another_task_hep_job_interference arr_seq sched j t1 t
+ = service_of_other_task_hep_jobs arr_seq sched j t1 t.
+ Proof.
+ apply: cumulative_pred_served_eq_service => //.
+ by move => ? /andP[].
+ Qed.
+
+ End InstantiatedServiceEquivalences.
+
+
End Equivalences.
End InterferenceAndInterferingWorkloadAuxiliary.
diff --git a/analysis/abstract/restricted_supply/bounded_bi/aux.v b/analysis/abstract/restricted_supply/bounded_bi/aux.v
index 657576fe275d094e6acbca5da6e02cc11832c93c..59733026b57da75093ac077ae21706c68d2775f4 100644
--- a/analysis/abstract/restricted_supply/bounded_bi/aux.v
+++ b/analysis/abstract/restricted_supply/bounded_bi/aux.v
@@ -156,7 +156,10 @@ Section BoundedBusyIntervalsAux.
}
}
rewrite cumulative_interfering_workload_split // cumulative_interference_split //.
- rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //; last by apply PREF.
+ rewrite cumulative_iw_hep_eq_workload_of_ohep cumulative_i_ohep_eq_service_of_ohep //;
+ [
+ | exact: unit_supply_is_unit_service
+ | by apply PREF ].
rewrite -[leqRHS]addnC -[leqRHS]addnA [(_ + workload_of_job _ _ _ _ )]addnC.
rewrite workload_job_and_ahep_eq_workload_hep //.
rewrite -addnC -addnA [(_ + service_during _ _ _ _ )]addnC.
diff --git a/analysis/abstract/restricted_supply/iw_instantiation.v b/analysis/abstract/restricted_supply/iw_instantiation.v
index 8d0a27938200ae22cfbd4c647629ff7a65562265..b2daab1abc06c93a1ce6db55c78884ebe4208efa 100644
--- a/analysis/abstract/restricted_supply/iw_instantiation.v
+++ b/analysis/abstract/restricted_supply/iw_instantiation.v
@@ -249,50 +249,6 @@ Section JLFPInstantiation.
End InstantiatedWorkloadEquivalence.
- (** In this section, we prove that the (abstract) cumulative
- interference of jobs with higher or equal priority is equal to
- total service of jobs with higher or equal priority. *)
- Section InstantiatedServiceEquivalences.
-
- (** Consider any job [j] of [tsk]. *)
- Variable j : Job.
- Hypothesis H_j_arrives : arrives_in arr_seq j.
- Hypothesis H_job_of_tsk : job_of_task tsk j.
-
- (** We consider an arbitrary time interval <<[t1, t)>> that
- starts with a (classic) quiet time. *)
- Variable t1 t : instant.
- Hypothesis H_quiet_time : classical.quiet_time arr_seq sched j t1.
-
- (** As follows from lemma [cumulative_pred_served_eq_service],
- the (abstract) instantiated function of interference is
- equal to the total service of any subset of jobs with higher
- or equal priority. *)
-
- (** The above is in particular true for the jobs other
- than [j] with higher or equal priority... *)
- Lemma cumulative_i_ohep_eq_service_of_ohep :
- cumulative_another_hep_job_interference arr_seq sched j t1 t
- = service_of_other_hep_jobs arr_seq sched j t1 t.
- Proof.
- apply: cumulative_pred_served_eq_service => //.
- - by apply unit_supply_is_unit_service.
- - by move => ? /andP[].
- Qed.
-
- (** ...and for jobs from other tasks than [j] with higher
- or equal priority. *)
- Lemma cumulative_i_thep_eq_service_of_othep :
- cumulative_another_task_hep_job_interference arr_seq sched j t1 t
- = service_of_other_task_hep_jobs arr_seq sched j t1 t.
- Proof.
- apply: cumulative_pred_served_eq_service => //.
- - by apply unit_supply_is_unit_service.
- - by move => ? /andP[].
- Qed.
-
- End InstantiatedServiceEquivalences.
-
(** In this section we prove that the abstract definition of busy
interval is equivalent to the conventional, concrete
definition of busy interval for JLFP scheduling. *)
@@ -303,15 +259,15 @@ Section JLFPInstantiation.
notion of quiet time in the _abstract_ sense as
[quiet_time_ab]. *)
Let quiet_time_cl := classical.quiet_time arr_seq sched.
- Let quiet_time_ab := definitions.quiet_time sched.
+ Let quiet_time_ab := abstract.definitions.quiet_time sched.
(** Same for the two notions of a busy interval prefix ... *)
Let busy_interval_prefix_cl := classical.busy_interval_prefix arr_seq sched.
- Let busy_interval_prefix_ab := definitions.busy_interval_prefix sched.
+ Let busy_interval_prefix_ab := abstract.definitions.busy_interval_prefix sched.
(** ... and the two notions of a busy interval. *)
Let busy_interval_cl := classical.busy_interval arr_seq sched.
- Let busy_interval_ab := definitions.busy_interval sched.
+ Let busy_interval_ab := abstract.definitions.busy_interval sched.
(** Consider any job [j] of [tsk]. *)
Variable j : Job.
@@ -332,7 +288,8 @@ Section JLFPInstantiation.
{ rewrite negb_and negbK; apply/orP.
by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
{ erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
- rewrite cumulative_i_ohep_eq_service_of_ohep//.
+ rewrite cumulative_i_ohep_eq_service_of_ohep //=; last first.
+ { exact: unit_supply_is_unit_service. }
rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
apply all_jobs_have_completed_equiv_workload_eq_service => //.
{ by apply unit_supply_is_unit_service. }
@@ -357,7 +314,8 @@ Section JLFPInstantiation.
erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
erewrite workload_of_jobs_case_on_pred with (P' := fun j' => j' != j) => //.
replace ((fun j0 : Job => hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
- rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //.
+ rewrite -/(service_of_other_hep_jobs arr_seq sched j 0 t) -cumulative_i_ohep_eq_service_of_ohep //; last first.
+ { exact: unit_supply_is_unit_service. }
rewrite -/(workload_of_other_hep_jobs arr_seq j 0 t) -cumulative_iw_hep_eq_workload_of_ohep //.
move: T1; rewrite negb_and => /orP [NA | /negPn COMP].
{ have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job => hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
@@ -586,8 +544,8 @@ Section JLFPInstantiation.
Proof.
move=> j t1.
rewrite cumulative_interference_split cumulative_interfering_workload_split.
- rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep; last first.
- { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
+ rewrite leq_add2l cumulative_i_ohep_eq_service_of_ohep //=; last first.
+ { exact: unit_supply_is_unit_service. }
rewrite cumulative_iw_hep_eq_workload_of_ohep.
apply service_of_jobs_le_workload => //.
by apply unit_supply_is_unit_service.
diff --git a/analysis/abstract/restricted_supply/task_intra_interference_bound.v b/analysis/abstract/restricted_supply/task_intra_interference_bound.v
index 725daae2bb05cff91a2e29b482d9aa11cd32b371..0fd3c36084cc7cb42f2184ee1f48b88fbbd44722 100644
--- a/analysis/abstract/restricted_supply/task_intra_interference_bound.v
+++ b/analysis/abstract/restricted_supply/task_intra_interference_bound.v
@@ -110,6 +110,7 @@ Section TaskIntraInterferenceIsBounded.
by rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + Δ)) //= leq_addr. }
{ erewrite cumulative_i_thep_eq_service_of_othep; eauto 2 => //; last first.
{ by apply instantiated_quiet_time_equivalent_quiet_time => //; apply BUSY. }
+ { exact: unit_supply_is_unit_service. }
apply: leq_trans.
{ by apply service_of_jobs_le_workload => //; apply unit_supply_is_unit_service. }
{ apply H_workload_is_bounded => //; apply: abstract_busy_interval_classic_quiet_time => //. }
diff --git a/analysis/facts/priority/fifo_ahep_bound.v b/analysis/facts/priority/fifo_ahep_bound.v
new file mode 100644
index 0000000000000000000000000000000000000000..d46cc3ca82533ceba23b0ea15a8b8eeace742191
--- /dev/null
+++ b/analysis/facts/priority/fifo_ahep_bound.v
@@ -0,0 +1,126 @@
+Require Export prosa.analysis.abstract.iw_auxiliary.
+Require Export prosa.analysis.facts.model.restricted_supply.schedule.
+Require Import prosa.analysis.facts.priority.fifo.
+Require Import prosa.analysis.facts.model.rbf.
+
+
+(** * Higher-or-Equal-Priority Interference Bound under FIFO *)
+
+(** In this file, we introduce a bound on the cumulative interference
+ from higher- and equal-priority under FIFO scheduling. *)
+Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
+
+ (** Consider any type of tasks, each characterized by a WCET
+ [task_cost] and an arrival curve [max_arrivals] ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{MaxArrivals Task}.
+
+ (** ... and any type of jobs associated with these tasks, where each
+ job has a task [job_task], a cost [job_cost], and an arrival
+ time [job_arrival]. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobCost Job}.
+ Context `{JobArrival Job}.
+
+ (** Consider any kind of unit-supply uniprocessor model. *)
+ Context `{PState : ProcessorState Job}.
+ Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+ Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+
+ (** Consider any arrival sequence [arr_seq] with consistent, non-duplicate arrivals. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
+
+ (** We further require that a job's cost cannot exceed its task's stated WCET. *)
+ Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.
+
+ (** We consider an arbitrary task set [ts] ... *)
+ Variable ts : seq Task.
+
+ (** ... and assume that all jobs stem from tasks in this task set. *)
+ Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+
+ (** We assume that [max_arrivals] is a family of valid arrival
+ curves that constrains the arrival sequence [arr_seq], i.e., for
+ any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+ bound of [tsk], and ... *)
+ Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+ (** ... (2) a monotonic function that equals 0 for the empty interval [delta = 0]. *)
+ Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+
+ (** Let [tsk] be any task in [ts] that is to be analyzed. *)
+ Variable tsk : Task.
+ Hypothesis H_tsk_in_ts : tsk \in ts.
+
+ (** Consider any schedule ... *)
+ Variable sched : schedule PState.
+
+ (** ... where jobs do not execute before their arrival nor 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.
+
+ (** Next, we establish a bound on the interference produced by higher- and
+ equal-priority jobs. *)
+
+ (** Consider a job [j] of the task under analysis [tsk] with a positive cost. *)
+ Variable j : Job.
+ Hypothesis H_job_of_task : job_of_task tsk j.
+ Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
+ Hypothesis H_job_cost_positive : job_cost_positive j.
+
+ (** Consider the busy window of [j] and denote it as <<[t1, t2)>>. *)
+ Variable t1 t2 : instant.
+ Hypothesis H_busy_window : classical.busy_interval arr_seq sched j t1 t2.
+
+ (** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy
+ window of [j]. *)
+ Variable Δ : instant.
+ Hypothesis H_in_busy : t1 + Δ < t2.
+
+ (** The cumulative interference from higher- and equal-priority jobs
+ during <<[t1, Δ)>> is bounded as follows. *)
+ Lemma bound_on_hep_workload :
+ cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <=
+ \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.
+ Proof.
+ move: (H_busy_window) => [[_ [_ [_ /andP [ARR1 ARR2]]]] _].
+ rewrite (cumulative_i_ohep_eq_service_of_ohep _ arr_seq) => //; last eauto 6 with basic_rt_facts; last first.
+ { by move: (H_busy_window) => [[_ [Q _]] _]. }
+ { exact: unit_supply_is_unit_service. }
+ eapply leq_trans.
+ { apply service_of_jobs_le_workload => //.
+ by apply unit_supply_is_unit_service. }
+ rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)) => //.
+ rewrite (workload_minus_job_cost j)//;
+ last by apply job_in_arrivals_between => //; last by rewrite addn1.
+ rewrite /workload_of_jobs (big_rem tsk) //=
+ (addnC (task_request_bound_function tsk (job_arrival j - t1 + ε))).
+ rewrite -addnBA; last first.
+ - apply leq_trans with (task_request_bound_function tsk ε).
+ { by apply: task_rbf_1_ge_task_cost; exact: non_pathological_max_arrivals. }
+ { by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
+ - eapply leq_trans; last first.
+ { by erewrite leq_add2l; apply task_rbf_without_job_under_analysis; (try apply ARR1) => //; lia. }
+ rewrite addnBA.
+ + rewrite leq_sub2r //; eapply leq_trans.
+ * apply sum_over_partitions_le => j' inJOBS => _.
+ by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
+ * rewrite (big_rem tsk) //= addnC leq_add //; last by rewrite addnA subnKC.
+ rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
+ apply leq_sum => tsk' _; rewrite andbC //=.
+ destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by [].
+ apply rem_in in IN.
+ eapply leq_trans;
+ last by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
+ by rewrite addnBAC //= subnKC //= addn1; apply leqW.
+ + move : H_job_of_task => TSKj.
+ rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=;
+ first by rewrite TSKj; apply leq_addr.
+ apply job_in_arrivals_between => //.
+ by lia.
+ Qed.
+
+End RTAforFullyPreemptiveFIFOModelwithArrivalCurves.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index b06002f920b9597f6d1a28a6e2cff66474d480c4..a1aed95cf58e9611b01f79654ab96672f5f18dd5 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -1,5 +1,6 @@
Require Import prosa.model.readiness.basic.
Require Import prosa.analysis.facts.priority.fifo.
+Require Export prosa.analysis.facts.priority.fifo_ahep_bound.
Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
Require Export prosa.analysis.abstract.ideal.abstract_rta.
Require Export prosa.analysis.facts.model.task_cost.
@@ -274,70 +275,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
(** *** Higher- and Equal-Priority Interference *)
- (** Next, we establish a bound on the interference produced by higher- and
- equal-priority jobs. *)
- Section BoundOnHEPWorkload.
-
- (** Consider again a job [j] of the task under analysis [tsk] with a positive cost. *)
- Variable j : Job.
- Hypothesis H_job_of_task : job_of_task tsk j.
- Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
- Hypothesis H_job_cost_positive : job_cost_positive j.
-
- (** Consider the (abstract) busy window of [j] and denote it as <<[t1, t2)>>. *)
- Variable t1 t2 : instant.
- Hypothesis H_busy_window :
- definitions.busy_interval sched j t1 t2.
-
- (** Consider any arbitrary sub-interval <<[t1, Δ)>> within the busy window
- of [j]. *)
- Variable Δ : instant.
- Hypothesis H_in_busy : t1 + Δ < t2.
-
- (** The cumulative interference from higher- and equal-priority jobs during
- <<[t1, Δ)>> is bounded as follows. *)
- Lemma bound_on_hep_workload :
- cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) <=
- \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.
- Proof.
- rewrite (cumulative_i_ohep_eq_service_of_ohep arr_seq) => //;
- last by eauto 6 with basic_rt_facts.
- eapply leq_trans; first exact: service_of_jobs_le_workload.
- rewrite (leqRW (workload_equal_subset _ _ _ _ _ _ _)) => //.
- rewrite (workload_minus_job_cost j)//;
- last by apply job_in_arrivals_between => //; last by rewrite addn1.
- rewrite /workload_of_jobs /IBF (big_rem tsk) //=
- (addnC (task_request_bound_function tsk (job_arrival j - t1 + ε))).
- rewrite -addnBA; last first.
- - apply leq_trans with (task_request_bound_function tsk ε).
- { by apply: task_rbf_1_ge_task_cost; exact: non_pathological_max_arrivals. }
- { by apply task_rbf_monotone; [apply H_valid_arrival_curve | lia]. }
- - eapply leq_trans;
- last by (
- erewrite leq_add2l;
- eapply task_rbf_without_job_under_analysis with (t1 := t1) =>//;
- lia).
- rewrite addnBA.
- + rewrite leq_sub2r //; eapply leq_trans.
- * apply sum_over_partitions_le => j' inJOBS => _.
- by apply H_all_jobs_from_taskset, (in_arrivals_implies_arrived _ _ _ _ inJOBS).
- * rewrite (big_rem tsk) //= addnC leq_add //;
- last by rewrite addnBAC //= subnKC // addn1; apply leqW.
- rewrite big_seq_cond [in X in _ <= X]big_seq_cond big_mkcond [in X in _ <= X]big_mkcond //=.
- apply leq_sum => tsk' _; rewrite andbC //=.
- destruct (tsk' \in rem (T:=Task) tsk ts) eqn:IN; last by [].
- apply rem_in in IN.
- eapply leq_trans;
- last by apply (task_workload_le_task_rbf _ _ _ IN H_valid_job_cost H_is_arrival_curve t1).
- by rewrite addnBAC //= subnKC //= addn1; apply leqW.
- + move : H_job_of_task => TSKj.
- rewrite /task_workload_between /task_workload /workload_of_jobs (big_rem j) //=;
- first by rewrite TSKj; apply leq_addr.
- apply job_in_arrivals_between => //.
- by lia.
- Qed.
-
- End BoundOnHEPWorkload.
+ (** We establish a bound on the interference produced by higher- and
+ equal-priority jobs in a separate file. To see the result,
+ simply click on the link bellow. *)
+ Let bound_on_hep_workload :=
+ @analysis.facts.priority.fifo_ahep_bound.bound_on_hep_workload.
(** *** Correctness of [IBF] *)
@@ -361,7 +303,8 @@ Section AbstractRTAforFIFOwithArrivalCurves.
have JPOS: job_cost_positive j by rewrite -ltnNge in NCOMPL; unfold job_cost_positive; lia.
rewrite (no_priority_inversion j ARRj _ JPOS _ t2) //= add0n.
have ->: A = job_arrival j - t1 by erewrite Pred with (t1 := t1); [lia | apply BUSY].
- exact: bound_on_hep_workload.
+ apply: bound_on_hep_workload; (try apply IN_BUSY) => //.
+ by apply instantiated_busy_interval_equivalent_busy_interval.
Qed.
(** The preceding lemma [IBF_correct] corresponds to Lemma 3 in the paper. To