Library prosa.classic.model.schedule.uni.limited.busy_interval
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.limited.platform.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require Import prosa.classic.model.arrival.basic.task
prosa.classic.model.arrival.basic.job
prosa.classic.model.arrival.basic.arrival_sequence
prosa.classic.model.priority
prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.uni.service
prosa.classic.model.schedule.uni.workload
prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.limited.platform.definitions.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Busy Interval for JLFP-models
In this module we define the notion of busy intervals for uniprocessor for JLFP schedulers.
Module BusyIntervalJLFP.
Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform Service Workload TaskArrival.
Section Definitions.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Variable higher_eq_priority: JLFP_policy Job.
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.
Let job_remaining_cost j t := remaining_cost job_cost sched j t.
Let arrivals_between := jobs_arrived_between arr_seq.
Section BusyInterval.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
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.
Definition busy_interval_prefix (t1 t_busy: time) :=
t1 < t_busy ∧
quiet_time t1 ∧
(∀ t, t1 < t < t_busy → ¬ quiet_time t) ∧
t1 ≤ job_arrival j < t_busy.
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
End BusyInterval.
Section JobPriorityInversionBound.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
Definition is_priority_inversion t :=
if sched t is Some jlp then
~~ higher_eq_priority jlp j
else false.
Definition cumulative_priority_inversion t1 t2 :=
\sum_(t1 ≤ t < t2) is_priority_inversion t.
Definition priority_inversion_of_job_is_bounded_by (B: time) :=
∀ (t1 t2: time),
busy_interval_prefix j t1 t2 →
cumulative_priority_inversion t1 t2 ≤ B.
End JobPriorityInversionBound.
Section TaskPriorityInversionBound.
Variable tsk: Task.
Definition priority_inversion_is_bounded_by (B: time) :=
∀ (j: Job),
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
priority_inversion_of_job_is_bounded_by j B.
End TaskPriorityInversionBound.
Section DecidableQuietTime.
Definition quiet_time_dec (j : Job) (t : time) :=
all
(fun j_hp ⇒ higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
(jobs_arrived_before arr_seq t).
Lemma quiet_time_P :
∀ j t, reflect (quiet_time j t) (quiet_time_dec j t).
End DecidableQuietTime.
Section Lemmas.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Let quiet_time t1 := quiet_time j t1.
Let busy_interval_prefix t1 t2 := busy_interval_prefix j t1 t2.
Let busy_interval t1 t2 := busy_interval j t1 t2.
Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by j K.
Section BasicLemma.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End BasicLemma.
Section ExistsPendingJob.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Variable t1 t2: time.
Hypothesis H_interval: t1 ≤ t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ¬ quiet_time t2.
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.
Section ProcessorAlwaysBusy.
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.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval_prefix: busy_interval_prefix t1 t2.
Lemma idle_time_implies_quiet_time_at_the_next_time_instant:
∀ t,
is_idle sched t →
quiet_time t.+1.
Lemma pending_hp_job_exists:
∀ t,
t1 ≤ t < t2 →
∃ jhp,
arrives_in arr_seq jhp ∧
job_pending_at jhp t ∧
higher_eq_priority jhp j.
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t < t2 →
¬ is_idle sched t.
End ProcessorAlwaysBusy.
Section QuietTimeAndServiceOfJobs.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Variable t1: time.
Hypothesis H_quiet_time: quiet_time t1.
Variable Δ: time.
Hypothesis H_no_quiet_time: ∀ t, t1 < t ≤ t1 + Δ → ¬ quiet_time t.
Let service_received_by_hep_jobs_released_during t_beg t_end :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t_beg t_end) higher_eq_priority j t1 (t1 + Δ).
Lemma hep_jobs_receive_no_service_before_quiet_time:
service_received_by_hep_jobs_released_during t1 (t1 + Δ) =
service_received_by_hep_jobs_released_during 0 (t1 + Δ).
Lemma no_idle_time_within_non_quiet_time_interval:
service_of_jobs sched (arrivals_between 0 (t1 + Δ)) predT t1 (t1 + Δ) = Δ.
End QuietTimeAndServiceOfJobs.
Section BoundingBusyInterval.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs
job_cost (arrivals_between t1 t2) higher_eq_priority j.
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t1 t2) higher_eq_priority j t1 t2.
Section BoundingBusyInterval.
Variable t_busy: time.
Hypothesis H_j_is_pending: job_pending_at j t_busy.
Section LowerBound.
Lemma exists_busy_interval_prefix:
∃ t1,
busy_interval_prefix t1 t_busy.+1 ∧
t1 ≤ job_arrival j ≤ t_busy.
End LowerBound.
Section UpperBound.
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
priority_inversion_bound + hp_workload t1 (t1 + delta) ≤ delta.
Section CannotBeBusyForSoLong.
Hypothesis H_no_quiet_time:
∀ t, t1 < t ≤ t1 + delta → ¬ quiet_time t.
Lemma busy_interval_has_uninterrupted_service:
delta ≤ priority_inversion_bound + hp_service t1 (t1 + delta).
Lemma busy_interval_too_much_workload:
hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
Corollary busy_interval_workload_larger_than_interval:
priority_inversion_bound + hp_workload t1 (t1 + delta) > delta.
End CannotBeBusyForSoLong.
Lemma busy_interval_is_bounded:
∃ t2,
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End UpperBound.
End BoundingBusyInterval.
Section BusyIntervalFromWorkloadBound.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, priority_inversion_bound + hp_workload t (t + delta) ≤ delta.
Hypothesis H_positive_cost: job_cost j > 0.
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
Section ResponseTimeBoundFromBusyInterval.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, priority_inversion_bound + hp_workload t (t + delta) ≤ delta.
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
Section NonOverloadedProcessor.
Definition no_carry_in (t: time) :=
∀ j_o,
arrives_in arr_seq j_o →
arrived_before job_arrival j_o t →
job_completed_by j_o t.
Lemma no_carry_in_implies_quiet_time :
∀ j t,
no_carry_in t →
quiet_time j t.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Lemma idle_instant_implies_no_carry_in_at_t :
∀ t,
is_idle sched t →
no_carry_in t.
Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
∀ t,
is_idle sched t →
no_carry_in t.+1.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) predT.
Let total_service t1 t2 :=
service_of_jobs sched (arrivals_between 0 t2) predT t1 t2.
Variable Δ: time.
Hypothesis H_delta_positive: Δ > 0.
Hypothesis H_workload_is_bounded: ∀ t, total_workload t (t + Δ) ≤ Δ.
Section ProcessorIsNotTooBusy.
Lemma no_carry_in_at_the_beginning :
no_carry_in 0.
Section ProcessorIsNotTooBusyInduction.
Variable t: time.
Hypothesis H_no_carry_in: no_carry_in t.
Lemma total_service_is_bounded_by_Δ :
total_service t (t + Δ) ≤ Δ.
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ no_carry_in (t.+1 + δ).
Lemma completion_of_all_jobs_implies_no_carry_in :
total_service t (t + Δ) = Δ →
no_carry_in (t + Δ).
End ProcessorIsNotTooBusyInduction.
Lemma processor_is_not_too_busy :
∀ t, ∃ δ, δ < Δ ∧ no_carry_in (t + δ).
End ProcessorIsNotTooBusy.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Corollary exists_busy_interval_from_total_workload_bound :
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + Δ ∧
busy_interval j t1 t2.
End NonOverloadedProcessor.
End Definitions.
End BusyIntervalJLFP.
Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform Service Workload TaskArrival.
Section Definitions.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → Task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
Variable sched: schedule Job.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched arr_seq.
Variable higher_eq_priority: JLFP_policy Job.
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.
Let job_remaining_cost j t := remaining_cost job_cost sched j t.
Let arrivals_between := jobs_arrived_between arr_seq.
Section BusyInterval.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
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.
Definition busy_interval_prefix (t1 t_busy: time) :=
t1 < t_busy ∧
quiet_time t1 ∧
(∀ t, t1 < t < t_busy → ¬ quiet_time t) ∧
t1 ≤ job_arrival j < t_busy.
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
End BusyInterval.
Section JobPriorityInversionBound.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
Definition is_priority_inversion t :=
if sched t is Some jlp then
~~ higher_eq_priority jlp j
else false.
Definition cumulative_priority_inversion t1 t2 :=
\sum_(t1 ≤ t < t2) is_priority_inversion t.
Definition priority_inversion_of_job_is_bounded_by (B: time) :=
∀ (t1 t2: time),
busy_interval_prefix j t1 t2 →
cumulative_priority_inversion t1 t2 ≤ B.
End JobPriorityInversionBound.
Section TaskPriorityInversionBound.
Variable tsk: Task.
Definition priority_inversion_is_bounded_by (B: time) :=
∀ (j: Job),
arrives_in arr_seq j →
job_task j = tsk →
job_cost j > 0 →
priority_inversion_of_job_is_bounded_by j B.
End TaskPriorityInversionBound.
Section DecidableQuietTime.
Definition quiet_time_dec (j : Job) (t : time) :=
all
(fun j_hp ⇒ higher_eq_priority j_hp j ==> (completed_by job_cost sched j_hp t))
(jobs_arrived_before arr_seq t).
Lemma quiet_time_P :
∀ j t, reflect (quiet_time j t) (quiet_time_dec j t).
End DecidableQuietTime.
Section Lemmas.
Variable tsk: Task.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_task: job_task j = tsk.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Let quiet_time t1 := quiet_time j t1.
Let busy_interval_prefix t1 t2 := busy_interval_prefix j t1 t2.
Let busy_interval t1 t2 := busy_interval j t1 t2.
Let is_priority_inversion_bounded_by K := priority_inversion_of_job_is_bounded_by j K.
Section BasicLemma.
Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End BasicLemma.
Section ExistsPendingJob.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Variable t1 t2: time.
Hypothesis H_interval: t1 ≤ t2.
Hypothesis H_quiet: quiet_time t1.
Hypothesis H_not_quiet: ¬ quiet_time t2.
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.
Section ProcessorAlwaysBusy.
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.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval_prefix: busy_interval_prefix t1 t2.
Lemma idle_time_implies_quiet_time_at_the_next_time_instant:
∀ t,
is_idle sched t →
quiet_time t.+1.
Lemma pending_hp_job_exists:
∀ t,
t1 ≤ t < t2 →
∃ jhp,
arrives_in arr_seq jhp ∧
job_pending_at jhp t ∧
higher_eq_priority jhp j.
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t < t2 →
¬ is_idle sched t.
End ProcessorAlwaysBusy.
Section QuietTimeAndServiceOfJobs.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Variable t1: time.
Hypothesis H_quiet_time: quiet_time t1.
Variable Δ: time.
Hypothesis H_no_quiet_time: ∀ t, t1 < t ≤ t1 + Δ → ¬ quiet_time t.
Let service_received_by_hep_jobs_released_during t_beg t_end :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t_beg t_end) higher_eq_priority j t1 (t1 + Δ).
Lemma hep_jobs_receive_no_service_before_quiet_time:
service_received_by_hep_jobs_released_during t1 (t1 + Δ) =
service_received_by_hep_jobs_released_during 0 (t1 + Δ).
Lemma no_idle_time_within_non_quiet_time_interval:
service_of_jobs sched (arrivals_between 0 (t1 + Δ)) predT t1 (t1 + Δ) = Δ.
End QuietTimeAndServiceOfJobs.
Section BoundingBusyInterval.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Let hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs
job_cost (arrivals_between t1 t2) higher_eq_priority j.
Let hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs
sched (arrivals_between t1 t2) higher_eq_priority j t1 t2.
Section BoundingBusyInterval.
Variable t_busy: time.
Hypothesis H_j_is_pending: job_pending_at j t_busy.
Section LowerBound.
Lemma exists_busy_interval_prefix:
∃ t1,
busy_interval_prefix t1 t_busy.+1 ∧
t1 ≤ job_arrival j ≤ t_busy.
End LowerBound.
Section UpperBound.
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
priority_inversion_bound + hp_workload t1 (t1 + delta) ≤ delta.
Section CannotBeBusyForSoLong.
Hypothesis H_no_quiet_time:
∀ t, t1 < t ≤ t1 + delta → ¬ quiet_time t.
Lemma busy_interval_has_uninterrupted_service:
delta ≤ priority_inversion_bound + hp_service t1 (t1 + delta).
Lemma busy_interval_too_much_workload:
hp_workload t1 (t1 + delta) > hp_service t1 (t1 + delta).
Corollary busy_interval_workload_larger_than_interval:
priority_inversion_bound + hp_workload t1 (t1 + delta) > delta.
End CannotBeBusyForSoLong.
Lemma busy_interval_is_bounded:
∃ t2,
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End UpperBound.
End BoundingBusyInterval.
Section BusyIntervalFromWorkloadBound.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, priority_inversion_bound + hp_workload t (t + delta) ≤ delta.
Hypothesis H_positive_cost: job_cost j > 0.
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
Section ResponseTimeBoundFromBusyInterval.
Variable priority_inversion_bound: time.
Hypothesis H_priority_inversion_is_bounded:
is_priority_inversion_bounded_by priority_inversion_bound.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, priority_inversion_bound + hp_workload t (t + delta) ≤ delta.
Lemma busy_interval_bounds_response_time:
job_completed_by j (job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
Section NonOverloadedProcessor.
Definition no_carry_in (t: time) :=
∀ j_o,
arrives_in arr_seq j_o →
arrived_before job_arrival j_o t →
job_completed_by j_o t.
Lemma no_carry_in_implies_quiet_time :
∀ j t,
no_carry_in t →
quiet_time j t.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
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.
Lemma idle_instant_implies_no_carry_in_at_t :
∀ t,
is_idle sched t →
no_carry_in t.
Lemma idle_instant_implies_no_carry_in_at_t_pl_1 :
∀ t,
is_idle sched t →
no_carry_in t.+1.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Let total_workload t1 t2 :=
workload_of_jobs job_cost (arrivals_between t1 t2) predT.
Let total_service t1 t2 :=
service_of_jobs sched (arrivals_between 0 t2) predT t1 t2.
Variable Δ: time.
Hypothesis H_delta_positive: Δ > 0.
Hypothesis H_workload_is_bounded: ∀ t, total_workload t (t + Δ) ≤ Δ.
Section ProcessorIsNotTooBusy.
Lemma no_carry_in_at_the_beginning :
no_carry_in 0.
Section ProcessorIsNotTooBusyInduction.
Variable t: time.
Hypothesis H_no_carry_in: no_carry_in t.
Lemma total_service_is_bounded_by_Δ :
total_service t (t + Δ) ≤ Δ.
Lemma low_total_service_implies_existence_of_time_with_no_carry_in :
total_service t (t + Δ) < Δ →
∃ δ, δ < Δ ∧ no_carry_in (t.+1 + δ).
Lemma completion_of_all_jobs_implies_no_carry_in :
total_service t (t + Δ) = Δ →
no_carry_in (t + Δ).
End ProcessorIsNotTooBusyInduction.
Lemma processor_is_not_too_busy :
∀ t, ∃ δ, δ < Δ ∧ no_carry_in (t + δ).
End ProcessorIsNotTooBusy.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
Corollary exists_busy_interval_from_total_workload_bound :
∃ t1 t2,
t1 ≤ job_arrival j < t2 ∧
t2 ≤ t1 + Δ ∧
busy_interval j t1 t2.
End NonOverloadedProcessor.
End Definitions.
End BusyIntervalJLFP.