Library prosa.model.aggregate.service_of_jobs
Service Received by Sets of Jobs
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Consider any kind of processor model, ...
... any job arrival sequence, ...
... and any given schedule.
First, we define the service received by a generic set of jobs.
Let P be any computable predicate over jobs, ...
... and let jobs denote any (finite) set of jobs.
... and the cumulative service received during the interval
[t1, t2) by jobs that satisfy predicate P.
Definition service_of_jobs (t1 t2 : instant) :=
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfSetOfJobs.
\sum_(j <- jobs | P j) service_during sched j t1 t2.
End ServiceOfSetOfJobs.
Next, we define the service received by jobs with higher or
equal priority under JLFP policies.
Consider any JLDP policy.
Let jobs denote any (finite) set of jobs.
Let j be the job to be analyzed.
Based on the definition of jobs of higher or equal priority, ...
...we define the service received during
[t1, t2) by jobs of higher or equal priority.
Definition service_of_higher_or_equal_priority_jobs (t1 t2 : instant) :=
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
Furthermore, we define similar notions on jobs arriving in a
given time interval, such as ...
... (1) service of all other jobs with higher-or-equal
priority (w.r.t. job j) distinct from job j, ...
Definition service_of_other_hep_jobs (t1 t2 : instant) :=
service_of_jobs
(fun jhp ⇒ another_hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
service_of_jobs
(fun jhp ⇒ another_hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
... (2) notion of service of higher-or-equal priority jobs
from other tasks, ...
Definition service_of_other_task_hep_jobs (t1 t2 : instant) :=
service_of_jobs
(fun jhp ⇒ another_task_hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
service_of_jobs
(fun jhp ⇒ another_task_hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
... (3) and service of jobs with higher-or-equal priority
arriving in an interval
[t1, t2).
Definition service_of_hep_jobs (t1 t2 : instant) :=
service_of_jobs
(fun jhp ⇒ hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
End PerJobPriority.
service_of_jobs
(fun jhp ⇒ hep_job jhp j)
(arrivals_between arr_seq t1 t2) t1 t2.
End PerJobPriority.
We define the notion of cumulative service received by
the jobs of a given task.
Let tsk be the task to be analyzed ...
... and let jobs denote any (finite) set of jobs.
We define the cumulative task service received by the jobs of
task tsk within time interval
[t1, t2).
Definition task_service_of_jobs_in t1 t2 :=
service_of_jobs (job_of_task tsk) jobs t1 t2.
End ServiceOfTask.
service_of_jobs (job_of_task tsk) jobs t1 t2.
End ServiceOfTask.
Finally, we define the notion of total service received by a set of jobs.
Let jobs denote any (finite) set of jobs.
We define the total service of jobs in an interval
(The predicate predT is the trivial predicate that always evaluates to
true, meaning that no jobs are filtered, and hence all jobs are
accounted for.)
[t1,t2) simply
as a sum of the service of individual jobs in interval [t1,t2).
Definition total_service_of_jobs_in (t1 t2 : instant) :=
service_of_jobs predT jobs t1 t2.
End TotalService.
End ServiceOfJobs.
service_of_jobs predT jobs t1 t2.
End TotalService.
End ServiceOfJobs.