Library prosa.analysis.definitions.overheads.schedule_change

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

Consider any type of jobs.

Consider any arrival sequence and any schedule.

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.

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.