Library prosa.analysis.facts.model.overheads.blackout_bound

Require Export prosa.model.processor.overhead_resource_model.

In this file, we prove a bound on the total blackout time (i.e., time during which no job makes progress due to overheads), assuming a given number of schedule changes.

Section TotalBlackoutDueToOverheadsBounded.

Consider any type of jobs.

  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.

  Context {JLFP : JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
  Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.

Consider any valid arrival sequence, ...

Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any schedule of this arrival sequence...

Variable sched : schedule (overheads.processor_state Job).

... where jobs do not execute before their arrival nor after completion.

Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.

Finally, we assume that the schedule respects a valid overhead resource model with dispatch overhead DB, context switch overhead CSB, and preemption-related overhead CRPDB.

  Variable DB CSB CRPDB : duration.
  Hypothesis H_valid_overheads_model :
    overhead_resource_model sched DB CSB CRPDB.

The total blackout duration in the interval [t1, t2) can be decomposed into time spent in dispatching, context switching, and CRPD (cache-related preemption delay).

  Lemma blackout_during_split :
    ∀ (t1 t2 : instant),
      blackout_during sched t1 t2
      = total_time_in_dispatch sched t1 t2
        + total_time_in_context_switch sched t1 t2
        + total_time_in_CRPD sched t1 t2.

If there are no schedule changes in the interval [t1, t2), then the processor must always be scheduling the same job (or be idle). In that case, the total dispatch time in that interval is equal to the time spent dispatching a specific job (or be idle).

  Lemma total_dispatch_time_eq_job_dispatch_time :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      ∃ (oj : option Job ),
        total_time_in_dispatch sched t1 t2
        = time_spent_in_dispatch sched oj t1 t2.

Similar statements are true for context-switch overhead...

  Lemma total_cswitch_time_eq_job_cswitch_time :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      ∃ (oj : option Job ),
        total_time_in_context_switch sched t1 t2
        = time_spent_in_context_switch sched oj t1 t2.

... and CRPD.

  Lemma total_CRPD_time_eq_job_CRPD_time :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      ∃ (oj : option Job ),
        total_time_in_CRPD sched t1 t2
        = time_spent_in_CRPD sched oj t1 t2.

If there are no schedule changes in [t1, t2), then the processor must be scheduling the same job (or be idle) throughout. In that case, since the dispatch time spent on a specific job is bounded by DB, the total dispatch time in [t1, t2) is also bounded by DB.

  Lemma total_time_in_dispatch_is_bounded :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      total_time_in_dispatch sched t1 t2 ≤ DB.

Same reasoning holds for context switches...

  Lemma total_time_in_cswitch_is_bounded :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      total_time_in_context_switch sched t1 t2 ≤ CSB.

... and CRPD.

  Lemma total_time_in_CRPD_is_bounded :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      total_time_in_CRPD sched t1 t2 ≤ CRPDB.

If there are no schedule changes in the interval [t1+1, t2), then the processor executes the same job (or remains idle) throughout the interval [t1, t2), possibly with some initial scheduling activity at t1. In that case, the total blackout time in [t1, t2) is at most the sum of: dispatch overhead (DB), a context switch before (CSB), and cache-related preemption delay (CRPD).

We exclude t1 from the schedule-change check because a change between t1−1 and t1 is irrelevant for bounding blackout in [t1, t2) as it only affects the boundary.

  Lemma no_sched_changes_bounded_overheads_blackout :
    ∀ (t1 t2 : instant),
      no_schedule_changes_during sched t1 t2 →
      blackout_during sched t1 t2 ≤ DB + CSB + CRPDB.

If there is exactly one schedule change in the interval

[t1,

t2)>>, and it occurs at the very beginning (i.e., at t1), then the processor schedules a job at t1 and continues executing the same job (or stays idle) for the rest of the interval.

  Lemma sched_changes_start_busy_pref_bounded_overheads_blackout :
    ∀ (t1 t2 : instant),
      number_schedule_changes sched t1 t2 = 1 →
      schedule_change sched t1 →
      blackout_during sched t1 t2 ≤ DB + CSB + CRPDB.

If there are exactly k schedule changes in the interval

[t1,

t2)>>, and one of them occurs at the beginning (i.e., at t1), then the blackout time over the interval is bounded by (DB + CSB + CRPDB) × k.

  Lemma fin_sched_changes_start_busy_pref_bounded_overheads_blackout :
    ∀ (k : nat) (t1 t2 : instant),
      schedule_change sched t1 →
      number_schedule_changes sched t1 t2 = k →
      blackout_during sched t1 t2 ≤ (DB + CSB + CRPDB ) × k.

If there are exactly k schedule changes in the interval [t1+1, t2), then the total blackout time in [t1, t2) is at most (DB + CSB + CRPDB) × (k + 1).

  Lemma finite_sched_changes_bounded_overheads_blackout :
    ∀ (k : nat) (t1 t2 : instant),
      number_schedule_changes sched t1 .+1 t2 = k →
      blackout_during sched t1 t2 ≤ (DB + CSB + CRPDB ) × (k + 1).

End TotalBlackoutDueToOverheadsBounded.