Library prosa.model.aggregate.workload
Cumulative Workload of Sets of Jobs
Consider any type of tasks ...
... and any type of jobs with execution costs that are
associated with these tasks.
Consider any job arrival sequence.
First, we define the workload for generic sets of jobs.
Given any computable predicate on jobs, ...
... and any (finite) set of jobs, ...
... we define the total workload of the jobs that satisfy
predicate P.
Next, we define the workload of jobs with higher or
equal priority under JLFP policies.
Consider any JLFP policy that indicates whether a job has
higher or equal priority.
Let j be the job to be analyzed.
Recall the notion of a job of higher or equal priority.
Then, we define the workload of higher or equal priority of all jobs
with higher-or-equal priority than j.
Definition workload_of_higher_or_equal_priority_jobs jobs :=
workload_of_jobs of_higher_or_equal_priority jobs.
workload_of_jobs of_higher_or_equal_priority jobs.
We extend the prior notion to define the workload all jobs
with higher-or-equal priority than j in a given interval.
Definition workload_of_hep_jobs (j : Job) (t1 t2 : instant) :=
workload_of_jobs
(fun jhp ⇒ hep_job jhp j)
(arrivals_between arr_seq t1 t2).
workload_of_jobs
(fun jhp ⇒ hep_job jhp j)
(arrivals_between arr_seq t1 t2).
We define a similar non-reflexive notion of higher-or-equal
priority workload in an interval.
Definition workload_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
workload_of_jobs
(fun jhp ⇒ another_hep_job jhp j)
(arrivals_between arr_seq t1 t2).
workload_of_jobs
(fun jhp ⇒ another_hep_job jhp j)
(arrivals_between arr_seq t1 t2).
For analysis purposes, we define the workload of a given job.
Definition workload_of_job (j : Job) (t1 t2 : instant) :=
workload_of_jobs (xpred1 j) (arrivals_between arr_seq t1 t2).
End PerJobPriority.
workload_of_jobs (xpred1 j) (arrivals_between arr_seq t1 t2).
End PerJobPriority.
We also define workload of a task.
Let tsk be the task to be analyzed.
We define the task workload as the workload of jobs of task
tsk.
Definition task_workload_between (t1 t2 : instant) :=
task_workload (arrivals_between arr_seq t1 t2).
End TaskWorkload.
End WorkloadOfJobs.
task_workload (arrivals_between arr_seq t1 t2).
End TaskWorkload.
End WorkloadOfJobs.