Library rt.model.schedule.uni.basic.busy_interval
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.service
rt.model.schedule.uni.workload.
Require Import rt.model.schedule.uni.basic.platform.
Module BusyInterval.
Import Job UniprocessorSchedule Priority Platform
Service Workload TaskArrival.
(* In this section, we define the notion of a busy interval. *)
Section Defs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent arrival times... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Assume a given JLFP policy. *)
Variable higher_eq_priority: JLFP_policy Job.
(* Let j be the job to be analyzed. *)
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
(* For simplicity, let's define some local names. *)
Let job_pending_at := pending job_arrival job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
(* We say that t is a quiet time for j iff every higher-priority job from
the arrival sequence that arrived before t has completed by that time. *)
Definition quiet_time (t: time) :=
∀ j_hp,
arrives_in arr_seq j_hp →
higher_eq_priority j_hp j →
arrived_before job_arrival j_hp t →
job_completed_by j_hp t.
(* Based on the definition of quiet time, we say that interval
[t1, t_busy) is a (potentially unbounded) busy-interval prefix
iff the interval starts with a quiet time and remains non-quiet. *)
Definition busy_interval_prefix (t1 t_busy: time) :=
t1 < t_busy ∧
quiet_time t1 ∧
(∀ t, t1 < t < t_busy → ¬ quiet_time t).
(* Next, we say that an interval [t1, t2) is a busy interval iff
[t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
(* Now we prove some lemmas about busy intervals. *)
Section Lemmas.
(* Recall the list of jobs that arrive in any interval. *)
Let arrivals_between := jobs_arrived_between arr_seq.
(* We begin by proving basic lemmas about the arrival and
completion of jobs that are pending during a busy interval. *)
Section BasicLemmas.
(* Assume that the priority relation is reflexive. *)
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
(* Consider any busy interval [t1, t2)... *)
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
(* ...and assume that job j is pending during this busy interval. *)
Variable t: time.
Hypothesis H_during_interval: t1 ≤ t < t2.
Hypothesis H_job_is_pending: job_pending_at j t.
(* First, we prove that job j completes by the end of the busy interval. *)
Section CompletesDuringBusyInterval.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End CompletesDuringBusyInterval.
(* Next, we prove that job j cannot have arrived before the
busy interval. *)
Section ArrivesDuringBusyInterval.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Then, we prove that j arrives no earlier than t1. *)
Lemma job_arrives_within_busy_interval:
t1 ≤ job_arrival j.
End ArrivesDuringBusyInterval.
End BasicLemmas.
(* In this section, we prove that during a busy interval there
always exists a pending job. *)
Section ExistsPendingJob.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Let [t1, t2] be any interval where time t1 is quiet and
time t2 is not quiet. *)
Variable t1 t2: time.
Hypothesis H_interval: t1 ≤ t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ¬ quiet_time t2.
(* Then, we prove that there exists a job pending at time t2
that has higher or equal priority (with respect ot tsk). *)
Lemma not_quiet_implies_exists_pending_job:
∃ j_hp,
arrives_in arr_seq j_hp ∧
arrived_between job_arrival j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
¬ job_completed_by j_hp t2.
End ExistsPendingJob.
(* In this section, we prove that during a busy interval the
processor is never idle. *)
Section ProcessorAlwaysBusy.
(* Assume that the schedule is work-conserving and that jobs do
not execute before their arrival or after completion. *)
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
(* Consider any interval [t1, t2] such that t1 < t2 and t1 is the only quiet time. *)
Variable t1 t2: time.
Hypothesis H_strictly_larger: t1 < t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ∀ t, t1 < t ≤ t2 → ¬ quiet_time t.
(* We prove that at every time t in [t1, t2], the processor is not idle. *)
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t ≤ t2 →
¬ is_idle sched t.
(* In fact, we can infer a stronger property. *)
Section OnlyHigherOrEqualPriority.
(* If the JLFP policy is transitive and is respected by the schedule, ...*)
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
(* ... then the processor is always busy with a job of higher or equal priority. *)
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 ≤ t < t2 →
∃ j_hp,
arrived_between job_arrival j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
job_scheduled_at j_hp t.
End OnlyHigherOrEqualPriority.
End ProcessorAlwaysBusy.
(* In this section, we show that the length of any busy interval
is bounded, as long as there is enough supply to accomodate
the workload of tasks with higher or equal priority. *)
Section BoundingBusyInterval.
(* Assume that there are no duplicate job arrivals... *)
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
(* ...and that jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Also assume a work-conserving FP schedule, ... *)
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
(* ...in which the priority relation is reflexive and transitive. *)
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
(* Next, we recall the notion of workload of all jobs released in a given interval
[t1, t2) that have higher-or-equal priority than the job j being analyzed. *)
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs job_cost (arrivals_between t1 t2)
higher_eq_priority j.
(* With regard to the jobs with higher-or-equal priority that are released
in a given interval [t1, t2), we also recall the service received by these
jobs in the same interval [t1, t2). *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs sched (arrivals_between t1 t2)
higher_eq_priority j t1 t2.
(* Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
(* Suppose that job j is pending at time t_busy. *)
Variable t_busy: time.
Hypothesis H_j_is_pending: job_pending_at j t_busy.
(* First, we show that there must exist a busy interval prefix. *)
Section LowerBound.
(* Since job j is pending, there exists a (potentially unbounded)
busy interval that starts prior to the arrival of j. *)
Lemma exists_busy_interval_prefix:
∃ t1,
busy_interval_prefix t1 t_busy.+1 ∧
t1 ≤ job_arrival j ≤ t_busy.
End LowerBound.
(* Next we prove that, if there is a point where the requested workload
is upper-bounded by the supply, then the busy interval eventually ends. *)
Section UpperBound.
(* Consider any busy interval that starts at time t1 <= job_arrival j. *)
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Hypothesis H_busy_prefix_contains_arrival: job_arrival j ≥ t1.
(* Next, assume that for some delta > 0, the requested workload
at time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded: hp_workload t1 (t1 + delta) ≤ delta.
(* If there exists a quiet time by time (t1 + delta), it trivially follows that
the busy interval is bounded.
Thus, let's consider first the harder case where there is no quiet time,
which turns out to be impossible. *)
Section CannotBeBusyForSoLong.
(* Assume that there is no quiet time in the interval (t1, t1 + delta]. *)
Hypothesis H_no_quiet_time:
∀ t, t1 < t ≤ t1 + delta → ¬ quiet_time t.
(* Since the interval is always non-quiet, the processor is always busy
with tasks of higher-or-equal priority. *)
Lemma busy_interval_has_uninterrupted_service:
hp_service t1 (t1 + delta) = delta.
(* Moreover, the fact that the interval is not quiet also implies
that there's more workload requested than service received. *)
Lemma busy_interval_too_much_workload:
hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
(* Using the two lemmas above, we infer that the workload is larger than the
interval length. However, this contradicts the assumption H_workload_is_bounded. *)
Corollary busy_interval_workload_larger_than_interval:
hp_workload t1 (t1 + delta) > delta.
End CannotBeBusyForSoLong.
(* Since the interval cannot remain busy for so long, we prove that
the busy interval finishes at some point t2 <= t1 + delta. *)
Lemma busy_interval_is_bounded:
∃ t2,
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End UpperBound.
End BoundingBusyInterval.
(* In this section, we show that from a workload bound we can infer
the existence of a busy interval. *)
Section BusyIntervalFromWorkloadBound.
(* Assume that for some delta > 0, the requested workload at
time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, hp_workload t (t + delta) ≤ delta.
(* By assuming that job j has positive cost, we can infer that
there always is a time in which j is pending. *)
Hypothesis H_positive_cost: job_cost j > 0.
(* Therefore there must exists a busy interval [t1, t2) that
contains the arrival time of j. *)
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
(* If we know that the workload is bounded, we can also use the
busy interval to infer a response-time bound. *)
Section ResponseTimeBoundFromBusyInterval.
(* Assume that for some delta > 0, the requested workload
at time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t,
hp_workload t (t + delta) ≤ delta.
(* Then, job j must complete by (job_arrival j + delta). *)
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
End Defs.
End BusyInterval.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.service
rt.model.schedule.uni.workload.
Require Import rt.model.schedule.uni.basic.platform.
Module BusyInterval.
Import Job UniprocessorSchedule Priority Platform
Service Workload TaskArrival.
(* In this section, we define the notion of a busy interval. *)
Section Defs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
(* Consider any arrival sequence with consistent arrival times... *)
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
(* ...and any uniprocessor schedule of these jobs. *)
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
(* Assume a given JLFP policy. *)
Variable higher_eq_priority: JLFP_policy Job.
(* Let j be the job to be analyzed. *)
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
(* For simplicity, let's define some local names. *)
Let job_pending_at := pending job_arrival job_cost sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
(* We say that t is a quiet time for j iff every higher-priority job from
the arrival sequence that arrived before t has completed by that time. *)
Definition quiet_time (t: time) :=
∀ j_hp,
arrives_in arr_seq j_hp →
higher_eq_priority j_hp j →
arrived_before job_arrival j_hp t →
job_completed_by j_hp t.
(* Based on the definition of quiet time, we say that interval
[t1, t_busy) is a (potentially unbounded) busy-interval prefix
iff the interval starts with a quiet time and remains non-quiet. *)
Definition busy_interval_prefix (t1 t_busy: time) :=
t1 < t_busy ∧
quiet_time t1 ∧
(∀ t, t1 < t < t_busy → ¬ quiet_time t).
(* Next, we say that an interval [t1, t2) is a busy interval iff
[t1, t2) is a busy-interval prefix and t2 is a quiet time. *)
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
(* Now we prove some lemmas about busy intervals. *)
Section Lemmas.
(* Recall the list of jobs that arrive in any interval. *)
Let arrivals_between := jobs_arrived_between arr_seq.
(* We begin by proving basic lemmas about the arrival and
completion of jobs that are pending during a busy interval. *)
Section BasicLemmas.
(* Assume that the priority relation is reflexive. *)
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
(* Consider any busy interval [t1, t2)... *)
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
(* ...and assume that job j is pending during this busy interval. *)
Variable t: time.
Hypothesis H_during_interval: t1 ≤ t < t2.
Hypothesis H_job_is_pending: job_pending_at j t.
(* First, we prove that job j completes by the end of the busy interval. *)
Section CompletesDuringBusyInterval.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End CompletesDuringBusyInterval.
(* Next, we prove that job j cannot have arrived before the
busy interval. *)
Section ArrivesDuringBusyInterval.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Then, we prove that j arrives no earlier than t1. *)
Lemma job_arrives_within_busy_interval:
t1 ≤ job_arrival j.
End ArrivesDuringBusyInterval.
End BasicLemmas.
(* In this section, we prove that during a busy interval there
always exists a pending job. *)
Section ExistsPendingJob.
(* Assume that jobs do not execute after completion. *)
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Let [t1, t2] be any interval where time t1 is quiet and
time t2 is not quiet. *)
Variable t1 t2: time.
Hypothesis H_interval: t1 ≤ t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ¬ quiet_time t2.
(* Then, we prove that there exists a job pending at time t2
that has higher or equal priority (with respect ot tsk). *)
Lemma not_quiet_implies_exists_pending_job:
∃ j_hp,
arrives_in arr_seq j_hp ∧
arrived_between job_arrival j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
¬ job_completed_by j_hp t2.
End ExistsPendingJob.
(* In this section, we prove that during a busy interval the
processor is never idle. *)
Section ProcessorAlwaysBusy.
(* Assume that the schedule is work-conserving and that jobs do
not execute before their arrival or after completion. *)
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
(* Consider any interval [t1, t2] such that t1 < t2 and t1 is the only quiet time. *)
Variable t1 t2: time.
Hypothesis H_strictly_larger: t1 < t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ∀ t, t1 < t ≤ t2 → ¬ quiet_time t.
(* We prove that at every time t in [t1, t2], the processor is not idle. *)
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t ≤ t2 →
¬ is_idle sched t.
(* In fact, we can infer a stronger property. *)
Section OnlyHigherOrEqualPriority.
(* If the JLFP policy is transitive and is respected by the schedule, ...*)
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
(* ... then the processor is always busy with a job of higher or equal priority. *)
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 ≤ t < t2 →
∃ j_hp,
arrived_between job_arrival j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
job_scheduled_at j_hp t.
End OnlyHigherOrEqualPriority.
End ProcessorAlwaysBusy.
(* In this section, we show that the length of any busy interval
is bounded, as long as there is enough supply to accomodate
the workload of tasks with higher or equal priority. *)
Section BoundingBusyInterval.
(* Assume that there are no duplicate job arrivals... *)
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
(* ...and that jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
(* Also assume a work-conserving FP schedule, ... *)
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost arr_seq sched higher_eq_priority.
(* ...in which the priority relation is reflexive and transitive. *)
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
(* Next, we recall the notion of workload of all jobs released in a given interval
[t1, t2) that have higher-or-equal priority than the job j being analyzed. *)
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs job_cost (arrivals_between t1 t2)
higher_eq_priority j.
(* With regard to the jobs with higher-or-equal priority that are released
in a given interval [t1, t2), we also recall the service received by these
jobs in the same interval [t1, t2). *)
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs sched (arrivals_between t1 t2)
higher_eq_priority j t1 t2.
(* Now we begin the proof. First, we show that the busy interval is bounded. *)
Section BoundingBusyInterval.
(* Suppose that job j is pending at time t_busy. *)
Variable t_busy: time.
Hypothesis H_j_is_pending: job_pending_at j t_busy.
(* First, we show that there must exist a busy interval prefix. *)
Section LowerBound.
(* Since job j is pending, there exists a (potentially unbounded)
busy interval that starts prior to the arrival of j. *)
Lemma exists_busy_interval_prefix:
∃ t1,
busy_interval_prefix t1 t_busy.+1 ∧
t1 ≤ job_arrival j ≤ t_busy.
End LowerBound.
(* Next we prove that, if there is a point where the requested workload
is upper-bounded by the supply, then the busy interval eventually ends. *)
Section UpperBound.
(* Consider any busy interval that starts at time t1 <= job_arrival j. *)
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Hypothesis H_busy_prefix_contains_arrival: job_arrival j ≥ t1.
(* Next, assume that for some delta > 0, the requested workload
at time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded: hp_workload t1 (t1 + delta) ≤ delta.
(* If there exists a quiet time by time (t1 + delta), it trivially follows that
the busy interval is bounded.
Thus, let's consider first the harder case where there is no quiet time,
which turns out to be impossible. *)
Section CannotBeBusyForSoLong.
(* Assume that there is no quiet time in the interval (t1, t1 + delta]. *)
Hypothesis H_no_quiet_time:
∀ t, t1 < t ≤ t1 + delta → ¬ quiet_time t.
(* Since the interval is always non-quiet, the processor is always busy
with tasks of higher-or-equal priority. *)
Lemma busy_interval_has_uninterrupted_service:
hp_service t1 (t1 + delta) = delta.
(* Moreover, the fact that the interval is not quiet also implies
that there's more workload requested than service received. *)
Lemma busy_interval_too_much_workload:
hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
(* Using the two lemmas above, we infer that the workload is larger than the
interval length. However, this contradicts the assumption H_workload_is_bounded. *)
Corollary busy_interval_workload_larger_than_interval:
hp_workload t1 (t1 + delta) > delta.
End CannotBeBusyForSoLong.
(* Since the interval cannot remain busy for so long, we prove that
the busy interval finishes at some point t2 <= t1 + delta. *)
Lemma busy_interval_is_bounded:
∃ t2,
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End UpperBound.
End BoundingBusyInterval.
(* In this section, we show that from a workload bound we can infer
the existence of a busy interval. *)
Section BusyIntervalFromWorkloadBound.
(* Assume that for some delta > 0, the requested workload at
time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, hp_workload t (t + delta) ≤ delta.
(* By assuming that job j has positive cost, we can infer that
there always is a time in which j is pending. *)
Hypothesis H_positive_cost: job_cost j > 0.
(* Therefore there must exists a busy interval [t1, t2) that
contains the arrival time of j. *)
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
(* If we know that the workload is bounded, we can also use the
busy interval to infer a response-time bound. *)
Section ResponseTimeBoundFromBusyInterval.
(* Assume that for some delta > 0, the requested workload
at time (t1 + delta) is bounded by delta (i.e., the supply). *)
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t,
hp_workload t (t + delta) ≤ delta.
(* Then, job j must complete by (job_arrival j + delta). *)
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
End Defs.
End BusyInterval.