Library rt.model.basic.priority
Require Import rt.util.all.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
Set Implicit Arguments.
(* Definitions of FP and JLFP/JLDP priority relations. *)
Module Priority.
Import SporadicTask Schedule.
Section PriorityDefs.
(* Assume a given job arrival sequence. *)
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Section Definitions.
(* In the following, we define all priority relations as non-strict, i.e., they specify that
"job_high has higher priority than (or the same priority as) job_low". *)
(* A JLDP policy is a generic relation between two jobs of an arrival sequence
that can vary with time. *)
Definition JLDP_policy := time → JobIn arr_seq → JobIn arr_seq → bool.
(* FP policy is simply a relation between tasks.
Because our model of processor platform is based on a generic JLDP policy,
we generate a JLDP policy from an FP policy whenever required. *)
Variable sporadic_task: eqType.
Definition FP_policy := sporadic_task → sporadic_task → bool.
End Definitions.
Section ValidJLFPPolicy.
Variable is_higher_priority: JLDP_policy.
(* A policy is reflexive, since a job has the same priority as itself. *)
Definition JLFP_is_reflexive :=
∀ t, reflexive (is_higher_priority t).
(* A policy is transitive. *)
Definition JLFP_is_transitive :=
∀ t, transitive (is_higher_priority t).
(* A policy is total, since it must know the priority of any two jobs at any time. *)
Definition JLFP_is_total :=
∀ t, total (is_higher_priority t).
(* A JLDP policy is valid iff it satisfies the three properties.
Note that, for generality, we don't enforce antisymmetry and allow multiple
jobs with same priority. *)
Definition valid_JLDP_policy :=
JLFP_is_reflexive ∧ JLFP_is_transitive ∧ JLFP_is_total.
End ValidJLFPPolicy.
Section MonotonicPriorities.
Context {sporadic_task: eqType}.
Variable job_task: Job → sporadic_task.
Variable higher_eq_priority: JLDP_policy.
Definition monotonic_priorities :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
job_arrival j < job_arrival j' →
higher_eq_priority t j j'.
End MonotonicPriorities.
Section ValidFPPolicy.
Context {sporadic_task: eqType}.
Variable is_higher_priority: FP_policy sporadic_task.
Definition FP_is_reflexive := reflexive is_higher_priority.
Definition FP_is_transitive := transitive is_higher_priority.
Definition FP_is_total := total is_higher_priority.
(* We enforce the same restrictions for FP policy: reflexive, transitive, total. *)
Definition valid_FP_policy :=
FP_is_reflexive ∧ FP_is_transitive ∧ FP_is_total.
End ValidFPPolicy.
End PriorityDefs.
Section RateDeadlineMonotonic.
Context {sporadic_task: eqType}.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Rate-Monotonic and Deadline-Monotonic as priority order *)
Definition RM (tsk1 tsk2: sporadic_task) := task_period tsk1 ≤ task_period tsk2.
Definition DM (tsk1 tsk2: sporadic_task) := task_deadline tsk1 ≤ task_deadline tsk2.
(* Rate-Montonic is a valid FP policy. *)
Lemma rm_is_valid : valid_FP_policy RM.
(* Deadline-Monotonic is a valid FP policy. *)
Lemma dm_is_valid : valid_FP_policy DM.
End RateDeadlineMonotonic.
Section GeneralizeFP.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Variable num_cpus: nat.
(* We define a function to get from FP to JLDP policy. *)
Definition FP_to_JLDP (task_hp: FP_policy sporadic_task) : JLDP_policy arr_seq :=
fun (t: time) (jhigh jlow: JobIn arr_seq) ⇒
task_hp (job_task jhigh) (job_task jlow).
(* With this function, from a valid FP policy comes a valid JLDP policy. *)
Lemma valid_FP_is_valid_JLDP :
∀ task_hp (FP: valid_FP_policy task_hp),
valid_JLDP_policy (FP_to_JLDP task_hp).
End GeneralizeFP.
Section JLFPDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Context {num_cpus: nat}.
Context {arr_seq: arrival_sequence Job}.
Variable is_higher_priority: JLDP_policy arr_seq.
(* JLFP policy is a JLDP policy where the priorities do not vary with time. *)
Definition is_JLFP_policy (is_higher_priority: JLDP_policy arr_seq) :=
∀ j1 j2 t t',
is_higher_priority t j1 j2 → is_higher_priority t' j1 j2.
(* Lemma: every FP policy is a JLFP policy. *)
Variable job_task: Job → sporadic_task.
Lemma FP_is_JLFP :
∀ FP_higher_priority,
is_JLFP_policy (FP_to_JLDP job_task FP_higher_priority).
End JLFPDefs.
Section EDFDefs.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Variable job_deadline: Job → time.
Definition EDF (t: time) (j1 j2: JobIn arr_seq) :=
job_arrival j1 + job_deadline j1 ≤ job_arrival j2 + job_deadline j2.
(* Lemma: EDF is a JLFP policy. *)
Lemma edf_JLFP : is_JLFP_policy EDF.
Lemma edf_valid_policy : valid_JLDP_policy EDF.
End EDFDefs.
End Priority.
Require Import rt.model.basic.task rt.model.basic.job rt.model.basic.schedule.
Set Implicit Arguments.
(* Definitions of FP and JLFP/JLDP priority relations. *)
Module Priority.
Import SporadicTask Schedule.
Section PriorityDefs.
(* Assume a given job arrival sequence. *)
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Section Definitions.
(* In the following, we define all priority relations as non-strict, i.e., they specify that
"job_high has higher priority than (or the same priority as) job_low". *)
(* A JLDP policy is a generic relation between two jobs of an arrival sequence
that can vary with time. *)
Definition JLDP_policy := time → JobIn arr_seq → JobIn arr_seq → bool.
(* FP policy is simply a relation between tasks.
Because our model of processor platform is based on a generic JLDP policy,
we generate a JLDP policy from an FP policy whenever required. *)
Variable sporadic_task: eqType.
Definition FP_policy := sporadic_task → sporadic_task → bool.
End Definitions.
Section ValidJLFPPolicy.
Variable is_higher_priority: JLDP_policy.
(* A policy is reflexive, since a job has the same priority as itself. *)
Definition JLFP_is_reflexive :=
∀ t, reflexive (is_higher_priority t).
(* A policy is transitive. *)
Definition JLFP_is_transitive :=
∀ t, transitive (is_higher_priority t).
(* A policy is total, since it must know the priority of any two jobs at any time. *)
Definition JLFP_is_total :=
∀ t, total (is_higher_priority t).
(* A JLDP policy is valid iff it satisfies the three properties.
Note that, for generality, we don't enforce antisymmetry and allow multiple
jobs with same priority. *)
Definition valid_JLDP_policy :=
JLFP_is_reflexive ∧ JLFP_is_transitive ∧ JLFP_is_total.
End ValidJLFPPolicy.
Section MonotonicPriorities.
Context {sporadic_task: eqType}.
Variable job_task: Job → sporadic_task.
Variable higher_eq_priority: JLDP_policy.
Definition monotonic_priorities :=
∀ (j j': JobIn arr_seq) t,
job_task j = job_task j' →
job_arrival j < job_arrival j' →
higher_eq_priority t j j'.
End MonotonicPriorities.
Section ValidFPPolicy.
Context {sporadic_task: eqType}.
Variable is_higher_priority: FP_policy sporadic_task.
Definition FP_is_reflexive := reflexive is_higher_priority.
Definition FP_is_transitive := transitive is_higher_priority.
Definition FP_is_total := total is_higher_priority.
(* We enforce the same restrictions for FP policy: reflexive, transitive, total. *)
Definition valid_FP_policy :=
FP_is_reflexive ∧ FP_is_transitive ∧ FP_is_total.
End ValidFPPolicy.
End PriorityDefs.
Section RateDeadlineMonotonic.
Context {sporadic_task: eqType}.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
(* Rate-Monotonic and Deadline-Monotonic as priority order *)
Definition RM (tsk1 tsk2: sporadic_task) := task_period tsk1 ≤ task_period tsk2.
Definition DM (tsk1 tsk2: sporadic_task) := task_deadline tsk1 ≤ task_deadline tsk2.
(* Rate-Montonic is a valid FP policy. *)
Lemma rm_is_valid : valid_FP_policy RM.
(* Deadline-Monotonic is a valid FP policy. *)
Lemma dm_is_valid : valid_FP_policy DM.
End RateDeadlineMonotonic.
Section GeneralizeFP.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → sporadic_task.
Variable arr_seq: arrival_sequence Job.
Variable num_cpus: nat.
(* We define a function to get from FP to JLDP policy. *)
Definition FP_to_JLDP (task_hp: FP_policy sporadic_task) : JLDP_policy arr_seq :=
fun (t: time) (jhigh jlow: JobIn arr_seq) ⇒
task_hp (job_task jhigh) (job_task jlow).
(* With this function, from a valid FP policy comes a valid JLDP policy. *)
Lemma valid_FP_is_valid_JLDP :
∀ task_hp (FP: valid_FP_policy task_hp),
valid_JLDP_policy (FP_to_JLDP task_hp).
End GeneralizeFP.
Section JLFPDefs.
Context {sporadic_task: eqType}.
Context {Job: eqType}.
Context {num_cpus: nat}.
Context {arr_seq: arrival_sequence Job}.
Variable is_higher_priority: JLDP_policy arr_seq.
(* JLFP policy is a JLDP policy where the priorities do not vary with time. *)
Definition is_JLFP_policy (is_higher_priority: JLDP_policy arr_seq) :=
∀ j1 j2 t t',
is_higher_priority t j1 j2 → is_higher_priority t' j1 j2.
(* Lemma: every FP policy is a JLFP policy. *)
Variable job_task: Job → sporadic_task.
Lemma FP_is_JLFP :
∀ FP_higher_priority,
is_JLFP_policy (FP_to_JLDP job_task FP_higher_priority).
End JLFPDefs.
Section EDFDefs.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Variable job_deadline: Job → time.
Definition EDF (t: time) (j1 j2: JobIn arr_seq) :=
job_arrival j1 + job_deadline j1 ≤ job_arrival j2 + job_deadline j2.
(* Lemma: EDF is a JLFP policy. *)
Lemma edf_JLFP : is_JLFP_policy EDF.
Lemma edf_valid_policy : valid_JLDP_policy EDF.
End EDFDefs.
End Priority.