Library prosa.model.priority.gel
GEL Priority Policy
We define a task-model parameter to express each task's relative priority point.
We define a job-model parameter to express each job's absolute priority point.
Based on a task-level relative priority-point parameter, we provide the
canonical definition of each job's absolute priority point.
#[global]
Instance jpp_from_tpp
(Job : JobType) (Task : TaskType)
`{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} :
JobPriorityPoint Job :=
{
job_priority_point (j : Job) :=
((job_arrival j)%:R + task_priority_point (job_task j))%R
}.
Instance jpp_from_tpp
(Job : JobType) (Task : TaskType)
`{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} :
JobPriorityPoint Job :=
{
job_priority_point (j : Job) :=
((job_arrival j)%:R + task_priority_point (job_task j))%R
}.
We define what it means for an abstract job-level fixed-priority policy to
behave as a GEL policy.
Consider jobs with absolute priority points.
A JLFP policy is GEL if it never assigns higher priority to a job with a
later absolute priority point. Ties among jobs with equal priority points
may be resolved by any reflexive, transitive, and total tie-breaking
rule.
Definition policy_is_GEL (JLFP : JLFP_policy Job) :=
(∀ j1 j2, hep_job j1 j2 →
(job_priority_point j1 ≤ job_priority_point j2)%R)
∧ reflexive_job_priorities JLFP
∧ transitive_job_priorities JLFP
∧ total_job_priorities JLFP.
End GELPolicy.
(∀ j1 j2, hep_job j1 j2 →
(job_priority_point j1 ≤ job_priority_point j2)%R)
∧ reflexive_job_priorities JLFP
∧ transitive_job_priorities JLFP
∧ total_job_priorities JLFP.
End GELPolicy.