Newer
Older
Require Import rt.model.task rt.model.job rt.model.task_arrival rt.model.priority.
Require Import rt.model.global.response_time rt.model.global.workload
rt.model.global.schedulability.
Require Import rt.model.global.basic.schedule rt.model.global.basic.platform
rt.model.global.basic.interference rt.model.global.basic.interference_edf.
Require Import rt.analysis.global.basic.workload_bound
rt.analysis.global.basic.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
TaskArrival 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_floor d_tsk p_other) * e_other +
minn e_other ((d_tsk %% p_other) - (d_other - R_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.
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 tsk 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.
(* 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 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:
forall (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.
(* Also assume that jobs are sequential and that there exists at
least one processor. *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
Hypothesis H_at_least_one_cpu: num_cpus > 0.
(* Consider a task set ts where all jobs come from the task set
and tasks have valid parameters and constrained deadlines. *)
Variable ts: taskset_of sporadic_task.
Hypothesis all_jobs_from_taskset:
forall (j: JobIn arr_seq), job_task j \in ts.
Hypothesis H_valid_task_parameters:
valid_sporadic_taskset task_cost task_period task_deadline ts.
Hypothesis H_constrained_deadlines:
forall 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_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 \in 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 \in 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 :
forall (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).
Loading
Loading full blame...