From c65ffcf113c1215fc6f3790ccc5dfe0c9d30f521 Mon Sep 17 00:00:00 2001
From: kimaya <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 25 Oct 2021 16:37:30 +0200
Subject: [PATCH] introduce the job-level predicate `preempted_at`
...and relate it to `nonpreemptive_schedule`, the existing notion of
non-preemptive schedules.
---
analysis/facts/preemption/job/nonpreemptive.v | 49 +++++++++++++++++--
model/preemption/parameter.v | 9 +++-
2 files changed, 54 insertions(+), 4 deletions(-)
diff --git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index be03b3fb3..d2c2ee7b6 100644
--- a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -7,16 +7,17 @@ Require Export prosa.model.schedule.nonpreemptive.
Require Import prosa.model.preemption.fully_nonpreemptive.
(** * Platform for Fully Non-Preemptive model *)
+
(** In this section, we prove that instantiation of predicate
[job_preemptable] to the fully non-preemptive model indeed
defines a valid preemption model. *)
Section FullyNonPreemptiveModel.
-
+
(** Consider any type of jobs. *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
-
+
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
@@ -28,7 +29,7 @@ Section FullyNonPreemptiveModel.
(** ... where jobs do not execute before their arrival or after completion. *)
Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
- Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
+ Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** For simplicity, let's define some local names. *)
Let job_pending := pending sched.
@@ -127,3 +128,45 @@ Section FullyNonPreemptiveModel.
End FullyNonPreemptiveModel.
Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
+
+(** In this section, we prove the equivalence between no preemptions and a non-preemptive schedule. *)
+Section NoPreemptionsEquivalence.
+
+ (** Consider any type of jobs with preemption points. *)
+ Context {Job : JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** Consider an ideal uniprocessor schedule. *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** We prove that no preemptions in a schedule is equivalent to a non-preemptive schedule. *)
+ Lemma no_preemptions_equiv_nonpreemptive :
+ (forall j t, ~~preempted_at sched j t) <-> nonpreemptive_schedule sched.
+ Proof.
+ split.
+ { move=> NOT_PREEMPTED j t t'.
+ elim: t'; first by rewrite leqn0 => /eqP ->.
+ move=> t' IH LE_tt' SCHEDULED INCOMP.
+ apply contraT => NOT_SCHEDULED'.
+ move: LE_tt'. rewrite leq_eqVlt => /orP [/eqP EQ |];
+ first by move: NOT_SCHEDULED' SCHEDULED; rewrite -EQ => /negP //.
+ rewrite ltnS => LEQ.
+ have SCHEDULED': scheduled_at sched j t'
+ by apply IH, (incompletion_monotonic _ _ _ t'.+1) => //.
+ move: (NOT_PREEMPTED j t'.+1).
+ rewrite /preempted_at -pred_Sn -andbA negb_and => /orP [/negP //|].
+ rewrite negb_and => /orP [/negPn|/negPn].
+ - by move: INCOMP => /negP.
+ - by move: NOT_SCHEDULED' => /negP. }
+ { move => NONPRE j t.
+ apply contraT => /negPn /andP [/andP [SCHED_PREV INCOMP] NOT_SCHED].
+ have SCHED: scheduled_at sched j t
+ by apply: (NONPRE j t.-1 t) => //; apply leq_pred.
+ contradict NOT_SCHED.
+ apply /negP.
+ by rewrite Bool.negb_involutive.
+ }
+ Qed.
+
+End NoPreemptionsEquivalence.
diff --git a/model/preemption/parameter.v b/model/preemption/parameter.v
index a02fe8b78..210792017 100644
--- a/model/preemption/parameter.v
+++ b/model/preemption/parameter.v
@@ -87,7 +87,7 @@ End MaxAndLastNonpreemptiveSegment.
model must satisfy. *)
Section PreemptionModel.
- (** Consider any type of jobs with arrival times and execution costs... *)
+ (** Consider any type of jobs with arrival times and execution costs... *)
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
@@ -105,6 +105,13 @@ Section PreemptionModel.
(** ... and any given schedule. *)
Variable sched : schedule PState.
+ (** We say that a job is [preempted_at t] if the job is scheduled at [t-1] and not scheduled at [t],
+ but not completed by [t]. *)
+ Definition preempted_at (j : Job) (t : instant) :=
+ scheduled_at sched j t.-1
+ && ~~ completed_by sched j t
+ && ~~ scheduled_at sched j t.
+
(** In the following, we define the notion of a valid preemption model. To
begin with, we require that a job has to be executed at least one time
instant in order to reach a nonpreemptive segment. In other words, a job
--
GitLab