From 0c43c153b0fa3fd857ab96785ebf28c624b3809e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Mon, 9 Dec 2019 12:45:48 +0100
Subject: [PATCH] define notion of job progress / lack of progress
---
restructuring/analysis/definitions/progress.v | 62 +++++++++++++++++++
1 file changed, 62 insertions(+)
create mode 100644 restructuring/analysis/definitions/progress.v
diff --git a/restructuring/analysis/definitions/progress.v b/restructuring/analysis/definitions/progress.v
new file mode 100644
index 000000000..de794d26c
--- /dev/null
+++ b/restructuring/analysis/definitions/progress.v
@@ -0,0 +1,62 @@
+Require Export rt.restructuring.analysis.facts.behavior.service.
+
+(** * Job Progress (or Lack Thereof) *)
+
+(** In the following section, we define a notion of "job progress", and
+ conversely a notion of a lack of progress. *)
+
+Section Progress.
+ (** Consider any type of jobs with a known cost... *)
+ Context {Job : JobType}.
+ Context `{JobCost Job}.
+
+ (** ... and any kind of schedule. *)
+ Context {PState : Type}.
+ Context `{ProcessorState Job PState}.
+
+ (** For a given job and a given schedule... *)
+ Variable sched : schedule PState.
+ Variable j : Job.
+
+ Section NotionsOfProgress.
+
+ (** ...and two ordered points in time... *)
+ Variable t1 t2 : nat.
+ Hypothesis H_t1_before_t2: t1 <= t2.
+
+ (** ... we say that the job has progressed between the two points iff its
+ total received service has increased. *)
+ Definition job_has_progressed := service sched j t1 < service sched j t2.
+
+ (** Conversely, if the accumulated service does not change, there is no
+ progress. *)
+ Definition no_progress := service sched j t1 == service sched j t2.
+
+ (** We note that the negation of the former is equivalent to the latter
+ definition. *)
+ Lemma no_progress_equiv: ~~ job_has_progressed <-> no_progress.
+ Proof.
+ rewrite /job_has_progressed /no_progress.
+ split.
+ { rewrite -leqNgt leq_eqVlt => /orP [EQ|LT]; first by rewrite eq_sym.
+ exfalso.
+ have MONO: service sched j t1 <= service sched j t2
+ by apply service_monotonic.
+ have NOT_MONO: ~~ (service sched j t1 <= service sched j t2)
+ by apply /negPf; apply ltn_geF.
+ move: NOT_MONO => /negP NOT_MONO.
+ contradiction. }
+ { move => /eqP ->.
+ rewrite -leqNgt.
+ by apply service_monotonic. }
+ Qed.
+
+ End NotionsOfProgress.
+
+ (** For convenience, we define a lack of progress also in terms of given
+ reference point [t] and the length of the preceding interval of
+ inactivity [delta], meaning that no progress has been made for at least
+ [delta] time units. *)
+ Definition no_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t.
+
+End Progress.
--
GitLab