From 2dc14ac2b5f9ed61f9b69c0c823a7e080085a79b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 12 Dec 2019 14:55:14 +0100
Subject: [PATCH] note that common priority policies are total
---
restructuring/model/priority/deadline_monotonic.v | 8 +++++++-
restructuring/model/priority/edf.v | 8 +++++++-
restructuring/model/priority/fifo.v | 8 +++++++-
restructuring/model/priority/numeric_fixed_priority.v | 8 +++++++-
restructuring/model/priority/rate_monotonic.v | 8 +++++++-
5 files changed, 35 insertions(+), 5 deletions(-)
diff --git a/restructuring/model/priority/deadline_monotonic.v b/restructuring/model/priority/deadline_monotonic.v
index ff88a5370..ff680b9dd 100644
--- a/restructuring/model/priority/deadline_monotonic.v
+++ b/restructuring/model/priority/deadline_monotonic.v
@@ -29,11 +29,17 @@ Section Properties.
Lemma DM_is_transitive : transitive_priorities.
Proof. by intros t y x z; apply leq_trans. Qed.
+ (** DM is total. *)
+ Lemma DM_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. 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.
+ DM_is_transitive
+ DM_is_total
+ : basic_facts.
diff --git a/restructuring/model/priority/edf.v b/restructuring/model/priority/edf.v
index aaa2db8a8..16f470985 100644
--- a/restructuring/model/priority/edf.v
+++ b/restructuring/model/priority/edf.v
@@ -28,11 +28,17 @@ Section PropertiesOfEDF.
Lemma EDF_is_transitive : transitive_priorities.
Proof. by intros t y x z; apply leq_trans. Qed.
+ (** EDF is total. *)
+ Lemma EDF_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. Qed.
+
End PropertiesOfEDF.
(** 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: basic_facts.
+ EDF_is_transitive
+ EDF_is_total
+ : basic_facts.
diff --git a/restructuring/model/priority/fifo.v b/restructuring/model/priority/fifo.v
index a8bf7af8b..2e16246e8 100644
--- a/restructuring/model/priority/fifo.v
+++ b/restructuring/model/priority/fifo.v
@@ -25,11 +25,17 @@ Section Properties.
Lemma FIFO_is_transitive : transitive_priorities.
Proof. by intros t y x z; apply leq_trans. Qed.
+ (** FIFO is total. *)
+ Lemma FIFO_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. 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.
+ FIFO_is_transitive
+ FIFO_is_total
+ : basic_facts.
diff --git a/restructuring/model/priority/numeric_fixed_priority.v b/restructuring/model/priority/numeric_fixed_priority.v
index dd926cf88..689f61b98 100644
--- a/restructuring/model/priority/numeric_fixed_priority.v
+++ b/restructuring/model/priority/numeric_fixed_priority.v
@@ -41,11 +41,17 @@ Section Properties.
by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
Qed.
+ (** The resulting priority policy is total. *)
+ Lemma NFP_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. 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.
+ NFP_is_transitive
+ NFP_is_total
+ : basic_facts.
diff --git a/restructuring/model/priority/rate_monotonic.v b/restructuring/model/priority/rate_monotonic.v
index 4d3606e01..3ab5fa7f2 100644
--- a/restructuring/model/priority/rate_monotonic.v
+++ b/restructuring/model/priority/rate_monotonic.v
@@ -31,11 +31,17 @@ Section Properties.
Lemma RM_is_transitive : transitive_priorities.
Proof. by intros t y x z; apply leq_trans. Qed.
+ (** RM is total. *)
+ Lemma RM_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. 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.
+ RM_is_transitive
+ RM_is_total
+ : basic_facts.
--
GitLab