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) := (Z.of_nat (job_arrival j) + task_priority_point (job_task j))%Z.
End AbsolutePriorityPoint.
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_priority (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)%Z
}.
`{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=
{
hep_job (j1 j2 : Job) := (job_priority_point j1 <=? job_priority_point j2)%Z
}.
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_priorities.
Proof. by move⇒ t y x z; apply Zbool.Zle_bool_trans. Qed.
Proof. by move⇒ t y x z; apply Zbool.Zle_bool_trans. Qed.
GEL is total.
Fact GEL_is_total : total_priorities.
Proof.
move⇒ t j1 j2; apply /orP.
case: (boolP (job_priority_point j1 <=? job_priority_point j2)%Z) ⇒ REL; [left | right] ⇒ //.
move: REL; rewrite -Z.ltb_antisym ⇒ /Z.ltb_spec0 REL.
by move: (Z.lt_le_incl _ _ REL) ⇒ /Z.leb_spec0.
Qed.
End PropertiesOfGEL.
Proof.
move⇒ t j1 j2; apply /orP.
case: (boolP (job_priority_point j1 <=? job_priority_point j2)%Z) ⇒ REL; [left | right] ⇒ //.
move: REL; rewrite -Z.ltb_antisym ⇒ /Z.ltb_spec0 REL.
by move: (Z.lt_le_incl _ _ REL) ⇒ /Z.leb_spec0.
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.