Library prosa.classic.analysis.apa.interference_bound_edf
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.platform prosa.classic.model.schedule.apa.interference
prosa.classic.model.schedule.apa.interference_edf prosa.classic.model.schedule.apa.affinity.
Require Import prosa.classic.analysis.apa.workload_bound prosa.classic.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDF.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
WorkloadBound ResponseTime Priority Affinity
TaskArrival Interference InterferenceEDF.
Export InterferenceBoundGeneric.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable tsk: sporadic_task.
Variable delta: time.
Variable tsk_other: sporadic_task.
Variable R_other: time.
Definition edf_specific_interference_bound :=
let d_tsk := task_deadline tsk in
let e_other := task_cost tsk_other in
let p_other := task_period tsk_other in
let d_other := task_deadline tsk_other in
(div_floor d_tsk p_other) × e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other)).
End SpecificBoundDef.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
Let task_with_response_time := (sporadic_task × time)%type.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable R_prev: seq task_with_response_time.
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
Let basic_interference_bound := interference_bound_generic task_cost task_period tsk delta tsk_R.
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
Section TotalInterference.
Let other_task_in alpha' := different_task_in alpha tsk alpha'.
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task_in alpha' tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
Section ProofSpecificBound.
Import Schedule Interference Platform SporadicTaskset Affinity.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Variable num_cpus: nat.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched 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_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_edf_weak_APA_scheduler:
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
sched alpha (EDF job_arrival job_deadline).
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
Variable j_i: Job.
Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
Variable R_k: time.
Hypothesis H_R_k_le_deadline: R_k ≤ task_deadline tsk_k.
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
Hypothesis H_all_previous_jobs_completed_on_time :
∀ j_k,
arrives_in arr_seq j_k →
job_task j_k = tsk_k →
job_arrival j_k + R_k < job_arrival j_i + delta →
completed job_cost sched j_k (job_arrival j_k + R_k).
Section MainProof.
Let x :=
task_interference job_arrival job_cost job_task sched alpha j_i
tsk_k (job_arrival j_i) (job_arrival j_i + delta).
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline tsk_i tsk_k R_k.
Let t1 := job_arrival j_i.
Let t2 := job_arrival j_i + delta.
Let D_i := task_deadline tsk_i.
Let D_k := task_deadline tsk_k.
Let p_k := task_period tsk_k.
Let n_k := div_floor D_i p_k.
Let interference_caused_by := job_interference job_arrival job_cost job_task sched alpha j_i.
Let interfering_jobs :=
filter (fun j' ⇒ (job_task j' == tsk_k) && (interference_caused_by j' t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival interfering_jobs.
Section SimplifyJobSequence.
Lemma interference_bound_edf_use_another_definition :
x ≤ \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2 =
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2.
Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j \in sorted_jobs →
arrives_in arr_seq j ∧
job_task j = tsk_k ∧
interference_caused_by j t1 t2 != 0 ∧
j \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j \in interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
End SimplifyJobSequence.
Section InterferenceFewJobs.
Hypothesis H_few_jobs: size sorted_jobs ≤ n_k.
Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2 ≤
interference_bound.
End InterferenceFewJobs.
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
Section FactsAboutFirstJob.
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
completed job_cost sched j_fst (a_fst + R_k) →
t1 ≤ a_fst + R_k.
End FactsAboutFirstJob.
Section InterferenceSingleJob.
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_simpl_when_there's_one_job :
D_i %% p_k - (D_k - R_k) = D_i - (D_k - R_k).
Section ResponseTimeOfSingleJobBounded.
Hypothesis H_j_fst_completed_by_rt_bound :
completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
job_interference job_arrival job_cost job_task sched alpha j_i j_fst t1 t2
≤ D_i - (D_k - R_k).
End ResponseTimeOfSingleJobBounded.
Section ResponseTimeOfSingleJobNotBounded.
Hypothesis H_j_fst_not_complete_by_rt_bound :
~~ completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
job_arrival j_fst + R_k ≥ job_arrival j_i + delta.
Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
D_i < D_k - R_k →
interference_caused_by j_fst t1 t2 = 0.
Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
D_i ≥ D_k - R_k →
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k).
End ResponseTimeOfSingleJobNotBounded.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k).
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
End InterferenceSingleJob.
Section InterferenceTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
Section FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k:
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + R_k).
End FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k ≥ num_mid_jobs.+1.
Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
interference_caused_by j_lst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
≤ n_k × task_cost tsk_k.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Section InterferenceOfFirstJob.
Lemma interference_bound_edf_remainder_ge_slack :
D_k - R_k ≤ D_i %% p_k.
Lemma interference_bound_edf_simpl_by_moving_to_left_side :
interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k ≤ D_i →
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k).
Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
interference_caused_by j_fst t1 t2 ≤ \sum_(t1 ≤ t < a_fst + R_k) 1.
Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k ≤
\sum_(t1 ≤ t < a_fst + R_k) 1
+ \sum_(a_fst + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1.
Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
\sum_(t1 ≤ t < a_fst + R_k) 1
+ \sum_(a_fst + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k).
End InterferenceOfFirstJob.
Lemma interference_bound_edf_holds_for_multiple_jobs :
\sum_(0 ≤ i < num_mid_jobs.+2)
interference_caused_by (nth elem sorted_jobs i) t1 t2 ≤ interference_bound.
End InterferenceTwoOrMoreJobs.
End InterferenceManyJobs.
Theorem interference_bound_edf_bounds_interference :
x ≤ interference_bound.
End MainProof.
End ProofSpecificBound.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
Variable delta delta' R R': time.
Hypothesis H_delta_monotonic: delta ≤ delta'.
Hypothesis H_response_time_monotonic: R ≤ R'.
Hypothesis H_cost_le_rt_bound: task_cost tsk_other ≤ R.
Lemma interference_bound_edf_monotonic :
interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) ≤
interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
End MonotonicitySpecificBound.
End InterferenceBoundEDF.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.workload prosa.classic.model.schedule.global.response_time
prosa.classic.model.schedule.global.schedulability.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.platform prosa.classic.model.schedule.apa.interference
prosa.classic.model.schedule.apa.interference_edf prosa.classic.model.schedule.apa.affinity.
Require Import prosa.classic.analysis.apa.workload_bound prosa.classic.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div path.
Module InterferenceBoundEDF.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
WorkloadBound ResponseTime Priority Affinity
TaskArrival Interference InterferenceEDF.
Export InterferenceBoundGeneric.
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable tsk: sporadic_task.
Variable delta: time.
Variable tsk_other: sporadic_task.
Variable R_other: time.
Definition edf_specific_interference_bound :=
let d_tsk := task_deadline tsk in
let e_other := task_cost tsk_other in
let p_other := task_period tsk_other in
let d_other := task_deadline tsk_other in
(div_floor d_tsk p_other) × e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_other)).
End SpecificBoundDef.
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
Let task_with_response_time := (sporadic_task × time)%type.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable R_prev: seq task_with_response_time.
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
Let basic_interference_bound := interference_bound_generic task_cost task_period tsk delta tsk_R.
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
Section TotalInterference.
Let other_task_in alpha' := different_task_in alpha tsk alpha'.
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task_in alpha' tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
Section ProofSpecificBound.
Import Schedule Interference Platform SporadicTaskset Affinity.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period job_arrival job_task arr_seq.
Hypothesis H_valid_job_parameters:
∀ j,
arrives_in arr_seq j →
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
Variable num_cpus: nat.
Variable sched: schedule Job num_cpus.
Hypothesis H_jobs_come_from_arrival_sequence:
jobs_come_from_arrival_sequence sched 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_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ j, arrives_in arr_seq j → job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk \in ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched tsk.
Hypothesis H_work_conserving: apa_work_conserving job_arrival job_cost job_task arr_seq
sched alpha.
Hypothesis H_edf_weak_APA_scheduler:
respects_JLFP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
sched alpha (EDF job_arrival job_deadline).
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i \in ts.
Variable j_i: Job.
Hypothesis H_j_i_arrives: arrives_in arr_seq j_i.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k \in ts.
Variable R_k: time.
Hypothesis H_R_k_le_deadline: R_k ≤ task_deadline tsk_k.
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
Hypothesis H_all_previous_jobs_completed_on_time :
∀ j_k,
arrives_in arr_seq j_k →
job_task j_k = tsk_k →
job_arrival j_k + R_k < job_arrival j_i + delta →
completed job_cost sched j_k (job_arrival j_k + R_k).
Section MainProof.
Let x :=
task_interference job_arrival job_cost job_task sched alpha j_i
tsk_k (job_arrival j_i) (job_arrival j_i + delta).
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline tsk_i tsk_k R_k.
Let t1 := job_arrival j_i.
Let t2 := job_arrival j_i + delta.
Let D_i := task_deadline tsk_i.
Let D_k := task_deadline tsk_k.
Let p_k := task_period tsk_k.
Let n_k := div_floor D_i p_k.
Let interference_caused_by := job_interference job_arrival job_cost job_task sched alpha j_i.
Let interfering_jobs :=
filter (fun j' ⇒ (job_task j' == tsk_k) && (interference_caused_by j' t1 t2 != 0))
(jobs_scheduled_between sched t1 t2).
Let earlier_arrival := fun x y ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := sort earlier_arrival interfering_jobs.
Section SimplifyJobSequence.
Lemma interference_bound_edf_use_another_definition :
x ≤ \sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2.
Lemma interference_bound_edf_simpl_by_filtering_interfering_jobs :
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_k)
interference_caused_by j t1 t2 =
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2.
Lemma interference_bound_edf_simpl_by_sorting_interfering_jobs :
\sum_(j <- interfering_jobs) interference_caused_by j t1 t2 =
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2.
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j \in interfering_jobs) = (j \in sorted_jobs).
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j \in sorted_jobs →
arrives_in arr_seq j ∧
job_task j = tsk_k ∧
interference_caused_by j t1 t2 != 0 ∧
j \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_jobs_ordered_by_arrival :
∀ i elem,
i < (size sorted_jobs).-1 →
earlier_arrival (nth elem sorted_jobs i) (nth elem sorted_jobs i.+1).
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j \in interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
End SimplifyJobSequence.
Section InterferenceFewJobs.
Hypothesis H_few_jobs: size sorted_jobs ≤ n_k.
Lemma interference_bound_edf_holds_for_at_most_n_k_jobs :
\sum_(j <- sorted_jobs) interference_caused_by j t1 t2 ≤
interference_bound.
End InterferenceFewJobs.
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
Variable elem: Job.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
Section FactsAboutFirstJob.
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
arrives_in arr_seq j_fst ∧
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 != 0 ∧
j_fst \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
Lemma interference_bound_edf_j_fst_completion_implies_rt_bound_inside_interval :
completed job_cost sched j_fst (a_fst + R_k) →
t1 ≤ a_fst + R_k.
End FactsAboutFirstJob.
Section InterferenceSingleJob.
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_simpl_when_there's_one_job :
D_i %% p_k - (D_k - R_k) = D_i - (D_k - R_k).
Section ResponseTimeOfSingleJobBounded.
Hypothesis H_j_fst_completed_by_rt_bound :
completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_holds_for_single_job_that_completes_on_time :
job_interference job_arrival job_cost job_task sched alpha j_i j_fst t1 t2
≤ D_i - (D_k - R_k).
End ResponseTimeOfSingleJobBounded.
Section ResponseTimeOfSingleJobNotBounded.
Hypothesis H_j_fst_not_complete_by_rt_bound :
~~ completed job_cost sched j_fst (a_fst + R_k).
Lemma interference_bound_edf_response_time_bound_of_j_fst_after_interval :
job_arrival j_fst + R_k ≥ job_arrival j_i + delta.
Lemma interference_bound_edf_holds_for_single_job_with_big_slack :
D_i < D_k - R_k →
interference_caused_by j_fst t1 t2 = 0.
Lemma interference_bound_edf_holds_for_single_job_with_small_slack :
D_i ≥ D_k - R_k →
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k).
End ResponseTimeOfSingleJobNotBounded.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_slack :
interference_caused_by j_fst t1 t2 ≤ D_i - (D_k - R_k).
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
End InterferenceSingleJob.
Section InterferenceTwoOrMoreJobs.
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
Section FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k:
arrives_in arr_seq j_lst ∧
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 != 0 ∧
j_lst \in jobs_scheduled_between sched t1 t2.
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + R_k).
End FactsAboutFirstAndLastJobs.
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Lemma interference_bound_edf_n_k_covers_middle_jobs_plus_one :
n_k ≥ num_mid_jobs.+1.
Lemma interference_bound_edf_holds_for_middle_and_last_jobs :
interference_caused_by j_lst t1 t2 +
\sum_(0 ≤ i < num_mid_jobs)
interference_caused_by (nth elem sorted_jobs i.+1) t1 t2
≤ n_k × task_cost tsk_k.
Lemma interference_bound_edf_n_k_equals_num_mid_jobs_plus_one :
n_k = num_mid_jobs.+1.
Section InterferenceOfFirstJob.
Lemma interference_bound_edf_remainder_ge_slack :
D_k - R_k ≤ D_i %% p_k.
Lemma interference_bound_edf_simpl_by_moving_to_left_side :
interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k ≤ D_i →
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k).
Lemma interference_bound_edf_interference_of_j_fst_bounded_by_response_time :
interference_caused_by j_fst t1 t2 ≤ \sum_(t1 ≤ t < a_fst + R_k) 1.
Lemma interference_bound_edf_bounding_interference_with_interval_lengths :
interference_caused_by j_fst t1 t2 + (D_k - R_k) + D_i %/ p_k × p_k ≤
\sum_(t1 ≤ t < a_fst + R_k) 1
+ \sum_(a_fst + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1.
Lemma interference_bound_edf_simpl_by_concatenation_of_intervals :
\sum_(t1 ≤ t < a_fst + R_k) 1
+ \sum_(a_fst + R_k ≤ t < a_fst + D_k) 1
+ \sum_(a_fst + D_k ≤ t < a_lst + D_k) 1 = (a_lst + D_k) - t1.
Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :
interference_caused_by j_fst t1 t2 ≤ D_i %% p_k - (D_k - R_k).
End InterferenceOfFirstJob.
Lemma interference_bound_edf_holds_for_multiple_jobs :
\sum_(0 ≤ i < num_mid_jobs.+2)
interference_caused_by (nth elem sorted_jobs i) t1 t2 ≤ interference_bound.
End InterferenceTwoOrMoreJobs.
End InterferenceManyJobs.
Theorem interference_bound_edf_bounds_interference :
x ≤ interference_bound.
End MainProof.
End ProofSpecificBound.
Section MonotonicitySpecificBound.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Variable tsk tsk_other: sporadic_task.
Hypothesis H_period_positive: task_period tsk_other > 0.
Variable delta delta' R R': time.
Hypothesis H_delta_monotonic: delta ≤ delta'.
Hypothesis H_response_time_monotonic: R ≤ R'.
Hypothesis H_cost_le_rt_bound: task_cost tsk_other ≤ R.
Lemma interference_bound_edf_monotonic :
interference_bound_edf task_cost task_period task_deadline tsk delta (tsk_other, R) ≤
interference_bound_edf task_cost task_period task_deadline tsk delta' (tsk_other, R').
End MonotonicitySpecificBound.
End InterferenceBoundEDF.