Commit 30ea7ca8 authored by Martin PORTALIER's avatar Martin PORTALIER

Update workload_bound_fp.v

parent 2d061778
Pipeline #18873 failed with stages
in 28 seconds
......@@ -32,19 +32,19 @@ Section WorkloadBoundFPP.
(* In this section, we define a bound for the workload of multiple tasks. *)
Section AllTasks.
Context {Task: eqType}.
Context `{TaskCost Task} `{SporadicModel Task}.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be the task to be analyzed. *)
Variable tsk: Task.
(* Let delta be the length of the interval of interest. *)
Variable delta: duration.
......@@ -54,15 +54,12 @@ Section WorkloadBoundFPP.
Let W tsk_other :=
task_workload_bound_FP tsk_other delta.
(* Check higher_eq_priority.
Check FP_policy Task. *)
(* Using the sum of individual workload bounds, we define the following bound
for the total workload of tasks of higher-or-equal priority (with respect
to tsk) in any interval of length delta. *)
Definition total_workload_bound_fp :nat :=
\sum_(x <- ts | is_hep_task x) (W x).
End AllTasks.
(* In this section, we prove some basic lemmas about the workload bound. *)
......@@ -73,10 +70,10 @@ Section WorkloadBoundFPP.
(* Assume any FP policy. *)
Variable higher_eq_priority: FP_policy Task.
(* Consider a task set ts... *)
Variable ts: list Task.
(* ...and let tsk be any task in ts. *)
Variable tsk: Task.
Hypothesis H_tsk_in_ts: tsk \in ts.
......@@ -100,32 +97,19 @@ Section WorkloadBoundFPP.
(* We prove that the workload bound of an interval of size (task_cost tsk)
cannot be smaller than (task_cost tsk). *)
Lemma total_workload_bound_fp_ge_cost:
workload_bound (task_cost tsk) >= task_cost tsk.
task_cost tsk <= workload_bound (task_cost tsk).
Proof.
(* hint: some useful lemmas
big_mkcond big_rem from ssreflect.bigop
leq_trans from ssreflect.seq
*)
unfold workload_bound. unfold total_workload_bound_fp.
(* Check big_rem. *)
rewrite (big_rem tsk H_tsk_in_ts).
have Refl: higher_eq_priority tsk tsk. { apply H_priority_is_reflexive. }
rewrite Refl.
rewrite big_mkcond. simpl.
unfold task_workload_bound_FP.
(* Check leq_trans. *)
rewrite Refl. rewrite big_mkcond. simpl. unfold task_workload_bound_FP.
have Inf: task_cost tsk <= max_jobs tsk (task_cost tsk) * task_cost tsk. {
unfold max_jobs. (* SearchAbout "ceil". *)
have Inf_div: 0 < div_ceil (task_cost tsk) (task_min_inter_arrival_time tsk).
{ apply (ceil_neq0 _ _ H_cost_positive H_task_min_inter_arrival_time_positive). }
(* SearchAbout (?n <= _ * ?n). *)
apply leq_pmull. apply Inf_div. }
(* Check leq_trans. *)
unfold max_jobs.
have Inf_div: 0 < div_ceil (task_cost tsk) (task_min_inter_arrival_time tsk). {
apply (ceil_neq0 _ _ H_cost_positive H_task_min_inter_arrival_time_positive). }
apply leq_pmull. apply Inf_div. }
apply leq_trans with (n:= max_jobs tsk (task_cost tsk) * task_cost tsk).
- apply Inf.
- (* SearchAbout (?n <= _ + ?n). *)
rewrite addnC.
apply leq_addl.
apply Inf. rewrite addnC. apply leq_addl.
Qed.
End NoSmallerThanCost.
......@@ -147,27 +131,22 @@ Section WorkloadBoundFPP.
workload_bound delta1 <= workload_bound delta2.
Proof.
move => delta1 delta2 H2. unfold workload_bound.
unfold total_workload_bound_fp. (* Search "leq" "sum". *)
apply leq_sum_seq. move => x H3 H4.
unfold task_workload_bound_FP. unfold max_jobs.
(* SearchAbout "leq" "mul". *) apply leq_mul.
- (* SearchAbout "ceil". *) apply leq_divceil2r.
+ apply (H_period_positive x H3).
+ exact: H2.
- easy.
unfold total_workload_bound_fp. apply leq_sum_seq. move => x H3 H4.
unfold task_workload_bound_FP. unfold max_jobs. apply leq_mul; auto.
apply leq_divceil2r. apply (H_period_positive x H3). exact: H2.
Qed.
End NonDecreasing.
End BasicLemmas.
(* In this section, we prove that any fixed point R = workload_bound R
is indeed a workload bound for an interval of length R. *)
Section ProofWorkloadBound.
Context {Task: eqType}.
Context `{TaskCost Task} `{SporadicModel Task} `{TaskDeadline Task}.
Context {Job: eqType}.
Context `{JobArrival Job} `{JobCost Job} `{JobDeadline Job} `{JobTask Job Task}.
......@@ -178,12 +157,7 @@ Section WorkloadBoundFPP.
(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).
(* TODO_:
for any task from ts:
its task_cost task_min_inter_arrival_time task_deadline are positive; and
task_cost <= deadline
task_cost <= task_min_inter_arrival_time*)
(* Consider any job arrival sequence with consistent, duplicate-free arrivals. *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_valid_arrival_sequence: valid_arrival_sequence arr_seq.
......@@ -200,7 +174,6 @@ for any task from ts:
job_cost j <= task_cost (job_task j)/\
job_cost j <= job_deadline j.
(* Assume that jobs arrived sporadically. *)
Hypothesis H_sporadic_arrivals: respects_sporadic_task_model arr_seq.
......@@ -210,7 +183,7 @@ for any task from ts:
(* Assume any fixed-priority policy. *)
Variable higher_eq_priority: FP_policy Task.
(* First, let's define some local names for clarity. *)
Let arrivals_between := jobs_arrived_between arr_seq.
Let hp_workload t1 t2:=
......@@ -231,9 +204,12 @@ for any task from ts:
Proof.
move => t. unfold hp_workload.
unfold workload_of_higher_or_equal_priority_tasks.
unfold workload_of_jobs.
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.
Admitted.
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