Library prosa.classic.model.schedule.apa.interference
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload Affinity.
Section PossibleInterferingTasks.
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.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable tsk_other: sporadic_task.
Definition higher_priority_task_in :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End FP.
Section JLFP.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable tsk_other: sporadic_task.
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.
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable j: Job.
Let job_is_backlogged (t: time) := backlogged job_arrival job_cost sched j t.
Section TotalInterference.
Definition total_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2) job_is_backlogged t.
End TotalInterference.
Section JobInterference.
Variable job_other: Job.
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.
Section TaskInterference.
Variable tsk_other: sporadic_task.
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.
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.
Section BasicLemmas.
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
Lemma job_interference_le_service :
∀ j_other t1 t2,
job_interference j_other t1 t2 ≤ service_during sched j_other t1 t2.
Lemma task_interference_le_workload :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ workload job_task sched tsk t1 t2.
End BasicLemmas.
Section InterferenceNoParallelism.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Lemma job_interference_le_delta :
∀ j_other t1 delta,
job_interference j_other t1 (t1 + delta) ≤ delta.
End InterferenceNoParallelism.
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 prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Module Interference.
Import Schedule ScheduleOfSporadicTask Priority Workload Affinity.
Section PossibleInterferingTasks.
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.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable tsk_other: sporadic_task.
Definition higher_priority_task_in :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk) &&
affinity_intersects alpha' (alpha tsk_other).
End FP.
Section JLFP.
Variable tsk: sporadic_task.
Variable alpha': affinity num_cpus.
Variable tsk_other: sporadic_task.
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.
Context {arr_seq: arrival_sequence Job}.
Context {num_cpus: nat}.
Variable sched: schedule Job num_cpus.
Variable alpha: task_affinity sporadic_task num_cpus.
Variable j: Job.
Let job_is_backlogged (t: time) := backlogged job_arrival job_cost sched j t.
Section TotalInterference.
Definition total_interference (t1 t2: time) :=
\sum_(t1 ≤ t < t2) job_is_backlogged t.
End TotalInterference.
Section JobInterference.
Variable job_other: Job.
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.
Section TaskInterference.
Variable tsk_other: sporadic_task.
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.
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.
Section BasicLemmas.
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
Lemma job_interference_le_service :
∀ j_other t1 t2,
job_interference j_other t1 t2 ≤ service_during sched j_other t1 t2.
Lemma task_interference_le_workload :
∀ tsk t1 t2,
task_interference tsk t1 t2 ≤ workload job_task sched tsk t1 t2.
End BasicLemmas.
Section InterferenceNoParallelism.
Hypothesis H_sequential_jobs: sequential_jobs sched.
Lemma job_interference_le_delta :
∀ j_other t1 delta,
job_interference j_other t1 (t1 + delta) ≤ delta.
End InterferenceNoParallelism.
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.