From 76c99fedf7a3c71f1165030db855c3d7158b9835 Mon Sep 17 00:00:00 2001
From: Mariam Vardishvili <mariamvardishvili@gmail.com>
Date: Fri, 15 Oct 2021 16:12:21 +0200
Subject: [PATCH] define GEL priority policy
file for gel
definition for gel
file for gel with basic facts
PriorityPoint and comment changes
PriorityPoint and comment changes
GEL rta with integer offset
Added set in proof
modified proof gel_is_total
spell check
spell check
moved defintion of offset and PriorityPoint, modified hep_job for GEL
spelling mistake
Added citation
spell check
---
model/priority/gel.v | 85 ++++++++++++++++++++++++++++++++++++++++++++
scripts/wordlist.pws | 5 ++-
2 files changed, 89 insertions(+), 1 deletion(-)
create mode 100644 model/priority/gel.v
diff --git a/model/priority/gel.v b/model/priority/gel.v
new file mode 100644
index 000000000..319574e09
--- /dev/null
+++ b/model/priority/gel.v
@@ -0,0 +1,85 @@
+Require Export prosa.model.priority.classes.
+Require Export BinInt.
+
+
+(** * GEL Priority Policy * *)
+
+(** We define the class of "Global-EDF-like" (GEL) priority policies,
+ as first introduced by Leontyev et al. ("Multiprocessor Extensions
+ to Real-Time Calculus", Real-Time Systems, 2011).
+
+ GEL scheduling is a (large) subset of the class of JLFP policies,
+ which structurally resembles EDF scheduling, hence the name. Under
+ GEL scheduling, each task has a constant "priority point offset."
+ Each job's priority point is given by its arrival time plus its
+ task's offset, with the interpretation that an earlier priority
+ point implies higher priority.
+
+ EDF and FIFO are both special cases of GEL with the offset
+ respectively being the relative deadline and zero. *)
+
+(** To begin, we define the offset type. Note that an offset may be negative. *)
+Definition offset := Z.
+
+(** We define a task-model parameter to express each task's relative priority point. *)
+Class PriorityPoint (Task : TaskType) := task_priority_point : Task -> offset.
+
+(** Based on the task-level relative priority-point parameter, we
+ define a job's absolute priority point in a straightforward manner.
+ To this end, we need to introduce some context first. *)
+Section AbsolutePriorityPoint.
+ (** For any type of tasks with relative priority points, ... *)
+ Context {Job : JobType} {Task : TaskType} `{JobTask Job Task} `{PriorityPoint Task} `{JobArrival Job}.
+
+ (** ... a job's absolute priority point is given by its arrival time
+ plus its task's relative priority point. *)
+ Definition job_priority_point (j : Job) := (Z.of_nat (job_arrival j) + task_priority_point (job_task j))%Z.
+End AbsolutePriorityPoint.
+
+(** The resulting definition of GEL is straightforward: a job [j1]'s
+ priority is higher than or equal to a job [j2]'s priority iff
+ [j1]'s absolute priority point is no later than [j2]'s absolute
+ priority point. *)
+Instance GEL_priority (Job : JobType) (Task : TaskType)
+ `{PriorityPoint Task} `{JobArrival Job} `{JobTask Job Task} : JLFP_policy Job :=
+{
+ hep_job (j1 j2 : Job) := (job_priority_point j1 <=? job_priority_point j2)%Z
+}.
+
+(** In this section, we note three basic properties of the GEL policy:
+ the priority relation is reflexive, transitive, and total. *)
+Section PropertiesOfGEL.
+
+ (** Consider any type of tasks with relative priority points...*)
+ Context {Task : TaskType} `{PriorityPoint Task}.
+
+ (** ...and jobs of these tasks. *)
+ Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.
+
+ (** GEL is reflexive. *)
+ Fact GEL_is_reflexive : reflexive_priorities.
+ Proof. by move=> t j; apply Z.leb_refl. Qed.
+
+ (** GEL is transitive. *)
+ Fact GEL_is_transitive : transitive_priorities.
+ Proof. by move=> t y x z; apply Zbool.Zle_bool_trans. Qed.
+
+ (** GEL is total. *)
+ Fact GEL_is_total : total_priorities.
+ Proof.
+ move=> t j1 j2; apply /orP.
+ case: (boolP (job_priority_point j1 <=? job_priority_point j2)%Z) => REL; [left | right] => //.
+ move: REL; rewrite -Z.ltb_antisym => /Z.ltb_spec0 REL.
+ by move: (Z.lt_le_incl _ _ REL) => /Z.leb_spec0.
+ Qed.
+
+End PropertiesOfGEL.
+
+(** We add the above facts into a "Hint Database" basic_facts, so Coq
+ will be able to apply them automatically where needed. *)
+Global Hint Resolve
+ GEL_is_reflexive
+ GEL_is_transitive
+ GEL_is_total
+ : basic_facts.
+
diff --git a/scripts/wordlist.pws b/scripts/wordlist.pws
index 548d71327..fce42c60a 100644
--- a/scripts/wordlist.pws
+++ b/scripts/wordlist.pws
@@ -70,4 +70,7 @@ ad
hoc
mailinglist
Gonthier
-setoid
\ No newline at end of file
+setoid
+Leontyev
+et
+al
\ No newline at end of file
--
GitLab