Commit c4ada686 authored by Xiaojie Guo's avatar Xiaojie Guo

comments

parent 24c14938
Pipeline #18836 failed with stages
in 27 seconds
......@@ -3,7 +3,7 @@ From rt.restructuring.behavior Require Export schedule
From rt.restructuring.model.schedule Require Export priority_based.priorities
work_conserving sequential.
From rt.restructuring.model Require Export workload sporadic.
From rt.restructuring.analysis.fpp_implicit_deadline Require Export facts.
From rt.restructuring.analysis.fpp_implicit_deadline Require Export facts fixedpoint_lemmas.
From mathcomp Require Import all_ssreflect seq.
From rt.util Require Import bigcat tactics ssromega sum.
......@@ -296,9 +296,11 @@ Section AnalyseInterval.
(n:=service sched j (end_of_analyse_interval)); auto.
have /eqP<-: (t2 == end_of_analyse_interval); auto.
have /eqP->: (len == t2 - t1); auto.
rewrite addnBCA. apply inf_service. apply leq_addr.
rewrite addnBA. apply inf_service. rewrite addnC -addnBA.
apply leq_addr.
apply start_inf_arrival. apply start_inf_end.
Qed.
Qed.
Let hp_service (t1 t2:instant) := \sum_(t1 <= t < t2)
( \sum_(j' <- jobs_arrived_between arr_seq t1 t2
......@@ -600,6 +602,13 @@ Section AnalyseInterval.
Let hp_workload delta := (other_hp_workload t1 (t1 + delta)) +
workload_from_same_task t1 (job_arrival j).+1.
(* Xiaojie: c'est mieux d'utiliser la definition ci-dessous qui affaiblit un peu la definition (c'est plus gentil pour prouver hp_workload d <= workload_bound d. quand tu en a besoin. ) *)
Let hp_workload' delta := (other_hp_workload t1 (t1 + delta)) +
if (t1 + delta) <= job_arrival j then
workload_from_same_task t1 (t1 + delta)
else
workload_from_same_task t1 (job_arrival j).+1.
Lemma completes_at_sched : forall jb t',
0 < t' -> completes_at sched jb t' -> sched t'.-1 = Some jb.
Proof.
......@@ -791,10 +800,13 @@ Section AnalyseInterval.
Let hp_workload_time t delta := (other_hp_workload t (t + delta)) +
workload_from_same_task t (job_arrival j).+1.
Hypothesis H_borne : forall t delta,
(* 0 < t <= task_deadline tsk -> *) workload_bound delta >= hp_workload_time t delta.
Hypothesis H_borne : forall delta,
workload_bound delta >= hp_workload delta.
Hypothesis H_fixpoint : workload_bound r = r.
Hypothesis H_fp_valid: r > 0.
(* Xiaojie: Ce lemme est trop general ! *)
Lemma Hfqli : forall t t' delta,
t < t' < t + delta -> ~~ quiet_time t'
-> delta < hp_workload_time t delta.
......@@ -802,27 +814,33 @@ Section AnalyseInterval.
move => t t' delta H_in H_quiet. unfold hp_workload_time.
unfold other_hp_workload. unfold workload_from_same_task.
unfold workload_of_jobs.
(* have H_tmp: t <= t' -> \sum_(t <= t0 < t') service_in jb (sched t0) <= job_cost jb.
*)Admitted.
(* have H_tmp: t <= t' -> \sum_(t <= t0 < t') service_in jb (sched t0) <= job_cost jb.
*)Admitted.
(* Xiaojie: il faut directement prouver ce lemme *)
Lemma ppf: forall d,
d > 0 -> d < len -> d < hp_workload d.
Proof.
move => d H_d_pos H_inf.
Admitted.
Admitted.
Lemma relation_wl: forall d,
d <= len -> hp_workload d <= workload_bound d.
d <= len -> hp_workload d <= workload_bound d.
Proof.
move => d H_inf. apply H_borne.
Qed.
Lemma resp_time_bound :
job_response_time_bound sched j r.
Proof.
apply completed with (t:=(job_arrival j + len)).
- rewrite leq_add2l. admit.
- rewrite leq_add2l.
(* rewrite eq_intermediate serv_eq_workload -H_fixpoint. *)
(* apply wl_plus_big;try rewrite -serv_eq_workload -eq_intermediate//. *)
(* apply H_fp_valid. *)
(* by symmetry. *)
admit.
(* intros;auto. *)
- apply job_finish_end_of_interval.
(* Qed. *) Admitted.
......
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