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

Update main_theorem.v

parent abff67d5
Pipeline #19189 failed with stages
in 36 seconds
......@@ -43,7 +43,7 @@ Hypothesis H_valid_job_parameters: forall j,
Let higher_eq_priority := hep_task.
Let jl_hep := (fun j1 j2 => higher_eq_priority (job_task j1) (job_task j2)).
Hypothesis H_reflexive : reflexive jl_hep.
Hypothesis H_reflexive : reflexive jl_hep /\ reflexive higher_eq_priority.
Hypothesis H_transitive : transitive jl_hep.
Hypothesis H_fpp : respects_preemptive_priorities arr_seq sched.
......@@ -59,7 +59,8 @@ Variable ts: list Task.
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).
/\ (task_cost tsk) <= (task_min_inter_arrival_time tsk)
/\ task_deadline 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.
......@@ -81,7 +82,7 @@ Let is_hep_task tsk_other := higher_eq_priority tsk_other tsk.
(* task_worload_bound *)
Definition formula (delta : duration) : nat :=
\sum_(x <- ts | is_hep_task x && (tsk != x))
\sum_(x <- ts | is_hep_task x && (x != tsk))
(task_workload_bound_FP x delta) + task_cost tsk.
Variable R : duration.
......@@ -119,11 +120,49 @@ Proof.
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.
rewrite -{1}H_fix. unfold total_workload_bound_fp.
rewrite big_mkcond (bigD1_seq tsk)/=; auto. rewrite H_job_task.
have ->: higher_eq_priority tsk tsk by apply H_reflexive.
rewrite addnC -big_mkcondl/=. unfold formula.
unfold task_workload_bound_FP. unfold max_jobs. rewrite ceil_eq1.
rewrite mul1n. auto. easy. apply leq_trans with (n:=task_deadline tsk).
easy. apply H_valid_task_parameters; auto.
Qed.
(* ****************************************************************************
---------------------BONUS : AS A BOUND, R IS REACHED.----------------------
**************************************************************************** *)
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.
Hypothesis is_schedulable: forall j1 j2 t,
~~ completed_by sched j1 t -> job_arrival j2 = t
-> same_task j1 j2 -> False.
Lemma start_interval_arrival:
start_of_analyse_interval arr_seq sched jl_hep j = job_arrival j.
Proof.
rewrite -> start_interval_arrival with (task_hep:=higher_eq_priority); try easy.
move => tsk' H_hp. apply H_all_arrives. rewrite -H_job_task. auto.
Qed.
Theorem all_arrives:
forall j jb, jl_hep jb j
Theorem max_bound_reach:
completes_at sched j ((job_arrival j) + R).
Proof.
Admitted.
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