Library prosa.analysis.definitions.interference
Interference and Interfering Workload
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any kind of processor state model.
Consider any arrival sequence ...
... and any schedule.
Definitions of interference for FP policies.
We first define interference from higher priority tasks.
Definition hp_task_interference (j : Job) (t : instant) :=
has (fun jhp ⇒ hp_task (job_task jhp) (job_task j)
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
Context {JLFP : JLFP_policy Job}.
has (fun jhp ⇒ hp_task (job_task jhp) (job_task j)
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
Context {JLFP : JLFP_policy Job}.
Then, to define interference from equal priority tasks, we first
define higher priority jobs from an equal priority task...
...and such jobs that are not the same.
This enables us to define interference from equal priority tasks.
Definition other_ep_task_hep_job_interference (j : Job) (t : instant) :=
has (fun jhp ⇒ other_ep_task_hep_job jhp j
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
End FPDefinitions.
has (fun jhp ⇒ other_ep_task_hep_job jhp j
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
End FPDefinitions.
Definitions of interference for JLFP policies.
Consider a JLFP-policy that indicates a higher-or-equal priority
relation.
We say that job j is incurring interference from another
job with higher-or-equal priority at time t if there exists a
job jhp (different from j) with a higher-or-equal priority
that executes at time t.
Definition another_hep_job_interference (j : Job) (t : instant) :=
has (fun jhp ⇒ another_hep_job jhp j && receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
has (fun jhp ⇒ another_hep_job jhp j && receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
Similarly, we say that job j is incurring interference from a
job with higher-or-equal priority of another task at time t
if there exists a job jhp (of a different task) with
higher-or-equal priority that executes at time t.
Definition another_task_hep_job_interference (j : Job) (t : instant) :=
has (fun jhp ⇒ another_task_hep_job jhp j
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
has (fun jhp ⇒ another_task_hep_job jhp j
&& receives_service_at sched jhp t)
(arrivals_up_to arr_seq t).
Now, we define the notion of cumulative interfering workload,
called other_hep_jobs_interfering_workload, that says how many
units of workload are generated by jobs with higher-or-equal
priority released at time t.
Definition other_hep_jobs_interfering_workload (j : Job) (t : instant) :=
\sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
\sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.
For each of the concepts defined above, we introduce a
corresponding cumulative function:
(a) cumulative interference from other jobs with higher-or-equal priority ...
Definition cumulative_another_hep_job_interference (j : Job) (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) another_hep_job_interference j t.
\sum_(t1 ≤ t < t2) another_hep_job_interference j t.
... (b) and cumulative interference from jobs with higher or
equal priority from other tasks, ...
Definition cumulative_another_task_hep_job_interference (j : Job) (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) another_task_hep_job_interference j t.
\sum_(t1 ≤ t < t2) another_task_hep_job_interference j t.
... and (c) cumulative workload from jobs with higher or equal priority.
Definition cumulative_other_hep_jobs_interfering_workload (j : Job) (t1 t2 : instant) :=
\sum_(t1 ≤ t < t2) other_hep_jobs_interfering_workload j t.
End JLFPDefinitions.
End Definitions.
\sum_(t1 ≤ t < t2) other_hep_jobs_interfering_workload j t.
End JLFPDefinitions.
End Definitions.