From d5c8671ad7153c869950dfdf195e63f8df9fcec3 Mon Sep 17 00:00:00 2001
From: kimaya <f20171026@goa.bits-pilani.ac.in>
Date: Mon, 25 Oct 2021 16:11:20 +0200
Subject: [PATCH] move general preemption lemmas
... out of the priority-inversion file, where they are used, but
topically don't belong.
---
.../facts/busy_interval/priority_inversion.v | 67 +--------
analysis/facts/model/preemption.v | 127 ++++++++++++++++++
2 files changed, 128 insertions(+), 66 deletions(-)
create mode 100644 analysis/facts/model/preemption.v
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index 51de4b7fd..a733dc918 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -5,76 +5,11 @@ Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.busy_interval.
Require Export prosa.analysis.facts.model.ideal_schedule.
Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.model.preemption.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
-(** In preparation of the derivation of the priority inversion bound, we
- establish two basic facts on preemption times. *)
-Section PreemptionTimes.
-
- (** Consider any type of tasks ... *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
- Context `{TaskMaxNonpreemptiveSegment Task}.
-
- (** ... and any type of jobs associated with these tasks. *)
- Context {Job : JobType}.
- Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
-
- (** In addition, we assume the existence of a function mapping a
- task to its maximal non-preemptive segment ... *)
- Context `{TaskMaxNonpreemptiveSegment Task}.
-
- (** ... and the existence of a function mapping a job and
- its progress to a boolean value saying whether this job is
- preemptable at its current point of execution. *)
- Context `{JobPreemptable 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.
-
- (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
- Variable sched : schedule (ideal.processor_state Job).
- Hypothesis H_jobs_come_from_arrival_sequence:
- jobs_come_from_arrival_sequence sched arr_seq.
-
- (** Consider a valid model with bounded nonpreemptive segments. *)
- Hypothesis H_model_with_bounded_nonpreemptive_segments:
- valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
-
- (** Then, we show that time 0 is a preemption time. *)
- Lemma zero_is_pt: preemption_time sched 0.
- Proof.
- unfold preemption_time.
- case SCHED: (sched 0) => [j | ]; last by done.
- move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.
- apply H_jobs_come_from_arrival_sequence in ARR.
- rewrite /service /service_during big_geq; last by done.
- destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
- by move: (T1 j ARR) => [PP _].
- Qed.
-
- (** Also, we show that the first instant of execution is a preemption time. *)
- Lemma first_moment_is_pt:
- forall j prt,
- arrives_in arr_seq j ->
- ~~ scheduled_at sched j prt ->
- scheduled_at sched j prt.+1 ->
- preemption_time sched prt.+1.
- Proof.
- intros s pt ARR NSCHED SCHED.
- unfold preemption_time.
- move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
- destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
- by move: (T1 s ARR) => [_ [_ [_ P]]]; apply P.
- Qed.
-
-End PreemptionTimes.
-
(** * Priority inversion is bounded *)
(** In this module we prove that any priority inversion that occurs in the model with bounded
nonpreemptive segments defined in module prosa.model.schedule.uni.limited.platform.definitions
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
new file mode 100644
index 000000000..d2feb8504
--- /dev/null
+++ b/analysis/facts/model/preemption.v
@@ -0,0 +1,127 @@
+Require Export prosa.model.schedule.priority_driven.
+Require Export prosa.analysis.facts.model.ideal_schedule.
+Require Export prosa.analysis.facts.behavior.completion.
+
+
+(** In this section, we establish two basic facts about preemption times. *)
+Section PreemptionTimes.
+
+ (** Consider any type of jobs. *)
+ Context {Job : JobType}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** In addition, we assume the existence of a function mapping a job and
+ its progress to a boolean value saying whether this job is
+ preemptable at its current point of execution. *)
+ Context `{JobPreemptable 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.
+
+ (** Next, consider any ideal uniprocessor schedule of this arrival sequence... *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** ...where, jobs come from the arrival sequence. *)
+ Hypothesis H_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched arr_seq.
+
+ (** Consider a valid preemption model. *)
+ Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+ (** We show that time 0 is a preemption time. *)
+ Lemma zero_is_pt: preemption_time sched 0.
+ Proof.
+ unfold preemption_time.
+ case SCHED: (sched 0) => [j | ]; last by done.
+ move: (SCHED) => /eqP; rewrite -scheduled_at_def; move => ARR.
+ apply H_jobs_come_from_arrival_sequence in ARR.
+ rewrite /service /service_during big_geq; last by done.
+ by move: (H_valid_preemption_model j ARR) => [PP _].
+ Qed.
+ (** Also, we show that the first instant of execution is a preemption time. *)
+ Lemma first_moment_is_pt:
+ forall j prt,
+ arrives_in arr_seq j ->
+ ~~ scheduled_at sched j prt ->
+ scheduled_at sched j prt.+1 ->
+ preemption_time sched prt.+1.
+ Proof.
+ intros s pt ARR NSCHED SCHED.
+ unfold preemption_time.
+ move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
+ by move: (H_valid_preemption_model s ARR) => [_ [_ [_ P]]]; apply P.
+ Qed.
+
+End PreemptionTimes.
+
+(** In this section, we prove a lemma relating scheduling and preemption times. *)
+Section PreemptionFacts.
+
+ (** Consider any type of jobs. *)
+ Context {Job : JobType}.
+ Context `{Arrival : JobArrival Job}.
+ Context `{Cost : JobCost Job}.
+ Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+
+ (** Consider any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** ...and, assume that the schedule is valid. *)
+ Hypothesis H_sched_valid : valid_schedule sched arr_seq.
+
+ (** In addition, we assume the existence of a function mapping jobs to their preemption points ... *)
+ Context `{JobPreemptable Job}.
+
+ (** ... and assume that it defines a valid preemption model. *)
+ Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+ (** We prove that every nonpreemptive segment always begins with a preemption time. *)
+ Lemma scheduling_of_any_segment_starts_with_preemption_time:
+ forall j t,
+ scheduled_at sched j t ->
+ exists pt,
+ job_arrival j <= pt <= t /\
+ preemption_time sched pt /\
+ (forall t', pt <= t' <= t -> scheduled_at sched j t').
+ Proof.
+ intros s t SCHEDst.
+ have EX: exists t', (t' <= t) && (scheduled_at sched s t')
+ && (all (fun t'' => scheduled_at sched s t'') (index_iota t' t.+1 )).
+ { exists t. apply/andP; split; [ by apply/andP; split | ].
+ apply/allP; intros t'.
+ by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.
+ }
+ have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts.
+ move : (H_sched_valid) => [COME_ARR READY].
+ have MIN := ex_minnP EX.
+ move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
+ destruct mpt.
+ - exists 0; repeat split.
+ + by apply/andP; split => //; apply MATE.
+ + eapply (zero_is_pt arr_seq); eauto 2.
+ + by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS.
+ - have NSCHED: ~~ scheduled_at sched s mpt.
+ { apply/negP; intros SCHED.
+ enough (F : mpt < mpt); first by rewrite ltnn in F.
+ apply MIN.
+ apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
+ apply/allP; intros t'.
+ rewrite mem_index_iota; move => /andP [GE LE].
+ move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].
+ - by subst t'.
+ - by apply ALL; rewrite mem_index_iota; apply/andP; split.
+ }
+ have PP: preemption_time sched mpt.+1 by eapply (first_moment_is_pt arr_seq) with (j := s); eauto 2.
+ exists mpt.+1; repeat split; try done.
+ + apply/andP; split; last by done.
+ by apply MATE in SCHEDsmpt.
+ + move => t' /andP [GE LE].
+ by apply ALL; rewrite mem_index_iota; apply/andP; split.
+ Qed.
+
+End PreemptionFacts.
--
GitLab