Library prosa.classic.model.schedule.uni.susp.suspension_intervals
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module SuspensionIntervals.
Export Job UniprocessorSchedule Suspension LastExecution.
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable next_suspension: job_suspension Job.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section JobSuspension.
Variable j: Job.
Section DefiningSuspension.
Variable t: time.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let current_service := service sched j suspension_start.
Definition suspension_duration := next_suspension j current_service.
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
Section SuspensionAwareSchedule.
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
Section Lemmas.
Section InsideSuspensionInterval.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
Section SameService.
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
Proof.
rename H_within_suspension_interval into BETWEEN,
H_respects_self_suspensions into SUSP, t_in into i.
generalize dependent i.
suff SAME:
∀ delta,
delta ≤ duration →
service sched j (suspension_start + delta) =
service sched j suspension_start.
{
move ⇒ i /andP [GE LT].
feed (SAME (i-suspension_start)); first by rewrite leq_subLR.
by rewrite addnBA // addKn in SAME.
}
induction delta; first by rewrite addn0.
intros LT.
feed IHdelta; first by apply ltnW.
rewrite addnS -[service _ _ suspension_start]addn0.
rewrite /service /service_during big_nat_recr //=.
f_equal; first by done.
apply/eqP; rewrite eqb0; apply/negP; intro SCHED.
move: (SCHED) ⇒ SCHED'.
apply SUSP in SCHED; apply SCHED; clear SCHED.
rewrite /suspended_at /suspension_duration.
case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
first by apply completed_implies_not_scheduled in COMP;
first by rewrite SCHED' in COMP.
rewrite andTb (same_service_implies_same_last_execution _ _ _ _
suspension_start) //.
rewrite /suspension_start last_execution_idempotent //.
apply/andP; split; first by apply leq_addr.
by rewrite ltn_add2l.
Qed.
End SameService.
Section JobSuspendedAtAllTimes.
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
Proof.
rename H_within_suspension_interval into BETWEEN.
move: BETWEEN ⇒ /andP [GE LT].
have ARR: has_arrived job_arrival j t_in.
{
apply leq_trans with (n := suspension_start); last by done.
rewrite -/(has_arrived job_arrival j suspension_start).
by apply last_execution_after_arrival.
}
apply/andP; split; first by done.
apply/andP; split;
first by apply last_execution_bounded_by_identity.
apply (leq_trans LT).
have SAME: time_after_last_execution job_arrival sched j t =
time_after_last_execution job_arrival sched j t_in.
{
set b := _ _ t.
rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ _ _ b);
first by rewrite last_execution_idempotent.
apply same_service_in_suspension_interval.
by apply/andP; split; last by apply ltnW.
}
rewrite /suspension_start SAME leq_add2l.
by rewrite /duration /suspension_duration SAME.
Qed.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
Section StateOfSuspendedJob.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
Proof.
rename H_j_is_suspended into SUSP.
move: SUSP ⇒ /andP [_ SUSP].
rewrite -[_ && _]negbK in SUSP; move: SUSP ⇒ /negP SUSP.
rewrite /has_arrived leqNgt; apply/negP; intro LT.
apply SUSP; clear SUSP.
rewrite negb_and; apply/orP; left.
rewrite -ltnNge.
apply: (leq_trans LT); clear LT.
rewrite /time_after_last_execution.
case EX: [∃ _, _]; last by apply leqnn.
set t' := \max_(_ < _ | _)_.
move: EX ⇒ /existsP [t0 EX].
apply bigmax_pred in EX; rewrite -/t' /job_scheduled_at in EX.
apply leq_trans with (n := t'); last by apply leq_addr.
rewrite leqNgt; apply/negP; intro LT.
have NOTSCHED: ~~ scheduled_at sched j t'.
{
rewrite -eqb0; apply/eqP.
by eapply service_before_job_arrival_zero; first by eauto.
}
by rewrite EX in NOTSCHED.
Qed.
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
Proof.
by move: H_j_is_suspended ⇒ /andP [NOTCOMP _].
Qed.
End StateOfSuspendedJob.
Section BoundOnCumulativeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
Proof.
unfold cumulative_suspension_of_j, cumulative_suspension_during,
total_suspension_of_j, total_suspension.
intros t1 t2.
apply leq_trans with (n := \sum_(0 ≤ s < job_cost j)
\sum_(t1 ≤ t < t2 | service sched j t == s) suspended_at j t).
{ rewrite (exchange_big_dep_nat (fun x ⇒ true)) //=.
apply leq_sum; intros s _.
destruct (boolP (suspended_at j s)) as [SUSP | NOTSUSP]; last by done.
rewrite (big_rem (service sched j s)); first by rewrite eq_refl.
rewrite mem_index_iota; apply/andP; split; first by done.
rewrite ltn_neqAle; apply/andP; split;
last by apply cumulative_service_le_job_cost.
apply suspended_implies_not_completed in SUSP.
rewrite neq_ltn; apply/orP; left.
by rewrite ltnNge.
}
{ apply leq_sum_nat; move ⇒ s /andP [_ LT] _.
destruct (boolP [∃ t:'I_t2, (t≥t1)&& (service sched j t==s)]) as [EX|ALL];
last first.
{
rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
rewrite big_nat_cond big1 //.
move ⇒ i /andP [/andP [GEi LTi] SERV].
by specialize (ALL (Ordinal LTi)); rewrite /= SERV GEi andbT in ALL.
}
move: EX ⇒ /existsP [t' /andP [GE' /eqP SERV]].
unfold suspended_at, suspension_duration.
set b := time_after_last_execution job_arrival sched j.
set n := next_suspension j s.
apply leq_trans with (n := \sum_(t1 ≤ t < t2 | b t' ≤ t < b t' + n) 1).
{
rewrite big_mkcond [\sum_(_ ≤ _ < _ | b t' ≤ _ < _) _]big_mkcond /=.
apply leq_sum_nat; intros t LEt _.
case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
[by case (_ == _) | simpl].
case EQ: (service _ _ _ == _); last by done.
move: EQ ⇒ /eqP EQ. rewrite /n -EQ.
case INT: (_ ≤ _ < _); last by done.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
move: INT ⇒ /andP [GEt LTt].
rewrite (same_service_in_suspension_interval _ _ _ _ t') //.
{
rewrite -/b [b t'](same_service_implies_same_last_execution _ _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split.
}
{
rewrite /suspension_duration -/b.
rewrite [b t'](same_service_implies_same_last_execution _ _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split; last by apply ltnW.
}
}
apply leq_trans with (n := \sum_(b t' ≤ t < b t' + n) 1);
last by simpl_sum_const; rewrite addKn.
by apply leq_sum1_smaller_range; move ⇒ i [LE LE']; split.
}
Qed.
End BoundOnCumulativeSuspension.
Section SuspendsForTotalSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
Proof.
rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
have EARLIER := exists_last_execution_with_smaller_service job_arrival
job_cost sched ARR j t COMP.
apply/eqP; rewrite eqn_leq; apply/andP; split;
first by apply cumulative_suspension_le_total_suspension.
rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
move: COMP ⇒ /eqP COMP.
apply leq_trans with (n := \sum_(0 ≤ s < job_cost j)
\sum_(0 ≤ t0 < t | service sched j t0 == s) suspended_at j t0);
last first.
{
rewrite (exchange_big_dep_nat (fun x ⇒ true)) //=.
apply leq_sum_nat; move ⇒ t0 /andP [_ LT] _.
case (boolP [∃ s: 'I_(job_cost j), service sched j t0 == s]) ⇒ [EX | ALL].
{
move: EX ⇒ /existsP [s /eqP EQs].
rewrite big_mkcond /=.
rewrite (bigD1_seq (nat_of_ord s)); [simpl | | by apply iota_uniq];
last by rewrite mem_index_iota; apply/andP;split; last by apply ltn_ord.
rewrite EQs eq_refl big1; first by rewrite addn0.
by move ⇒ i /negbTE NEQ; rewrite eq_sym NEQ.
}
{
rewrite big_nat_cond big1; first by done.
move ⇒ i /andP [/andP [_ LTi] /eqP SERV].
rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
by specialize (ALL (Ordinal LTi)); rewrite /= SERV eq_refl in ALL.
}
}
{
apply leq_sum_nat; move ⇒ s /andP [_ LTs] _.
rewrite /suspended_at /suspension_duration.
set b := time_after_last_execution job_arrival sched j.
set n := next_suspension j.
move: (EARLIER s LTs) ⇒ [t' EQ'].
apply leq_trans with (n := \sum_(0 ≤ t0 < t | (service sched j t0 == s) &&
(b t' ≤ t0 < b t' + n (service sched j (b t')))) 1); last first.
{ rewrite big_mkcond [\sum_(_ ≤ _ < _ | _ == s)_]big_mkcond.
apply leq_sum_nat; move ⇒ i /andP [_ LTi] _.
case EQi: (service sched j i == s); [rewrite andTb | by rewrite andFb].
case LE: (_ ≤ _ ≤ _); last by done.
rewrite lt0n eqb0 negbK.
apply suspended_in_suspension_interval with (t := t'); try (by done).
rewrite -ltnNge.
by apply: (leq_ltn_trans _ LTs); apply eq_leq; apply/eqP.
}
{ apply leq_trans with (n := \sum_(b t'≤ t0< b t'+ n (service sched j (b t')) |
(0 ≤ t0 < t) && (service sched j t0 == s)) 1).
{
apply leq_trans with (n := \sum_(b t' ≤ t0 < b t'
+ n (service sched j (b t'))) 1);
first by simpl_sum_const; rewrite addKn -EQ'.
rewrite [in X in _ ≤ X]big_mkcond /=.
apply leq_sum_nat; move ⇒ i /andP [LEi GTi] _.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
apply/andP; split.
{
have SUSPi: suspended_at j i.
{
apply: (suspended_in_suspension_interval _ _ _ _ t');
try (by done); last by apply/andP; split.
rewrite -ltnNge.
rewrite (same_service_in_suspension_interval _ _ _ _ t') //;
first by rewrite EQ'.
by apply/andP; split; last by apply ltnW.
}
apply contraT; rewrite -leqNgt; intro LE.
apply suspended_implies_not_completed in SUSPi.
exfalso; move: SUSPi ⇒ /negP COMPi; apply COMPi.
try ( apply completion_monotonic with (t0 := t); try (by done) ) ||
apply completion_monotonic with (t := t); try (by done).
by apply/eqP.
}
{
rewrite -EQ'; apply/eqP.
apply same_service_in_suspension_interval; try (by done).
by apply/andP; split; last by apply ltnW.
}
}
{
apply leq_sum1_smaller_range.
by move ⇒ i [LEb /andP [LE EQs]]; split;
last by apply/andP; split.
}
}
}
Qed.
End SuspendsForTotalSuspension.
Section ExecutionBeforeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
Lemma executes_before_suspension:
scheduled_at sched j t.
Proof.
rename H_not_suspended_at_t into NOTSUSPs, H_begins_suspension into SUSPs'.
move: SUSPs' ⇒ /andP [NOTCOMP' /andP [GE LT]].
apply contraT; intro NOTSCHED.
suff BUG: suspended_at j t by rewrite BUG in NOTSUSPs.
apply suspended_in_suspension_interval with (t := t.+1); try done.
{
apply contraT; rewrite negbK; intro COMP.
suff COMP': completed_by job_cost sched j t.+1 by rewrite COMP' in NOTCOMP'.
try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
}
apply/andP; split; last by apply: (leq_ltn_trans _ LT).
apply leq_trans with (n := time_after_last_execution job_arrival sched j t);
last by apply last_execution_bounded_by_identity.
apply eq_leq, same_service_implies_same_last_execution.
rewrite /service /service_during big_nat_recr //= /service_at.
by apply negbTE in NOTSCHED; rewrite NOTSCHED addn0.
Qed.
End ExecutionBeforeSuspension.
End Lemmas.
End DefiningSuspensionIntervals.
End SuspensionIntervals.
Require Import prosa.classic.model.suspension.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
Require Import prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.susp.last_execution.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module SuspensionIntervals.
Export Job UniprocessorSchedule Suspension LastExecution.
Section DefiningSuspensionIntervals.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable next_suspension: job_suspension Job.
Variable sched: schedule Job.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Section JobSuspension.
Variable j: Job.
Section DefiningSuspension.
Variable t: time.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let current_service := service sched j suspension_start.
Definition suspension_duration := next_suspension j current_service.
Definition suspended_at :=
~~ completed_by job_cost sched j t &&
(suspension_start ≤ t < suspension_start + suspension_duration).
End DefiningSuspension.
Definition cumulative_suspension_during (t1 t2: time) :=
\sum_(t1 ≤ t < t2) (suspended_at t).
Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.
End JobSuspension.
Section SuspensionAwareSchedule.
Definition respects_self_suspensions :=
∀ j t,
job_scheduled_at j t → ¬ suspended_at j t.
End SuspensionAwareSchedule.
Section Lemmas.
Section InsideSuspensionInterval.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_has_arrived: has_arrived job_arrival j t.
Let suspension_start := time_after_last_execution job_arrival sched j t.
Let duration := suspension_duration j t.
Section SameService.
Variable t_in: time.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in ≤ suspension_start + duration.
Lemma same_service_in_suspension_interval:
service sched j t_in = service sched j suspension_start.
Proof.
rename H_within_suspension_interval into BETWEEN,
H_respects_self_suspensions into SUSP, t_in into i.
generalize dependent i.
suff SAME:
∀ delta,
delta ≤ duration →
service sched j (suspension_start + delta) =
service sched j suspension_start.
{
move ⇒ i /andP [GE LT].
feed (SAME (i-suspension_start)); first by rewrite leq_subLR.
by rewrite addnBA // addKn in SAME.
}
induction delta; first by rewrite addn0.
intros LT.
feed IHdelta; first by apply ltnW.
rewrite addnS -[service _ _ suspension_start]addn0.
rewrite /service /service_during big_nat_recr //=.
f_equal; first by done.
apply/eqP; rewrite eqb0; apply/negP; intro SCHED.
move: (SCHED) ⇒ SCHED'.
apply SUSP in SCHED; apply SCHED; clear SCHED.
rewrite /suspended_at /suspension_duration.
case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
first by apply completed_implies_not_scheduled in COMP;
first by rewrite SCHED' in COMP.
rewrite andTb (same_service_implies_same_last_execution _ _ _ _
suspension_start) //.
rewrite /suspension_start last_execution_idempotent //.
apply/andP; split; first by apply leq_addr.
by rewrite ltn_add2l.
Qed.
End SameService.
Section JobSuspendedAtAllTimes.
Variable t_in: time.
Hypothesis H_not_completed: ~~ job_completed_by j t_in.
Hypothesis H_within_suspension_interval:
suspension_start ≤ t_in < suspension_start + duration.
Lemma suspended_in_suspension_interval:
suspended_at j t_in.
Proof.
rename H_within_suspension_interval into BETWEEN.
move: BETWEEN ⇒ /andP [GE LT].
have ARR: has_arrived job_arrival j t_in.
{
apply leq_trans with (n := suspension_start); last by done.
rewrite -/(has_arrived job_arrival j suspension_start).
by apply last_execution_after_arrival.
}
apply/andP; split; first by done.
apply/andP; split;
first by apply last_execution_bounded_by_identity.
apply (leq_trans LT).
have SAME: time_after_last_execution job_arrival sched j t =
time_after_last_execution job_arrival sched j t_in.
{
set b := _ _ t.
rewrite [_ _ t_in](same_service_implies_same_last_execution _ _ _ _ b);
first by rewrite last_execution_idempotent.
apply same_service_in_suspension_interval.
by apply/andP; split; last by apply ltnW.
}
rewrite /suspension_start SAME leq_add2l.
by rewrite /duration /suspension_duration SAME.
Qed.
End JobSuspendedAtAllTimes.
End InsideSuspensionInterval.
Section StateOfSuspendedJob.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Variable j: Job.
Variable t: time.
Hypothesis H_j_is_suspended: suspended_at j t.
Lemma suspended_implies_arrived: has_arrived job_arrival j t.
Proof.
rename H_j_is_suspended into SUSP.
move: SUSP ⇒ /andP [_ SUSP].
rewrite -[_ && _]negbK in SUSP; move: SUSP ⇒ /negP SUSP.
rewrite /has_arrived leqNgt; apply/negP; intro LT.
apply SUSP; clear SUSP.
rewrite negb_and; apply/orP; left.
rewrite -ltnNge.
apply: (leq_trans LT); clear LT.
rewrite /time_after_last_execution.
case EX: [∃ _, _]; last by apply leqnn.
set t' := \max_(_ < _ | _)_.
move: EX ⇒ /existsP [t0 EX].
apply bigmax_pred in EX; rewrite -/t' /job_scheduled_at in EX.
apply leq_trans with (n := t'); last by apply leq_addr.
rewrite leqNgt; apply/negP; intro LT.
have NOTSCHED: ~~ scheduled_at sched j t'.
{
rewrite -eqb0; apply/eqP.
by eapply service_before_job_arrival_zero; first by eauto.
}
by rewrite EX in NOTSCHED.
Qed.
Corollary suspended_implies_not_completed:
~~ completed_by job_cost sched j t.
Proof.
by move: H_j_is_suspended ⇒ /andP [NOTCOMP _].
Qed.
End StateOfSuspendedJob.
Section BoundOnCumulativeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Let cumulative_suspension_of_j :=
cumulative_suspension_during j.
Let total_suspension_of_j :=
total_suspension job_cost next_suspension j.
Lemma cumulative_suspension_le_total_suspension:
∀ t1 t2,
cumulative_suspension_of_j t1 t2 ≤ total_suspension_of_j.
Proof.
unfold cumulative_suspension_of_j, cumulative_suspension_during,
total_suspension_of_j, total_suspension.
intros t1 t2.
apply leq_trans with (n := \sum_(0 ≤ s < job_cost j)
\sum_(t1 ≤ t < t2 | service sched j t == s) suspended_at j t).
{ rewrite (exchange_big_dep_nat (fun x ⇒ true)) //=.
apply leq_sum; intros s _.
destruct (boolP (suspended_at j s)) as [SUSP | NOTSUSP]; last by done.
rewrite (big_rem (service sched j s)); first by rewrite eq_refl.
rewrite mem_index_iota; apply/andP; split; first by done.
rewrite ltn_neqAle; apply/andP; split;
last by apply cumulative_service_le_job_cost.
apply suspended_implies_not_completed in SUSP.
rewrite neq_ltn; apply/orP; left.
by rewrite ltnNge.
}
{ apply leq_sum_nat; move ⇒ s /andP [_ LT] _.
destruct (boolP [∃ t:'I_t2, (t≥t1)&& (service sched j t==s)]) as [EX|ALL];
last first.
{
rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
rewrite big_nat_cond big1 //.
move ⇒ i /andP [/andP [GEi LTi] SERV].
by specialize (ALL (Ordinal LTi)); rewrite /= SERV GEi andbT in ALL.
}
move: EX ⇒ /existsP [t' /andP [GE' /eqP SERV]].
unfold suspended_at, suspension_duration.
set b := time_after_last_execution job_arrival sched j.
set n := next_suspension j s.
apply leq_trans with (n := \sum_(t1 ≤ t < t2 | b t' ≤ t < b t' + n) 1).
{
rewrite big_mkcond [\sum_(_ ≤ _ < _ | b t' ≤ _ < _) _]big_mkcond /=.
apply leq_sum_nat; intros t LEt _.
case: (boolP (completed_by _ _ _ _)) ⇒ [COMP | NOTCOMP];
[by case (_ == _) | simpl].
case EQ: (service _ _ _ == _); last by done.
move: EQ ⇒ /eqP EQ. rewrite /n -EQ.
case INT: (_ ≤ _ < _); last by done.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
move: INT ⇒ /andP [GEt LTt].
rewrite (same_service_in_suspension_interval _ _ _ _ t') //.
{
rewrite -/b [b t'](same_service_implies_same_last_execution _ _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split.
}
{
rewrite /suspension_duration -/b.
rewrite [b t'](same_service_implies_same_last_execution _ _ _ _ t);
last by rewrite SERV EQ.
by apply/andP; split; last by apply ltnW.
}
}
apply leq_trans with (n := \sum_(b t' ≤ t < b t' + n) 1);
last by simpl_sum_const; rewrite addKn.
by apply leq_sum1_smaller_range; move ⇒ i [LE LE']; split.
}
Qed.
End BoundOnCumulativeSuspension.
Section SuspendsForTotalSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_j_has_completed: completed_by job_cost sched j t.
Lemma cumulative_suspension_eq_total_suspension:
cumulative_suspension j t = total_suspension job_cost next_suspension j.
Proof.
rename H_j_has_completed into COMP, H_jobs_must_arrive_to_execute into ARR.
have EARLIER := exists_last_execution_with_smaller_service job_arrival
job_cost sched ARR j t COMP.
apply/eqP; rewrite eqn_leq; apply/andP; split;
first by apply cumulative_suspension_le_total_suspension.
rewrite /total_suspension /cumulative_suspension /cumulative_suspension_during.
move: COMP ⇒ /eqP COMP.
apply leq_trans with (n := \sum_(0 ≤ s < job_cost j)
\sum_(0 ≤ t0 < t | service sched j t0 == s) suspended_at j t0);
last first.
{
rewrite (exchange_big_dep_nat (fun x ⇒ true)) //=.
apply leq_sum_nat; move ⇒ t0 /andP [_ LT] _.
case (boolP [∃ s: 'I_(job_cost j), service sched j t0 == s]) ⇒ [EX | ALL].
{
move: EX ⇒ /existsP [s /eqP EQs].
rewrite big_mkcond /=.
rewrite (bigD1_seq (nat_of_ord s)); [simpl | | by apply iota_uniq];
last by rewrite mem_index_iota; apply/andP;split; last by apply ltn_ord.
rewrite EQs eq_refl big1; first by rewrite addn0.
by move ⇒ i /negbTE NEQ; rewrite eq_sym NEQ.
}
{
rewrite big_nat_cond big1; first by done.
move ⇒ i /andP [/andP [_ LTi] /eqP SERV].
rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
by specialize (ALL (Ordinal LTi)); rewrite /= SERV eq_refl in ALL.
}
}
{
apply leq_sum_nat; move ⇒ s /andP [_ LTs] _.
rewrite /suspended_at /suspension_duration.
set b := time_after_last_execution job_arrival sched j.
set n := next_suspension j.
move: (EARLIER s LTs) ⇒ [t' EQ'].
apply leq_trans with (n := \sum_(0 ≤ t0 < t | (service sched j t0 == s) &&
(b t' ≤ t0 < b t' + n (service sched j (b t')))) 1); last first.
{ rewrite big_mkcond [\sum_(_ ≤ _ < _ | _ == s)_]big_mkcond.
apply leq_sum_nat; move ⇒ i /andP [_ LTi] _.
case EQi: (service sched j i == s); [rewrite andTb | by rewrite andFb].
case LE: (_ ≤ _ ≤ _); last by done.
rewrite lt0n eqb0 negbK.
apply suspended_in_suspension_interval with (t := t'); try (by done).
rewrite -ltnNge.
by apply: (leq_ltn_trans _ LTs); apply eq_leq; apply/eqP.
}
{ apply leq_trans with (n := \sum_(b t'≤ t0< b t'+ n (service sched j (b t')) |
(0 ≤ t0 < t) && (service sched j t0 == s)) 1).
{
apply leq_trans with (n := \sum_(b t' ≤ t0 < b t'
+ n (service sched j (b t'))) 1);
first by simpl_sum_const; rewrite addKn -EQ'.
rewrite [in X in _ ≤ X]big_mkcond /=.
apply leq_sum_nat; move ⇒ i /andP [LEi GTi] _.
apply eq_leq; symmetry; apply/eqP; rewrite eqb1.
apply/andP; split.
{
have SUSPi: suspended_at j i.
{
apply: (suspended_in_suspension_interval _ _ _ _ t');
try (by done); last by apply/andP; split.
rewrite -ltnNge.
rewrite (same_service_in_suspension_interval _ _ _ _ t') //;
first by rewrite EQ'.
by apply/andP; split; last by apply ltnW.
}
apply contraT; rewrite -leqNgt; intro LE.
apply suspended_implies_not_completed in SUSPi.
exfalso; move: SUSPi ⇒ /negP COMPi; apply COMPi.
try ( apply completion_monotonic with (t0 := t); try (by done) ) ||
apply completion_monotonic with (t := t); try (by done).
by apply/eqP.
}
{
rewrite -EQ'; apply/eqP.
apply same_service_in_suspension_interval; try (by done).
by apply/andP; split; last by apply ltnW.
}
}
{
apply leq_sum1_smaller_range.
by move ⇒ i [LEb /andP [LE EQs]]; split;
last by apply/andP; split.
}
}
}
Qed.
End SuspendsForTotalSuspension.
Section ExecutionBeforeSuspension.
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Hypothesis H_respects_self_suspensions: respects_self_suspensions.
Variable j: Job.
Variable t: time.
Hypothesis H_arrived: has_arrived job_arrival j t.
Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
Hypothesis H_begins_suspension: suspended_at j t.+1.
Lemma executes_before_suspension:
scheduled_at sched j t.
Proof.
rename H_not_suspended_at_t into NOTSUSPs, H_begins_suspension into SUSPs'.
move: SUSPs' ⇒ /andP [NOTCOMP' /andP [GE LT]].
apply contraT; intro NOTSCHED.
suff BUG: suspended_at j t by rewrite BUG in NOTSUSPs.
apply suspended_in_suspension_interval with (t := t.+1); try done.
{
apply contraT; rewrite negbK; intro COMP.
suff COMP': completed_by job_cost sched j t.+1 by rewrite COMP' in NOTCOMP'.
try ( by apply completion_monotonic with (t0 := t) ) ||
by apply completion_monotonic with (t := t).
}
apply/andP; split; last by apply: (leq_ltn_trans _ LT).
apply leq_trans with (n := time_after_last_execution job_arrival sched j t);
last by apply last_execution_bounded_by_identity.
apply eq_leq, same_service_implies_same_last_execution.
rewrite /service /service_during big_nat_recr //= /service_at.
by apply negbTE in NOTSCHED; rewrite NOTSCHED addn0.
Qed.
End ExecutionBeforeSuspension.
End Lemmas.
End DefiningSuspensionIntervals.
End SuspensionIntervals.