Commit e444a980 authored by Martin PORTALIER's avatar Martin PORTALIER

Update intermediate.v

parent caba5af6
Pipeline #19240 failed with stages
in 2 minutes and 10 seconds
......@@ -17,7 +17,6 @@ Section AnalyseInterval.
Context {Job: JobType}.
Context `{JobArrival Job} `{JobCost Job} `{JobTask Job Task}.
Context `{JobDeadline Job}.
(* Context `{ProcessorState Job (option Job)}. *)
(* Consider any job arrival sequence... *)
Variable arr_seq: arrival_sequence Job.
......@@ -30,7 +29,9 @@ Section AnalyseInterval.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_sched : valid_schedule sched arr_seq.
Hypothesis H_positive_cost : forall j, 0 < job_cost j.
Hypothesis H_positive_task: forall jb, 0 < task_min_inter_arrival_time (job_task jb).
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_sporadic_arrivals: respects_sporadic_task_model arr_seq.
Variable higher_eq_priority: JLFP_policy Job.
......@@ -121,8 +122,6 @@ Section AnalyseInterval.
Hypothesis H_same_task_same_priority : forall j1 j2,
same_task j1 j2 <->
higher_eq_priority j1 j2 && higher_eq_priority j2 j1.
Hypothesis H_sporadic : forall j j',
job_arrival j = job_arrival j' -> same_task j j' -> j = j'.
(* Facts on service and completed_by. *)
......@@ -696,12 +695,11 @@ Section AnalyseInterval.
apply H_sequential_jobs with (j2:=j); auto.
rewrite ltn_neqAle. apply /andP. split; auto.
case E'': (job_arrival jb != job_arrival j); auto.
move /eqP in E''. have H_contr: j == jb. apply /eqP.
apply H_sporadic; auto. unfold same_task.
unfold same_task in H_same. move /eqP in H_same.
apply esym in H_same. rewrite H_same. easy. move /eqP in H_contr.
rewrite H_contr in E'. rewrite -E'. easy.
simpl. rewrite H_sched. easy. }
move /eqP in E''. move /eqP in E'. apply H_sporadic_arrivals in E'.
have H_contr: job_arrival j + task_min_inter_arrival_time (job_task j) <=
job_arrival j. rewrite E'' in E'. apply E'; auto. move /eqP in H_same; auto.
have H_pos: task_min_inter_arrival_time (job_task j) > 0 by easy. ssromega.
simpl. rewrite H_sched. easy. }
have H_contr: completed_by sched jb t2. {
apply incr_completed with (t:=t2.-1); auto; try ssromega. }
contradict E H_contr.
......@@ -875,10 +873,11 @@ Section AnalyseInterval.
rewrite big_mkcond. rewrite -sum_nat_eq0_nat. apply /allP.
move => jb H_in. case E: (jb != j); auto. move /eqP in E.
case E': (job_task j == job_task jb); auto. move /eqP in E'.
apply arr_seq_arrival in H_in.
have H_contr: jb = j. apply esym. apply H_sporadic; auto.
unfold same_task. rewrite E'. auto.
easy. apply job_in_arrival.
apply arr_seq_arrival in H_in. apply H_sporadic_arrivals in E.
have H_contr: job_arrival j + task_min_inter_arrival_time (job_task jb) <=
job_arrival j. rewrite -H_in in E. apply E; auto.
have H_pos: task_min_inter_arrival_time (job_task jb) > 0 by easy.
ssromega. apply job_in_arrival.
destruct H_valid_arrival_sequence as [_ H_uniq]. auto.
apply vlib__leq_split; auto. apply start_inf_arrival.
......@@ -1004,9 +1003,6 @@ Section AnalyseInterval.
---------------FOURTH STEP : AS A BOUND, R IS REACHED.----------------------
**************************************************************************** *)
Hypothesis H_sporadic_arrivals: respects_sporadic_task_model arr_seq.
Variable task_hep : JLFP_policy Task.
Hypothesis H_policy: forall j1 j2,
task_hep (job_task j1) (job_task j2) = higher_eq_priority j1 j2.
......@@ -1016,12 +1012,8 @@ Section AnalyseInterval.
-> exists jb, jb \in jobs_arriving_at arr_seq (job_arrival j)
/\ job_task jb = tsk'.
Hypothesis is_schedulable: forall j1 j2 t,
~~ completed_by sched j1 t -> job_arrival j2 = t
-> same_task j1 j2 -> False.
Hypothesis is_schedulable_2: forall jb t,
completes_at sched jb t -> t <= job_deadline jb.
Hypothesis H_is_schedulable: forall jb,
completed_by sched jb (job_arrival jb + (job_deadline jb)).
Hypothesis H_implicit_deadline: forall jb:Job,
job_deadline jb = task_min_inter_arrival_time (job_task jb).
......@@ -1035,9 +1027,18 @@ Section AnalyseInterval.
destruct E as [jb [H_arrived [H_hp H_comp]]].
have H_tsk: task_hep (job_task jb) (job_task j). rewrite H_policy. auto.
apply H_all_arrives in H_tsk. destruct H_tsk as [jb0 [H_in H_tsk]].
exfalso. apply is_schedulable with (j1:=jb) (j2:=jb0) (t:=job_arrival j).
easy. apply arr_seq_arrival in H_in. auto. unfold same_task. rewrite H_tsk; auto.
apply arr_seq_arrival in H_in. exfalso.
have H_contr: job_arrival jb + task_min_inter_arrival_time (job_task jb0) <=
job_arrival j. {
rewrite H_in H_tsk. apply H_sporadic_arrivals; auto.
case E: (jb == jb0).
* move /eqP in E. rewrite -E in H_in. unfold arrived_before in H_arrived. ssromega.
* move /eqP in E. auto. rewrite H_in in H_arrived. unfold arrived_before in H_arrived.
ssromega. }
rewrite H_tsk in H_contr. apply decr_no_completed with (jb:=jb) in H_contr.
rewrite -H_implicit_deadline in H_contr.
contradict H_contr H_is_schedulable. auto.
Lemma rewrite_workload:
hp_workload len = \sum_(j0 <- jobs_arrived_between arr_seq t1 (t1 + len)
......@@ -1065,15 +1066,19 @@ Section AnalyseInterval.
destruct H_in as [H_tsk H_in]. apply jobs_arrived_in in H_in.
move /andP in H_in. destruct H_in as [H_sup H_inf].
rewrite H_len in H_inf. have H_comp: completes_at sched j t2 by auto.
apply is_schedulable_2 in H_comp. rewrite H_implicit_deadline in H_comp.
unfold respects_sporadic_task_model in H_sporadic_arrivals.
move /eqP in H_tsk. apply H_sporadic_arrivals in H_tsk.
apply ltn_trans with (p:=t2) in H_sup; auto.
apply leq_ltn_trans with (p:=t2) in H_tsk; auto.
apply ltn_leq_trans with (p:=task_min_inter_arrival_time (job_task j)) in H_tsk; auto.
ssromega. unfold not. move => H_jb. rewrite H_jb in H_sup. ssromega.
exists (job_arrival j); apply job_in_arrival.
exists (job_arrival jb); apply job_in_arrival. rewrite ltnW; auto.
case E: (job_arrival j + job_deadline j < t2). apply lt_leq1 in E.
unfold completes_at in H_comp. move /andP in H_comp.
have H_no_comp: ~~ completed_by sched j t2.-1 by easy.
apply decr_no_completed with (t:=job_arrival j + job_deadline j) in H_no_comp; auto.
have H_contr: completed_by sched j (job_arrival j + job_deadline j)
by apply H_is_schedulable. contradict H_no_comp H_contr. easy.
apply leq_ltn_trans with (n:=job_arrival j); auto.
have E': t2 <= job_arrival j + job_deadline j. ssromega.
apply ltn_leq_trans with (m:=job_arrival jb) in E'; try ssromega.
have H_contr: job_arrival j + job_deadline j <= job_arrival jb.
rewrite H_implicit_deadline. apply H_sporadic_arrivals; auto.
unfold not. move => H_jb. rewrite H_jb in H_sup. ssromega.
move /eqP in H_tsk; auto. ssromega.
- rewrite has_filter in H_has. move /eqP in H_has.
rewrite filter_predT in H_has. auto. }
rewrite H_nil big_nil; auto. apply vlib__leq_split.
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