Library prosa.analysis.definitions.overheads.schedule_change

Require Export prosa.model.processor.overheads.

In this section, we define predicates and functions to reason about schedule changes over time intervals.
Section ScheduleChanges.

Consider any type of jobs.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any arrival sequence and any schedule.
  Variable arr_seq : arrival_sequence Job.
  Variable sched : schedule (overheads.processor_state Job).

A schedule change occurs at time t if the processor state (i.e., which job is scheduled or whether it is idle) at time t differs from that at time t−1.
  Definition schedule_change (t : instant) :=
    scheduled_job sched t.-1 != scheduled_job sched t.

In addition, we define the number of schedule changes in the interval [t1, t2).
  Definition number_schedule_changes (t1 t2 : instant) :=
    count schedule_change (index_iota t1 t2).

The predicate no_schedule_changes_during t1 t2 holds if the number of schedule changes in the interval (t1, t2) is zero. Note that we count changes only from time t1+1 onward because a change between t1−1 and t1 does not reflect any change occurring *within* the interval.
  Definition no_schedule_changes_during (t1 t2 : instant) :=
    number_schedule_changes t1.+1 t2 == 0.

The predicate scheduled_job_invariant oj t1 t2 holds if the processor always schedules either a specific job or is being idle at every instant in [t1, t2).
Unlike number_schedule_changes, scheduled_job_invariant fixes a specific job (or idle state). This is useful when bounding overheads that can be attributed to a specific job.
  Definition scheduled_job_invariant (oj : option Job) (t1 t2 : instant) :=
    all (fun t ⇒ scheduled_job sched t == oj) (index_iota t1 t2).

End ScheduleChanges.