Commit 3d62f31b authored by Martin PORTALIER's avatar Martin PORTALIER

Update workload_bound_fp.v

parent d4eae082
Pipeline #19219 canceled with stages
......@@ -169,12 +169,10 @@ Section WorkloadBoundFPP.
forall j, arrives_in arr_seq j -> job_task j \in ts.
(* ...and have valid parameters. *)
Hypothesis H_valid_job_parameters:
forall j,
arrives_in arr_seq j ->
job_cost j > 0 /\
job_cost j <= task_cost (job_task j)/\
job_cost j <= job_deadline j.
Hypothesis H_valid_job_parameters: forall j,
arrives_in arr_seq j -> job_cost j > 0 /\
job_cost j <= task_cost (job_task j)/\ job_cost j <= job_deadline j
/\ job_deadline j = task_deadline (job_task j).
(* Assume that jobs arrived sporadically. *)
Hypothesis H_sporadic_arrivals: respects_sporadic_task_model arr_seq.
......@@ -195,6 +193,13 @@ Section WorkloadBoundFPP.
Let workload_bound :=
total_workload_bound_fp higher_eq_priority ts tsk.
Lemma rwt_hp_workload: forall t r,
hp_workload t (t + r) = \sum_(j0 <- jobs_arrived_between arr_seq t (t + r) |
higher_eq_priority (job_task j0) tsk) job_cost j0.
Proof.
move => t r. auto.
Qed.
(* Consider any R that is a fixed point of the following equation,
i.e., the claimed workload bound is equal to the interval length. *)
Variable R: duration.
......@@ -340,9 +345,7 @@ Section WorkloadBoundFPP.
forall t,
hp_workload t (t + R) <= R.
Proof.
move => t. unfold hp_workload.
unfold workload_of_higher_or_equal_priority_tasks.
unfold workload_of_jobs. rewrite H_fixed_point.
move => t. rewrite rwt_hp_workload. rewrite H_fixed_point.
rewrite -{1}H_fixed_point.
unfold workload_bound. unfold total_workload_bound_fp.
unfold task_workload_bound_FP.
......@@ -382,20 +385,11 @@ Section WorkloadBoundFPP.
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.
- rewrite mulnC. apply inf_less1. 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.
......@@ -408,12 +402,6 @@ Section WorkloadBoundFPP.
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')
......@@ -437,16 +425,16 @@ Section WorkloadBoundFPP.
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.
Lemma sum_eq_max_jobs : forall tsk' r,
0 < r -> 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.
move => tsk' r H_pos_r 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
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)).
......@@ -466,27 +454,24 @@ Section WorkloadBoundFPP.
= 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.
apply sum_inf_3; 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.
Lemma pre_workload_reach: forall r, 0 < r ->
hp_workload (job_arrival j) ((job_arrival j) + r) =
\sum_(x <- ts | higher_eq_priority x tsk) max_jobs x r * task_cost x.
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.
move => r H_fp. rewrite rwt_hp_workload.
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.
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)
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. }
......@@ -498,6 +483,15 @@ Section WorkloadBoundFPP.
destruct H_in as [i H_in]. exists i. easy.
Qed.
Lemma workload_reach:
hp_workload (job_arrival j) ((job_arrival j) + R) = R.
Proof.
rewrite rwt_hp_workload. rewrite {-1}H_fixed_point.
unfold workload_bound. unfold total_workload_bound_fp.
unfold task_workload_bound_FP.
apply pre_workload_reach; 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