Library prosa.classic.model.schedule.uni.jitter.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.
Require Import prosa.classic.model.schedule.uni.jitter.schedule prosa.classic.model.schedule.uni.jitter.platform.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module BusyInterval.
Import Job UniprocessorScheduleWithJitter Priority Platform
Service Workload TaskArrival.
Section Defs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: 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.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Let job_pending_at := pending job_arrival job_cost job_jitter sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Definition quiet_time (t: time) :=
∀ j_hp,
arrives_in arr_seq j_hp →
higher_eq_priority j_hp j →
actual_arrival_before job_arrival job_jitter 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).
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
Section Lemmas.
Let actual_arrivals t1 t2 := actual_arrivals_between job_arrival job_jitter arr_seq t1 t2.
Section BasicLemmas.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
Variable t: time.
Hypothesis H_during_interval: t1 ≤ t < t2.
Hypothesis H_job_is_pending: job_pending_at j t.
Section CompletesDuringBusyInterval.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End CompletesDuringBusyInterval.
Section ArrivesDuringBusyInterval.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Lemma job_arrives_within_busy_interval:
t1 ≤ actual_job_arrival j.
End ArrivesDuringBusyInterval.
End BasicLemmas.
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 ∧
actual_job_arrival_between 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 job_jitter arr_seq sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
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.
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t ≤ t2 →
¬ is_idle sched t.
Section OnlyHigherOrEqualPriority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 ≤ t < t2 →
∃ j_hp,
actual_job_arrival_between j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
job_scheduled_at j_hp t.
End OnlyHigherOrEqualPriority.
End ProcessorAlwaysBusy.
Section BoundingBusyInterval.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Let actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs job_cost (actual_arrivals t1 t2)
higher_eq_priority j.
Let actual_hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs sched (actual_arrivals 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 ≤ actual_job_arrival j ≤ t_busy.
End LowerBound.
Section UpperBound.
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Hypothesis H_busy_prefix_contains_arrival: actual_job_arrival j ≥ t1.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded: actual_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:
actual_hp_service t1 (t1 + delta) = delta.
Lemma busy_interval_too_much_workload:
actual_hp_workload t1 (t1 + delta) > actual_hp_service t1 (t1 + delta).
Corollary busy_interval_workload_larger_than_interval:
actual_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 delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, actual_hp_workload t (t + delta) ≤ delta.
Hypothesis H_positive_cost: job_cost j > 0.
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ actual_job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
Section ResponseTimeBoundFromBusyInterval.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t,
actual_hp_workload t (t + delta) ≤ delta.
Lemma busy_interval_bounds_response_time:
job_completed_by j (actual_job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
End Defs.
End BusyInterval.
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.
Require Import prosa.classic.model.schedule.uni.jitter.schedule prosa.classic.model.schedule.uni.jitter.platform.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module BusyInterval.
Import Job UniprocessorScheduleWithJitter Priority Platform
Service Workload TaskArrival.
Section Defs.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_jitter: 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.
Variable j: Job.
Hypothesis H_from_arrival_sequence: arrives_in arr_seq j.
Let job_pending_at := pending job_arrival job_cost job_jitter sched.
Let job_scheduled_at := scheduled_at sched.
Let job_completed_by := completed_by job_cost sched.
Let actual_job_arrival := actual_arrival job_arrival job_jitter.
Let actual_job_arrival_between := actual_arrival_between job_arrival job_jitter.
Definition quiet_time (t: time) :=
∀ j_hp,
arrives_in arr_seq j_hp →
higher_eq_priority j_hp j →
actual_arrival_before job_arrival job_jitter 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).
Definition busy_interval (t1 t2: time) :=
busy_interval_prefix t1 t2 ∧
quiet_time t2.
Section Lemmas.
Let actual_arrivals t1 t2 := actual_arrivals_between job_arrival job_jitter arr_seq t1 t2.
Section BasicLemmas.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Variable t1 t2: time.
Hypothesis H_busy_interval: busy_interval t1 t2.
Variable t: time.
Hypothesis H_during_interval: t1 ≤ t < t2.
Hypothesis H_job_is_pending: job_pending_at j t.
Section CompletesDuringBusyInterval.
Lemma job_completes_within_busy_interval:
job_completed_by j t2.
End CompletesDuringBusyInterval.
Section ArrivesDuringBusyInterval.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
Lemma job_arrives_within_busy_interval:
t1 ≤ actual_job_arrival j.
End ArrivesDuringBusyInterval.
End BasicLemmas.
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 ∧
actual_job_arrival_between 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 job_jitter arr_seq sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
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.
Lemma not_quiet_implies_not_idle:
∀ t,
t1 ≤ t ≤ t2 →
¬ is_idle sched t.
Section OnlyHigherOrEqualPriority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 ≤ t < t2 →
∃ j_hp,
actual_job_arrival_between j_hp t1 t2 ∧
higher_eq_priority j_hp j ∧
job_scheduled_at j_hp t.
End OnlyHigherOrEqualPriority.
End ProcessorAlwaysBusy.
Section BoundingBusyInterval.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_is_a_set arr_seq.
Hypothesis H_jobs_execute_after_jitter:
jobs_execute_after_jitter job_arrival job_jitter sched.
Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
Hypothesis H_respects_policy:
respects_JLFP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
Let actual_hp_workload t1 t2 :=
workload_of_higher_or_equal_priority_jobs job_cost (actual_arrivals t1 t2)
higher_eq_priority j.
Let actual_hp_service t1 t2 :=
service_of_higher_or_equal_priority_jobs sched (actual_arrivals 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 ≤ actual_job_arrival j ≤ t_busy.
End LowerBound.
Section UpperBound.
Variable t1: time.
Hypothesis H_is_busy_prefix: busy_interval_prefix t1 t_busy.+1.
Hypothesis H_busy_prefix_contains_arrival: actual_job_arrival j ≥ t1.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded: actual_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:
actual_hp_service t1 (t1 + delta) = delta.
Lemma busy_interval_too_much_workload:
actual_hp_workload t1 (t1 + delta) > actual_hp_service t1 (t1 + delta).
Corollary busy_interval_workload_larger_than_interval:
actual_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 delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t, actual_hp_workload t (t + delta) ≤ delta.
Hypothesis H_positive_cost: job_cost j > 0.
Corollary exists_busy_interval:
∃ t1 t2,
t1 ≤ actual_job_arrival j < t2 ∧
t2 ≤ t1 + delta ∧
busy_interval t1 t2.
End BusyIntervalFromWorkloadBound.
Section ResponseTimeBoundFromBusyInterval.
Variable delta: time.
Hypothesis H_delta_positive: delta > 0.
Hypothesis H_workload_is_bounded:
∀ t,
actual_hp_workload t (t + delta) ≤ delta.
Lemma busy_interval_bounds_response_time:
job_completed_by j (actual_job_arrival j + delta).
End ResponseTimeBoundFromBusyInterval.
End BoundingBusyInterval.
End Lemmas.
End Defs.
End BusyInterval.