Commit 65f28df9 authored by Björn Brandenburg's avatar Björn Brandenburg

fix EDF priority definition to not depend on task abstraction

EDF is defined in terms of jobs, whether or not those jobs stem from
tasks. Make sure our definition is general enough to capture the
possibility of a set of jobs without associated tasks scheduled by
EDF.
parent 9933d50d
......@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.floating.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -42,7 +42,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
Let D tsk := task_deadline tsk.
(** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
......@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.limited.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -40,7 +40,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
Let D tsk := task_deadline tsk.
(** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
......@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -42,7 +42,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
Let D tsk := task_deadline tsk.
(** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
......@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -42,7 +42,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
Let D tsk := task_deadline tsk.
(** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
......@@ -15,7 +15,7 @@ Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.jo
Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -57,7 +57,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
Note that we do not relate the EDF policy with the scheduler. However, we
define functions for Interference and Interfering Workload that actively use
the concept of priorities. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
......@@ -15,7 +15,7 @@ Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
Require Import rt.restructuring.analysis.facts.edf.
Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
......@@ -70,7 +70,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
Note that we do not relate the EDF policy with the scheduler. However, we
define functions for Interference and Interfering Workload that actively use
the concept of priorities. *)
Let EDF := EDF Task Job.
Let EDF := EDF Job.
(** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
Variable arr_seq : arrival_sequence Job.
......
Require Export rt.restructuring.model.priority.edf.
Require Export rt.restructuring.model.task.absolute_deadline.
(** In this section, we prove a few properties about EDF policy. *)
Section PropertiesOfEDF.
(** Consider any type of tasks with relative deadlines ... *)
Context {Task : TaskType}.
Context `{TaskDeadline Task}.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** EDF respects sequential tasks hypothesis. *)
Lemma EDF_respects_sequential_tasks:
policy_respects_sequential_tasks.
Proof.
intros j1 j2 TSK ARR.
move: TSK => /eqP TSK.
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
by rewrite leq_add2r.
Qed.
End PropertiesOfEDF.
(** We add the above lemma into a "Hint Database" basic_facts, so Coq
will be able to apply them automatically. *)
Hint Resolve
EDF_respects_sequential_tasks : basic_facts.
Require Export rt.restructuring.model.task.absolute_deadline.
Require Import rt.restructuring.model.priority.classes.
From mathcomp Require Export seq.
Require Export rt.restructuring.model.priority.classes.
(** 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 :=
{
Program Instance EDF (Job : JobType) `{JobDeadline Job} : 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. *)
Section PropertiesOfEDF.
(** Consider any type of tasks ... *)
Context {Task : TaskType}.
Context `{TaskDeadline Task}.
(** ... and any type of jobs associated with these tasks. *)
(** Consider any type of jobs with deadlines. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Context `{JobDeadline Job}.
(** Consider any arrival sequence. *)
Variable arr_seq : arrival_sequence Job.
(** EDF is reflexive. *)
Lemma EDF_is_reflexive : reflexive_priorities.
Proof. by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, EDF. Qed.
......@@ -32,22 +23,12 @@ Section PropertiesOfEDF.
(** EDF is transitive. *)
Lemma EDF_is_transitive : transitive_priorities.
Proof. by intros t y x z; apply leq_trans. Qed.
(** EDF respects sequential tasks hypothesis. *)
Lemma EDF_respects_sequential_tasks:
policy_respects_sequential_tasks.
Proof.
intros j1 j2 TSK ARR.
move: TSK => /eqP TSK.
unfold hep_job, EDF, job_deadline, job_deadline_from_task_deadline; rewrite TSK.
by rewrite leq_add2r.
Qed.
End PropertiesOfEDF.
(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
(** 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_transitive: basic_facts.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment