Commit 1b90d37b authored by Martin PORTALIER's avatar Martin PORTALIER

Update workload_bound_fp.v

parent 70d8f5bd
Pipeline #19192 failed with stages
in 40 seconds
From rt.restructuring.model Require Export task_cost workload.
From rt.restructuring.model.arrival Require Export sporadic.
From rt.restructuring.model Require Export priority_based.priorities.
From rt.restructuring.analysis Require Export intermediate.
From rt.restructuring.analysis Require Export facts.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
From rt.util Require Import tactics bigcat div_mod sum ssromega.
......@@ -157,7 +157,8 @@ Section WorkloadBoundFPP.
forall tsk, tsk \in ts ->
(task_cost tsk) > 0 /\ (task_min_inter_arrival_time tsk) > 0
/\ (task_deadline tsk) > 0 /\ (task_cost tsk) <= (task_deadline tsk)
/\ (task_cost tsk) <= (task_min_inter_arrival_time tsk).
/\ (task_cost tsk) <= (task_min_inter_arrival_time tsk)
/\ task_deadline tsk <= task_min_inter_arrival_time tsk.
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
......@@ -198,6 +199,7 @@ Section WorkloadBoundFPP.
i.e., the claimed workload bound is equal to the interval length. *)
Variable R: duration.
Hypothesis H_fixed_point: R = workload_bound R.
Hypothesis H_positive: 0 < R.
Lemma partition_sum: forall (r:list Job) P F,
(forall j, j \in r -> job_task j \in ts)
......@@ -364,6 +366,138 @@ Section WorkloadBoundFPP.
destruct H_in as [i H_in]. exists i. easy.
Qed.
Variable j: Job.
Hypothesis H_job_task: job_task j = tsk.
Hypothesis H_all_arrives:
forall tsk', higher_eq_priority tsk' tsk
-> exists jb, jb \in jobs_arriving_at arr_seq (job_arrival j)
/\ job_task jb = tsk'.
Hypothesis H_task_cost: forall jb,
job_cost jb = task_cost (job_task jb).
Hypothesis H_periodic: forall j1 t,
j1 \in jobs_arriving_at arr_seq t -> exists j2,
j2 \in jobs_arriving_at arr_seq (t + task_min_inter_arrival_time (job_task j1))
/\ same_task j1 j2.
Lemma clc: forall n m p,
0 < m -> m * n < p + n -> (m - 1) * n < p.
Proof.
move => n m p. destruct m as [|m]; auto.
have ->: (succn m - 1) = m by ssromega.
have ->: succn m * n = m * n + n by ssromega.
rewrite ltn_add2r. auto.
Qed.
Lemma div_sup : forall n m,
0 < n -> 0 < m -> m * ((div_ceil n m) - 1) < n.
Proof.
move => n m H_pos_n H_pos_m. unfold div_ceil. case E: (m %| n).
- rewrite mulnC. apply clc. rewrite lt0n. case E': (n %/ m == 0); auto.
move /eqP in E'. have H_eq: (n = n %/ m * m + n %% m) by apply divn_eq.
rewrite E' in H_eq. rewrite mul0n in H_eq. rewrite add0n in H_eq.
have H_contr: n < m. rewrite H_eq. apply ltn_pmod; auto.
apply dvdn_leq in E; auto. ssromega. rewrite divnK; auto. ssromega.
- have ->: (succn (n %/ m) - 1) = n %/m by ssromega. rewrite mulnC.
case E': (n %/ m * m == n). rewrite -dvdn_eq in E'. rewrite E in E'. auto.
have H_inf: n %/ m * m <= n by apply leq_trunc_div.
rewrite leq_eqVlt in H_inf. move /orP in H_inf.
destruct H_inf as [H_eq | H_inf]. rewrite E' in H_eq. auto.
exact: H_inf.
Qed.
Lemma soul: forall k m p,
0 < p -> k + m <= k + m + p - 1.
Proof.
move => k m p H_pos. ssromega.
Qed.
Lemma exists_job_tsk : forall tsk' i,
higher_eq_priority tsk' tsk ->
0 < \sum_(j0 <- arr_seq (job_arrival j + i * task_min_inter_arrival_time tsk')
| job_task j0 == tsk') 1.
Proof.
move => tsk' i H_hp. set T_min := task_min_inter_arrival_time tsk'.
have H_exists: exists jb,
jb \in jobs_arriving_at arr_seq (job_arrival j + i * T_min)
/\ job_task jb = tsk'. {
elim: i => [| i IH].
- rewrite mul0n addn0. apply H_all_arrives in H_hp.
destruct H_hp as [jb [H_in H_tsk]]. exists jb. auto.
- destruct IH as [j1 [H_in H_tsk]]. apply H_periodic in H_in.
destruct H_in as [j2 [H_in2 H_tsk2]]. rewrite H_tsk in H_in2.
exists j2. have ->: (succn i) = i + 1 by ssromega.
rewrite mulnDl addnA mul1n. split; auto. move /eqP in H_tsk2.
rewrite -H_tsk2. auto. }
destruct H_exists as [jb [H_in H_tsk]].
rewrite big_mkcond (bigD1_seq jb)/=; auto.
rewrite H_tsk. have ->: tsk' == tsk' by auto. ssromega.
unfold valid_arrival_sequence in H_valid_arrival_sequence. easy.
Qed.
Lemma sum_eq_max_jobs : forall tsk',
tsk' \in ts -> higher_eq_priority tsk' tsk ->
\sum_(j0 <- arrivals_between (job_arrival j) ((job_arrival j) + R)
| job_task j0 == tsk') 1 >= max_jobs tsk' R.
Proof.
move => tsk' H_in H_hp. unfold max_jobs. unfold arrivals_between.
unfold jobs_arrived_between. unfold jobs_arriving_at.
rewrite sommable. set T_min := task_min_inter_arrival_time tsk'.
have H_pos: 0 < T_min. apply H_valid_task_parameters; auto.
set div := div_ceil R T_min. apply leq_trans with
(n := \sum_((job_arrival j) <= t0 < (job_arrival j) + T_min * (div - 1) + 1)
\sum_(i <- arr_seq t0 | job_task i == tsk') 1).
rewrite -> big_cat_nat with (n:=job_arrival j + T_min * (div - 1)).
simpl. have ->: job_arrival j + T_min * (div - 1) + 1
= succn (job_arrival j + T_min * (div - 1)) by ssromega.
rewrite big_nat1.
have {1}->: div = div - 1 + 1. {
have H_div: 0 < div. apply ceil_neq0; easy. ssromega. }
rewrite sum_interval.
have {1}->: div - 1 = \sum_(0 <= i < div - 1) 1. {
rewrite sum_nat_const_nat muln1. ssromega. }
apply sum_inf_2.
- apply leq_sum. move => i _.
have H_jb: job_arrival j + (i + 1) * T_min > 0.
rewrite mulnDl mul1n addnA. apply ltn_addl; auto.
have ->: job_arrival j + (i + 1) * T_min
= succn (job_arrival j + (i + 1) * T_min - 1) by ssromega.
rewrite big_nat_recl. rewrite addn_gt0. apply /orP. left.
apply exists_job_tsk; auto. rewrite mulnDl mul1n addnA.
apply soul; auto.
- rewrite mulnC. apply exists_job_tsk; auto.
rewrite leq_addr; auto. ssromega.
apply extend_sum; auto. apply lt1_leq. rewrite ltn_add2l.
apply div_sup; easy.
Qed.
Lemma workload_reach:
hp_workload (job_arrival j) ((job_arrival j) + R) = R.
Proof.
unfold hp_workload. unfold workload_of_higher_or_equal_priority_tasks.
unfold workload_of_jobs. rewrite H_fixed_point.
rewrite -{1}H_fixed_point.
unfold workload_bound. unfold total_workload_bound_fp.
unfold task_workload_bound_FP.
rewrite -> partition_sum with (P:=(fun x => higher_eq_priority x tsk)).
rewrite big_seq_cond. rewrite [\sum_(x <- ts | higher_eq_priority x tsk)
max_jobs x R * task_cost x]big_seq_cond. apply eq_bigr.
move => tsk' H_bool. move /andP in H_bool.
have ->: max_jobs tsk' R =
\sum_(j0 <- arrivals_between (job_arrival j) (job_arrival j + R)
| job_task j0 == tsk') 1. {
apply /eqP. rewrite eqn_leq. apply /andP. split.
apply sum_eq_max_jobs; easy. apply sum_inf_max_jobs; easy. }
rewrite -sum_prod mul1n. apply eq_bigr. move => jb H_tsk.
move /eqP in H_tsk. rewrite -H_tsk. apply H_task_cost.
move => jb H_in. apply H_all_jobs_from_taskset.
unfold arrivals_between in H_in. unfold jobs_arrived_between in H_in.
apply mem_bigcat_nat_exists in H_in.
destruct H_in as [i H_in]. exists i. easy.
Qed.
End ProofWorkloadBound.
End WorkloadBoundFPP.
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment