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

Update main_theorem.v

parent 18b649ce
Pipeline #19157 failed with stages
in 23 seconds
......@@ -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
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