Library prosa.classic.analysis.global.parallel.workload_bound
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.response_time prosa.classic.model.schedule.global.workload
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable tsk: sporadic_task.
Variable R_tsk: time. Variable delta: time.
Definition max_jobs :=
div_ceil (delta + R_tsk) (task_period tsk).
Definition W := max_jobs × task_cost tsk.
End WorkloadBoundDef.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable tsk: sporadic_task.
Hypothesis H_period_positive: task_period tsk > 0.
Variable R1 R2: time.
Hypothesis H_R_lower_bound: R1 ≥ task_cost tsk.
Hypothesis H_R1_le_R2: R1 ≤ R2.
Let workload_bound := W task_cost task_period tsk.
Lemma W_monotonic :
∀ t1 t2,
t1 ≤ t2 →
workload_bound R1 t1 ≤ workload_bound R2 t2.
Proof.
intros t1 t2 LEt.
unfold workload_bound, W, max_jobs.
rewrite leq_mul2r; apply/orP; right.
by apply leq_divceil2r; last by apply leq_add.
Qed.
End BasicLemmas.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_jobs_have_valid_parameters :
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Let job_has_completed_by := completed job_cost sched.
Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
workload job_task sched tsk t1 t2.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable t1 delta: time.
Variable R_tsk: time.
Hypothesis H_response_time_bound :
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_arrival j + R_tsk < t1 + delta →
job_has_completed_by j (job_arrival j + R_tsk).
Section MainProof.
Let t2 := t1 + delta.
Let n_k := max_jobs task_period tsk R_tsk delta.
Let workload_bound := W task_cost task_period tsk R_tsk delta.
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival scheduled_jobs).
Section SimplifyJobSequence.
Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
Lemma workload_bound_all_jobs_from_tsk :
∀ j_i,
j_i \in sorted_jobs →
arrives_in arr_seq j_i ∧
job_task j_i = tsk ∧
service_during sched j_i t1 t2 != 0 ∧
j_i \in jobs_scheduled_between sched t1 t2.
Proof.
rename H_jobs_come_from_arrival_sequence into FROMarr.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
repeat split; try (by done); first by apply (FROMarr j_i i).
{
apply service_implies_cumulative_service with (t := i);
first by apply/andP; split.
by rewrite -not_scheduled_no_service negbK.
}
{
rewrite mem_undup.
apply mem_bigcat_nat with (j := i); first by auto.
by rewrite mem_scheduled_jobs_eq_scheduled.
}
Qed.
Lemma workload_bound_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Proof.
intros i elem LT.
assert (SORT: sorted earlier_arrival sorted_jobs).
by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.
End SimplifyJobSequence.
Section WorkloadNotManyJobs.
Lemma workload_bound_holds_for_at_most_n_k_jobs :
size sorted_jobs ≤ n_k →
\sum_(i <- sorted_jobs) service_during sched i t1 t2 ≤
workload_bound.
Proof.
unfold workload_bound, W; intros LEnk.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
apply leq_sum; intros j_i; move/andP ⇒ [INi _].
apply workload_bound_all_jobs_from_tsk in INi; des.
eapply cumulative_service_le_task_cost;
[by apply H_completed_jobs_dont_execute | by apply INi0 |].
by apply H_jobs_have_valid_parameters.
Qed.
End WorkloadNotManyJobs.
Section WorkloadSingleJob.
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Lemma workload_bound_j_fst_is_job_of_tsk :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk ∧
service_during sched j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Proof.
by apply workload_bound_all_jobs_from_tsk, mem_nth.
Qed.
Lemma workload_bound_holds_for_a_single_job :
\sum_(0 ≤ i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 ≤
workload_bound.
Proof.
rename H_valid_task_parameters into PARAMS.
unfold is_valid_sporadic_task in ×.
unfold workload_bound, W; fold n_k.
have INfst := workload_bound_j_fst_is_job_of_tsk; des.
rewrite big_nat_recr // big_geq // [nth]lock /= -lock add0n.
apply leq_trans with (n := task_cost tsk).
{
eapply cumulative_service_le_task_cost; [by eauto 1 | by apply INfst0 |].
by apply H_jobs_have_valid_parameters.
}
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
apply ceil_neq0; last by apply PARAMS0.
{
apply leq_trans with (n := delta); last by apply leq_addr.
rewrite lt0n; apply/eqP; intro EQ0.
move: INfst1 ⇒ /eqP BUG; apply BUG.
unfold t2; rewrite EQ0 addn0.
by unfold service_during; rewrite big_geq.
}
Qed.
End WorkloadSingleJob.
Section WorkloadTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Lemma workload_bound_j_lst_is_job_of_tsk :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk ∧
service_during sched j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Proof.
apply workload_bound_all_jobs_from_tsk, mem_nth.
by rewrite H_at_least_two_jobs.
Qed.
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
Proof.
rewrite leqNgt; apply /negP; unfold not; intro LTt1.
exploit workload_bound_all_jobs_from_tsk.
{
apply mem_nth; instantiate (1 := 0).
apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
}
instantiate (1 := elem); move ⇒ [FSTarr [FSTtsk [/eqP FSTserv FSTin]]].
apply FSTserv.
apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk);
try (by done); last by apply ltnW.
apply H_response_time_bound; try (by done).
by apply leq_trans with (n := t1); last by apply leq_addr.
Qed.
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Proof.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
exploit workload_bound_all_jobs_from_tsk.
{
apply mem_nth; instantiate (1 := num_mid_jobs.+1).
by rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
}
instantiate (1 := elem); move ⇒ [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
unfold service_during; apply LSTserv.
by eapply cumulative_service_before_job_arrival_zero; eauto 1.
Qed.
Lemma workload_bound_service_of_middle_jobs :
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2 ≤
num_mid_jobs × task_cost tsk.
Proof.
apply leq_trans with (n := num_mid_jobs × task_cost tsk);
last by rewrite leq_mul2l; apply/orP; right.
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs) task_cost tsk);
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 ≤ i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
exploit workload_bound_all_jobs_from_tsk.
{
instantiate (1 := nth elem sorted_jobs i.+1).
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
move ⇒ [ARR [TSK _]].
eapply cumulative_service_le_task_cost; eauto 1.
by apply H_jobs_have_valid_parameters.
Qed.
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
Proof.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
unfold j_fst, j_lst; rewrite EQnk telescoping_sum;
last by ins; apply workload_bound_jobs_ordered_by_arrival.
rewrite -[_ × _ tsk]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat.
rewrite big_nat_cond [\sum_(0 ≤ i < _)(_-_)]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.
assert (ARRle: job_arrival cur ≤ job_arrival next).
by unfold cur, next; apply workload_bound_jobs_ordered_by_arrival.
feed (workload_bound_all_jobs_from_tsk cur).
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].
feed (workload_bound_all_jobs_from_tsk next).
by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].
assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) ≤ job_arrival next).
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ ⇒ /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ ⇒ /eqP EQ; ssrlia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
Lemma workload_bound_n_k_covers_all_jobs :
n_k ≥ num_mid_jobs.+2.
Proof.
rename H_valid_task_parameters into PARAMS.
unfold is_valid_sporadic_task in *; des.
rewrite leqNgt; apply/negP; unfold not; intro LTnk.
assert (DISTmax: job_arrival j_lst - job_arrival j_fst ≥ delta + R_tsk).
{
apply leq_trans with (n := num_mid_jobs.+1 × task_period tsk);
last by apply workload_bound_many_periods_in_between.
apply leq_trans with (n := n_k × task_period tsk);
last by rewrite leq_mul2r; apply/orP; right.
unfold n_k, max_jobs, div_ceil.
destruct (task_period tsk %| delta + R_tsk) eqn:DIV.
{
rewrite dvdn_eq in DIV; move: DIV ⇒ /eqP DIV.
by rewrite DIV.
}
by apply ltnW, ltn_ceil, PARAMS0.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
by ins; apply workload_bound_jobs_ordered_by_arrival.
}
rewrite -[job_arrival j_lst + _ - _]subnBA // subnn subn0 in DISTmax.
rewrite [delta + _]addnC addnA in DISTmax.
apply leq_trans with (m := t1 + delta) in DISTmax; last first.
{
rewrite leq_add2r.
by apply workload_bound_response_time_of_first_job_inside_interval.
}
have LST := workload_bound_last_job_arrives_before_end_of_interval.
by apply leq_ltn_trans with (m := t2) in LST; first by rewrite ltnn in LST.
Qed.
Lemma workload_bound_holds :
\sum_(0 ≤ i < num_mid_jobs.+2)
service_during sched (nth elem sorted_jobs i) t1 t2
≤ workload_bound.
Proof.
unfold workload_bound, W; fold n_k.
have ALL := workload_bound_n_k_covers_all_jobs.
apply leq_trans with (n := num_mid_jobs.+2 × task_cost tsk);
last by rewrite leq_mul2r; apply/orP; right.
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs.+2) task_cost tsk);
last by rewrite big_const_nat iter_addn addn0 subn0 mulnC.
rewrite big_nat_cond [\sum_(_ ≤ _ < _ | true)_]big_nat_cond.
apply leq_sum; intro i; move ⇒ /andP [/andP [_ LEi] _].
exploit workload_bound_all_jobs_from_tsk.
{
instantiate (1 := nth elem sorted_jobs i).
by apply mem_nth; rewrite H_at_least_two_jobs.
}
move ⇒ [ARR [TSK _]].
eapply cumulative_service_le_task_cost; eauto 1.
by apply H_jobs_have_valid_parameters.
Qed.
End WorkloadTwoOrMoreJobs.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
Proof.
unfold workload_of, workload_bound, W in *; ins; des.
fold n_k.
rewrite workload_eq_workload_joblist.
rewrite workload_bound_simpl_by_sorting_scheduled_jobs.
destruct (size sorted_jobs ≤ n_k) eqn:NUM;
first by apply workload_bound_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.
assert (EX: ∃ elem: Job, True).
destruct sorted_jobs; [ by rewrite ltn0 in NUM | by ∃ s].
destruct EX as [elem _].
rewrite (big_nth elem).
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.
destruct n as [| num_mid_jobs];
first by apply workload_bound_holds_for_a_single_job; rewrite SIZE.
by apply workload_bound_holds.
Qed.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.response_time prosa.classic.model.schedule.global.workload
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.
Module WorkloadBound.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability Workload.
Section WorkloadBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable tsk: sporadic_task.
Variable R_tsk: time. Variable delta: time.
Definition max_jobs :=
div_ceil (delta + R_tsk) (task_period tsk).
Definition W := max_jobs × task_cost tsk.
End WorkloadBoundDef.
Section BasicLemmas.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable tsk: sporadic_task.
Hypothesis H_period_positive: task_period tsk > 0.
Variable R1 R2: time.
Hypothesis H_R_lower_bound: R1 ≥ task_cost tsk.
Hypothesis H_R1_le_R2: R1 ≤ R2.
Let workload_bound := W task_cost task_period tsk.
Lemma W_monotonic :
∀ t1 t2,
t1 ≤ t2 →
workload_bound R1 t1 ≤ workload_bound R2 t2.
Proof.
intros t1 t2 LEt.
unfold workload_bound, W, max_jobs.
rewrite leq_mul2r; apply/orP; right.
by apply leq_divceil2r; last by apply leq_add.
Qed.
End BasicLemmas.
Section ProofWorkloadBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_jobs_have_valid_parameters :
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Let job_has_completed_by := completed job_cost sched.
Let workload_of (tsk: sporadic_task) (t1 t2: time) :=
workload job_task sched tsk t1 t2.
Variable tsk: sporadic_task.
Hypothesis H_valid_task_parameters:
is_valid_sporadic_task task_cost task_period task_deadline tsk.
Variable t1 delta: time.
Variable R_tsk: time.
Hypothesis H_response_time_bound :
∀ j,
arrives_in arr_seq j →
job_task j = tsk →
job_arrival j + R_tsk < t1 + delta →
job_has_completed_by j (job_arrival j + R_tsk).
Section MainProof.
Let t2 := t1 + delta.
Let n_k := max_jobs task_period tsk R_tsk delta.
Let workload_bound := W task_cost task_period tsk R_tsk delta.
Let scheduled_jobs :=
jobs_of_task_scheduled_between job_task sched tsk t1 t2.
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival scheduled_jobs).
Section SimplifyJobSequence.
Lemma workload_bound_simpl_by_sorting_scheduled_jobs :
workload_joblist job_task sched tsk t1 t2 =
\sum_(i <- sorted_jobs) service_during sched i t1 t2.
Proof.
unfold workload_joblist; fold scheduled_jobs.
rewrite (perm_big sorted_jobs) /= //.
by rewrite -(perm_sort earlier_arrival).
Qed.
Lemma workload_bound_job_in_same_sequence :
∀ j,
(j \in scheduled_jobs) = (j \in sorted_jobs).
Proof.
by apply perm_mem; rewrite -(perm_sort earlier_arrival).
Qed.
Lemma workload_bound_all_jobs_from_tsk :
∀ j_i,
j_i \in sorted_jobs →
arrives_in arr_seq j_i ∧
job_task j_i = tsk ∧
service_during sched j_i t1 t2 != 0 ∧
j_i \in jobs_scheduled_between sched t1 t2.
Proof.
rename H_jobs_come_from_arrival_sequence into FROMarr.
intros j_i LTi.
rewrite -workload_bound_job_in_same_sequence mem_filter in LTi; des.
unfold jobs_scheduled_between in *; rewrite mem_undup in LTi0.
apply mem_bigcat_nat_exists in LTi0; des.
rewrite mem_scheduled_jobs_eq_scheduled in LTi0.
repeat split; try (by done); first by apply (FROMarr j_i i).
{
apply service_implies_cumulative_service with (t := i);
first by apply/andP; split.
by rewrite -not_scheduled_no_service negbK.
}
{
rewrite mem_undup.
apply mem_bigcat_nat with (j := i); first by auto.
by rewrite mem_scheduled_jobs_eq_scheduled.
}
Qed.
Lemma workload_bound_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Proof.
intros i elem LT.
assert (SORT: sorted earlier_arrival sorted_jobs).
by apply sort_sorted; unfold total, earlier_arrival; ins; apply leq_total.
by destruct sorted_jobs; simpl in *; [by rewrite ltn0 in LT | by apply/pathP].
Qed.
End SimplifyJobSequence.
Section WorkloadNotManyJobs.
Lemma workload_bound_holds_for_at_most_n_k_jobs :
size sorted_jobs ≤ n_k →
\sum_(i <- sorted_jobs) service_during sched i t1 t2 ≤
workload_bound.
Proof.
unfold workload_bound, W; intros LEnk.
apply leq_trans with (n := \sum_(x <- sorted_jobs) task_cost tsk);
last by rewrite big_const_seq iter_addn addn0 mulnC leq_mul2r; apply/orP; right.
rewrite [\sum_(_ <- _) service_during _ _ _ _]big_seq_cond.
rewrite [\sum_(_ <- _) task_cost _]big_seq_cond.
apply leq_sum; intros j_i; move/andP ⇒ [INi _].
apply workload_bound_all_jobs_from_tsk in INi; des.
eapply cumulative_service_le_task_cost;
[by apply H_completed_jobs_dont_execute | by apply INi0 |].
by apply H_jobs_have_valid_parameters.
Qed.
End WorkloadNotManyJobs.
Section WorkloadSingleJob.
Hypothesis H_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Lemma workload_bound_j_fst_is_job_of_tsk :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk ∧
service_during sched j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Proof.
by apply workload_bound_all_jobs_from_tsk, mem_nth.
Qed.
Lemma workload_bound_holds_for_a_single_job :
\sum_(0 ≤ i < 1) service_during sched (nth elem sorted_jobs i) t1 t2 ≤
workload_bound.
Proof.
rename H_valid_task_parameters into PARAMS.
unfold is_valid_sporadic_task in ×.
unfold workload_bound, W; fold n_k.
have INfst := workload_bound_j_fst_is_job_of_tsk; des.
rewrite big_nat_recr // big_geq // [nth]lock /= -lock add0n.
apply leq_trans with (n := task_cost tsk).
{
eapply cumulative_service_le_task_cost; [by eauto 1 | by apply INfst0 |].
by apply H_jobs_have_valid_parameters.
}
rewrite -{1}[task_cost tsk]mul1n leq_mul2r; apply/orP; right.
apply ceil_neq0; last by apply PARAMS0.
{
apply leq_trans with (n := delta); last by apply leq_addr.
rewrite lt0n; apply/eqP; intro EQ0.
move: INfst1 ⇒ /eqP BUG; apply BUG.
unfold t2; rewrite EQ0 addn0.
by unfold service_during; rewrite big_geq.
}
Qed.
End WorkloadSingleJob.
Section WorkloadTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Lemma workload_bound_j_lst_is_job_of_tsk :
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk ∧
service_during sched j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Proof.
apply workload_bound_all_jobs_from_tsk, mem_nth.
by rewrite H_at_least_two_jobs.
Qed.
Lemma workload_bound_response_time_of_first_job_inside_interval :
t1 ≤ job_arrival j_fst + R_tsk.
Proof.
rewrite leqNgt; apply /negP; unfold not; intro LTt1.
exploit workload_bound_all_jobs_from_tsk.
{
apply mem_nth; instantiate (1 := 0).
apply ltn_trans with (n := 1); [by done | by rewrite H_at_least_two_jobs].
}
instantiate (1 := elem); move ⇒ [FSTarr [FSTtsk [/eqP FSTserv FSTin]]].
apply FSTserv.
apply (cumulative_service_after_job_rt_zero job_arrival job_cost) with (R := R_tsk);
try (by done); last by apply ltnW.
apply H_response_time_bound; try (by done).
by apply leq_trans with (n := t1); last by apply leq_addr.
Qed.
Lemma workload_bound_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Proof.
rewrite leqNgt; apply/negP; unfold not; intro LT2.
exploit workload_bound_all_jobs_from_tsk.
{
apply mem_nth; instantiate (1 := num_mid_jobs.+1).
by rewrite -(ltn_add2r 1) addn1 H_at_least_two_jobs addn1.
}
instantiate (1 := elem); move ⇒ [LSTarr [LSTtsk [/eqP LSTserv LSTin]]].
unfold service_during; apply LSTserv.
by eapply cumulative_service_before_job_arrival_zero; eauto 1.
Qed.
Lemma workload_bound_service_of_middle_jobs :
\sum_(0 ≤ i < num_mid_jobs)
service_during sched (nth elem sorted_jobs i.+1) t1 t2 ≤
num_mid_jobs × task_cost tsk.
Proof.
apply leq_trans with (n := num_mid_jobs × task_cost tsk);
last by rewrite leq_mul2l; apply/orP; right.
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs) task_cost tsk);
last by rewrite big_const_nat iter_addn addn0 mulnC subn0.
rewrite big_nat_cond [\sum_(0 ≤ i < num_mid_jobs) task_cost _]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
exploit workload_bound_all_jobs_from_tsk.
{
instantiate (1 := nth elem sorted_jobs i.+1).
apply mem_nth; rewrite H_at_least_two_jobs.
by rewrite ltnS; apply leq_trans with (n := num_mid_jobs).
}
move ⇒ [ARR [TSK _]].
eapply cumulative_service_le_task_cost; eauto 1.
by apply H_jobs_have_valid_parameters.
Qed.
Lemma workload_bound_many_periods_in_between :
job_arrival j_lst - job_arrival j_fst ≥ num_mid_jobs.+1 × (task_period tsk).
Proof.
assert (EQnk: num_mid_jobs.+1=(size sorted_jobs).-1).
by rewrite H_at_least_two_jobs.
unfold j_fst, j_lst; rewrite EQnk telescoping_sum;
last by ins; apply workload_bound_jobs_ordered_by_arrival.
rewrite -[_ × _ tsk]addn0 mulnC -iter_addn -{1}[_.-1]subn0 -big_const_nat.
rewrite big_nat_cond [\sum_(0 ≤ i < _)(_-_)]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move ⇒ /andP LT; des.
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.
assert (ARRle: job_arrival cur ≤ job_arrival next).
by unfold cur, next; apply workload_bound_jobs_ordered_by_arrival.
feed (workload_bound_all_jobs_from_tsk cur).
by apply mem_nth, (ltn_trans LT0); destruct sorted_jobs.
intros [CURarr [CURtsk [_ CURin]]].
feed (workload_bound_all_jobs_from_tsk next).
by apply mem_nth; destruct sorted_jobs.
intros [NEXTarr [NEXTtsk [_ NEXTin]]].
assert (CUR_LE_NEXT: job_arrival cur + task_period (job_task cur) ≤ job_arrival next).
{
apply H_sporadic_tasks; try (by done).
unfold cur, next, not; intro EQ; move: EQ ⇒ /eqP EQ.
rewrite nth_uniq in EQ; first by move: EQ ⇒ /eqP EQ; ssrlia.
by apply ltn_trans with (n := (size sorted_jobs).-1); destruct sorted_jobs; ins.
by destruct sorted_jobs; ins.
by rewrite sort_uniq -/scheduled_jobs filter_uniq // undup_uniq.
by rewrite CURtsk.
}
by rewrite leq_subRL_impl // addnC -CURtsk.
Qed.
Lemma workload_bound_n_k_covers_all_jobs :
n_k ≥ num_mid_jobs.+2.
Proof.
rename H_valid_task_parameters into PARAMS.
unfold is_valid_sporadic_task in *; des.
rewrite leqNgt; apply/negP; unfold not; intro LTnk.
assert (DISTmax: job_arrival j_lst - job_arrival j_fst ≥ delta + R_tsk).
{
apply leq_trans with (n := num_mid_jobs.+1 × task_period tsk);
last by apply workload_bound_many_periods_in_between.
apply leq_trans with (n := n_k × task_period tsk);
last by rewrite leq_mul2r; apply/orP; right.
unfold n_k, max_jobs, div_ceil.
destruct (task_period tsk %| delta + R_tsk) eqn:DIV.
{
rewrite dvdn_eq in DIV; move: DIV ⇒ /eqP DIV.
by rewrite DIV.
}
by apply ltnW, ltn_ceil, PARAMS0.
}
rewrite <- leq_add2r with (p := job_arrival j_fst) in DISTmax.
rewrite addnC addnBAC in DISTmax; last first.
{
unfold j_fst, j_lst; rewrite -[_.+1]add0n.
apply prev_le_next; last by rewrite H_at_least_two_jobs add0n leqnn.
by ins; apply workload_bound_jobs_ordered_by_arrival.
}
rewrite -[job_arrival j_lst + _ - _]subnBA // subnn subn0 in DISTmax.
rewrite [delta + _]addnC addnA in DISTmax.
apply leq_trans with (m := t1 + delta) in DISTmax; last first.
{
rewrite leq_add2r.
by apply workload_bound_response_time_of_first_job_inside_interval.
}
have LST := workload_bound_last_job_arrives_before_end_of_interval.
by apply leq_ltn_trans with (m := t2) in LST; first by rewrite ltnn in LST.
Qed.
Lemma workload_bound_holds :
\sum_(0 ≤ i < num_mid_jobs.+2)
service_during sched (nth elem sorted_jobs i) t1 t2
≤ workload_bound.
Proof.
unfold workload_bound, W; fold n_k.
have ALL := workload_bound_n_k_covers_all_jobs.
apply leq_trans with (n := num_mid_jobs.+2 × task_cost tsk);
last by rewrite leq_mul2r; apply/orP; right.
apply leq_trans with (n := \sum_(0 ≤ i < num_mid_jobs.+2) task_cost tsk);
last by rewrite big_const_nat iter_addn addn0 subn0 mulnC.
rewrite big_nat_cond [\sum_(_ ≤ _ < _ | true)_]big_nat_cond.
apply leq_sum; intro i; move ⇒ /andP [/andP [_ LEi] _].
exploit workload_bound_all_jobs_from_tsk.
{
instantiate (1 := nth elem sorted_jobs i).
by apply mem_nth; rewrite H_at_least_two_jobs.
}
move ⇒ [ARR [TSK _]].
eapply cumulative_service_le_task_cost; eauto 1.
by apply H_jobs_have_valid_parameters.
Qed.
End WorkloadTwoOrMoreJobs.
Theorem workload_bounded_by_W :
workload_of tsk t1 (t1 + delta) ≤ workload_bound.
Proof.
unfold workload_of, workload_bound, W in *; ins; des.
fold n_k.
rewrite workload_eq_workload_joblist.
rewrite workload_bound_simpl_by_sorting_scheduled_jobs.
destruct (size sorted_jobs ≤ n_k) eqn:NUM;
first by apply workload_bound_holds_for_at_most_n_k_jobs.
apply negbT in NUM; rewrite -ltnNge in NUM.
assert (EX: ∃ elem: Job, True).
destruct sorted_jobs; [ by rewrite ltn0 in NUM | by ∃ s].
destruct EX as [elem _].
rewrite (big_nth elem).
destruct (size sorted_jobs) as [| n] eqn:SIZE;
first by rewrite big_geq.
destruct n as [| num_mid_jobs];
first by apply workload_bound_holds_for_a_single_job; rewrite SIZE.
by apply workload_bound_holds.
Qed.
End MainProof.
End ProofWorkloadBound.
End WorkloadBound.