# Cumulative Workload of Sets of Jobs

In this module, we define the notion of the cumulative workload of a set of jobs.

Consider any type of tasks ...

... and any type of jobs with execution costs that are associated with these tasks.
Context {Job : JobType}.
Context `{JobCost Job}.

Consider any job arrival sequence.
Variable arr_seq : arrival_sequence Job.

First, we define the workload for generic sets of jobs.

Given any computable predicate on jobs, ...
Variable P : pred Job.

... and any (finite) set of jobs, ...
Variable jobs : seq Job.

... we define the total workload of the jobs that satisfy predicate P.
Definition workload_of_jobs := \sum_(j <- jobs | P j) job_cost j.

Next, we define the workload of jobs with higher or equal priority under JLFP policies.
Section PerJobPriority.

Consider any JLFP policy that indicates whether a job has higher or equal priority.
Context `{JLFP_policy Job}.

Let j be the job to be analyzed.
Variable j : Job.

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.
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) :=
(fun jhphep_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) :=
(fun jhpanother_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.