# Library prosa.analysis.facts.model.overheads.schedule_change

Require Export prosa.model.processor.overheads.
Require Export prosa.analysis.definitions.overheads.schedule_change.
Require Export prosa.analysis.facts.model.overheads.schedule.
In this section, we prove a few basic properties about the number of schedule changes in a given interval.
Section ScheduleChange.
Consider any type of jobs..
Context {Job : JobType}.
... and any schedule with explicit overheads.
Variable sched : schedule (overheads.processor_state Job).
The number of schedule changes over `[t1, t2)` is equal to the number of changes in `[t1, t)` plus the number in `[t, t2)`.
Lemma number_schedule_changes_cat :
∀ (t t1 t2 : instant),
t1 ≤ t ≤ t2 →
number_schedule_changes sched t1 t2
= number_schedule_changes sched t1 t + number_schedule_changes sched t t2.
Proof.
move⇒ t t1 t2 NEQ.
by rewrite /number_schedule_changes (index_iota_cat t t1 t2) // count_cat.
Qed.
If there is at least one schedule change in `[t1, t2)`, then there exists the first time `t ∈ [t1, t2)` where the change occurs, and no change happens before t.
Lemma first_schedule_change_exists :
∀ (t1 t2 : instant) (k : nat),
k > 0 →
number_schedule_changes sched t1 t2 = k →
∃ t,
t1 ≤ t < t2
∧ schedule_change sched t
∧ number_schedule_changes sched t1 t = 0
∧ number_schedule_changes sched t t2 = k.
Proof.
move⇒ t1 t2 k POS EQ.
have EX: ∃ t, (fun t ⇒ (t1 ≤ t < t2) && schedule_change sched t) t.
{ move: POS; rewrite -EQ.
rewrite /number_schedule_changes -has_count.
move=>/hasP [to]; rewrite mem_index_iota ⇒ NEQo SCo.
by ∃ to; rewrite SCo NEQo.
}
apply find_ex_minn in EX; move: EX ⇒ [t /andP [NEQ SC] MIN].
∃ t; rewrite NEQ SC; do 2 split ⇒ //.
have ZE : number_schedule_changes sched t1 t = 0.
{ apply/eqP; rewrite -leqn0; move_neq_up NUM.
move: NUM; rewrite /number_schedule_changes -has_count.
move=>/hasP [to]; rewrite mem_index_iota ⇒ NEQo SCo.
by move: (MIN to ltac:(lia)) ⇒ LE2; lia.
}
{ by rewrite ZE; split ⇒ //; move: EQ; rewrite (number_schedule_changes_cat t); lia. }
Qed.
Widening the interval can only increase the number of schedule changes.
Lemma number_schedule_changes_widen :
∀ (t1 t2 t1' t2' : instant),
t1 ≤ t1' →
t2' ≤ t2 →
number_schedule_changes sched t1' t2'
≤ number_schedule_changes sched t1 t2.
Proof.
move ⇒ t1 t2 t1' t2' LE1 LE2.
rewrite /number_schedule_changes.
have [/eqP LE|LT] := leqP t2' t1'.
{ by rewrite /index_iota LE. }
rewrite (index_iota_cat t1' t1 t2); last by lia.
move: LE2; rewrite leq_eqVlt ⇒ /orP [/eqP EQ|LT2].
{ by subst; rewrite count_cat; lia. }
{ rewrite (index_iota_cat t2' t1' t2); last by lia.
by rewrite !count_cat; lia.
}
Qed.
End ScheduleChange.
In this section, we prove properties of the predicate scheduled_job_invariant.
Section ScheduleInterruptions.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any valid arrival sequence
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Next, consider any schedule of the arrival sequence where jobs don't execute before their arrival time.
Variable sched : schedule (overheads.processor_state Job).
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_must_arrive : jobs_must_arrive_to_execute sched.
If the processor has the same scheduled state oj1 in `[t1, t)` and the same state oj2 in `[t, t2)`, and there is no schedule change at time t, then both intervals must have the same scheduled state oj1 = oj2.
Lemma same_scheduled_state_merge :
∀ (t1 t2 t : instant) (oj1 oj2 : option Job),
t1 < t < t2 →
~~ schedule_change sched t →
scheduled_job_invariant sched oj1 t1 t →
scheduled_job_invariant sched oj2 t t2 →
oj1 = oj2.
Proof.
move⇒ t1 t2 t oj1 oj2 /andP [NEQ1 NEQ2] EQ /allP SC1 /allP SC2.
have IN1: t.-1 \in index_iota t1 t by rewrite mem_index_iota; lia.
have IN2: t \in index_iota t t2 by rewrite mem_index_iota; lia.
move: (SC1 _ IN1) (SC2 _ IN2) ⇒ /eqP EQ1 /eqP EQ2.
rewrite /schedule_change EQ1 EQ2 in EQ.
by apply/eqP/negPn.
Qed.
If there are no schedule changes in an interval `[t1, t2)`, then the scheduled job must remain the same at every instant within the interval.
Lemma no_schedule_changes_implies_constant_schedule :
∀ (t1 t2 t : instant),
t1 ≤ t < t2 →
number_schedule_changes sched t1 t2 = 0 →
~~ schedule_change sched t.
Proof.
move⇒ t1 t2 t NEQ ⇒ /eqP.
rewrite -leqn0 leqNgt -has_count -all_predC ⇒ /allP IN.
rewrite /schedule_change; apply/negPn/eqP.
specialize (IN t).
rewrite mem_index_iota //= in IN.
apply/eqP/negPn/negP ⇒ NEQ2.
rewrite /schedule_change NEQ2 in IN.
by rewrite NEQ in IN.
Qed.
If there are no schedule changes during the interval `[t1, t2)`, then scheduled_job remains constant throughout the interval.
Lemma no_changes_implies_same_scheduled_job :
∀ (t1 t2 t t' : instant) (oj : option Job),
no_schedule_changes_during sched t1 t2 →
t1 ≤ t < t2 →
t1 ≤ t' < t2 →
scheduled_job sched t = oj →
scheduled_job sched t' = oj.
Proof.
move⇒ t1 t2 t t' oj NSC NEQ1 NEQ2 SC.
have [A1|A2] := leqP t t'.
{ interval_to_duration t t' k.
induction k as [ | k IHk]; first by rewrite addn0.
rewrite addnS; rewrite addnS in NEQ2.
feed IHk; first by lia.
move: NSC ⇒ /eqP; rewrite /number_schedule_changes.
move=>/eqP; rewrite -leqn0 leqNgt -has_count -all_predC ⇒ /allP NSC.
move: (NSC (t+k).+1 ltac:(rewrite mem_index_iota; lia)); clear NSC.
rewrite /predC /schedule_change //= negbK ⇒ /eqP EQ.
by rewrite -EQ.
}
{ interval_to_duration t' t k.
induction k as [ | k IHk]; first by rewrite addn0 in SC.
rewrite addnS in SC, NEQ2.
feed IHk; first by lia.
apply: IHk.
move: NSC ⇒ /eqP; rewrite /number_schedule_changes.
move=>/eqP; rewrite -leqn0 leqNgt -has_count -all_predC ⇒ /allP NSC.
move: (NSC (t'+k).+1 ltac:(rewrite mem_index_iota; lia)); clear NSC.
rewrite /predC /schedule_change //= negbK ⇒ /eqP EQ.
by rewrite EQ.
}
Qed.
End ScheduleInterruptions.