Library rt.model.schedule.apa.interference
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload Affinity.
(* In this section, we define the notion of a possible interfering task. *)
Section PossibleInterferingTasks.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Consider an APA platform with affinity alpha. *)
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
Section FP.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ...assuming a subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
(* Let tsk_other be another task. *)
Variable tsk_other: sporadic_task.
(* Under FP scheduling with constrained deadlines, tsk_other can only interfere
with tsk if it is a different task with higher or equal priority and
intersecting affinity. *)
Definition higher_priority_task_in :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End FP.
Section JLFP.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ...assuming a subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
(* Let tsk_other be another task. *)
Variable tsk_other: sporadic_task.
(* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
with tsk if it is a different task with intersecting affinity. *)
Definition different_task_in :=
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End JLFP.
End PossibleInterferingTasks.
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...*)
Context {arr_seq: arrival_sequence Job}.
(* ... and any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Assume that every job at any time has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task 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 &&
can_execute_on alpha (job_task j) cpu &&
scheduled_on sched job_other cpu t).
End JobInterference.
(* Next, we define task interference. *)
Section TaskInterference.
(* 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 &&
can_execute_on alpha (job_task j) cpu &&
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.
(* Total interference cannot be larger than the considered time window. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* 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.
(* 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 InterferenceNoParallelism.
(* 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 InterferenceNoParallelism.
(* Next, we show that the cumulative per-task interference bounds the total
interference. *)
Section BoundUsingPerTaskInterference.
Lemma interference_le_interference_joblist :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ task_interference_joblist tsk t1 t2.
End BoundUsingPerTaskInterference.
End InterferenceDefs.
End Interference.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority.
Require Import rt.model.schedule.global.workload.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload Affinity.
(* In this section, we define the notion of a possible interfering task. *)
Section PossibleInterferingTasks.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Consider an APA platform with affinity alpha. *)
Context {num_cpus: nat}.
Variable alpha: task_affinity sporadic_task num_cpus.
Section FP.
(* Assume an FP policy. *)
Variable higher_eq_priority: FP_policy sporadic_task.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ...assuming a subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
(* Let tsk_other be another task. *)
Variable tsk_other: sporadic_task.
(* Under FP scheduling with constrained deadlines, tsk_other can only interfere
with tsk if it is a different task with higher or equal priority and
intersecting affinity. *)
Definition higher_priority_task_in :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End FP.
Section JLFP.
(* Let tsk be the task to be analyzed ... *)
Variable tsk: sporadic_task.
(* ...assuming a subaffinity alpha'. *)
Variable alpha': affinity num_cpus.
(* Let tsk_other be another task. *)
Variable tsk_other: sporadic_task.
(* Under JLFP/JLDP scheduling with constrained deadlines, tsk_other can only interfere
with tsk if it is a different task with intersecting affinity. *)
Definition different_task_in :=
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End JLFP.
End PossibleInterferingTasks.
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...*)
Context {arr_seq: arrival_sequence Job}.
(* ... and any schedule. *)
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
(* Assume that every job at any time has a processor affinity alpha. *)
Variable alpha: task_affinity sporadic_task 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 &&
can_execute_on alpha (job_task j) cpu &&
scheduled_on sched job_other cpu t).
End JobInterference.
(* Next, we define task interference. *)
Section TaskInterference.
(* 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 &&
can_execute_on alpha (job_task j) cpu &&
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.
(* Total interference cannot be larger than the considered time window. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* 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.
(* 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 InterferenceNoParallelism.
(* 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 InterferenceNoParallelism.
(* Next, we show that the cumulative per-task interference bounds the total
interference. *)
Section BoundUsingPerTaskInterference.
Lemma interference_le_interference_joblist :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ task_interference_joblist tsk t1 t2.
End BoundUsingPerTaskInterference.
End InterferenceDefs.
End Interference.