Commit 194d67da authored by Xiaojie Guo's avatar Xiaojie Guo

comments

parent c4ada686
Pipeline #18837 failed with stages
in 25 seconds
......@@ -180,6 +180,8 @@ Section AnalyseInterval.
Hypothesis H_transitive : forall j1 j2 j3,
higher_eq_priority j1 j2 -> higher_eq_priority j2 j3
-> higher_eq_priority j1 j3.
(* Xiaojie: il manque job_arrival jb <= t *)
Hypothesis H_hp_completed : forall jb jb' t,
~~ completed_by sched jb t -> sched t = Some jb'
-> higher_eq_priority jb' jb.
......@@ -797,6 +799,7 @@ Section AnalyseInterval.
Variable workload_bound : nat -> nat.
Variable r : nat.
(* Xiaojie: affaiblir cette definition comme hp_workload' *)
Let hp_workload_time t delta := (other_hp_workload t (t + delta)) +
workload_from_same_task t (job_arrival j).+1.
......@@ -806,7 +809,7 @@ Section AnalyseInterval.
Hypothesis H_fp_valid: r > 0.
(* Xiaojie: Ce lemme est trop general ! *)
(* Xiaojie: c'est trop général *)
Lemma Hfqli : forall t t' delta,
t < t' < t + delta -> ~~ quiet_time t'
-> delta < hp_workload_time t delta.
......
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