Commit 0c922d98 authored by Sergey Bozhko's avatar Sergey Bozhko

Change definition of completion

parent 09703078
......@@ -972,8 +972,6 @@ Module ResponseTimeIterationEDF.
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -981,8 +979,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
by done.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -246,12 +246,7 @@ Module ResponseTimeAnalysisEDF.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -357,7 +352,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done.
apply completion_monotonic with (t0 := job_arrival j0 + R0).
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS | by apply CONSTR; rewrite FROMTS].
......@@ -976,7 +971,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' ->
service sched j0 (job_arrival j0 + R0) == job_cost j0).
service sched j0 (job_arrival j0 + R0) >= job_cost j0).
{
by ins; apply IH with (tsk := tsk0) (R := R0).
}
......
......@@ -696,7 +696,6 @@ Module ResponseTimeIterationFP.
} des.
exploit (RLIST tsk R EX j ARRj); [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 cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -704,8 +703,7 @@ Module ResponseTimeIterationFP.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
by done.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -258,12 +258,7 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite [R]REC // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -369,14 +364,10 @@ Module ResponseTimeAnalysisFP.
intros j0 ARR0 INTERF.
exploit (HAS (job_task j0));
[by rewrite FROMTS | by done | move => [R0 INbounds]].
apply completion_monotonic with (t := job_arrival j0 + R0); first by done.
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
apply completion_monotonic with (t := job_arrival j0 + R0).
- rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS' | by apply CONSTR; rewrite FROMTS].
}
{
by apply (RESP (job_task j0)).
}
- by apply (RESP (job_task j0)).
Qed.
(* 3) Next, we prove that the sum of the interference of each task is equal to the
......@@ -656,8 +647,7 @@ Module ResponseTimeAnalysisFP.
}
{
intros j0 JOB0 ARR0 LT0.
apply completion_monotonic with (t0 := job_arrival j0 + R);
[by done | | by apply BEFOREok].
apply completion_monotonic with (t0 := job_arrival j0 + R); [| by apply BEFOREok].
by rewrite leq_add2l; apply leq_trans with (n := task_deadline tsk);
last by apply CONSTR; rewrite -JOBtsk FROMTS.
}
......@@ -1028,7 +1018,7 @@ Module ResponseTimeAnalysisFP.
arrives_in arr_seq j0 ->
job_task j0 = tsk ->
job_arrival j0 < job_arrival j ->
service sched j0 (job_arrival j0 + R) == job_cost j0).
service sched j0 (job_arrival j0 + R) >= job_cost j0).
{
by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH.
......
......@@ -960,8 +960,6 @@ Module ResponseTimeIterationEDF.
exploit (HAS rt_bounds tsk); [by ins | by ins | clear HAS; intro HAS; des].
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R); try (by done); clear DL; intro DL.
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -969,8 +967,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
by done.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -234,12 +234,7 @@ Module ResponseTimeAnalysisEDF.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -345,7 +340,7 @@ Module ResponseTimeAnalysisEDF.
intros t j0 ARR0 LEt LE.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 + R0); first by done.
apply completion_monotonic with (t0 := job_arrival j0 + R0).
{
rewrite leq_add2l; apply leq_trans with (n := task_deadline (job_task j0));
[by apply NOMISS | by apply CONSTR; rewrite FROMTS].
......@@ -774,7 +769,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' ->
service sched j0 (job_arrival j0 + R0) == job_cost j0).
service sched j0 (job_arrival j0 + R0) >= job_cost j0).
{
by ins; apply IH with (tsk := tsk0) (R := R0).
}
......
......@@ -679,16 +679,11 @@ Module ResponseTimeIterationFP.
} des.
exploit (RLIST tsk R EX j ARRj); [by done | 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 cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
apply leq_trans with (n := service sched j (job_arrival j + R)); first by done.
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
apply extend_sum; rewrite // leq_add2l.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -242,12 +242,7 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite [R](REC) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -761,7 +756,7 @@ Module ResponseTimeAnalysisFP.
arrives_in arr_seq j0 ->
job_task j0 = tsk ->
job_arrival j0 < job_arrival j ->
service sched j0 (job_arrival j0 + R) == job_cost j0).
service sched j0 (job_arrival j0 + R) >= job_cost j0).
{
by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH.
......
......@@ -1054,8 +1054,6 @@ Module ResponseTimeIterationEDF.
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + task_jitter tsk + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -1063,8 +1061,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS2.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by rewrite -addnA; apply COMPLETED.
by rewrite -addnA.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -250,12 +250,7 @@ Module ResponseTimeAnalysisEDFJitter.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(t1 <= t < t1 + R)
backlogged job_arrival job_cost job_jitter sched j t) +
service sched j (t1 + R)); last first.
......@@ -384,8 +379,7 @@ Module ResponseTimeAnalysisEDFJitter.
intros t j0 LEt ARR0 LE.
cut ((job_task j0) \in unzip1 rt_bounds = true); last by rewrite UNZIP FROMTS.
move => /mapP [p IN EQ]; destruct p as [tsk' R0]; simpl in *; subst tsk'.
apply completion_monotonic with (t0 := job_arrival j0 +
task_jitter (job_task j0) + R0); first by done.
apply completion_monotonic with (t0 := job_arrival j0 + task_jitter (job_task j0) + R0).
{
rewrite -addnA leq_add2l.
apply leq_trans with (n := task_deadline (job_task j0));
......@@ -820,7 +814,7 @@ Module ResponseTimeAnalysisEDFJitter.
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + task_jitter tsk + R0 < job_arrival j + task_jitter tsk' + R' ->
service sched j0 (job_arrival j0 + task_jitter tsk + R0) == job_cost j0).
service sched j0 (job_arrival j0 + task_jitter tsk + R0) >= job_cost j0).
{
by ins; apply IH with (tsk := tsk0) (R := R0).
}
......
......@@ -695,8 +695,6 @@ Module ResponseTimeIterationFP.
} des.
exploit (RLIST tsk R); [by done | by apply ARRj | by done | 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 cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + (task_jitter tsk + R)));
last first.
{
......@@ -704,7 +702,6 @@ Module ResponseTimeIterationFP.
apply extend_sum; rewrite // leq_add2l.
by specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS2 JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
Qed.
......
......@@ -255,12 +255,8 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite [R](REC) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(t1 <= t < t1 + R)
backlogged job_arrival job_cost job_jitter sched j t) +
service sched j (t1 + R)); last first.
......@@ -806,7 +802,7 @@ Module ResponseTimeAnalysisFP.
(* Now we start the proof. Assume by contradiction that job j
is not complete at time (job_arrival j + job_jitter j + R'). *)
rewrite addnA.
apply completion_monotonic with (t := job_arrival j + job_jitter j + R); first by done.
apply completion_monotonic with (t := job_arrival j + job_jitter j + R).
{
rewrite leq_add2r leq_add2l.
specialize (PARAMS j ARRj); des.
......
......@@ -955,8 +955,6 @@ Module ResponseTimeIterationEDF.
have COMPLETED := RLIST tsk R HAS j ARRj JOBtsk.
exploit (DL rt_bounds tsk R);
[by ins | by ins | clear DL; intro DL].
rewrite eqn_leq; apply/andP; split; first by apply cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -964,8 +962,7 @@ Module ResponseTimeIterationEDF.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
by done.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -234,12 +234,7 @@ Module ResponseTimeAnalysisEDF.
rewrite subh1; last by rewrite [R](REC tsk) // leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -461,7 +456,7 @@ Module ResponseTimeAnalysisEDF.
job_task j0 = tsk ->
(tsk, R0) \in rt_bounds ->
job_arrival j0 + R0 < job_arrival j + R' ->
service sched j0 (job_arrival j0 + R0) == job_cost j0).
service sched j0 (job_arrival j0 + R0) >= job_cost j0).
{
by ins; apply IH with (tsk := tsk0) (R := R0).
}
......
......@@ -659,7 +659,6 @@ Module ResponseTimeIterationFP.
} des.
exploit (RLIST tsk R); eauto 1; 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 cumulative_service_le_job_cost.
apply leq_trans with (n := service sched j (job_arrival j + R)); last first.
{
unfold valid_sporadic_taskset, is_valid_sporadic_task in *.
......@@ -667,8 +666,7 @@ Module ResponseTimeIterationFP.
specialize (JOBPARAMS j ARRj); des; rewrite JOBPARAMS1.
by rewrite JOBtsk.
}
rewrite leq_eqVlt; apply/orP; left; rewrite eq_sym.
by apply COMPLETED.
by done.
Qed.
(* For completeness, since all jobs of the arrival sequence
......
......@@ -228,12 +228,7 @@ Module ResponseTimeAnalysisFP.
rewrite subh1; last by rewrite REC leq_addr.
rewrite -addnBA // subnn addn0.
move: (NOTCOMP) => /negP NOTCOMP'.
rewrite neq_ltn in NOTCOMP.
move: NOTCOMP => /orP [LT | BUG]; last first.
{
exfalso; rewrite ltnNge in BUG; move: BUG => /negP BUG; apply BUG.
by apply cumulative_service_le_job_cost.
}
rewrite -ltnNge in NOTCOMP.
apply leq_ltn_trans with (n := (\sum_(job_arrival j <= t < job_arrival j + R)
backlogged job_arrival job_cost sched j t) +
service sched j (job_arrival j + R)); last first.
......@@ -448,7 +443,7 @@ Module ResponseTimeAnalysisFP.
arrives_in arr_seq j0 ->
job_task j0 = tsk ->
job_arrival j0 < job_arrival j ->
service sched j0 (job_arrival j0 + R) == job_cost j0).
service sched j0 (job_arrival j0 + R) >= job_cost j0).
{
by ins; apply IH; try (by done); rewrite ltn_add2r.
} clear IH.
......
......@@ -99,10 +99,7 @@ Module ResponseTimeAnalysisFP.
rename H_response_time_is_fixed_point into FIX.
intros j ARRj JOBtsk.
move: (posnP (job_cost j)) => [Z|POS].
{ rewrite /is_response_time_bound_of_job /completed_by eqn_leq; apply/andP; split.
- by apply H_completed_jobs_dont_execute.
- by rewrite Z.
}
{ by rewrite /is_response_time_bound_of_job /completed_by Z. }
set prio := FP_to_JLFP job_task higher_eq_priority.
apply busy_interval_bounds_response_time with
(arr_seq0 := arr_seq)
......@@ -115,8 +112,8 @@ Module ResponseTimeAnalysisFP.
destruct (sched t) eqn:SCHED; last by done.
have HP := pending_hp_job_exists
job_arrival job_cost arr_seq _ sched
prio _ ARRj _ _ _ _ _ _ BUSY _ NEQ.
feed_n 5 HP; try done.
prio _ ARRj _ _ _ _ _ BUSY _ NEQ.
feed_n 4 HP; try done.
{ by intros x; apply H_priority_is_reflexive. }
move: HP => [jhp [ARRjhp [PEND PRIO]]].
apply/eqP; rewrite eqb0 Bool.negb_involutive.
......
......@@ -187,7 +187,7 @@ Module ResponseTimeAnalysisTDMA.
Theorem uniprocessor_response_time_bound_TDMA: response_time_bounded_by tsk BOUND.
Proof.
intros j arr_seq_j JobTsk.
apply completion_monotonic with (t:=job_arrival j + RT j);first exact.
apply completion_monotonic with (t:=job_arrival j + RT j); try done.
- rewrite leq_add2l /BOUND.
apply (response_time_le_WCRT)
with (task_cost0:=task_cost) (task_deadline0:=task_deadline)(sched0:=sched)
......
......@@ -186,8 +186,8 @@ Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Sche
- rewrite /has_arrived. auto.
- rewrite /completed_by /service /service_during.
rewrite ->cumulative_service_before_job_arrival_zero
with (job_arrival0:=job_arrival). rewrite neq_ltn. apply /orP.
left. apply H_valid_job. apply H_jobs_must_arrive_to_execute. auto.
with (job_arrival0:=job_arrival). rewrite -ltnNge.
apply H_valid_job. apply H_jobs_must_arrive_to_execute. auto.
Qed.
(* Job is pending at t.+1 if
......
......@@ -244,10 +244,9 @@ Module JitterScheduleProperties.
rewrite sched_jitter_uses_construction_function /reduction.build_schedule
-/hp_job_other_than_j.
destruct (hp_job_other_than_j t) as [j_hp|] eqn:HP; last first.
{
case PENDj: pending; last by done.
{ case PENDj: pending; last by done.
apply/eqP; case => SAME; subst j0; move: PENDj => /andP [_ NOTCOMPj].
by rewrite /completed_by EQ eq_refl in NOTCOMPj.
by rewrite /completed_by EQ leqnn in NOTCOMPj.
}
rewrite /hp_job_other_than_j /reduction.highest_priority_job_other_than_j in HP.
apply seq_min_in_seq in HP; rewrite mem_filter /pending /completed_by in HP.
......@@ -256,12 +255,12 @@ Module JitterScheduleProperties.
{
move: PENDj => /andP [_ NOTCOMPj].
case: (~~ higher_eq_priority _ _); apply/eqP; case => SAME; subst j0;
first by rewrite /completed_by EQ eq_refl in NOTCOMPj.
by rewrite EQ eq_refl in NOTCOMPhp.
first by rewrite /completed_by EQ leqnn in NOTCOMPj.
by rewrite EQ leqnn in NOTCOMPhp.
}
{
apply/eqP; case => SAME; subst j0.
by rewrite EQ eq_refl in NOTCOMPhp.
by rewrite EQ leqnn in NOTCOMPhp.
}
Qed.
......
......@@ -257,11 +257,9 @@ Module JitterScheduleService.
by apply actual_arrivals_between_sub with (t3 := 0) (t4 := t).
}
apply leq_sum_seq; rewrite /act /actual_arrivals; intros j0 IN0 HP0.
apply eq_leq; symmetry; apply/eqP.
have ARRin: arrives_in arr_seq j0.
by apply in_actual_arrivals_between_implies_arrived in IN0.
apply in_actual_arrivals_implies_arrived_before in IN0.
by apply WORK.
apply WORK; try done.
- by apply in_actual_arrivals_between_implies_arrived in IN0.
- by apply in_actual_arrivals_implies_arrived_before in IN0.
Qed.
End ServiceEqualsWorkload.
......@@ -378,9 +376,7 @@ Module JitterScheduleService.
}
rewrite /inflated_job_cost /reduction.inflated_job_cost.
apply negbTE in NEQ; rewrite NEQ.
apply eq_leq; symmetry; apply/eqP.
apply completion_monotonic with (t := arr_hp + job_deadline j_hp);
[by done | | by apply NOMISS].
apply completion_monotonic with (t := arr_hp + job_deadline j_hp); last by apply NOMISS.
rewrite H_job_deadlines_equal_task_deadlines //.
apply leq_trans with (n := arr_hp + task_period (job_task j_hp));
first by rewrite leq_add2l DL // FROM.
......@@ -458,7 +454,7 @@ Module JitterScheduleService.
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
last by apply extend_sum.
apply leq_trans with (n := cost_hp);
last by apply eq_leq; symmetry; apply/eqP; apply RESPhp; last by apply/andP; split.
last by apply RESPhp; last by apply/andP; split.
apply leq_trans with (n := inflated_job_cost j_hp);
last by rewrite /inflated_job_cost /reduction.inflated_job_cost -[_==_]negbK NEQ.
apply cumulative_service_le_job_cost.
......@@ -507,7 +503,7 @@ Module JitterScheduleService.
{
rewrite /cost_hp leq_subLR.
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
first by apply eq_leq;symmetry;apply/eqP; apply RESPhp; last by apply/andP; split.
first by apply RESPhp; last by apply/andP; split.
rewrite /service /service_during.
apply leq_trans with (n := \sum_(arr_j <= t' < arr_hp+Rhp)
1 + service sched_susp j_hp arr_j);
......@@ -527,7 +523,7 @@ Module JitterScheduleService.
have LEcost: cost_hp <= Rhp.
{
apply leq_trans with (n := service sched_susp j_hp (arr_hp + Rhp));
first by apply eq_leq;symmetry;apply/eqP;apply RESPhp; last by apply/andP;split.
first by apply RESPhp; last by apply/andP;split.
apply leq_trans with (n := \sum_(arr_hp <= t' < arr_hp + Rhp) 1);
last by simpl_sum_const; rewrite addKn.
rewrite /service /service_during.
......@@ -871,8 +867,7 @@ Module JitterScheduleService.
feed (EQWORKj (t1 + d).+1); first by rewrite ltn_add2l.
apply EQWORKj.
intros j0 ARRin0 ARR0 HEP0; specialize (ALL j0 ARRin0 HEP0 ARR0).
by apply completion_monotonic with (t := t1 + d);
first by apply reduction_prop.sched_jitter_completed_jobs_dont_execute.
by apply completion_monotonic with (t := t1 + d).
Qed.
(* By combining each inequality above in sequence, we complete the induction
......@@ -1231,33 +1226,30 @@ Module JitterScheduleService.
is also bounded by R_j. *)
Corollary jitter_reduction_job_j_completes_no_later:
job_response_time_in_sched_susp_bounded_by j R_j.
Proof.
Proof.
move: (H_valid_schedule) => [_ [MUSTARRs [COMPs [WORK [PRIO SELF]]]]].
rename H_response_time_of_j_in_sched_jitter into COMPj.
apply contraT; intro NOTCOMPs.
suff NOTCOMPj: ~~ job_response_time_in_sched_jitter_bounded_by j R_j;
[by rewrite COMPj in NOTCOMPj | clear