Library prosa.model.aggregate.service_of_jobs

Service Received by Sets of Jobs

In this file, we define the notion of service received by a set of jobs.

Section ServiceOfJobs.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

Consider any kind of processor model, ...
  Context {PState : ProcessorState Job}.

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

... and any given schedule.
  Variable sched : schedule PState.

First, we define the service received by a generic set of jobs.
  Section ServiceOfSetOfJobs.

Let P be any computable predicate over jobs, ...
    Variable P : pred Job.

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

We define the cumulative service received at time t by jobs in jobs that satisfy predicate P ...
    Definition service_of_jobs_at (t : instant) :=
      \sum_(j <- jobs | P j) service_at sched j t.

... 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.

Next, we define the service received by jobs with higher or equal priority under JLFP policies.
  Section PerJobPriority.

Consider any JLDP policy.
    Context `{JLFP_policy Job}.

Let jobs denote any (finite) set of jobs.
    Variable jobs : seq Job.

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

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.
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 jhpanother_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 jhpanother_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 jhphep_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.
  Section ServiceOfTask.

Let tsk be the task to be analyzed ...
    Variable tsk : Task.

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

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.

Finally, we define the notion of total service received by a set of jobs.
  Section TotalService.

Let jobs denote any (finite) set of jobs.
    Variable jobs : seq Job.

We define the total service of jobs in an interval [t1,t2) simply as a sum of the service of individual jobs in interval [t1,t2).
(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.)
    Definition total_service_of_jobs_in (t1 t2 : instant) :=
      service_of_jobs predT jobs t1 t2.

  End TotalService.

End ServiceOfJobs.