# 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.
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.
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.
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.
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.
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.
End ScheduleInterruptions.