augment model with definitions of well-known priority policies

restructuring/model/priority/classes.v

@@ -16,6 +16,11 @@ Class JLFP_policy (Job: JobType) := hep_job : rel Job.
 (** ... a JLDP policy as a relation among jobs that may vary over time. *)
 Class JLDP_policy (Job: JobType) := hep_job_at : instant -> rel Job.
 
+(** NB: The preceding definitions currently make it difficult to express
+        priority policies in which the priority of a job at a given time varies
+        depending on the preceding schedule prefix (e.g., least-laxity
+        first). *)
+
 (** Since FP policies are also JLFP and JLDP policies, we define
    conversions that express the generalization. *)
 Instance FP_to_JLFP (Job: JobType) (Task: TaskType)
@@ -108,4 +113,4 @@ End Priorities.
 
 (** We add the above lemma into a "Hint Database" basic_facts, so Coq 
     will be able to apply them automatically. *)
-Hint Resolve respects_sequential_tasks : basic_facts.
+Hint Resolve respects_sequential_tasks : basic_facts.
\ No newline at end of file

restructuring/model/priority/deadline_monotonic.v

+Require Export rt.restructuring.model.priority.classes.
+
+(** * Deadline-Monotonic Fixed-Priority Policy *)
+
+(** We define the notion of deadline-monotonic task priorities, i.e., tasks are
+    prioritized in order of their relative deadlines. The DM policy belongs to
+    the class of FP policies. *)
+Instance DM (Task : TaskType) `{TaskDeadline Task} : FP_policy Task :=
+{
+  hep_task (tsk1 tsk2 : Task) := task_deadline tsk1 <= task_deadline tsk2
+}.
+
+(** In this section, we prove a few basic properties of the DM policy. *)
+Section Properties.
+
+  (**  Consider any kind of tasks with relative deadlines... *)
+  Context {Task : TaskType}.
+  Context `{TaskDeadline Task}.
+
+  (** ...and jobs stemming from these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+
+  (** DM is reflexive. *)
+  Lemma DM_is_reflexive : reflexive_priorities.
+  Proof. by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /DM. Qed.
+
+  (** DM is transitive. *)
+  Lemma DM_is_transitive : transitive_priorities.
+  Proof. by intros t y x z; apply leq_trans. Qed.
+
+End Properties.
+
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+    will be able to apply them automatically. *)
+Hint Resolve
+     DM_is_reflexive
+     DM_is_transitive: basic_facts.
+

restructuring/model/priority/edf.v

 Require Export rt.restructuring.model.priority.classes.
 
-(** In this section we introduce the notion of EDF priorities. *)
-Program Instance EDF (Job : JobType) `{JobDeadline Job} : JLFP_policy Job :=
-  {
-    hep_job (j1 j2 : Job) := job_deadline j1 <= job_deadline j2
-  }.
+(** * EDF Priority Policy *)
+
+(** We introduce the notion of EDF priorities, wherein jobs are scheduled in
+    order of their urgency. The EDF policy belongs to the class of JLFP
+    policies. *)
+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.

restructuring/model/priority/fifo.v

+Require Export rt.restructuring.model.priority.classes.
+
+(** * FIFO Priority Policy *)
+
+(** We define the notion of FIFO priorities, i.e., jobs are prioritized in
+    order of their arrival times. The FIFO policy belongs to the class of JLFP
+    policies. *)
+Instance FIFO (Job : JobType) `{JobArrival Job} : JLFP_policy Job :=
+{
+  hep_job (j1 j2 : Job) := job_arrival j1 <= job_arrival j2
+}.
+
+(** In this section, we prove a few basic properties of the FIFO policy. *)
+Section Properties.
+
+  (**  Consider any type of jobs with arrival times. *)
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+
+  (** FIFO is reflexive. *)
+  Lemma FIFO_is_reflexive : reflexive_priorities.
+  Proof.  by intros t j; unfold hep_job_at, JLFP_to_JLDP, hep_job, FIFO. Qed.
+
+  (** FIFO is transitive. *)
+  Lemma FIFO_is_transitive : transitive_priorities.
+  Proof. by intros t y x z; apply leq_trans. Qed.
+
+End Properties.
+
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+    will be able to apply them automatically. *)
+Hint Resolve
+     FIFO_is_reflexive
+     FIFO_is_transitive: basic_facts.
+

restructuring/model/priority/numeric_fixed_priority.v

+Require Export rt.restructuring.model.priority.classes.
+
+(** * 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 POSIX). *)
+
+(** 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 the corresponding FP policy. *)
+Instance NumericFP (Task : TaskType) `{TaskPriority Task} : FP_policy Task :=
+{
+  hep_task (tsk1 tsk2 : Task) := task_priority tsk1 >= task_priority tsk2
+}.
+
+(** In this section, we prove a few basic properties of numeric fixed priorities. *)
+Section Properties.
+
+  (**  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. *)
+  Lemma NFP_is_reflexive : reflexive_priorities.
+  Proof. by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP. Qed.
+
+  (** The resulting priority policy is transitive. *)
+  Lemma NFP_is_transitive : transitive_priorities.
+  Proof.
+    move=> t y x z.
+    rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /NumericFP.
+    by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
+  Qed.
+
+End Properties.
+
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+    will be able to apply them automatically. *)
+Hint Resolve
+     NFP_is_reflexive
+     NFP_is_transitive: basic_facts.
+

restructuring/model/priority/rate_monotonic.v

+Require Export rt.restructuring.model.priority.classes.
+Require Export rt.restructuring.model.arrival.sporadic.
+
+
+(** * Rate-Monotonic Fixed-Priority Policy *)
+
+(** We define the notion of rate-monotonic task priorities, i.e., tasks are
+    prioritized in order of their minimum inter-arrival times (or periods). The
+    RM policy belongs to the class of FP policies. *)
+Instance RM (Task : TaskType) `{SporadicModel Task} : FP_policy Task :=
+{
+  hep_task (tsk1 tsk2 : Task) := task_min_inter_arrival_time tsk1 <= task_min_inter_arrival_time tsk2
+}.
+
+(** In this section, we prove a few basic properties of the RM policy. *)
+Section Properties.
+
+  (**  Consider sporadic tasks... *)
+  Context {Task : TaskType}.
+  Context `{SporadicModel Task}.
+
+  (** ...and jobs stemming from these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+
+  (** RM is reflexive. *)
+  Lemma RM_is_reflexive : reflexive_priorities.
+  Proof. by move=> ?; rewrite /hep_job_at /JLFP_to_JLDP /hep_job /FP_to_JLFP /hep_task /RM. Qed.
+
+  (** RM is transitive. *)
+  Lemma RM_is_transitive : transitive_priorities.
+  Proof. by intros t y x z; apply leq_trans. Qed.
+
+End Properties.
+
+(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+    will be able to apply them automatically. *)
+Hint Resolve
+     RM_is_reflexive
+     RM_is_transitive: basic_facts.
+

scripts/wordlist.pws

@@ -25,6 +25,8 @@ preemptable
 preemptions
 EDF
 FP
+DM
+POSIX
 JLFP
 JLDP
 TDMA