From 7a653e51399b9bfe82f21e5b9bc6299a6d66fe1e Mon Sep 17 00:00:00 2001
From: Marco Maida <mmaida@mpi-sws.org>
Date: Thu, 7 Apr 2022 10:02:27 +0000
Subject: [PATCH] revise ideal uniprocessor schedule facts
- Slightly change `valid_nonpreemptive_readiness` so that `sched` is a
parameter. This way, the proposition can be assumed to hold only for a
certain schedule (making weaker assumptions).
- Modify `prev_job_nonpreemptive, to unconditionally get
`jobs_must_be_ready_to_execute`.
- Revise lemmas accordingly.
---
analysis/definitions/readiness.v | 4 +-
.../definitions/ideal_uni_scheduler.v | 11 +-
.../facts/ideal_uni/preemption_aware.v | 178 ++++++++++++------
implementation/facts/ideal_uni/prio_aware.v | 25 +--
4 files changed, 142 insertions(+), 76 deletions(-)
diff --git a/analysis/definitions/readiness.v b/analysis/definitions/readiness.v
index c54d8a99a..10ece80b7 100644
--- a/analysis/definitions/readiness.v
+++ b/analysis/definitions/readiness.v
@@ -41,8 +41,8 @@ Section ReadinessModelProperties.
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,
+ Definition valid_nonpreemptive_readiness sched :=
+ forall j t,
~~ job_preemptable j (service sched j t) -> job_ready sched j t.
End ReadinessModelProperties.
diff --git a/implementation/definitions/ideal_uni_scheduler.v b/implementation/definitions/ideal_uni_scheduler.v
index ba842ed21..9924b7e04 100644
--- a/implementation/definitions/ideal_uni_scheduler.v
+++ b/implementation/definitions/ideal_uni_scheduler.v
@@ -31,9 +31,7 @@ Section UniprocessorScheduler.
(** ** Preemption-Aware Scheduler *)
(** First, we define the notion of a generic uniprocessor scheduler that is
- cognizant of non-preemptive sections, ... *)
-
- (** ... so consider any preemption model. *)
+ cognizant of non-preemptive sections, so consider any preemption model. *)
Context `{JobPreemptable Job}.
Section NonPreemptiveSectionAware.
@@ -61,7 +59,8 @@ Section UniprocessorScheduler.
match t with
| 0 => false
| S t' => if sched_prefix t' is Some j then
- ~~job_preemptable j (service sched_prefix j t)
+ job_ready sched_prefix j t &&
+ ~~job_preemptable j (service sched_prefix j t)
else
false
end.
@@ -76,8 +75,8 @@ Section UniprocessorScheduler.
choose_job t (jobs_backlogged_at arr_seq sched_prefix t).
End JobAllocation.
- (* A preemption-policy-aware ideal uniprocessor schedule is then produced
- when using [allocation_at] as the policy for the generic scheduler. *)
+ (** A preemption-policy-aware ideal uniprocessor schedule is then produced
+ when using [allocation_at] as the policy for the generic scheduler. *)
Definition np_uni_schedule : schedule PState := generic_schedule allocation_at idle_state.
End NonPreemptiveSectionAware.
diff --git a/implementation/facts/ideal_uni/preemption_aware.v b/implementation/facts/ideal_uni/preemption_aware.v
index 693699313..43b2dc66d 100644
--- a/implementation/facts/ideal_uni/preemption_aware.v
+++ b/implementation/facts/ideal_uni/preemption_aware.v
@@ -1,6 +1,7 @@
Require Export prosa.implementation.facts.generic_schedule.
Require Export prosa.implementation.definitions.ideal_uni_scheduler.
Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.model.task.sequentiality.
Require Export prosa.model.schedule.limited_preemptive.
(** * Properties of the Preemption-Aware Ideal Uniprocessor Scheduler *)
@@ -14,7 +15,7 @@ Require Import prosa.model.processor.ideal.
Section NPUniprocessorScheduler.
(** Consider any type of jobs with costs and arrival times, ... *)
- Context {Job : JobType} {JC : JobCost Job} {JA : JobArrival Job}.
+ Context {Job : JobType} `{JobCost Job} `{JobArrival Job}.
(** ... in the context of an ideal uniprocessor model. *)
Let PState := ideal.processor_state Job.
@@ -61,9 +62,9 @@ Section NPUniprocessorScheduler.
elim: t => [|t _]; first by apply H_non_idling.
rewrite /allocation_at /prev_job_nonpreemptive.
elim: (sched t) => [j'|]; last by apply H_non_idling.
- rewrite if_neg.
- elim: (job_preemptable j' (service sched j' t.+1)); first by apply H_non_idling.
- by discriminate.
+ move=> SCHED.
+ destruct (job_ready sched j' t.+1 && ~~ job_preemptable j' (service sched j' t.+1)) => //.
+ by apply (H_non_idling t.+1).
Qed.
(** As a stepping stone, we observe that the generated schedule is idle at
@@ -110,63 +111,116 @@ Section NPUniprocessorScheduler.
sequence and only ready jobs are scheduled. *)
Section Validity.
- (** Any reasonable job selection policy will not create jobs "out of thin
- air," i.e., if a job is selected, it was among those given to choose
- from. *)
- Hypothesis H_chooses_from_set:
- forall t s j, choose_job t s = Some j -> j \in s.
-
- (** For the schedule to be valid, we require the notion of readiness to be
- consistent with the preemption model: a non-preemptive job remains
- ready until (at least) the end of its current non-preemptive
- section. *)
- Hypothesis H_valid_preemption_behavior:
- valid_nonpreemptive_readiness RM.
-
- (** First, we show that if a job is chosen from the list of backlogged jobs, then it must be ready. *)
- Lemma choose_job_implies_job_ready:
- forall t j,
- choose_job t.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t) t.+1) = Some j
- -> job_ready schedule j t.+1.
+ (** First, any reasonable job selection policy will not create jobs "out
+ of thin air," i.e., if a job is selected, it was among those given
+ to choose from. *)
+ Hypothesis H_chooses_from_set: forall t s j, choose_job t s = Some j -> j \in s.
+
+ (** Second, for the schedule to be valid, we require the notion of readiness
+ to be consistent with the preemption model: a non-preemptive job remains
+ ready until (at least) the end of its current non-preemptive section. *)
+ Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule.
+
+ (** Finally, we assume the readiness model to be non-clairvoyant. *)
+ Hypothesis H_nonclairvoyant_readiness: nonclairvoyant_readiness RM.
+
+ (** For notational convenience, recall the definition of a prefix of the
+ schedule based on which the next decision is made. *)
+ Let sched_prefix t :=
+ if t is t'.+1 then schedule_up_to policy None t' else empty_schedule idle_state.
+
+ (** We begin by showing that any job in the schedule must come from the arrival
+ sequence used to generate it. *)
+ Lemma np_schedule_jobs_from_arrival_sequence:
+ jobs_come_from_arrival_sequence schedule arr_seq.
+ Proof.
+ move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+ elim: t => [/eqP | t' IH /eqP].
+ - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
+ move: (H_chooses_from_set _ _ _ IN).
+ by apply backlogged_job_arrives_in.
+ - rewrite schedule_up_to_def /allocation_at.
+ case: (prev_job_nonpreemptive (schedule_up_to _ _ t') t'.+1) => [|IN].
+ + by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
+ + move: (H_chooses_from_set _ _ _ IN).
+ by apply backlogged_job_arrives_in.
+ Qed.
+
+ (** Next, we show that any job selected by the job selection policy must
+ be ready. *)
+ Theorem chosen_job_is_ready:
+ forall j t,
+ choose_job t (jobs_backlogged_at arr_seq (sched_prefix t) t) == Some j ->
+ job_ready schedule j t.
Proof.
- move=> t j IN.
- move: (H_chooses_from_set _ _ _ IN).
- rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
- rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t) schedule j t.+1) //.
- by apply schedule_up_to_identical_prefix.
+ move=> j t /eqP SCHED.
+ apply H_chooses_from_set in SCHED.
+ move: SCHED; rewrite mem_filter => /andP [/andP[READY _] IN].
+ rewrite (H_nonclairvoyant_readiness _ (sched_prefix t) j t) //.
+ move=> t' LEQt'.
+ rewrite /schedule /np_uni_schedule /generic_schedule
+ schedule_up_to_def /sched_prefix.
+ destruct t => //=.
+ rewrite -schedule_up_to_def.
+ by apply (schedule_up_to_prefix_inclusion policy).
Qed.
- (** Next, we show that, under these natural assumptions, the generated schedule is valid. *)
+ (** Starting from the previous result we show that, at any instant, only
+ a ready job can be scheduled. *)
+ Theorem jobs_must_be_ready:
+ jobs_must_be_ready_to_execute schedule.
+ Proof.
+ move=> j t SCHED.
+ rewrite scheduled_at_def /schedule /uni_schedule /np_uni_schedule
+ /allocation_at /generic_schedule schedule_up_to_def //= in SCHED.
+ destruct (prev_job_nonpreemptive _) eqn:PREV.
+ { destruct t => //; rewrite //= in SCHED, PREV.
+ destruct (schedule_up_to) => //.
+ move: PREV => /andP [READY _].
+ move: SCHED=> /eqP SCHED.
+ injection SCHED => EQ; rewrite -> EQ in *.
+ erewrite (H_nonclairvoyant_readiness _ _ j t.+1); [by apply READY| |by done].
+ move=> t' LT.
+ rewrite /schedule /np_uni_schedule /generic_schedule //=.
+ rewrite /allocation_at //=.
+ by apply (schedule_up_to_prefix_inclusion policy). }
+ { by apply chosen_job_is_ready. }
+ Qed.
+
+ (** Finally, we show that the generated schedule is valid. *)
Theorem np_schedule_valid:
valid_schedule schedule arr_seq.
Proof.
- split; move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
- { elim: t => [/eqP | t' IH /eqP].
- - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
- move: (H_chooses_from_set _ _ _ IN).
- by apply backlogged_job_arrives_in.
- - rewrite schedule_up_to_def /allocation_at.
- case: (prev_job_nonpreemptive (schedule_up_to _ _ t') t'.+1) => [|IN];
- first by rewrite -pred_Sn => SCHED; apply IH; apply /eqP.
- move: (H_chooses_from_set _ _ _ IN).
- by apply backlogged_job_arrives_in. }
- { elim: t => [/eqP |t' IH /eqP].
- - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
+ rewrite /valid_schedule; split; first by apply np_schedule_jobs_from_arrival_sequence.
+ move=> j t; rewrite scheduled_at_def /schedule /np_uni_schedule /generic_schedule.
+ elim: t => [/eqP |t' IH /eqP].
+ { rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive => IN.
+ move: (H_chooses_from_set _ _ _ IN).
+ rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
+ now rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0). }
+ { rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
+ have JOB: choose_job t'.+1 (jobs_backlogged_at arr_seq (schedule_up_to policy idle_state t') t'.+1)
+ = Some j
+ -> job_ready schedule j t'.+1.
+ { move=> IN.
move: (H_chooses_from_set _ _ _ IN).
rewrite mem_filter /backlogged => /andP [/andP [READY _] _].
- by rewrite -(H_nonclairvoyant_job_readiness (empty_schedule idle_state) schedule j 0).
- - rewrite schedule_up_to_def /allocation_at /prev_job_nonpreemptive.
- case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply choose_job_implies_job_ready.
- destruct (~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply choose_job_implies_job_ready.
- apply H_valid_preemption_behavior.
- injection EQ => <-.
- move: NP.
- have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
- = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
- rewrite /service.
- apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
- by rewrite (schedule_up_to_prefix_inclusion _ _ t t'). }
- Qed.
+ rewrite -(H_nonclairvoyant_job_readiness (schedule_up_to policy idle_state t') schedule j t'.+1) //.
+ rewrite /identical_prefix /schedule /np_uni_schedule /generic_schedule => t'' LT.
+ now rewrite (schedule_up_to_prefix_inclusion _ _ t'' t') //. }
+ case: (schedule_up_to _ _ t' t') => [j' | IN]; last by apply JOB.
+ destruct (job_ready _ _ _ && ~~ job_preemptable j' _) eqn:NP => [EQ|IN]; last by apply JOB.
+ apply H_valid_preemption_behavior.
+ injection EQ => <-.
+ move: NP.
+ have <-: (service (schedule_up_to policy idle_state t') j' t'.+1
+ = service (fun t : instant => schedule_up_to policy idle_state t t) j' t'.+1) => //.
+ rewrite /service.
+ apply equal_prefix_implies_same_service_during => t /andP [_ BOUND].
+ now rewrite (schedule_up_to_prefix_inclusion _ _ t t').
+ rewrite //=.
+ by move=> /andP [? ?]. }
+ Qed.
End Validity.
@@ -210,7 +264,8 @@ Section NPUniprocessorScheduler.
service (schedule_up_to policy idle_state t) j t.+1) => //.
rewrite /service.
apply equal_prefix_implies_same_service_during => t' /andP [_ BOUND].
- by rewrite (schedule_up_to_prefix_inclusion _ _ t' t).
+ rewrite (schedule_up_to_prefix_inclusion _ _ t' t) //.
+ by move=> /andP [? ?].
Qed.
End PreemptionTimes.
@@ -226,6 +281,11 @@ Section NPUniprocessorScheduler.
forall j,
arrives_in arr_seq j ->
job_cannot_become_nonpreemptive_before_execution j.
+
+ (** Second, for the schedule to be valid, we require the notion of readiness
+ to be consistent with the preemption model: a non-preemptive job remains
+ ready until (at least) the end of its current non-preemptive section. *)
+ Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM schedule.
(** Given such a valid preemption model, we establish that the generated
schedule indeed respects the preemption model semantics. *)
@@ -233,7 +293,7 @@ Section NPUniprocessorScheduler.
schedule_respects_preemption_model arr_seq schedule.
Proof.
move=> j.
- elim => [| t' IH]; first by rewrite service0 => ARR /negP NP; move: (H_valid_preemption_function j ARR).
+ elim => [| t' IH];[by rewrite service0=>ARR /negP ?;move:(H_valid_preemption_function j ARR)|].
move=> ARR NP.
have: scheduled_at schedule j t'.
{ apply contraT => NOT_SCHED.
@@ -242,8 +302,12 @@ Section NPUniprocessorScheduler.
by move /negP in NOT_SCHED. }
rewrite !scheduled_at_def /schedule/np_uni_schedule/generic_schedule => /eqP SCHED.
rewrite -SCHED (schedule_up_to_prefix_inclusion _ _ t' t'.+1) // np_job_remains_scheduled //.
- rewrite /prev_job_nonpreemptive SCHED (identical_prefix_service _ schedule) //.
- by apply schedule_up_to_identical_prefix.
+ rewrite /prev_job_nonpreemptive SCHED.
+ rewrite (identical_prefix_service _ schedule); last by apply schedule_up_to_identical_prefix.
+ apply /andP; split => //.
+ rewrite (H_nonclairvoyant_job_readiness _ schedule _ t'.+1) //.
+ - by apply H_valid_preemption_behavior.
+ - by apply schedule_up_to_identical_prefix.
Qed.
End PreemptionCompliance.
diff --git a/implementation/facts/ideal_uni/prio_aware.v b/implementation/facts/ideal_uni/prio_aware.v
index 62b928314..e50693862 100644
--- a/implementation/facts/ideal_uni/prio_aware.v
+++ b/implementation/facts/ideal_uni/prio_aware.v
@@ -19,12 +19,11 @@ Section PrioAwareUniprocessorScheduler.
Hypothesis H_consistent_arrival_times: consistent_arrival_times arr_seq.
(** ... a non-clairvoyant readiness model, ... *)
- Context {RM: JobReady Job (ideal.processor_state Job)}.
+ Context {RM : JobReady Job (ideal.processor_state Job)}.
Hypothesis H_nonclairvoyant_job_readiness: nonclairvoyant_readiness RM.
- (** ... a preemption model that is consistent with the readiness model, ... *)
- Context `{JobPreemptable Job}.
- Hypothesis H_valid_preemption_behavior: valid_nonpreemptive_readiness RM.
+ (** ... a preemption model, ... *)
+ Context `{JobPreemptable Job}.
(** ... and reflexive, total, and transitive JLDP priority policy. *)
Context `{JLDP : JLDP_policy Job}.
@@ -33,9 +32,14 @@ Section PrioAwareUniprocessorScheduler.
Hypothesis H_transitive: transitive_priorities.
(** Consider the schedule generated by the preemption-policy- and
- priority-aware ideal uniprocessor scheduler. *)
+ priority-aware ideal uniprocessor scheduler... *)
Let schedule := uni_schedule arr_seq.
+ (** ...and assume that the preemption model is consistent with the
+ readiness model. *)
+ Hypothesis H_valid_preemption_behavior:
+ valid_nonpreemptive_readiness RM schedule.
+
(** First, we note that the priority-aware job selection policy obviously
maintains work-conservation. *)
Corollary uni_schedule_work_conserving:
@@ -54,7 +58,7 @@ Section PrioAwareUniprocessorScheduler.
Proof.
apply np_schedule_valid => //.
move=> t jobs j.
- now apply supremum_in.
+ by apply supremum_in.
Qed.
(** Third, the schedule respects also the preemption model semantics. *)
@@ -77,7 +81,7 @@ Section PrioAwareUniprocessorScheduler.
Qed.
End PreemptionCompliance.
-
+
(** Now we proceed to the main property of the priority-aware scheduler: in
the following section we establish that [uni_schedule arr_seq] is
compliant with the given priority policy whenever jobs are
@@ -88,9 +92,7 @@ Section PrioAwareUniprocessorScheduler.
policy and a prefix of the schedule based on which the next decision is
made. *)
Let policy := allocation_at arr_seq choose_highest_prio_job.
- Let prefix t := if t is t'.+1
- then schedule_up_to policy idle_state t'
- else empty_schedule idle_state.
+ Let prefix t := if t is t'.+1 then schedule_up_to policy idle_state t' else empty_schedule idle_state.
(** To start, we observe that, at preemption times, the scheduled job is a
supremum w.r.t. to the priority order and the set of backlogged
@@ -120,7 +122,7 @@ Section PrioAwareUniprocessorScheduler.
move=> j1 j2 t ARRIVES PREEMPT BACK_j1 SCHED_j2.
case: (boolP (scheduled_at (uni_schedule arr_seq) j1 t)) => [SCHED_j1|NOT_SCHED_j1].
{ have <-: j1 = j2 by apply (ideal_proc_model_is_a_uniprocessor_model j1 j2 (uni_schedule arr_seq) t).
- now apply H_reflexive_priorities. }
+ by apply H_reflexive_priorities. }
{ move: BACK_j1.
have ->: backlogged (uni_schedule arr_seq) j1 t = backlogged (prefix t) j1 t.
{ apply backlogged_prefix_invariance' with (h := t) => //.
@@ -139,3 +141,4 @@ Section PrioAwareUniprocessorScheduler.
End Priority.
End PrioAwareUniprocessorScheduler.
+
--
GitLab