Library rt.analysis.parallel.interference_bound_edf
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
rt.model.basic.interference rt.model.basic.interference_edf.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
Module InterferenceBoundEDF.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
WorkloadBound ResponseTime Priority
SporadicTaskArrival Interference InterferenceEDF.
Export InterferenceBoundGeneric.
(* In this section, we define Bertogna and Cirinei's EDF-specific
interference bound. *)
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
(* Consider the interference incurred by tsk in a window of length delta... *)
Variable delta: time.
(* due to a different task tsk_other, with response-time bound R_other. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
(* Bertogna and Cirinei define the following bound for task interference
under EDF scheduling. *)
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_ceil (d_tsk + R_other - d_other + 1) p_other) × e_other.
End SpecificBoundDef.
(* Next, we define the total interference bound for EDF, which combines the generic
and the EDF-specific bounds. *)
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* By combining Bertogna's interference bound for a work-conserving
scheduler ... *)
Let basic_interference_bound := interference_bound_generic task_cost task_period delta tsk_R.
(* ... with and EDF-specific interference bound, ... *)
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
(* Bertogna and Cirinei define the following interference bound
under EDF scheduling. *)
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
(* Next we define the computation of the total interference for APA scheduling. *)
Section TotalInterference.
(* Let other_task denote tasks different from tsk. *)
Let other_task := different_task tsk.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences of the other tasks. *)
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
(* In this section, we show that the EDF-specific interference bound is safe. *)
Section ProofSpecificBound.
Import Schedule Interference Platform SporadicTaskset.
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_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs do not execute before their arrival times nor longer
than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume there exists at least one processor. *)
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that we have a task set where all tasks have valid
parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ (j: JobIn arr_seq), job_task j ∈ ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk ∈ ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume that the scheduler is a work-conserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_scheduler:
enforces_JLDP_policy job_cost sched (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i ∈ ts.
(* and j_i one of its jobs. *)
Variable j_i: JobIn arr_seq.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
(* Let tsk_k denote any interfering task, ... *)
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k ∈ ts.
(* ...and R_k its response-time bound. *)
Variable R_k: time.
Hypothesis H_R_k_le_deadline: R_k ≤ task_deadline tsk_k.
(* Consider a time window of length delta <= D_i, starting with j_i's arrival time. *)
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
(* Assume that the jobs of tsk_k satisfy the response-time bound before the end of the interval *)
Hypothesis H_all_previous_jobs_completed_on_time :
∀ (j_k: JobIn arr_seq),
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).
(* In this section, we prove that Bertogna and Cirinei's EDF interference bound
indeed bounds the interference caused by task tsk_k in the interval t1, t1 + delta). *)
Section MainProof.
(* Let's call x the task interference incurred by job j due to tsk_k. *)
Let x :=
task_interference job_cost job_task sched j_i
tsk_k (job_arrival j_i) (job_arrival j_i + delta).
(* Also, recall the EDF-specific interference bound for EDF. *)
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline tsk_i tsk_k R_k.
(* Let's simplify the names a bit. *)
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_ceil (D_i + R_k - D_k + 1) p_k.
(* Let's give a simpler name to job interference. *)
Let interference_caused_by := job_interference job_cost sched j_i.
(* Identify the subset of jobs that actually cause interference *)
Let interfering_jobs :=
filter (fun (x: JobIn arr_seq) ⇒
(job_task x = tsk_k) ∧ (interference_caused_by x t1 t2 ≠ 0))
(jobs_scheduled_between sched t1 t2).
(* Now, consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun (x y: JobIn arr_seq) ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival interfering_jobs).
(* Now we proceed with the proof.
The first step consists in simplifying the sum corresponding to the workload. *)
Section SimplifyJobSequence.
(* Use the alternative definition of task interference, based on
individual job interference. *)
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.
(* Remove the elements that we don't care about from the sum *)
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.
(* Then, we consider the sum over the sorted sequence of jobs. *)
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.
(* Note that both sequences have the same set of elements. *)
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j ∈ interfering_jobs) = (j ∈ sorted_jobs).
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j ∈ sorted_jobs →
job_task j = tsk_k ∧
interference_caused_by j t1 t2 ≠ 0 ∧
j ∈ jobs_scheduled_between sched t1 t2.
(* ...and consecutive jobs are ordered by arrival. *)
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).
(* Also, for any job of task tsk_k, the interference is bounded by the task cost. *)
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j ∈ interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
End SimplifyJobSequence.
(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)
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.
(* Otherwise, assume that the number of jobs is larger than n_k >= 0. *)
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
(* This trivially implies that there's at least one job. *)
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
(* Let j_fst be the first job, and a_fst its arrival time. *)
Variable elem: JobIn arr_seq.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
(* In this section, we prove some basic lemmas about j_fst. *)
Section FactsAboutFirstJob.
(* The first job is an interfering job of task tsk_k. *)
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 ≠ 0 ∧
j_fst ∈ jobs_scheduled_between sched t1 t2.
(* The deadline of j_fst is the deadline of tsk_k. *)
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
(* The deadline of j_i is the deadline of tsk_i. *)
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
(* If j_fst completes by its response-time bound, then t1 <= a_fst + R_k,
where t1 is the beginning of the time window (arrival of j_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.
(* Now, let's prove the interference bound for the particular case of a single job.
This case must be solved separately because the single job can simultaneously
be carry-in and carry-out job, so its response time is not necessarily
bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)
Section InterferenceSingleJob.
(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
End InterferenceSingleJob.
(* Next, consider the other case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)
Section InterferenceTwoOrMoreJobs.
(* Assume there are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
(* Let j_lst be the last job of the sequence and a_lst its arrival time. *)
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
(* In this section, we prove some basic lemmas about the first and last jobs. *)
Section FactsAboutFirstAndLastJobs.
(* The last job is an interfering job of task tsk_k. *)
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 ≠ 0 ∧
j_lst ∈ jobs_scheduled_between sched t1 t2.
(* The deadline of j_lst is the deadline of tsk_k. *)
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
(* The first job arrives before the last job. *)
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
(* The last job arrives before the end of the interval. *)
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
(* Since there are multiple jobs, j_fst is far enough from the end of
the interval that its response-time bound is valid
(by the assumption H_all_previous_jobs_completed_on_time). *)
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + R_k).
End FactsAboutFirstAndLastJobs.
(* Next, we prove that the distance between the first and last jobs is at least
num_mid_jobs + 1 periods. *)
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Lemma interference_bound_edf_slack_le_delta:
D_k - R_k ≤ D_i.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
middle jobs + 1, ... *)
Lemma interference_bound_edf_n_k_covers_all_jobs :
n_k ≥ num_mid_jobs.+2.
(* ... which allows bounding the interference of the middle and last jobs
using n_k multiplied by the cost. *)
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.
(* As required by the proof of convergence of EDF RTA, we show that the
EDF-specific bound is monotonically increasing with both the size
of the interval and the value of the previous response-time bounds. *)
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 rt.model.basic.task rt.model.basic.job rt.model.basic.schedule
rt.model.basic.task_arrival rt.model.basic.platform rt.model.basic.response_time
rt.model.basic.workload rt.model.basic.priority rt.model.basic.schedulability
rt.model.basic.interference rt.model.basic.interference_edf.
Require Import rt.analysis.parallel.workload_bound rt.analysis.parallel.interference_bound.
Module InterferenceBoundEDF.
Import Job SporadicTaskset Schedule ScheduleOfSporadicTask Schedulability
WorkloadBound ResponseTime Priority
SporadicTaskArrival Interference InterferenceEDF.
Export InterferenceBoundGeneric.
(* In this section, we define Bertogna and Cirinei's EDF-specific
interference bound. *)
Section SpecificBoundDef.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
(* Consider the interference incurred by tsk in a window of length delta... *)
Variable delta: time.
(* due to a different task tsk_other, with response-time bound R_other. *)
Variable tsk_other: sporadic_task.
Variable R_other: time.
(* Bertogna and Cirinei define the following bound for task interference
under EDF scheduling. *)
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_ceil (d_tsk + R_other - d_other + 1) p_other) × e_other.
End SpecificBoundDef.
(* Next, we define the total interference bound for EDF, which combines the generic
and the EDF-specific bounds. *)
Section TotalInterferenceBoundEDF.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Let tsk be the task to be analyzed. *)
Variable tsk: sporadic_task.
Let task_with_response_time := (sporadic_task × time)%type.
(* Assume a known response-time bound for each interfering task ... *)
Variable R_prev: seq task_with_response_time.
(* ... and an interval length delta. *)
Variable delta: time.
Section RecallInterferenceBounds.
Variable tsk_R: task_with_response_time.
Let tsk_other := fst tsk_R.
Let R_other := snd tsk_R.
(* By combining Bertogna's interference bound for a work-conserving
scheduler ... *)
Let basic_interference_bound := interference_bound_generic task_cost task_period delta tsk_R.
(* ... with and EDF-specific interference bound, ... *)
Let edf_specific_bound := edf_specific_interference_bound task_cost task_period task_deadline tsk tsk_other R_other.
(* Bertogna and Cirinei define the following interference bound
under EDF scheduling. *)
Definition interference_bound_edf :=
minn basic_interference_bound edf_specific_bound.
End RecallInterferenceBounds.
(* Next we define the computation of the total interference for APA scheduling. *)
Section TotalInterference.
(* Let other_task denote tasks different from tsk. *)
Let other_task := different_task tsk.
(* The total interference incurred by tsk is bounded by the sum
of individual task interferences of the other tasks. *)
Definition total_interference_bound_edf :=
\sum_((tsk_other, R_other) <- R_prev | other_task tsk_other)
interference_bound_edf (tsk_other, R_other).
End TotalInterference.
End TotalInterferenceBoundEDF.
(* In this section, we show that the EDF-specific interference bound is safe. *)
Section ProofSpecificBound.
Import Schedule Interference Platform SporadicTaskset.
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_cost: Job → time.
Variable job_deadline: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence... *)
Context {arr_seq: arrival_sequence Job}.
(* ... in which jobs arrive sporadically and have valid parameters. *)
Hypothesis H_sporadic_tasks:
sporadic_task_model task_period arr_seq job_task.
Hypothesis H_valid_job_parameters:
∀ (j: JobIn arr_seq),
valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.
(* Consider any schedule such that...*)
Variable num_cpus: nat.
Variable sched: schedule num_cpus arr_seq.
(* ...jobs do not execute before their arrival times nor longer
than their execution costs. *)
Hypothesis H_jobs_must_arrive_to_execute:
jobs_must_arrive_to_execute sched.
Hypothesis H_completed_jobs_dont_execute:
completed_jobs_dont_execute job_cost sched.
(* Assume there exists at least one processor. *)
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Assume that we have a task set where all tasks have valid
parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
∀ (j: JobIn arr_seq), job_task j ∈ ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
∀ tsk, tsk ∈ ts → task_deadline tsk ≤ task_period tsk.
Let no_deadline_is_missed_by_tsk (tsk: sporadic_task) :=
task_misses_no_deadline job_cost job_deadline job_task sched tsk.
Let response_time_bounded_by (tsk: sporadic_task) :=
is_response_time_bound_of_task job_cost job_task tsk sched.
(* Assume that the scheduler is a work-conserving EDF scheduler. *)
Hypothesis H_work_conserving: work_conserving job_cost sched.
Hypothesis H_edf_scheduler:
enforces_JLDP_policy job_cost sched (EDF job_deadline).
(* Let tsk_i be the task to be analyzed, ...*)
Variable tsk_i: sporadic_task.
Hypothesis H_tsk_i_in_task_set: tsk_i ∈ ts.
(* and j_i one of its jobs. *)
Variable j_i: JobIn arr_seq.
Hypothesis H_job_of_tsk_i: job_task j_i = tsk_i.
(* Let tsk_k denote any interfering task, ... *)
Variable tsk_k: sporadic_task.
Hypothesis H_tsk_k_in_task_set: tsk_k ∈ ts.
(* ...and R_k its response-time bound. *)
Variable R_k: time.
Hypothesis H_R_k_le_deadline: R_k ≤ task_deadline tsk_k.
(* Consider a time window of length delta <= D_i, starting with j_i's arrival time. *)
Variable delta: time.
Hypothesis H_delta_le_deadline: delta ≤ task_deadline tsk_i.
(* Assume that the jobs of tsk_k satisfy the response-time bound before the end of the interval *)
Hypothesis H_all_previous_jobs_completed_on_time :
∀ (j_k: JobIn arr_seq),
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).
(* In this section, we prove that Bertogna and Cirinei's EDF interference bound
indeed bounds the interference caused by task tsk_k in the interval t1, t1 + delta). *)
Section MainProof.
(* Let's call x the task interference incurred by job j due to tsk_k. *)
Let x :=
task_interference job_cost job_task sched j_i
tsk_k (job_arrival j_i) (job_arrival j_i + delta).
(* Also, recall the EDF-specific interference bound for EDF. *)
Let interference_bound :=
edf_specific_interference_bound task_cost task_period task_deadline tsk_i tsk_k R_k.
(* Let's simplify the names a bit. *)
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_ceil (D_i + R_k - D_k + 1) p_k.
(* Let's give a simpler name to job interference. *)
Let interference_caused_by := job_interference job_cost sched j_i.
(* Identify the subset of jobs that actually cause interference *)
Let interfering_jobs :=
filter (fun (x: JobIn arr_seq) ⇒
(job_task x = tsk_k) ∧ (interference_caused_by x t1 t2 ≠ 0))
(jobs_scheduled_between sched t1 t2).
(* Now, consider the list of interfering jobs sorted by arrival time. *)
Let earlier_arrival := fun (x y: JobIn arr_seq) ⇒ job_arrival x ≤ job_arrival y.
Let sorted_jobs := (sort earlier_arrival interfering_jobs).
(* Now we proceed with the proof.
The first step consists in simplifying the sum corresponding to the workload. *)
Section SimplifyJobSequence.
(* Use the alternative definition of task interference, based on
individual job interference. *)
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.
(* Remove the elements that we don't care about from the sum *)
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.
(* Then, we consider the sum over the sorted sequence of jobs. *)
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.
(* Note that both sequences have the same set of elements. *)
Lemma interference_bound_edf_job_in_same_sequence :
∀ j,
(j ∈ interfering_jobs) = (j ∈ sorted_jobs).
(* Also recall that all jobs in the sorted sequence is an interfering job of tsk_k, ... *)
Lemma interference_bound_edf_all_jobs_from_tsk_k :
∀ j,
j ∈ sorted_jobs →
job_task j = tsk_k ∧
interference_caused_by j t1 t2 ≠ 0 ∧
j ∈ jobs_scheduled_between sched t1 t2.
(* ...and consecutive jobs are ordered by arrival. *)
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).
(* Also, for any job of task tsk_k, the interference is bounded by the task cost. *)
Lemma interference_bound_edf_interference_le_task_cost :
∀ j,
j ∈ interfering_jobs →
interference_caused_by j t1 t2 ≤ task_cost tsk_k.
End SimplifyJobSequence.
(* Next, we show that if the number of jobs is no larger than n_k,
the workload bound trivially holds. *)
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.
(* Otherwise, assume that the number of jobs is larger than n_k >= 0. *)
Section InterferenceManyJobs.
Hypothesis H_many_jobs: n_k < size sorted_jobs.
(* This trivially implies that there's at least one job. *)
Lemma interference_bound_edf_at_least_one_job: size sorted_jobs > 0.
(* Let j_fst be the first job, and a_fst its arrival time. *)
Variable elem: JobIn arr_seq.
Let j_fst := nth elem sorted_jobs 0.
Let a_fst := job_arrival j_fst.
(* In this section, we prove some basic lemmas about j_fst. *)
Section FactsAboutFirstJob.
(* The first job is an interfering job of task tsk_k. *)
Lemma interference_bound_edf_j_fst_is_job_of_tsk_k :
job_task j_fst = tsk_k ∧
interference_caused_by j_fst t1 t2 ≠ 0 ∧
j_fst ∈ jobs_scheduled_between sched t1 t2.
(* The deadline of j_fst is the deadline of tsk_k. *)
Lemma interference_bound_edf_j_fst_deadline :
job_deadline j_fst = task_deadline tsk_k.
(* The deadline of j_i is the deadline of tsk_i. *)
Lemma interference_bound_edf_j_i_deadline :
job_deadline j_i = task_deadline tsk_i.
(* If j_fst completes by its response-time bound, then t1 <= a_fst + R_k,
where t1 is the beginning of the time window (arrival of j_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.
(* Now, let's prove the interference bound for the particular case of a single job.
This case must be solved separately because the single job can simultaneously
be carry-in and carry-out job, so its response time is not necessarily
bounded by R_k (from the hypothesis H_all_previous_jobs_completed_on_time). *)
Section InterferenceSingleJob.
(* Assume that there's at least one job in the sorted list. *)
Hypothesis H_only_one_job: size sorted_jobs = 1.
Lemma interference_bound_edf_holds_for_a_single_job :
interference_caused_by j_fst t1 t2 ≤ interference_bound.
End InterferenceSingleJob.
(* Next, consider the other case where there are at least two jobs:
the first job j_fst, and the last job j_lst. *)
Section InterferenceTwoOrMoreJobs.
(* Assume there are at least two jobs. *)
Variable num_mid_jobs: nat.
Hypothesis H_at_least_two_jobs : size sorted_jobs = num_mid_jobs.+2.
(* Let j_lst be the last job of the sequence and a_lst its arrival time. *)
Let j_lst := nth elem sorted_jobs num_mid_jobs.+1.
Let a_lst := job_arrival j_lst.
(* In this section, we prove some basic lemmas about the first and last jobs. *)
Section FactsAboutFirstAndLastJobs.
(* The last job is an interfering job of task tsk_k. *)
Lemma interference_bound_edf_j_lst_is_job_of_tsk_k :
job_task j_lst = tsk_k ∧
interference_caused_by j_lst t1 t2 ≠ 0 ∧
j_lst ∈ jobs_scheduled_between sched t1 t2.
(* The deadline of j_lst is the deadline of tsk_k. *)
Lemma interference_bound_edf_j_lst_deadline :
job_deadline j_lst = task_deadline tsk_k.
(* The first job arrives before the last job. *)
Lemma interference_bound_edf_j_fst_before_j_lst :
job_arrival j_fst ≤ job_arrival j_lst.
(* The last job arrives before the end of the interval. *)
Lemma interference_bound_edf_last_job_arrives_before_end_of_interval :
job_arrival j_lst < t2.
(* Since there are multiple jobs, j_fst is far enough from the end of
the interval that its response-time bound is valid
(by the assumption H_all_previous_jobs_completed_on_time). *)
Lemma interference_bound_edf_j_fst_completed_on_time :
completed job_cost sched j_fst (a_fst + R_k).
End FactsAboutFirstAndLastJobs.
(* Next, we prove that the distance between the first and last jobs is at least
num_mid_jobs + 1 periods. *)
Lemma interference_bound_edf_many_periods_in_between :
a_lst - a_fst ≥ num_mid_jobs.+1 × p_k.
Lemma interference_bound_edf_slack_le_delta:
D_k - R_k ≤ D_i.
(* Using the lemma above, we prove that the ratio n_k is at least the number of
middle jobs + 1, ... *)
Lemma interference_bound_edf_n_k_covers_all_jobs :
n_k ≥ num_mid_jobs.+2.
(* ... which allows bounding the interference of the middle and last jobs
using n_k multiplied by the cost. *)
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.
(* As required by the proof of convergence of EDF RTA, we show that the
EDF-specific bound is monotonically increasing with both the size
of the interval and the value of the previous response-time bounds. *)
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.