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