Library prosa.classic.model.priority
Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
Module Priority.
Import SporadicTaskset ArrivalSequence.
Section PriorityDefs.
Variable Task: eqType.
Variable Job: eqType.
Definition FP_policy := rel Task.
Definition JLFP_policy := rel Job.
Definition JLDP_policy := time → rel Job.
End PriorityDefs.
Section Generalization.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Definition FP_to_JLFP (task_hp: FP_policy Task) :=
fun (jhigh jlow: Job) ⇒
task_hp (job_task jhigh) (job_task jlow).
Definition FP_to_JLDP (task_hp: FP_policy Task) :=
fun (t: time) ⇒ FP_to_JLFP task_hp.
Definition JLFP_to_JLDP (job_hp: JLFP_policy Job) :=
fun (t: time) ⇒ job_hp.
End Generalization.
Section PropertiesFP.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Variable task_priority: FP_policy Task.
Definition FP_is_reflexive := reflexive task_priority.
Definition FP_is_irreflexive := irreflexive task_priority.
Definition FP_is_transitive := transitive task_priority.
Section Antisymmetry.
Variable ts: seq Task.
Definition FP_is_total_over_task_set :=
total_over_list task_priority ts.
Definition FP_is_antisymmetric_over_task_set :=
antisymmetric_over_list task_priority ts.
End Antisymmetry.
End PropertiesFP.
Section PropertiesJLFP.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable job_priority: JLFP_policy Job.
Definition JLFP_is_reflexive := reflexive job_priority.
Definition JLFP_is_irreflexive := irreflexive job_priority.
Definition JLFP_is_transitive := transitive job_priority.
Definition JLFP_is_total :=
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_priority j1 j2 || job_priority j2 j1.
Definition JLFP_respects_sequential_jobs :=
∀ j1 j2,
job_task j1 == job_task j2 →
job_arrival j1 ≤ job_arrival j2 →
job_priority j1 j2.
End PropertiesJLFP.
Section PropertiesJLDP.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Variable job_priority: JLDP_policy Job.
Definition JLDP_is_reflexive :=
∀ t, reflexive (job_priority t).
Definition JLDP_is_irreflexive :=
∀ t, irreflexive (job_priority t).
Definition JLDP_is_transitive :=
∀ t, transitive (job_priority t).
Definition JLDP_is_total :=
∀ j1 j2 t,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_priority t j1 j2 || job_priority t j2 j1.
End PropertiesJLDP.
Section KnownFPPolicies.
Context {Job: eqType}.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Definition RM (tsk1 tsk2: Task) :=
task_period tsk1 ≤ task_period tsk2.
Definition DM (tsk1 tsk2: Task) :=
task_deadline tsk1 ≤ task_deadline tsk2.
Section Properties.
Lemma RM_is_reflexive : FP_is_reflexive RM.
Lemma RM_is_transitive : FP_is_transitive RM.
Lemma DM_is_reflexive : FP_is_reflexive DM.
Lemma DM_is_transitive : FP_is_transitive DM.
Lemma any_reflexive_FP_respects_sequential_jobs:
∀ job_priority: FP_policy Task,
FP_is_reflexive job_priority →
JLFP_respects_sequential_jobs
job_task job_arrival (FP_to_JLFP job_task job_priority).
End Properties.
End KnownFPPolicies.
Section KnownJLFPPolicies.
Section EDF.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition EDF (j1 j2: Job) :=
job_arrival j1 + job_deadline j1 ≤ job_arrival j2 + job_deadline j2.
Section Properties.
Lemma EDF_is_reflexive : JLFP_is_reflexive EDF.
Lemma EDF_is_transitive : JLFP_is_transitive EDF.
Lemma EDF_is_total : JLFP_is_total arr_seq EDF.
End Properties.
End EDF.
Section EDFwithTasks.
Context {Task: eqType}.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Definition job_relative_dealine (j: Job) := task_deadline (job_task j).
Lemma EDF_respects_sequential_jobs:
JLFP_respects_sequential_jobs
job_task job_arrival (EDF job_arrival job_relative_dealine).
End EDFwithTasks.
End KnownJLFPPolicies.
Section PossibleInterferingTasks.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Variable tsk: sporadic_task.
Variable tsk_other: sporadic_task.
Definition higher_priority_task :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk).
End FP.
Section JLFP.
Variable tsk: sporadic_task.
Variable tsk_other: sporadic_task.
Definition different_task := tsk_other != tsk.
End JLFP.
End PossibleInterferingTasks.
End Priority.
Require Import prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq.
Module Priority.
Import SporadicTaskset ArrivalSequence.
Section PriorityDefs.
Variable Task: eqType.
Variable Job: eqType.
Definition FP_policy := rel Task.
Definition JLFP_policy := rel Job.
Definition JLDP_policy := time → rel Job.
End PriorityDefs.
Section Generalization.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Definition FP_to_JLFP (task_hp: FP_policy Task) :=
fun (jhigh jlow: Job) ⇒
task_hp (job_task jhigh) (job_task jlow).
Definition FP_to_JLDP (task_hp: FP_policy Task) :=
fun (t: time) ⇒ FP_to_JLFP task_hp.
Definition JLFP_to_JLDP (job_hp: JLFP_policy Job) :=
fun (t: time) ⇒ job_hp.
End Generalization.
Section PropertiesFP.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Variable task_priority: FP_policy Task.
Definition FP_is_reflexive := reflexive task_priority.
Definition FP_is_irreflexive := irreflexive task_priority.
Definition FP_is_transitive := transitive task_priority.
Section Antisymmetry.
Variable ts: seq Task.
Definition FP_is_total_over_task_set :=
total_over_list task_priority ts.
Definition FP_is_antisymmetric_over_task_set :=
antisymmetric_over_list task_priority ts.
End Antisymmetry.
End PropertiesFP.
Section PropertiesJLFP.
Context {Task: eqType}.
Context {Job: eqType}.
Variable job_task: Job → Task.
Variable job_arrival: Job → time.
Variable arr_seq: arrival_sequence Job.
Variable job_priority: JLFP_policy Job.
Definition JLFP_is_reflexive := reflexive job_priority.
Definition JLFP_is_irreflexive := irreflexive job_priority.
Definition JLFP_is_transitive := transitive job_priority.
Definition JLFP_is_total :=
∀ j1 j2,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_priority j1 j2 || job_priority j2 j1.
Definition JLFP_respects_sequential_jobs :=
∀ j1 j2,
job_task j1 == job_task j2 →
job_arrival j1 ≤ job_arrival j2 →
job_priority j1 j2.
End PropertiesJLFP.
Section PropertiesJLDP.
Context {Job: eqType}.
Variable arr_seq: arrival_sequence Job.
Variable job_priority: JLDP_policy Job.
Definition JLDP_is_reflexive :=
∀ t, reflexive (job_priority t).
Definition JLDP_is_irreflexive :=
∀ t, irreflexive (job_priority t).
Definition JLDP_is_transitive :=
∀ t, transitive (job_priority t).
Definition JLDP_is_total :=
∀ j1 j2 t,
arrives_in arr_seq j1 →
arrives_in arr_seq j2 →
job_priority t j1 j2 || job_priority t j2 j1.
End PropertiesJLDP.
Section KnownFPPolicies.
Context {Job: eqType}.
Context {Task: eqType}.
Variable task_period: Task → time.
Variable task_deadline: Task → time.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Definition RM (tsk1 tsk2: Task) :=
task_period tsk1 ≤ task_period tsk2.
Definition DM (tsk1 tsk2: Task) :=
task_deadline tsk1 ≤ task_deadline tsk2.
Section Properties.
Lemma RM_is_reflexive : FP_is_reflexive RM.
Lemma RM_is_transitive : FP_is_transitive RM.
Lemma DM_is_reflexive : FP_is_reflexive DM.
Lemma DM_is_transitive : FP_is_transitive DM.
Lemma any_reflexive_FP_respects_sequential_jobs:
∀ job_priority: FP_policy Task,
FP_is_reflexive job_priority →
JLFP_respects_sequential_jobs
job_task job_arrival (FP_to_JLFP job_task job_priority).
End Properties.
End KnownFPPolicies.
Section KnownJLFPPolicies.
Section EDF.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_deadline: Job → time.
Variable arr_seq: arrival_sequence Job.
Definition EDF (j1 j2: Job) :=
job_arrival j1 + job_deadline j1 ≤ job_arrival j2 + job_deadline j2.
Section Properties.
Lemma EDF_is_reflexive : JLFP_is_reflexive EDF.
Lemma EDF_is_transitive : JLFP_is_transitive EDF.
Lemma EDF_is_total : JLFP_is_total arr_seq EDF.
End Properties.
End EDF.
Section EDFwithTasks.
Context {Task: eqType}.
Variable task_deadline: Task → time.
Context {Job: eqType}.
Variable job_arrival: Job → time.
Variable job_task: Job → Task.
Definition job_relative_dealine (j: Job) := task_deadline (job_task j).
Lemma EDF_respects_sequential_jobs:
JLFP_respects_sequential_jobs
job_task job_arrival (EDF job_arrival job_relative_dealine).
End EDFwithTasks.
End KnownJLFPPolicies.
Section PossibleInterferingTasks.
Context {sporadic_task: eqType}.
Variable task_cost: sporadic_task → time.
Variable task_period: sporadic_task → time.
Variable task_deadline: sporadic_task → time.
Section FP.
Variable higher_eq_priority: FP_policy sporadic_task.
Variable tsk: sporadic_task.
Variable tsk_other: sporadic_task.
Definition higher_priority_task :=
higher_eq_priority tsk_other tsk &&
(tsk_other != tsk).
End FP.
Section JLFP.
Variable tsk: sporadic_task.
Variable tsk_other: sporadic_task.
Definition different_task := tsk_other != tsk.
End JLFP.
End PossibleInterferingTasks.
End Priority.