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.