Library rt.model.schedule.global.basic.interference
Require Import rt.util.all.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload.
Section InterferenceDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Consider any job j that incurs interference. *)
Variable j: Job.
(* Recall the definition of backlogged (pending and not scheduled). *)
Let job_is_backlogged (t: time) :=
backlogged job_arrival job_cost sched j t.
(* First, we define total interference. *)
Section TotalInterference.
(* The total interference incurred by job j during [t1, t2) is the
cumulative time in which j is backlogged in this interval. *)
Definition total_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2) job_is_backlogged t.
End TotalInterference.
(* Next, we define job interference. *)
Section JobInterference.
(* Let job_other be a job that interferes with j. *)
Variable job_other: Job.
(* The interference caused by job_other during [t1, t2) is the cumulative
time in which j is backlogged while job_other is scheduled. *)
Definition job_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t).
End JobInterference.
(* Next, we define task interference. *)
Section TaskInterference.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
(* The interference caused by tsk during [t1, t2) is the cumulative time
in which j is backlogged while tsk is scheduled. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t &&
task_scheduled_on job_task sched tsk_other cpu t).
End TaskInterference.
(* Next, we define an approximation of the total interference based on
each per-task interference. *)
Section TaskInterferenceJobList.
Variable tsk_other: sporadic_task.
Definition task_interference_joblist (t1 t2: time) :=
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_other)
job_interference j t1 t2.
End TaskInterferenceJobList.
(* Now we prove some basic lemmas about interference. *)
Section BasicLemmas.
(* First, we show that the total interference cannot be larger than the interval length. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* Next, we show that job interference is bounded by the service of the interfering job. *)
Lemma job_interference_le_service :
∀ j_other t1 t2,
job_interference j_other t1 t2 ≤ service_during sched j_other t1 t2.
(* We also prove that task interference is bounded by the workload of the interfering task. *)
Lemma task_interference_le_workload :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ workload job_task sched tsk t1 t2.
End BasicLemmas.
(* Now we prove some bounds on interference for sequential jobs. *)
Section InterferenceSequentialJobs.
(* If jobs are sequential, ... *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... then the interference incurred by a job in an interval
of length delta is at most delta. *)
Lemma job_interference_le_delta :
∀ j_other t1 delta,
job_interference j_other t1 (t1 + delta) ≤ delta.
End InterferenceSequentialJobs.
(* Next, we show that the cumulative per-task interference bounds the total
interference. *)
Section BoundUsingPerJobInterference.
Lemma interference_le_interference_joblist :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ task_interference_joblist tsk t1 t2.
End BoundUsingPerJobInterference.
End InterferenceDefs.
End Interference.
Require Import rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.priority.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload.
Section InterferenceDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_cost: Job → time.
Variable job_task: Job → sporadic_task.
(* Assume any job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Consider any job j that incurs interference. *)
Variable j: Job.
(* Recall the definition of backlogged (pending and not scheduled). *)
Let job_is_backlogged (t: time) :=
backlogged job_arrival job_cost sched j t.
(* First, we define total interference. *)
Section TotalInterference.
(* The total interference incurred by job j during [t1, t2) is the
cumulative time in which j is backlogged in this interval. *)
Definition total_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2) job_is_backlogged t.
End TotalInterference.
(* Next, we define job interference. *)
Section JobInterference.
(* Let job_other be a job that interferes with j. *)
Variable job_other: Job.
(* The interference caused by job_other during [t1, t2) is the cumulative
time in which j is backlogged while job_other is scheduled. *)
Definition job_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t && scheduled_on sched job_other cpu t).
End JobInterference.
(* Next, we define task interference. *)
Section TaskInterference.
(* In order to define task interference, consider any interfering task tsk_other. *)
Variable tsk_other: sporadic_task.
(* The interference caused by tsk during [t1, t2) is the cumulative time
in which j is backlogged while tsk is scheduled. *)
Definition task_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2)
\sum_(cpu < num_cpus)
(job_is_backlogged t &&
task_scheduled_on job_task sched tsk_other cpu t).
End TaskInterference.
(* Next, we define an approximation of the total interference based on
each per-task interference. *)
Section TaskInterferenceJobList.
Variable tsk_other: sporadic_task.
Definition task_interference_joblist (t1 t2: time) :=
\sum_(j <- jobs_scheduled_between sched t1 t2 | job_task j == tsk_other)
job_interference j t1 t2.
End TaskInterferenceJobList.
(* Now we prove some basic lemmas about interference. *)
Section BasicLemmas.
(* First, we show that the total interference cannot be larger than the interval length. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* Next, we show that job interference is bounded by the service of the interfering job. *)
Lemma job_interference_le_service :
∀ j_other t1 t2,
job_interference j_other t1 t2 ≤ service_during sched j_other t1 t2.
(* We also prove that task interference is bounded by the workload of the interfering task. *)
Lemma task_interference_le_workload :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ workload job_task sched tsk t1 t2.
End BasicLemmas.
(* Now we prove some bounds on interference for sequential jobs. *)
Section InterferenceSequentialJobs.
(* If jobs are sequential, ... *)
Hypothesis H_sequential_jobs: sequential_jobs sched.
(* ... then the interference incurred by a job in an interval
of length delta is at most delta. *)
Lemma job_interference_le_delta :
∀ j_other t1 delta,
job_interference j_other t1 (t1 + delta) ≤ delta.
End InterferenceSequentialJobs.
(* Next, we show that the cumulative per-task interference bounds the total
interference. *)
Section BoundUsingPerJobInterference.
Lemma interference_le_interference_joblist :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ task_interference_joblist tsk t1 t2.
End BoundUsingPerJobInterference.
End InterferenceDefs.
End Interference.