Library rt.restructuring.model.schedule.priority_based.edf
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.restructuring.model Require Import job task job_deadline
schedule.priority_based.priorities.
From mathcomp Require Export seq.
In this section we introduce the notion of EDF priorities.
Program Instance EDF (Task : TaskType) (Job : JobType)
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=
{
hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2
}.
`{TaskDeadline Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=
{
hep_job (j1 j2 : Job) := job_deadline j1 ≤ job_deadline j2
}.
In this section, we prove a few properties about EDF policy.
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 arrival sequence.
EDF is reflexive.
Lemma EDF_is_reflexive : reflexive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 68)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
reflexive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
EDF is transitive.
Lemma EDF_is_transitive : transitive_priorities.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t y x z; apply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 79)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
transitive_priorities
----------------------------------------------------------------------------- *)
Proof. by intros t y x z; apply leq_trans.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
EDF respects sequential tasks hypothesis.
Lemma EDF_respects_sequential_tasks:
policy_respects_sequential_tasks.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
policy_respects_sequential_tasks
----------------------------------------------------------------------------- *)
Proof.
intros j1 j2 TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
TSK : job_task j1 == job_task j2
ARR : job_arrival j1 <= job_arrival j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
move: TSK ⇒ /eqP TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 133)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
----------------------------------------------------------------------------- *)
by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
policy_respects_sequential_tasks.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 92)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
============================
policy_respects_sequential_tasks
----------------------------------------------------------------------------- *)
Proof.
intros j1 j2 TSK ARR.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 97)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
TSK : job_task j1 == job_task j2
ARR : job_arrival j1 <= job_arrival j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
move: TSK ⇒ /eqP TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 133)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
hep_job j1 j2
----------------------------------------------------------------------------- *)
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
(* ----------------------------------[ coqtop ]---------------------------------
1 subgoal (ID 137)
Task : TaskType
H : TaskDeadline Task
Job : JobType
H0 : JobTask Job Task
H1 : JobArrival Job
H2 : JobCost Job
arr_seq : arrival_sequence Job
j1, j2 : Job
ARR : job_arrival j1 <= job_arrival j2
TSK : job_task j1 = job_task j2
============================
job_arrival j1 + task_deadline (job_task j2) <=
job_arrival j2 + task_deadline (job_task j2)
----------------------------------------------------------------------------- *)
by rewrite leq_add2r.
(* ----------------------------------[ coqtop ]---------------------------------
No more subgoals.
----------------------------------------------------------------------------- *)
Qed.
End PropertiesOfEDF.
We add the above lemmas into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically.
Hint Resolve
EDF_is_reflexive
EDF_is_transitive
EDF_respects_sequential_tasks : basic_facts.
EDF_is_reflexive
EDF_is_transitive
EDF_respects_sequential_tasks : basic_facts.