diff --git a/restructuring/analysis/fpp_implicit_deadline/main_theorem.v b/restructuring/analysis/fpp_implicit_deadline/main_theorem.v index 2068f880180fbe458a11aee471c075e6b6dbbb0c..ed8ffe027f75079e7dc6e6c4bcc2bbb1c277550b 100644 --- a/restructuring/analysis/fpp_implicit_deadline/main_theorem.v +++ b/restructuring/analysis/fpp_implicit_deadline/main_theorem.v @@ -8,7 +8,7 @@ From rt.restructuring.analysis.fpp_implicit_deadline Require Export From rt.restructuring.behavior.schedule Require Export ideal. From mathcomp Require Import seq. -From rt.util Require Import div_mod sum. +From rt.util Require Import div_mod sum tactics. Section main. @@ -35,10 +35,13 @@ Hypothesis H_sched_none : forall t, sched t = None -> arr_seq t = [::]. Hypothesis H_sequential_jobs: sequential_jobs sched. -Hypothesis H_positive_cost : forall jb, 0 < job_cost jb. +(* ...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. Let higher_eq_priority := hep_task. -Let jl_hep := FP_to_JLFP Job Task. +Let jl_hep := (fun j1 j2 => higher_eq_priority (job_task j1) (job_task j2)). Hypothesis H_reflexive : reflexive jl_hep. Hypothesis H_transitive : transitive jl_hep. @@ -52,13 +55,21 @@ Hypothesis H_sporadic : forall j j', Variable tsk: Task. Variable ts: list Task. -(* Variable delta: duration. *) +Hypothesis H_valid_task_parameters: 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). +(* Assume that all jobs come from the task set ...*) +Hypothesis H_all_jobs_from_taskset: forall j, + arrives_in arr_seq j -> job_task j \in ts. Hypothesis H_tsk_in_ts: tsk \in ts. - +Hypothesis H_uniq: uniq ts. Hypothesis H_sporadic_tasks: respects_sporadic_task_model arr_seq. +Hypothesis H_implicit_deadline: task_deadline tsk = task_min_inter_arrival_time tsk. + (* Definition max_jobs : nat := div_ceil delta (task_min_inter_arrival_time tsk). @@ -77,8 +88,6 @@ Variable R : duration. Hypothesis H_valid_R : formula R = R /\ R > 0 /\ R <= task_deadline tsk. -Hypothesis H_implicit_deadline: task_deadline tsk = task_min_inter_arrival_time tsk. - Section exists_t2. Let workload_bound := formula. @@ -102,15 +111,19 @@ Proof. apply exists_t2 with (delta:=R); easy. apply resp_time_bound with (arr_seq0:=arr_seq) (higher_eq_priority0:=jl_hep) (end_of_analyse_interval:=t2) - (workload_bound:=formula); try easy. move => d. + (workload_bound:=formula); try easy. + move => j0; apply H_valid_job_parameters; auto. set t1 := start_of_analyse_interval arr_seq sched jl_hep j. - unfold workload_of_jobs. unfold formula. - - - SearchAbout "big" "cond". - rewrite big_filter_cond big_filter. SearchAbout "big" "change". - - + unfold workload_of_jobs. + apply leq_trans with (n:=\sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + R) | + higher_eq_priority (job_task j0) (job_task j)) job_cost j0). + apply inf_workload; auto. have H_fix: formula R = R by easy. rewrite H_fix. + apply fp_workload_bound_holds with (ts0:=ts); auto. + rewrite -{1}H_fix. unfold total_workload_bound_fp. unfold formula. + rewrite big_mkcondr/=. unfold is_hep_task. rewrite H_job_task. Admitted. +Theorem all_arrives: + forall j jb, jl_hep jb j + End main. \ No newline at end of file