From e1426920179f0ef3464daa30d84292811d64e326 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Wed, 1 Apr 2020 01:23:18 +0200
Subject: [PATCH] add readiness properties and facts on backlogged
add lemmas on consistency of backlogged jobs set
add notion of a non-clairvoyant readiness model
---
analysis/definitions/readiness.v | 48 ++++++++++
analysis/facts/readiness/backlogged.v | 130 ++++++++++++++++++++++++++
2 files changed, 178 insertions(+)
create mode 100644 analysis/definitions/readiness.v
create mode 100644 analysis/facts/readiness/backlogged.v
diff --git a/analysis/definitions/readiness.v b/analysis/definitions/readiness.v
new file mode 100644
index 000000000..88c69d9e0
--- /dev/null
+++ b/analysis/definitions/readiness.v
@@ -0,0 +1,48 @@
+Require Export prosa.behavior.ready.
+Require Export prosa.analysis.definitions.schedule_prefix.
+Require Export prosa.model.preemption.parameter.
+
+(** * Properties of Readiness Models *)
+
+(** In this file, we define commonsense properties of readiness models. *)
+Section ReadinessModelProperties.
+ (** For any type of jobs with costs and arrival times... *)
+ Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
+
+ (** ... and any kind of processor model, ... *)
+ Context {PState: Type} `{ProcessorState Job PState}.
+
+ (** ... consider a notion of job readiness. *)
+ Variable ReadinessModel : JobReady Job PState.
+
+ (** First, we define a notion of non-clairvoyance for readiness
+ models. Intuitively, whether a job is ready or not should depend only on
+ the past (i.e., prior allocation decisions and job behavior), not on
+ future events. Formally, we say that the [ReadinessModel] is
+ non-clairvoyant if a job's readiness at a given time does not vary across
+ schedules with identical prefixes. That is, given two schedules [sched]
+ and [sched'], the predicates [job_ready sched j t] and [job_ready sched'
+ j t] may not differ if [sched] and [sched'] are identical prior to time
+ [t]. *)
+ Definition nonclairvoyant_readiness :=
+ forall sched sched' j h,
+ identical_prefix sched sched' h ->
+ forall t,
+ t <= h ->
+ job_ready sched j t = job_ready sched' j t.
+
+ (** Next, we relate the readiness model to the preemption model. *)
+ Context `{JobPreemptable Job}.
+
+ (** In a preemption-policy-compliant schedule, nonpreemptive jobs must remain
+ scheduled. Further, in a valid schedule, scheduled jobs must be
+ ready. Consequently, in a valid preemption-policy-compliant schedule, a
+ nonpreemptive job must remain ready until at least the end of its
+ nonpreemptive section. *)
+ Definition valid_nonpreemptive_readiness :=
+ forall sched j t,
+ ~~ job_preemptable j (service sched j t) -> job_ready sched j t.
+
+End ReadinessModelProperties.
+
+
diff --git a/analysis/facts/readiness/backlogged.v b/analysis/facts/readiness/backlogged.v
new file mode 100644
index 000000000..f7b88aa84
--- /dev/null
+++ b/analysis/facts/readiness/backlogged.v
@@ -0,0 +1,130 @@
+Require Export prosa.model.schedule.work_conserving.
+Require Export prosa.analysis.facts.behavior.arrivals.
+Require Export prosa.analysis.definitions.readiness.
+
+(** In this file, we establish basic facts about backlogged jobs. *)
+
+Section BackloggedJobs.
+
+ (** Consider any kind of jobs with arrival times and costs... *)
+ Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
+
+ (** ... and any kind of processor model, ... *)
+ Context {PState : Type} `{ProcessorState Job PState}.
+
+ (** ... and allow for any notion of job readiness. *)
+ Context `{JobReady Job PState}.
+
+ (** Given an arrival sequence and a schedule ... *)
+ Variable arr_seq : arrival_sequence Job.
+ Variable sched : schedule PState.
+
+ (** ... with consistent arrival times, ... *)
+ Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
+
+ (** ... we observe that any backlogged job is indeed in the set of backlogged
+ jobs. *)
+ Lemma mem_backlogged_jobs:
+ forall j t,
+ arrives_in arr_seq j ->
+ backlogged sched j t ->
+ j \in jobs_backlogged_at arr_seq sched t.
+ Proof.
+ move=> j t ARRIVES BACKLOGGED.
+ rewrite /jobs_backlogged_at /arrivals_up_to.
+ rewrite mem_filter.
+ apply /andP; split; first by exact.
+ apply arrived_between_implies_in_arrivals => //.
+ rewrite /arrived_between.
+ apply /andP; split => //.
+ rewrite ltnS -/(has_arrived _ _).
+ now apply (backlogged_implies_arrived sched).
+ Qed.
+
+ (** Trivially, it is also the case that any backlogged job comes from the
+ respective arrival sequence. *)
+ Lemma backlogged_job_arrives_in:
+ forall j t,
+ j \in jobs_backlogged_at arr_seq sched t ->
+ arrives_in arr_seq j.
+ Proof.
+ move=> j t.
+ rewrite /jobs_backlogged_at mem_filter => /andP [_ IN].
+ move: IN. rewrite /arrivals_up_to.
+ now apply in_arrivals_implies_arrived.
+ Qed.
+
+End BackloggedJobs.
+
+(** In the following section, we make one more crucial assumption: namely, that
+ the readiness model is non-clairvoyant, which allows us to relate
+ backlogged jobs in schedules with a shared prefix. *)
+Section NonClairvoyance.
+
+ (** Consider any kind of jobs with arrival times and costs... *)
+ Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
+
+ (** ... any kind of processor model, ... *)
+ Context {PState : Type} `{ProcessorState Job PState}.
+
+ (** ... and allow for any non-clairvoyant notion of job readiness. *)
+ Context {RM : JobReady Job PState}.
+ Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
+
+ (** Consider any arrival sequence ... *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** ... and two schedules ... *)
+ Variable sched sched': schedule PState.
+
+ (** ... with a shared prefix to a fixed horizon. *)
+ Variable h : instant.
+ Hypothesis H_shared_prefix: identical_prefix sched sched' h.
+
+ (** We observe that a job is backlogged at a time in the prefix in one
+ schedule iff it is backlogged in the other schedule due to the
+ non-clairvoyance of the notion of job readiness ... *)
+ Lemma backlogged_prefix_invariance:
+ forall t j,
+ t < h ->
+ backlogged sched j t = backlogged sched' j t.
+ Proof.
+ move=> t j IN_PREFIX.
+ rewrite /backlogged.
+ rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //.
+ rewrite /scheduled_at H_shared_prefix //.
+ now apply ltnW.
+ Qed.
+
+ (** As a corollary, if we further know that j is not scheduled at time [h],
+ we can expand the previous lemma to [t <= h]. *)
+ Corollary backlogged_prefix_invariance':
+ forall t j,
+ ~~ scheduled_at sched j t ->
+ ~~ scheduled_at sched' j t ->
+ t <= h ->
+ backlogged sched j t = backlogged sched' j t.
+ Proof.
+ move=> t j NOT_SCHED NOT_SCHED'.
+ rewrite leq_eqVlt => /orP [/eqP EQ | LT]; last by apply backlogged_prefix_invariance.
+ rewrite /backlogged.
+ rewrite (H_nonclairvoyant_job_readiness sched sched' j h) //;
+ last by rewrite EQ.
+ now rewrite NOT_SCHED NOT_SCHED'.
+ Qed.
+
+ (** ... and also lift this observation to the set of all backlogged jobs at
+ any given time in the shared prefix. *)
+ Lemma backlogged_jobs_prefix_invariance:
+ forall t,
+ t < h ->
+ jobs_backlogged_at arr_seq sched t = jobs_backlogged_at arr_seq sched' t.
+ Proof.
+ move=> t IN_PREFIX.
+ rewrite /jobs_backlogged_at.
+ apply eq_filter.
+ rewrite /eqfun => j.
+ now apply backlogged_prefix_invariance.
+ Qed.
+
+End NonClairvoyance.
--
GitLab