# Library prosa.model.priority.gel

# GEL Priority Policy

We define a task-model parameter to express each task's relative priority point.

Based on the task-level relative priority-point parameter, we
define a job's absolute priority point in a straightforward manner.
To this end, we need to introduce some context first.

For any type of tasks with relative priority points, ...

Context {Job : JobType} {Task : TaskType} `{JobTask Job Task} `{PriorityPoint Task} `{JobArrival Job}.

... a job's absolute priority point is given by its arrival time
plus its task's relative priority point.

Definition job_priority_point (j : Job) :=

((job_arrival j)%:R + task_priority_point (job_task j))%R.

End AbsolutePriorityPoint.

((job_arrival j)%:R + task_priority_point (job_task j))%R.

End AbsolutePriorityPoint.

The resulting definition of GEL is straightforward: a job j1's
priority is higher than or equal to a job j2's priority iff
j1's absolute priority point is no later than j2's absolute
priority point.

#[export] Instance GEL (Job : JobType) (Task : TaskType)

`{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=

{

hep_job (j1 j2 : Job) := (job_priority_point j1 ≤ job_priority_point j2)%R

}.

`{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=

{

hep_job (j1 j2 : Job) := (job_priority_point j1 ≤ job_priority_point j2)%R

}.

In this section, we note three basic properties of the GEL policy:
the priority relation is reflexive, transitive, and total.

Consider any type of tasks with relative priority points...

...and jobs of these tasks.

GEL is reflexive.

GEL is transitive.

Fact GEL_is_transitive : transitive_job_priorities (GEL Job Task).

Proof. move⇒ x y z; exact: le_trans. Qed.

Proof. move⇒ x y z; exact: le_trans. Qed.

GEL is total.

Fact GEL_is_total : total_job_priorities (GEL Job Task).

Proof. move⇒ j1 j2; exact: le_total. Qed.

End PropertiesOfGEL.

Proof. move⇒ j1 j2; exact: le_total. Qed.

End PropertiesOfGEL.

We add the above facts into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically where needed.

Global Hint Resolve

GEL_is_reflexive

GEL_is_transitive

GEL_is_total

: basic_rt_facts.

GEL_is_reflexive

GEL_is_transitive

GEL_is_total

: basic_rt_facts.