From 00a1ec2842bcc0d94e0b395b05d40cf483f1661d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 28 Feb 2025 09:42:55 +0100
Subject: [PATCH 1/2] fix `t = 0` cornercase in definition of `completes_at`
This definition isn't actually used anywhere important, maybe it's
time to get rid of it.
---
behavior/service.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/behavior/service.v b/behavior/service.v
index 507ecddc6..6b7dd9e0a 100644
--- a/behavior/service.v
+++ b/behavior/service.v
@@ -43,8 +43,9 @@ Section Service.
Definition completed_by (j : Job) (t : instant) := service j t >= job_cost j.
(** We say that job [j] completes at time [t] if it has completed by time [t] but
- not by time [t - 1]. *)
- Definition completes_at (j : Job) (t : instant) := ~~ completed_by j t.-1 && completed_by j t.
+ not by time [t - 1] (or if [t == 0]). *)
+ Definition completes_at (j : Job) (t : instant) :=
+ (~~ completed_by j t.-1 || (t == 0)) && completed_by j t.
(** We say that a constant [R] is a response time bound of a job [j] if [j]
has completed by [R] units after its arrival. *)
--
GitLab
From d5f22a4e4e12985fc1245f8e5dfed6c07f7ce60f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 27 Feb 2025 22:03:51 +0100
Subject: [PATCH 2/2] add definition of a job's (precise) finish time
---
analysis/definitions/finish_time.v | 83 ++++++++++++++++++++++++++++++
1 file changed, 83 insertions(+)
create mode 100644 analysis/definitions/finish_time.v
diff --git a/analysis/definitions/finish_time.v b/analysis/definitions/finish_time.v
new file mode 100644
index 000000000..4cf10e0da
--- /dev/null
+++ b/analysis/definitions/finish_time.v
@@ -0,0 +1,83 @@
+Require Export prosa.behavior.service.
+
+(** * Finish Time of a Job *)
+
+(** In this file, we define a job's precise finish time.
+
+ Note that in general a job's finish time may not be defined: if a job never
+ finishes in a given schedule, it does not have a finish time. To get around
+ this, we define a job's finish time under the assumption that _some_ (not
+ necessarily tight) response-time bound [R] is known for the job.
+
+ Under this assumption, we can simply re-use ssreflect's existing [ex_minn]
+ search mechanism (for finding the minimum natural number satisfying a given
+ predicate given a witness that some natural number satisfies the predicate)
+ and benefit from the existing corresponding lemmas. This file briefly
+ illustrates how this can be done. *)
+
+Section JobFinishTime.
+
+ (** Consider any type of jobs with arrival times and costs ... *)
+ Context {Job : JobType} `{JobArrival Job} `{JobCost Job}.
+
+ (** ... and any schedule of such jobs. *)
+ Context {PState : ProcessorState Job}.
+ Variable sched : schedule PState.
+
+ (** Consider an arbitrary job [j]. *)
+ Variable j : Job.
+
+ (** In the following, we proceed under the assumption that [j] finishes
+ eventually (i.e., no later than [R] time units after its arrival, for any
+ finite [R]). *)
+ Variable R : nat.
+ Hypothesis H_response_time_bounded : job_response_time_bound sched j R.
+
+ (** For technical reasons, we restate the response-time assumption explicitly
+ as an existentially quantified variable. *)
+ #[local] Corollary job_finishes : exists t, completed_by sched j t.
+ Proof. by exists (job_arrival j + R); exact: H_response_time_bounded. Qed.
+
+ (** We are now ready for the main definition: job [j]'s finish time is the
+ earliest time [t] such that [completed_by sched j t] holds. This time can
+ be computed with ssreflect's [ex_minn] utility function, which is
+ convenient because then we can reuse the corresponding lemmas. *)
+ Definition finish_time : instant := ex_minn job_finishes.
+
+ (** In the following, we demonstrate the reuse of [ex_minn] properties by
+ establishing three natural properties of a job's finish time. *)
+
+ (** First, a job is indeed complete at its finish time. *)
+ Corollary finished_at_finish_time : completed_by sched j finish_time.
+ Proof.
+ rewrite /finish_time/ex_minn.
+ by case: find_ex_minn.
+ Qed.
+
+ (** Second, a job's finish time is the earliest time that it is complete. *)
+ Corollary earliest_finish_time :
+ forall t,
+ completed_by sched j t ->
+ finish_time <= t.
+ Proof.
+ move=> t COMP.
+ rewrite /finish_time/ex_minn.
+ by case: find_ex_minn.
+ Qed.
+
+ (** Third, Prosa's notion of [completes_at] is satisfied at the finish time. *)
+ Corollary completes_at_finish_time :
+ completes_at sched j finish_time.
+ Proof.
+ apply/andP; split; last exact: finished_at_finish_time.
+ apply/orP; case FIN: finish_time; [by right|left].
+ apply: contra_ltnN => [?|];
+ first by apply: earliest_finish_time.
+ by lia.
+ Qed.
+
+ (** Finally, we can define a job's precise response time as usual as the time
+ from its arrival until its finish time. *)
+ Definition response_time : duration := finish_time - job_arrival j.
+
+End JobFinishTime.
--
GitLab