Library prosa.classic.model.schedule.global.jitter.interference
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.global.basic.interference.
Module Interference.
Import ScheduleOfSporadicTaskWithJitter Priority Workload.
(* We import some of the basic definitions, but we need to re-define almost everything
since the definition of backlogged (and thus the definition of interference)
changes with jitter. *)
Import prosa.classic.model.schedule.global.basic.interference.
Export Interference.
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.
Variable job_jitter: Job → time.
(* Consider any job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule of those jobs. *)
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 := backlogged job_arrival job_cost job_jitter sched j.
(* 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 total interference cannot be larger than the interval length. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* Next, we prove 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 prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.jitter.job prosa.classic.model.schedule.global.jitter.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Require prosa.classic.model.schedule.global.basic.interference.
Module Interference.
Import ScheduleOfSporadicTaskWithJitter Priority Workload.
(* We import some of the basic definitions, but we need to re-define almost everything
since the definition of backlogged (and thus the definition of interference)
changes with jitter. *)
Import prosa.classic.model.schedule.global.basic.interference.
Export Interference.
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.
Variable job_jitter: Job → time.
(* Consider any job arrival sequence...*)
Variable arr_seq: arrival_sequence Job.
(* ... and any schedule of those jobs. *)
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 := backlogged job_arrival job_cost job_jitter sched j.
(* 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 total interference cannot be larger than the interval length. *)
Lemma total_interference_le_delta :
∀ t1 t2,
total_interference t1 t2 ≤ t2 - t1.
(* Next, we prove 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.