Library prosa.analysis.facts.busy_interval.carry_in
Require Export prosa.analysis.facts.model.workload.
Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
Require Export prosa.analysis.facts.busy_interval.quiet_time.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.util.tactics.
Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
Require Export prosa.analysis.facts.busy_interval.quiet_time.
Require Export prosa.analysis.facts.busy_interval.existence.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.model.schedule.work_conserving.
Require Export prosa.util.tactics.
Busy Interval From Workload Bound
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context {Arrival: JobArrival Job}.
Context {Cost : JobCost Job}.
Context `{JobTask Job Task}.
Context {Arrival: JobArrival Job}.
Context {Cost : JobCost Job}.
Consider any valid arrival sequence.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arr_seq : valid_arrival_sequence arr_seq.
Allow for any uniprocessor model that ensures ideal progress.
Context {PState : ProcessorState Job}.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_uniproc : uniprocessor_model PState.
Hypothesis H_ideal_progress_proc_model : ideal_progress_proc_model PState.
Hypothesis H_uniproc : uniprocessor_model PState.
Next, consider any schedule of the arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
... where jobs do not execute before their arrival or after completion.
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
Assume a given reflexive JLFP policy.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Further, allow for any work-bearing notion of job readiness ...
Context `{@JobReady Job PState Cost Arrival}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
... and assume that the schedule is work-conserving.
Times without Carry-In
Next, we relate idle times to the no-carry-in condition. First, the
presence of a pending job implies that the processor isn't idle due to
work-conservation.
Lemma pending_job_not_idle :
∀ j t,
arrives_in arr_seq j →
pending sched j t →
¬ is_idle arr_seq sched t.
∀ j t,
arrives_in arr_seq j →
pending sched j t →
¬ is_idle arr_seq sched t.
Second, an idle time implies no carry in at this time instant.
Moreover, an idle time implies no carry in at the next time instant, too.
Lemma idle_instant_next_no_carry_in :
∀ t,
is_idle arr_seq sched t →
no_carry_in arr_seq sched t.+1.
∀ t,
is_idle arr_seq sched t →
no_carry_in arr_seq sched t.+1.
Bounded-Workload Assumption
[t1, t2)
...
... and total service of jobs within some time interval
[t1, t2)
.
We assume that, for some positive Δ, the total workload generated in any
interval of length Δ is bounded by Δ (i.e., the supply provided by an
ideal-progress unit-speed processor). Note that this assumption bounds the
total workload of jobs released in a time interval
[t, t + Δ)
regardless of their priorities.
Variable Δ : duration.
Hypothesis H_delta_positive : Δ > 0.
Hypothesis H_workload_is_bounded : ∀ t, total_workload t (t + Δ) ≤ Δ.
Hypothesis H_delta_positive : Δ > 0.
Hypothesis H_workload_is_bounded : ∀ t, total_workload t (t + Δ) ≤ Δ.
In the following, we also require a unit-speed processor.
Existence of a No-Carry-In Instant
As a stepping stone, we prove in the following section that for any time
instant t there exists another time instant
t' ∈ (t, t + Δ]
such
that the processor has no carry-in at time t'.
Consider an arbitrary time instant t ...
... such that there is no carry-in at time t.
First, recall that the total service is bounded by the total
workload. Therefore the total service of jobs in the interval
[t, t + Δ)
is bounded by Δ.
Next we consider two cases:
(1) The case when the total service is strictly less than Δ, and
(2) the case when the total service is equal to Δ.
In the first case, we use the pigeonhole principle to
conclude that there is an idle time instant; which in turn
implies existence of a time instant with no carry-in.
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ no_carry_in arr_seq sched (t.+1 + δ).
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ no_carry_in arr_seq sched (t.+1 + δ).
In the second case, the total service within the time interval
[t, t + Δ)
is equal to Δ. We also know that the total
workload is lower-bounded by the total service and upper-bounded
by Δ. Therefore, the total workload is equal to the total service,
which implies completion of all jobs by time t + Δ and hence no
carry-in at time t + Δ.
Lemma completion_of_all_jobs_implies_no_carry_in :
total_service t (t + Δ) = Δ →
no_carry_in arr_seq sched (t + Δ).
End ProcessorIsNotTooBusyInduction.
total_service t (t + Δ) = Δ →
no_carry_in arr_seq sched (t + Δ).
End ProcessorIsNotTooBusyInduction.
Finally, we show that any interval of length Δ contains a time instant
with no carry-in.
Lemma processor_is_not_too_busy :
∀ t, ∃ δ,
δ < Δ ∧ no_carry_in arr_seq sched (t + δ).
End ProcessorIsNotTooBusy.
∀ t, ∃ δ,
δ < Δ ∧ no_carry_in arr_seq sched (t + δ).
End ProcessorIsNotTooBusy.
Busy Interval Existence
Consider an arbitrary job j with positive cost.
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
We show that there must exist a busy interval
[t1, t2)
that
contains the arrival time of j.