Library prosa.analysis.facts.workload.elf_athep_bound
Require Export prosa.model.priority.elf.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.workload.bounded.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.workload.elf_athep_bound.
Require Export prosa.analysis.facts.model.rbf.
Require Export prosa.model.task.absolute_deadline.
Require Export prosa.analysis.definitions.workload.bounded.
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.definitions.workload.elf_athep_bound.
Require Export prosa.analysis.facts.model.rbf.
Bound on Higher-or-Equal Priority Workload under ELF Scheduling is Valid
Consider any type of tasks, each characterized by a WCET
task_cost, a relative deadline task_deadline, an arrival
curve max_arrivals, and a relative priority point, ...
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{PriorityPoint Task}.
Context `{TaskCost Task}.
Context `{MaxArrivals Task}.
Context `{PriorityPoint 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 `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of processor model.
Consider any valid arrival sequence arr_seq ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... with valid job costs.
We consider an arbitrary task set ts ...
... and assume that all jobs stem from tasks in this task set.
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 an arrival bound of
tsk.
Let tsk be any task to be analyzed.
Consider any schedule.
Variable sched : schedule PState.
(* Consider any fixed-priority scheduling policy. *)
Context (FP : FP_policy Task).
(* Consider any fixed-priority scheduling policy. *)
Context (FP : FP_policy Task).
Before we prove the main result, we establish some auxiliary lemmas.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive: job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_of_tsk : job_of_task tsk j.
Hypothesis H_job_cost_positive: job_cost_positive j.
Consider the busy interval
[t1, t2)
of job j.
Consider an arbitrary shift delta inside the busy interval ...
Now, we define a predicate to identify jobs from a given task that have
priority higher than or equal to j.
Let hep_job_from_tsk (tsk_o : Task) (jo : Job) := hep_job jo j && (job_task jo == tsk_o).
Section ShortenRange.
Section ShortenRange.
Then we prove that the total workload of jobs with higher-or-equal priority
from task tsk_o over the interval [t1, t1 + Δ] is bounded by the workload
over the interval [t1, t1 + ep_task_interfering_interval_length tsk tsk_o A].
The intuition behind this inequality is that jobs that arrive after time instant
t1 + ep_task_interfering_interval_length tsk tsk_o A have lower priority
than job j.
Lemma total_ep_tsk_workload_shorten_range :
ep_task tsk tsk_o →
workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta))
≤ workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 `|Num.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|).
Proof.
move ⇒ EP_tsk.
have BOUNDED: `|Num.max 0%R (t1%:R + (ep_task_interfering_interval_length tsk tsk_o A))%R| ≤ t1 + delta
by clear - H_delta_ge; lia.
rewrite /hep_job_from_tsk /hep_job /ELF.
rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) //.
move ⇒ j' IN' ARR'.
apply /contraT ⇒ /negPn /andP [/orP [/negP+ | /andP [_ HEP]] /eqP TSKo].
{ rewrite /ep_task in EP_tsk.
rewrite /hp_task TSKo.
move: H_job_of_tsk.
rewrite /job_of_task ⇒ /eqP →.
by move: EP_tsk ⇒ /andP [-> ->]. }
move: ARR'; rewrite /ep_task_interfering_interval_length -TSKo.
move: H_job_of_tsk ⇒ /eqP <-.
move: HEP; rewrite /hep_job /GEL /job_priority_point.
by clear; lia.
Qed.
End ShortenRange.
ep_task tsk tsk_o →
workload_of_jobs (hep_job_from_tsk tsk_o) (arrivals_between arr_seq t1 (t1 + delta))
≤ workload_of_jobs (hep_job_from_tsk tsk_o)
(arrivals_between arr_seq t1 `|Num.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|).
Proof.
move ⇒ EP_tsk.
have BOUNDED: `|Num.max 0%R (t1%:R + (ep_task_interfering_interval_length tsk tsk_o A))%R| ≤ t1 + delta
by clear - H_delta_ge; lia.
rewrite /hep_job_from_tsk /hep_job /ELF.
rewrite (workload_of_jobs_nil_tail _ _ BOUNDED) //.
move ⇒ j' IN' ARR'.
apply /contraT ⇒ /negPn /andP [/orP [/negP+ | /andP [_ HEP]] /eqP TSKo].
{ rewrite /ep_task in EP_tsk.
rewrite /hp_task TSKo.
move: H_job_of_tsk.
rewrite /job_of_task ⇒ /eqP →.
by move: EP_tsk ⇒ /andP [-> ->]. }
move: ARR'; rewrite /ep_task_interfering_interval_length -TSKo.
move: H_job_of_tsk ⇒ /eqP <-.
move: HEP; rewrite /hep_job /GEL /job_priority_point.
by clear; lia.
Qed.
End ShortenRange.
Consider the jobs that have priority higher than or equal to j released
by any task in the same priority band as tsk (excluding tsk).
We prove that the workload of these jobs is at most bound_on_ep_task_workload.
Corollary sum_of_ep_tsk_workloads_is_at_most_bound_on_ep_task_workload :
\sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_ep_task_workload ts tsk A delta.
Proof.
rewrite /bound_on_ep_task_workload.
apply leq_sum_seq ⇒ tsk_o INtsko /andP [EP_tsk NEQT].
have [LEQ|GT] := leqP delta `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)%R|; [| apply ltnW in GT].
{ apply: leq_trans; last by apply rbf_spec with (t := t1).
by apply: workload_of_jobs_weaken ⇒ ? /andP[]. }
{ eapply leq_trans; first by apply total_ep_tsk_workload_shorten_range ⇒ //; clear - GT H_delta_in_busy; lia.
rewrite (workload_of_jobs_equiv_pred _ _ (fun jo : Job ⇒ hep_job jo j && (job_task jo == tsk_o))) ⇒ //.
{ case: (boolP (0 ≤ ep_task_interfering_interval_length tsk tsk_o A)%R) ⇒ EQ;
last by rewrite arrivals_between_geq; [rewrite workload_of_jobs0 | clear - EQ; lia].
have → : `|Num.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|
= t1 + `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| by clear -EQ; lia.
by apply: rbf_spec' ⇒ // ? /andP[].
}
}
Qed.
\sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_ep_task_workload ts tsk A delta.
Proof.
rewrite /bound_on_ep_task_workload.
apply leq_sum_seq ⇒ tsk_o INtsko /andP [EP_tsk NEQT].
have [LEQ|GT] := leqP delta `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)%R|; [| apply ltnW in GT].
{ apply: leq_trans; last by apply rbf_spec with (t := t1).
by apply: workload_of_jobs_weaken ⇒ ? /andP[]. }
{ eapply leq_trans; first by apply total_ep_tsk_workload_shorten_range ⇒ //; clear - GT H_delta_in_busy; lia.
rewrite (workload_of_jobs_equiv_pred _ _ (fun jo : Job ⇒ hep_job jo j && (job_task jo == tsk_o))) ⇒ //.
{ case: (boolP (0 ≤ ep_task_interfering_interval_length tsk tsk_o A)%R) ⇒ EQ;
last by rewrite arrivals_between_geq; [rewrite workload_of_jobs0 | clear - EQ; lia].
have → : `|Num.max 0%R (t1%:R + ep_task_interfering_interval_length tsk tsk_o A)%R|
= t1 + `|Num.max 0%R (ep_task_interfering_interval_length tsk tsk_o A)| by clear -EQ; lia.
by apply: rbf_spec' ⇒ // ? /andP[].
}
}
Qed.
Next, consider a workload of all jobs with priority higher
than j released by any task in higher priority band.
we establish that this workload is at most bound_on_hp_task_workload.
Corollary sum_of_hp_tsk_workloads_is_at_most_bound_on_hp_task_workload :
\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_hp_task_workload ts tsk delta.
Proof.
rewrite /bound_on_hp_task_workload.
rewrite /total_hp_request_bound_function_FP.
apply leq_sum_seq ⇒ tsk' IN' HP_TSK.
by apply: rbf_spec' ⇒ // ? /andP[].
Qed.
\sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_hp_task_workload ts tsk delta.
Proof.
rewrite /bound_on_hp_task_workload.
rewrite /total_hp_request_bound_function_FP.
apply leq_sum_seq ⇒ tsk' IN' HP_TSK.
by apply: rbf_spec' ⇒ // ? /andP[].
Qed.
To help with further analysis, we establish a useful lemma on partitioning
higher-or-equal priority workloads.
Lemma sum_of_hep_workloads_partitioned :
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
= \sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
+ \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs.
Proof.
rewrite (bigID (fun (tsk_o : Task) ⇒ hep_task tsk_o tsk)) //=.
rewrite (bigID (fun (tsk_o : Task) ⇒ hep_task tsk tsk_o)) //=.
under eq_bigl.
{ move ⇒ tsk'.
rewrite -andbA andbC.
rewrite (@andbC (hep_task tsk' tsk) (hep_task tsk tsk')).
over. }
have ->: \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs = 0.
{ under eq_bigr.
{ move ⇒ tsk' /andP [NEQ HEP].
rewrite /workload_of_jobs.
under big_pred0.
{ move⇒ j'.
rewrite /hep_job_from_tsk /hep_job /ELF /hp_task.
elim Tsk_j' : (job_task j' == tsk'); last by rewrite andbF.
move: Tsk_j' ⇒ /eqP →.
move: H_job_of_tsk.
rewrite /job_of_task ⇒ /eqP →.
by move: HEP ⇒ /negbTE →. }
over. }
apply /eqP.
by rewrite big_const_idem.
}
rewrite addn0 /ep_task.
apply /eqP.
rewrite eqn_add2l /hp_task.
rewrite (eq_bigl (fun (tsk_o : Task) ⇒ hep_task tsk_o tsk && ~~ hep_task tsk tsk_o)) //=.
rewrite /eqfun ⇒ tsk'.
elim NEQ: (tsk' != tsk) ⇒ //=.
move: NEQ ⇒ /idP /idP /eqP NEQ.
rewrite NEQ.
by rewrite andbN.
Qed.
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
= \sum_(tsk_o <- ts | (ep_task tsk tsk_o) && (tsk_o != tsk)) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
+ \sum_(tsk_o <- ts | hp_task tsk_o tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs.
Proof.
rewrite (bigID (fun (tsk_o : Task) ⇒ hep_task tsk_o tsk)) //=.
rewrite (bigID (fun (tsk_o : Task) ⇒ hep_task tsk tsk_o)) //=.
under eq_bigl.
{ move ⇒ tsk'.
rewrite -andbA andbC.
rewrite (@andbC (hep_task tsk' tsk) (hep_task tsk tsk')).
over. }
have ->: \sum_(i <- ts | (i != tsk) && ~~ hep_task i tsk)
workload_of_jobs (hep_job_from_tsk i) jobs = 0.
{ under eq_bigr.
{ move ⇒ tsk' /andP [NEQ HEP].
rewrite /workload_of_jobs.
under big_pred0.
{ move⇒ j'.
rewrite /hep_job_from_tsk /hep_job /ELF /hp_task.
elim Tsk_j' : (job_task j' == tsk'); last by rewrite andbF.
move: Tsk_j' ⇒ /eqP →.
move: H_job_of_tsk.
rewrite /job_of_task ⇒ /eqP →.
by move: HEP ⇒ /negbTE →. }
over. }
apply /eqP.
by rewrite big_const_idem.
}
rewrite addn0 /ep_task.
apply /eqP.
rewrite eqn_add2l /hp_task.
rewrite (eq_bigl (fun (tsk_o : Task) ⇒ hep_task tsk_o tsk && ~~ hep_task tsk tsk_o)) //=.
rewrite /eqfun ⇒ tsk'.
elim NEQ: (tsk' != tsk) ⇒ //=.
move: NEQ ⇒ /idP /idP /eqP NEQ.
rewrite NEQ.
by rewrite andbN.
Qed.
Finally, we establish that the workload of jobs with priority higher than or equal to
j is at most bound_on_athep_workload.
Corollary sum_of_workloads_is_at_most_bound_on_total_hep_workload:
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_athep_workload ts tsk A delta.
Proof.
rewrite sum_of_hep_workloads_partitioned.
rewrite /bound_on_athep_workload.
move: sum_of_hp_tsk_workloads_is_at_most_bound_on_hp_task_workload ⇒ LT_HP.
move: sum_of_ep_tsk_workloads_is_at_most_bound_on_ep_task_workload ⇒ LT_EP.
by lia.
Qed.
End HepWorkloadBound.
\sum_(tsk_o <- ts | tsk_o != tsk) workload_of_jobs (hep_job_from_tsk tsk_o) jobs
≤ bound_on_athep_workload ts tsk A delta.
Proof.
rewrite sum_of_hep_workloads_partitioned.
rewrite /bound_on_athep_workload.
move: sum_of_hp_tsk_workloads_is_at_most_bound_on_hp_task_workload ⇒ LT_HP.
move: sum_of_ep_tsk_workloads_is_at_most_bound_on_ep_task_workload ⇒ LT_EP.
by lia.
Qed.
End HepWorkloadBound.
The validity of bound_on_athep_workload then easily follows
from lemma sum_of_workloads_is_at_most_bound_on_total_hep_workload.
Corollary bound_on_athep_workload_is_valid :
athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).
Proof.
move⇒ j t1 delta POS TSK QT.
eapply leq_trans.
+ eapply reorder_summation ⇒ j' IN _.
by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
+ move : TSK ⇒ /eqP TSK; rewrite TSK.
by apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload ⇒ //; apply /eqP.
Qed.
End ATHEPWorkloadBoundIsValidForELF.
athep_workload_is_bounded arr_seq sched tsk (bound_on_athep_workload ts tsk).
Proof.
move⇒ j t1 delta POS TSK QT.
eapply leq_trans.
+ eapply reorder_summation ⇒ j' IN _.
by apply H_all_jobs_from_taskset; eapply in_arrivals_implies_arrived; exact IN.
+ move : TSK ⇒ /eqP TSK; rewrite TSK.
by apply: sum_of_workloads_is_at_most_bound_on_total_hep_workload ⇒ //; apply /eqP.
Qed.
End ATHEPWorkloadBoundIsValidForELF.