Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
(** * Numeric Fixed Task Priorities *) (** We define the notion of arbitrary numeric fixed task priorities, i.e., tasks are prioritized in order of user-provided numeric priority values, where numerically smaller values indicate lower priorities (as for instance it is the case in Linux). *) (** First, we define a new task parameter [task_priority] that maps each task to a numeric priority value. *) Class TaskPriority (Task : TaskType) := task_priority : Task -> nat. (** Based on this parameter, we define two corresponding FP policies. In one instance, a lower numeric value indicates lower priority, while in the other instance, a lower numeric value indicates higher priority. Both these interpretations can be found in practice and in the literature. For example, Linux uses "higher numeric value <-> higher priority", whereas many papers assume "lower numeric value <-> higher priority". *) (** In this section, we define ascending numeric fixed priorities, where a larger numeric value indicates higher priority, and note some trivial facts about this interpretation of priority values. *) Section PropertiesNFPA. (** The instance [NumericFPAscending] assigns higher priority to tasks with higher numeric [task_priority] value. *) #[local] Instance NumericFPAscending (Task : TaskType) `{TaskPriority Task} : FP_policy Task := { hep_task (tsk1 tsk2 : Task) := task_priority tsk1 >= task_priority tsk2 }. (** Consider any kind of tasks with specified priorities... *) Context {Task : TaskType}. Context `{TaskPriority Task}. (** ...and jobs stemming from these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. (** The resulting priority policy is reflexive. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

reflexive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

reflexive_priorities
by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPAscending. Qed. (** The resulting priority policy is transitive. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

transitive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

transitive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job

hep_job_at t x y -> hep_job_at t y z -> hep_job_at t x z
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job

task_priority (job_task y) <= task_priority (job_task x) -> task_priority (job_task z) <= task_priority (job_task y) -> task_priority (job_task z) <= task_priority (job_task x)
by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)). Qed. (** The resulting priority policy is total. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

total_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

total_priorities
by move=> t j1 j2; apply leq_total. Qed. End PropertiesNFPA. (** Next, we define descending numeric fixed priorities, where a larger numeric value indicates lower priority, and again note some trivial facts about this alternate interpretation of priority values. *) Section PropertiesNFPD. (** The instance [NumericFPDescending] assigns lower priority to tasks with higher numeric [task_priority] value. *) #[local] Instance NumericFPDescending (Task : TaskType) `{TaskPriority Task} : FP_policy Task := { hep_task (tsk1 tsk2 : Task) := task_priority tsk1 <= task_priority tsk2 }. (** Consider any kind of tasks with specified priorities... *) Context {Task : TaskType}. Context `{TaskPriority Task}. (** ...and jobs stemming from these tasks. *) Context {Job : JobType}. Context `{JobTask Job Task}. (** The resulting priority policy is reflexive. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

reflexive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

reflexive_priorities
by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFPDescending. Qed. (** The resulting priority policy is transitive. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

transitive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

transitive_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job

hep_job_at t x y -> hep_job_at t y z -> hep_job_at t x z
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task
t: instant
y, x, z: Job

task_priority (job_task x) <= task_priority (job_task y) -> task_priority (job_task y) <= task_priority (job_task z) -> task_priority (job_task x) <= task_priority (job_task z)
by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)). Qed. (** The resulting priority policy is total. *)
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

total_priorities
Task: TaskType
H: TaskPriority Task
Job: JobType
H0: JobTask Job Task

total_priorities
by move=> t j1 j2; apply leq_total. Qed. End PropertiesNFPD. (** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *) Global Hint Resolve NFPA_is_reflexive NFPA_is_transitive NFPA_is_total NFPD_is_reflexive NFPD_is_transitive NFPD_is_total : basic_rt_facts.