Skip to content

GitLab

Commit 5d2ce255 authored by Felipe Cerqueira's avatar Felipe Cerqueira
Browse files

Fix references to service lemmas

parent 7c69093d
Hide whitespace changes
Inline Side-by-side
bertogna_edf_comp.v
View file @ 5d2ce255
......@@ -866,7 +866,7 @@ Module ResponseTimeIterationEDF.
H_all_jobs_from_taskset into ALLJOBS,
H_test_succeeds into TEST.
move => tsk INtsk j /eqP JOBtsk.
move => tsk INtsk j JOBtsk.
have RLIST := (R_list_has_response_time_bounds).
have DL := (R_list_le_deadline ts).
have HAS := (R_list_has_R_for_every_tsk ts).
......@@ -878,7 +878,7 @@ Module ResponseTimeIterationEDF.
exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -922,7 +922,7 @@ Module ResponseTimeIterationEDF.
intros j.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
apply SCHED with (tsk := job_task j); last by done.
by apply H_all_jobs_from_taskset.
Qed.
......
bertogna_edf_theory.v
View file @ 5d2ce255
......@@ -287,7 +287,7 @@ Module ResponseTimeAnalysisEDF.
| by ins; rewrite RATE
| by ins; apply TASK_PARAMS
| by ins; apply RESTR |].
red; move => j'' /eqP JOBtsk' LEdl; unfold job_misses_no_deadline.
red; move => j'' JOBtsk' LEdl; unfold job_misses_no_deadline.
assert (PARAMS' := PARAMS j''); des; rewrite PARAMS'1 JOBtsk'.
apply completion_monotonic with (t := job_arrival j'' + (R_k)); ins;
first by rewrite leq_add2l; apply NOMISS.
......@@ -345,12 +345,11 @@ Module ResponseTimeAnalysisEDF.
assert (LTserv: forall j (INi: j \in interfering_jobs),
job_interference job_cost rate sched j_i j t1 t2 <= task_cost tsk_k).
{
intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _]; rewrite -JOBj.
intros j; rewrite mem_filter; move => /andP [/andP [/eqP JOBj _] _].
specialize (PARAMS j); des.
apply leq_trans with (n := job_cost j); last by ins.
apply leq_trans with (n := service_during rate sched j t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
by apply service_interval_le_cost.
by apply cumulative_service_le_task_cost with (job_task0 := job_task) (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline).
}
(* Order the sequence of interfering jobs by arrival time, so that
......@@ -456,9 +455,8 @@ Module ResponseTimeAnalysisEDF.
move: FSTserv => /negP FSTserv; apply FSTserv.
rewrite -leqn0; apply leq_trans with (n := service_during rate sched j_fst t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
unfold service_during.
by rewrite -> sum_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply ltnW.
rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k); try (by done); apply ltnW.
}
assert (COMPok: completed job_cost rate sched j_fst (a_fst + R_k) -> job_interference job_cost rate sched j_i j_fst t1 t2 <= D_i - (D_k - R_k)).
......@@ -483,7 +481,7 @@ Module ResponseTimeAnalysisEDF.
apply leq_trans with (n := service_during rate sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service; ins; rewrite RATE.
unfold service_during.
by rewrite -> sum_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
by rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); apply leqnn.
}
{
......@@ -517,7 +515,7 @@ Module ResponseTimeAnalysisEDF.
by apply job_interference_le_service; ins; rewrite RATE.
}
unfold service_during.
rewrite -> sum_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); last by apply leqnn.
rewrite addn0; apply extend_sum; first by apply leqnn.
by rewrite leq_add2l; apply NOMISS.
......@@ -535,7 +533,7 @@ Module ResponseTimeAnalysisEDF.
by apply job_interference_le_service; ins; rewrite RATE.
}
unfold service_during.
rewrite -> sum_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
rewrite -> cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k);
try (by done); last by apply leqnn.
rewrite addn0.
apply leq_trans with (n := (\sum_(t1 <= t < a_fst + R_k) 1) +
......@@ -648,7 +646,8 @@ Module ResponseTimeAnalysisEDF.
apply/eqP; rewrite -leqn0.
apply leq_trans with (n := service_during rate sched j_lst t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
by unfold service_during; rewrite sum_service_before_arrival.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
assert (FSTok: completed job_cost rate sched j_fst (a_fst + R_k)).
......@@ -664,7 +663,8 @@ Module ResponseTimeAnalysisEDF.
move: INTERF2 => /negP INTERF2; apply INTERF2.
rewrite -leqn0; apply leq_trans with (n := service_during rate sched j_snd t1 t2);
first by apply job_interference_le_service; ins; rewrite RATE.
by unfold service_during; rewrite sum_service_before_arrival.
rewrite leqn0; apply/eqP.
by apply cumulative_service_before_job_arrival_zero.
}
apply leq_trans with (n := a_fst + p_k).
{
......@@ -819,8 +819,8 @@ Module ResponseTimeAnalysisEDF.
first by apply leq_sum; ins; apply leq_b1.
apply leq_trans with (n := service_during rate sched j_fst (a_fst + R_k) t2);
first by apply job_interference_le_service; ins; rewrite RATE.
unfold service_during.
by rewrite -> sum_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k); rewrite ?leqnn.
rewrite leqn0; apply/eqP.
by apply cumulative_service_after_job_rt_zero with (job_cost0 := job_cost) (R := R_k); rewrite ?leqnn.
}
}
......
bertogna_fp_comp.v
View file @ 5d2ce255
......@@ -677,7 +677,7 @@ Module ResponseTimeIterationFP.
H_all_jobs_from_taskset into ALLJOBS,
H_test_succeeds into TEST.
move => tsk INtsk j /eqP JOBtsk.
move => tsk INtsk j JOBtsk.
have RLIST := (R_list_has_response_time_bounds).
have NONEMPTY := (R_list_non_empty ts).
have DL := (R_list_le_deadline ts).
......@@ -687,7 +687,7 @@ Module ResponseTimeIterationFP.
exploit (RLIST rt_bounds tsk R); [by ins | by ins | by apply JOBtsk | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -732,7 +732,7 @@ Module ResponseTimeIterationFP.
intros j.
have SCHED := taskset_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
apply SCHED with (tsk := job_task j); last by done.
by apply H_all_jobs_from_taskset.
Qed.
......
bertogna_fp_jitter_comp.v
View file @ 5d2ce255
......@@ -679,7 +679,7 @@ Module ResponseTimeIterationFPWithJitter.
H_test_succeeds into TEST.
destruct H_valid_policy as [REFL [TRANS TOTAL]].
move => tsk INtsk j /eqP JOBtsk.
move => tsk INtsk j JOBtsk.
have RLIST := (R_list_has_response_time_bounds).
have NONEMPTY := (R_list_non_empty ts).
have DL := (R_list_le_deadline ts).
......@@ -689,7 +689,7 @@ Module ResponseTimeIterationFPWithJitter.
exploit (RLIST rt_bounds tsk R); [by ins | by ins | by apply JOBtsk | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -734,7 +734,7 @@ Module ResponseTimeIterationFPWithJitter.
intros j.
have SCHED := taskset_with_jitter_schedulable_by_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
apply SCHED with (tsk := job_task j); last by done.
by apply H_all_jobs_from_taskset.
Qed.
......
bertogna_fp_jitter_theory.v
View file @ 5d2ce255
......@@ -269,7 +269,7 @@ Module ResponseTimeAnalysisJitter.
| by apply RESTR
| by red; red; ins; apply (RESP tsk_k)
| by apply GE_COST |].
red; red; move => j' /eqP JOBtsk' _;
red; red; move => j' JOBtsk' _;
unfold job_misses_no_deadline.
specialize (PARAMS j'); des.
rewrite PARAMS2 JOBtsk'.
......
bertogna_fp_theory.v
View file @ 5d2ce255
......@@ -238,7 +238,7 @@ Module ResponseTimeAnalysis.
| by ins; rewrite RATE
| by ins; apply TASK_PARAMS
| by ins; apply RESTR |].
red; red; move => j' /eqP JOBtsk' _;
red; red; move => j' JOBtsk' _;
unfold job_misses_no_deadline.
specialize (PARAMS j'); des.
rewrite PARAMS1 JOBtsk'.
......
guan_fp_comp.v
View file @ 5d2ce255
......@@ -713,7 +713,7 @@ Module ResponseTimeIterationFPGuan.
H_test_succeeds into TEST.
destruct H_valid_policy as [REFL [TRANS TOTAL]].
move => tsk INtsk j /eqP JOBtsk.
move => tsk INtsk j JOBtsk.
have RLIST := (R_list_has_response_time_bounds).
have NONEMPTY := (R_list_non_empty ts).
have DL := (R_list_le_deadline ts).
......@@ -723,7 +723,7 @@ Module ResponseTimeIterationFPGuan.
exploit (RLIST rt_bounds tsk R); [by ins | by ins | by apply JOBtsk | intro COMPLETED].
exploit (DL rt_bounds tsk R); [by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply service_interval_le_cost.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service rate sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -768,7 +768,7 @@ Module ResponseTimeIterationFPGuan.
intros j.
have SCHED := taskset_schedulable_by_guan_fp_rta.
unfold no_deadline_missed_by_task, task_misses_no_deadline in *.
apply SCHED with (tsk := job_task j); last by rewrite eq_refl.
apply SCHED with (tsk := job_task j); last by done.
by apply H_all_jobs_from_taskset.
Qed.
......
workload.v
View file @ 5d2ce255
......@@ -56,15 +56,13 @@ Module Workload.
rewrite [\sum_(_ < _ | _) _]big_mkcond.
destruct num_cpus; first by rewrite 2!big_ord0 in_nil.
assert (LT0: 0 < n.+1); first by done.
rewrite (big_nth (Ordinal LT0)).
rewrite (big_nth (Ordinal LT0)).
rewrite 2!(big_nth (Ordinal LT0)).
set m := size (index_enum (ordinal_finType n.+1)).
induction m; first by rewrite big_geq // big_geq //.
{
rewrite big_nat_recr; last by done.
rewrite big_nat_recr; last by done.
rewrite mem_cat.
rewrite IHm.
rewrite mem_cat IHm.
destruct ( (j
\in make_sequence
(sched
......@@ -84,20 +82,14 @@ Module Workload.
}
{
unfold make_sequence in SUBST.
destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m ) t).
destruct (sched (nth (Ordinal LT0) (index_enum (ordinal_finType n.+1)) m ) t);
last by desf; rewrite orbF /= addn0.
{
rewrite mem_seq1 in SUBST.
destruct (Some j0 == Some j) eqn:SOME.
{
move: SOME SUBST => /eqP SOME /eqP SUBST; inversion SOME. rewrite H0 in SUBST. by done.
}
{
rewrite SOME. rewrite orbF. simpl. rewrite addn0.
ins.
}
}
{
desf. rewrite orbF /= addn0. ins.
destruct (Some j0 == Some j) eqn:SOME;
last by rewrite SOME orbF /= addn0.
move: SOME SUBST => /eqP SOME /eqP SUBST; inversion SOME.
by rewrite H0 in SUBST.
}
}
}
......
workload_guan.v
View file @ 5d2ce255
......@@ -319,7 +319,7 @@ Module WorkloadBoundGuan.
have PROP := job_properties j_i; des.
move: JOBi => /eqP JOBi; rewrite -JOBi.
apply leq_trans with (n := job_cost j_i); last by ins.
by apply service_interval_le_cost.
by apply cumulative_service_le_job_cost.
}
(* Order the sequence of interfering jobs by arrival time, so that
......@@ -388,7 +388,7 @@ Module WorkloadBoundGuan.
rewrite leq_min; apply/andP; split; last first.
{
apply leq_trans with (n := job_cost (nth elem sorted_jobs 0));
first by apply service_interval_le_cost.
first by apply cumulative_service_le_job_cost.
by rewrite -FSTtask; have PROP := job_properties (nth elem sorted_jobs 0); des.
}
{
......@@ -462,7 +462,7 @@ Module WorkloadBoundGuan.
move: LTsize => /andP [LTsize _]; des.
move: LTsize => /andP [_ SERV].
move: SERV => /eqP SERV; apply SERV.
by unfold service_during; rewrite sum_service_before_arrival.
by apply cumulative_service_before_job_arrival_zero.
}
assert (BEFOREarr: job_arrival j_fst <= job_arrival j_lst).
......@@ -543,8 +543,8 @@ Module WorkloadBoundGuan.
unfold n_k, max_jobs_NC in LTnk.
rewrite ltn_divLR in LTnk; last by done.
apply (leq_trans LTnk) in DIST.
move: INlst1 => /negP BUG; apply BUG.
unfold service_during; rewrite sum_service_before_arrival; try (by ins).
move: INlst1 => /negP BUG; apply BUG; apply/eqP.
apply cumulative_service_before_job_arrival_zero; try (by done).
unfold t2. apply leq_trans with (n := job_arrival j_fst + delta);
first by rewrite leq_add2r.
rewrite -(ltn_add2l (job_arrival j_fst)) addnBA // in DIST.
......@@ -562,7 +562,7 @@ Module WorkloadBoundGuan.
rewrite mulSn; apply leq_add.
{
apply leq_trans with (n := job_cost (nth elem sorted_jobs 0));
first by apply service_interval_le_cost.
first by apply cumulative_service_le_job_cost.
by rewrite -FSTtask; have PROP := job_properties (nth elem sorted_jobs 0); des.
}
{
......@@ -570,7 +570,7 @@ Module WorkloadBoundGuan.
rewrite big_nat_cond [\sum_(_ <= _ < _ | true)_]big_nat_cond.
apply leq_sum; intros i; rewrite andbT; move => /andP [_ LE].
apply leq_trans with (n := job_cost (nth elem sorted_jobs i.+1));
first by apply service_interval_le_cost.
first by apply cumulative_service_le_job_cost.
assert (TASKnth: job_task (nth elem sorted_jobs i.+1) = tsk).
{
exploit (mem_nth elem); last intros IN.
......@@ -585,14 +585,14 @@ Module WorkloadBoundGuan.
{
move: INlst => /eqP INlst; rewrite -INlst.
apply leq_trans with (n := job_cost j_lst);
first by apply service_interval_le_cost.
first by apply cumulative_service_le_job_cost.
by have PROP := job_properties j_lst; des.
}
{
unfold service_during.
rewrite -> big_cat_nat with (n := job_arrival j_lst); simpl;
try (by ins); last by apply ltnW.
rewrite sum_service_before_arrival ?leqnn // add0n.
rewrite cumulative_service_before_job_arrival_zero ?leqnn // add0n.
apply leq_trans with (n := \sum_(job_arrival j_lst <= i < t2) 1).
apply leq_sum; first by ins; apply service_at_le_max_rate.
rewrite big_const_nat iter_addn mul1n addn0.
......@@ -690,7 +690,7 @@ Module WorkloadBoundGuan.
have PROP := job_properties j_i; des.
move: JOBi => /eqP JOBi; rewrite -JOBi.
apply leq_trans with (n := job_cost j_i); last by ins.
by apply service_interval_le_cost.
by apply cumulative_service_le_job_cost.
}
(* Order the sequence of interfering jobs by arrival time, so that
......@@ -794,7 +794,7 @@ Module WorkloadBoundGuan.
{
rewrite leqNgt; apply /negP; unfold not; intro LTt1.
move: FSTserv => /eqP FSTserv; apply FSTserv.
apply (sum_service_after_job_rt_zero job_cost) with (R := R_tsk);
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
try (by ins); last by apply ltnW.
apply H_response_time_bound; first by apply/eqP.
by apply leq_trans with (n := t1); last by apply leq_addr.
......@@ -838,7 +838,7 @@ Module WorkloadBoundGuan.
{
rewrite leqNgt; apply/negP; unfold not; intro LT2.
move: LSTserv => /eqP LSTserv; apply LSTserv.
by unfold service_during; rewrite sum_service_before_arrival.
by apply cumulative_service_before_job_arrival_zero.
}
assert (BEFOREarr: job_arrival j_fst <= job_arrival j_lst).
......@@ -1038,10 +1038,3 @@ Module WorkloadBoundGuan.
End WorkloadBoundGuan.
\ No newline at end of file
workload_jitter.v
View file @ 5d2ce255
......@@ -255,12 +255,9 @@ Module WorkloadWithJitter.
assert (LTserv: forall j_i (INi: j_i \in interfering_jobs),
service_during rate sched j_i t1 t2 <= task_cost tsk).
{
ins; move: INi; rewrite mem_filter; move => /andP xxx; des.
move: xxx; move => /andP JOBi; des; clear xxx0 JOBi0.
have PROP := job_properties j_i; des.
move: JOBi => /eqP JOBi; rewrite -JOBi.
apply leq_trans with (n := job_cost j_i); last by ins.
by apply service_interval_le_cost.
ins; apply cumulative_service_le_task_cost with (task_deadline0 := task_deadline) (job_cost0 := job_cost) (job_deadline0 := job_deadline) (job_task0 := job_task); try (by done);
last by apply job_properties.
by move: INi; rewrite mem_filter; move => /andP [/andP [/eqP JOBtsk _] _].
}
(* Order the sequence of interfering jobs by arrival time, so that
......@@ -335,7 +332,7 @@ Module WorkloadWithJitter.
rewrite leq_min; apply/andP; split.
{
apply leq_trans with (n := job_cost (nth elem sorted_jobs 0));
first by apply service_interval_le_cost.
first by apply cumulative_service_le_job_cost.
by rewrite -FSTtask; have PROP := job_properties (nth elem sorted_jobs 0); des.
}
{
......@@ -356,16 +353,12 @@ Module WorkloadWithJitter.
set j_lst := (nth elem sorted_jobs n.+1).
(* Now we infer some facts about how first and last are ordered in the timeline *)
assert (INfst: j_fst \in interfering_jobs).
by unfold j_fst; rewrite INboth; apply mem_nth; destruct sorted_jobs; ins.
move: INfst; rewrite mem_filter; move => /andP INfst; des.
move: INfst => /andP INfst; des.
assert (AFTERt1: t1 <= job_arrival j_fst + R_tsk).
{
rewrite leqNgt; apply /negP; unfold not; intro LTt1.
move: INfst1 => /eqP INfst1; apply INfst1.
apply (sum_service_after_job_rt_zero job_cost) with (R := R_tsk);
move: FSTserv => /eqP FSTserv; apply FSTserv.
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
try (by ins); last by apply ltnW.
by apply response_time_bound.
}
......@@ -380,7 +373,7 @@ Module WorkloadWithJitter.
move: LTsize => /andP [LTsize _]; des.
move: LTsize => /andP [_ SERV].
move: SERV => /eqP SERV; apply SERV.
unfold service_during; rewrite sum_service_before_arrival; try (by ins).
apply cumulative_service_before_job_arrival_zero; try (by ins).
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
}
......@@ -405,7 +398,7 @@ Module WorkloadWithJitter.
rewrite -> big_cat_nat with (n := job_arrival j_fst + R_tsk); [| by ins | by ins].
rewrite -{2}[\sum_(_ <= _ < _) _]addn0 /=.
rewrite leq_add2l leqn0; apply/eqP.
apply (sum_service_after_job_rt_zero job_cost) with (R := R_tsk);
apply (cumulative_service_after_job_rt_zero job_cost) with (R := R_tsk);
try (by ins); last by apply leqnn.
by apply response_time_bound.
}
......@@ -425,8 +418,9 @@ Module WorkloadWithJitter.
rewrite -> big_cat_nat with (n := job_arrival j_lst); [|by apply ltnW| by apply ltnW].
rewrite /= -[\sum_(_ <= _ < _) 1]add0n; apply leq_add.
{
rewrite sum_service_before_arrival; [by ins| |by apply leqnn].
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
rewrite cumulative_service_before_job_arrival_zero;
[by ins| |by apply leqnn].
by apply arrival_before_jitter with (job_jitter0 := job_jitter).
}
by apply leq_sum; ins; apply service_at_le_max_rate.
}
......@@ -476,7 +470,7 @@ Module WorkloadWithJitter.
set cur := nth elem sorted_jobs i.
set next := nth elem sorted_jobs i.+1.
clear BOUNDend BOUNDmid LT LTserv j_fst j_lst
INfst INfst0 INfst1 AFTERt1 BEFOREt2 FSTserv FSTtask FSTin.
AFTERt1 BEFOREt2 FSTserv FSTtask FSTin.
(* Show that cur arrives earlier than next *)
assert (ARRle: job_arrival cur <= job_arrival next).
......@@ -541,7 +535,7 @@ Module WorkloadWithJitter.
(* Show that j_fst doesn't execute d_k units after its arrival. *)
unfold t2; rewrite leq_add2r; rename H_completed_jobs_dont_execute into EXEC.
unfold task_misses_no_deadline_before, job_misses_no_deadline, completed in *; des.
exploit (no_dl_misses j_fst INfst); last intros COMP.
exploit (no_dl_misses j_fst FSTtask); last intros COMP.
{
(* Prove that arr_fst + d_k <= t2 *)
apply leq_ltn_trans with (n := job_arrival j_lst); last by done.
......@@ -557,7 +551,7 @@ Module WorkloadWithJitter.
equals 0, which contradicts the previous assumption that j_fst interferes in
the scheduling window. *)
clear BEFOREt2 DISTmax LTnk DIST BOUNDend BOUNDmid FSTin; move: EXEC => EXEC.
move: INfst1 => /eqP SERVnonzero; apply SERVnonzero.
move: FSTserv => /eqP SERVnonzero; apply SERVnonzero.
{
unfold service_during; apply/eqP; rewrite -leqn0.
rewrite <- leq_add2l with (p := job_cost j_fst); rewrite addn0.
......
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