# Library prosa.analysis.facts.busy_interval.carry_in

Require Export prosa.analysis.facts.model.workload.

Require Export prosa.analysis.definitions.carry_in.

Require Export prosa.analysis.facts.busy_interval.busy_interval.

Require Export prosa.analysis.definitions.carry_in.

Require Export prosa.analysis.facts.busy_interval.busy_interval.

Throughout this file, we assume ideal uniprocessor schedules.

Require Import prosa.model.processor.ideal.

Require Export prosa.analysis.facts.model.ideal.service_of_jobs.

Require Export prosa.analysis.facts.model.ideal.service_of_jobs.

# Existence of No Carry-In Instant

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 arrival sequence with consistent arrivals.

Variable arr_seq : arrival_sequence Job.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.

Next, consider any ideal uniprocessor schedule of this arrival sequence ...

Variable sched : schedule (ideal.processor_state Job).

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 JLFP policy.

For simplicity, let's define some local names.

Let job_pending_at := pending sched.

Let job_completed_by := completed_by sched.

Let arrivals_between := arrivals_between arr_seq.

Let no_carry_in := no_carry_in arr_seq sched.

Let quiet_time := quiet_time arr_seq sched.

Let job_completed_by := completed_by sched.

Let arrivals_between := arrivals_between arr_seq.

Let no_carry_in := no_carry_in arr_seq sched.

Let quiet_time := quiet_time arr_seq sched.

Further, allow for any work-bearing notion of job readiness.

Context `{@JobReady Job (ideal.processor_state Job) Cost Arrival}.

Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.

Assume that the schedule is work-conserving, ...

... and there are no duplicate job arrivals.

We show that an idle time implies no carry in at this time instant.

Moreover, an idle time implies no carry in at the next time instant.

Let the priority relation be reflexive.

Recall the notion of workload of all jobs released in a given interval

`[t1, t2)`

...
... and total service of jobs within some time interval

`[t1, t2)`

.
Assume that for some positive Δ, the sum of requested workload
at time t + Δ is bounded by Δ (i.e., the supply). 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 + Δ) ≤ Δ.

Next we prove that, since for any time instant t there is a
point where the total workload is upper-bounded by the supply,
the processor encounters no-carry-in instants at least every Δ
time units.

We start by proving that the processor has no carry-in at the
beginning (i.e., has no carry-in at time instant 0).

In this section, we prove 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 the processor has 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 (t.+1 + δ).

total_service t (t + Δ) < Δ →

∃ δ, δ < Δ ∧ no_carry_in (t.+1 + δ).

In the second case, the total service within the time
interval

`[t, t + Δ)`

is equal to Δ. On the other hand,
we 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 (t + Δ).

End ProcessorIsNotTooBusyInduction.

total_service t (t + Δ) = Δ →

no_carry_in (t + Δ).

End ProcessorIsNotTooBusyInduction.

Finally, we show that any interval of length Δ contains a time instant with no carry-in.

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.