From 00a56667ae7e712ffc9ff78fa2deebcba22a8da3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 24 Oct 2019 19:13:27 +0200
Subject: [PATCH] make the proof term in the readiness type class
"unreferencable"
As discussed at the RT-PROOFS meeting in Paris, proof terms should not
have a name so that we don't actually directly depend on them in
proofs. This patch removes the explicit name of the proof term in the
readiness type class and introduces an equivalent lemma.
---
restructuring/analysis/basic_facts/arrivals.v | 20 ++++++++++++++++---
.../analysis/basic_facts/completion.v | 2 +-
restructuring/behavior/ready.v | 13 ++++++++----
3 files changed, 27 insertions(+), 8 deletions(-)
diff --git a/restructuring/analysis/basic_facts/arrivals.v b/restructuring/analysis/basic_facts/arrivals.v
index 3b0c19700..c225c2660 100644
--- a/restructuring/analysis/basic_facts/arrivals.v
+++ b/restructuring/analysis/basic_facts/arrivals.v
@@ -14,14 +14,28 @@ Section Arrived.
readiness. *)
Context `{JobCost Job}.
Context `{JobArrival Job}.
- Context `{JobReady Job PState}.
+ (* We give the readiness typeclass instance a name here because we rely on it
+ explicitly in proofs. *)
+ Context {ReadyParam : JobReady Job PState}.
+
+ (** First, we note that readiness models are by definition consistent
+ w.r.t. [pending]. *)
+ Lemma any_ready_job_is_pending:
+ forall j t,
+ job_ready sched j t -> pending sched j t.
+ Proof.
+ move: ReadyParam => [is_ready CONSISTENT].
+ move=> j t READY.
+ apply CONSISTENT.
+ by exact READY.
+ Qed.
- (** We observe that a given job must have arrived to be ready... *)
+ (** Next, we observe that a given job must have arrived to be ready... *)
Lemma ready_implies_arrived:
forall j t, job_ready sched j t -> has_arrived j t.
Proof.
move=> j t READY.
- move: (any_ready_job_is_pending sched j t READY).
+ move: (any_ready_job_is_pending j t READY).
by rewrite /pending => /andP [ARR _].
Qed.
diff --git a/restructuring/analysis/basic_facts/completion.v b/restructuring/analysis/basic_facts/completion.v
index bb9ed0f1f..7a5eab4e7 100644
--- a/restructuring/analysis/basic_facts/completion.v
+++ b/restructuring/analysis/basic_facts/completion.v
@@ -1,5 +1,5 @@
From rt.restructuring.behavior Require Export all.
-From rt.restructuring.analysis.basic_facts Require Export service.
+From rt.restructuring.analysis.basic_facts Require Export service arrivals.
From rt.util Require Import nat.
diff --git a/restructuring/behavior/ready.v b/restructuring/behavior/ready.v
index ea7133f2a..a2a5d2ee3 100644
--- a/restructuring/behavior/ready.v
+++ b/restructuring/behavior/ready.v
@@ -3,15 +3,20 @@ From rt.restructuring.behavior Require Export service.
(** We define a general notion of readiness of a job: a job can be
- scheduled only when it is ready. This notion of readiness is a general
- concept that is used to model jitter, self-suspensions, etc. Crucially, we
- require that any sensible notion of readiness is a refinement of the notion
+ scheduled only when it is ready, as determined by the predicate
+ [job_ready]. This notion of readiness is a general concept that is
+ used to model jitter, self-suspensions, etc. Crucially, we require
+ that any sensible notion of readiness is a refinement of the notion
of a pending job, i.e., any ready job must also be pending. *)
Class JobReady (Job : JobType) (PState : Type)
`{ProcessorState Job PState} `{JobCost Job} `{JobArrival Job} :=
{
job_ready : schedule PState -> Job -> instant -> bool;
- any_ready_job_is_pending : forall sched j t, job_ready sched j t -> pending sched j t;
+
+ (** What follows is the consistency requirement: We require any
+ reasonable readiness model to consider only pending jobs to be
+ ready. *)
+ _ : forall sched j t, job_ready sched j t -> pending sched j t;
}.
(** Based on the general notion of readiness, we define what it means to be
--
GitLab