Library rt.restructuring.model.aggregate.service_of_jobs
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import tactics sum.
From rt.restructuring.behavior Require Export all.
From rt.restructuring.model Require Import task schedule.priority_based.priorities processor.ideal.
From rt.restructuring.analysis Require Import workload.
From rt.restructuring.analysis.basic_facts Require Import arrivals completion ideal_schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
Service Received by Sets of Jobs
In this file, we define the notion of service received by a set of jobs.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of processor state 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 predicate over jobs, ...
... and let jobs denote any (finite) set of jobs.
Then we define the cumulative service received at
time t by the jobs that satisfy this predicate ...
... and the cumulative service received during time
interval [t1, t2) by the jobs that satisfy the predicate.
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 tasks with
higher-or-equal priority under a given FP policy.
Consider any FP policy.
Let jobs denote any (finite) set of jobs.
Let tsk be the task to be analyzed.
Based on the definition of jobs of higher or equal priority (with respect to tsk), ...
...we define the service received during [t1, t2) by jobs of higher or equal priority.
Definition service_of_higher_or_equal_priority_tasks (t1 t2 : instant) :=
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
End PerTaskPriority.
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
End PerTaskPriority.
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.
End PerJobPriority.
service_of_jobs of_higher_or_equal_priority jobs t1 t2.
End PerJobPriority.
In this section, we define the notion of workload for sets of jobs.
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 from the task 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.
End ServiceOfJobs.
service_of_jobs (job_of_task tsk) jobs t1 t2.
End ServiceOfTask.
End ServiceOfJobs.