From 9cc286c23e7d6f641c796552614cecd0bcec6033 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Wed, 6 Oct 2021 16:16:15 +0200
Subject: [PATCH] move lemma [early_hep_job_is_scheduled] to separate file
---
analysis/definitions/always_higher_priority.v | 20 ++++
analysis/facts/{ => priority}/edf.v | 64 +++----------
analysis/facts/priority/sequential.v | 94 +++++++++++++++++++
results/edf/rta/bounded_pi.v | 2 +-
4 files changed, 127 insertions(+), 53 deletions(-)
create mode 100644 analysis/definitions/always_higher_priority.v
rename analysis/facts/{ => priority}/edf.v (59%)
create mode 100644 analysis/facts/priority/sequential.v
diff --git a/analysis/definitions/always_higher_priority.v b/analysis/definitions/always_higher_priority.v
new file mode 100644
index 000000000..34aa16969
--- /dev/null
+++ b/analysis/definitions/always_higher_priority.v
@@ -0,0 +1,20 @@
+Require Export prosa.model.priority.classes.
+
+(** * Always Higher Priority *)
+(** In this section, we define what it means for a job to always have
+ a higher priority than another job. *)
+Section AlwaysHigherPriority.
+
+ (** Consider any type of jobs ... *)
+ Context {Job : JobType}.
+
+ (** ... and any JLDP policy. *)
+ Context `{JLDP_policy Job}.
+
+ (** We say that a job [j1] always has higher priority than job [j2]
+ if, at any time [t], the priority of job [j1] is strictly higher than
+ the priority of job [j2]. *)
+ Definition always_higher_priority (j1 j2 : Job) :=
+ forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.
+
+End AlwaysHigherPriority.
diff --git a/analysis/facts/edf.v b/analysis/facts/priority/edf.v
similarity index 59%
rename from analysis/facts/edf.v
rename to analysis/facts/priority/edf.v
index 95d1d7c38..340dc68e8 100644
--- a/analysis/facts/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -36,6 +36,7 @@ Global Hint Resolve EDF_respects_sequential_tasks : basic_facts.
Require Export prosa.model.task.sequentiality.
Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.priority.sequential.
(** In this section, we prove that EDF priority policy
implies that tasks are sequential. *)
@@ -81,64 +82,23 @@ Section SequentialEDF.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
(** Next, we assume that the schedule respects the policy defined by
- the [job_preemptable] function (i.e., jobs have bounded
- non-preemptive segments). *)
+ the [job_preemptable] function (i.e., jobs have bounded
+ non-preemptive segments). *)
Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
-
- (** We say that a job [j1] always has higher priority than job [j2]
- if, at any time [t], the priority of job [j1] is strictly higher than
- priority of job [j2].
-
- NB: this definition and the following lemma are general facts about
- priority policies on uniprocessors that depend on neither EDF nor the ideal uniprocessor assumption. Generalizing to any priority policy and processor
- model left to future work.
- (https://gitlab.mpi-sws.org/RT-PROOFS/rt-proofs/-/issues/78). *)
- Definition always_higher_priority j1 j2 :=
- forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.
-
- (** First, we show that, given two jobs [j1] and [j2], if job [j1]
- arrives earlier than job [j2] and [j1] always has higher
- priority than [j2], then [j2] is scheduled only after [j1] is
- completed. *)
- Lemma early_hep_job_is_scheduled:
- forall j1 j2,
- arrives_in arr_seq j1 ->
- job_arrival j1 < job_arrival j2 ->
- always_higher_priority j1 j2 ->
- forall t,
- scheduled_at sched j2 t ->
- completed_by sched j1 t.
- Proof.
- move=> j1 j2 ARR LE AHP t SCHED; apply/negPn/negP; intros NCOMPL.
- move: H_sched_valid => [COARR MBR].
- have ARR_EXEC := jobs_must_arrive_to_be_ready sched MBR.
- edestruct scheduling_of_any_segment_starts_with_preemption_time
- as [pt [LET [PT ALL_SCHED]]]; try eauto 2.
- move: LET => /andP [LE1 LE2].
- specialize (ALL_SCHED pt); feed ALL_SCHED; first by apply/andP; split.
- have PEND1: pending sched j1 pt.
- { apply/andP; split.
- - by rewrite /has_arrived; ssrlia.
- - by move: NCOMPL; apply contra, completion_monotonic.
- }
- apply H_job_ready in PEND1 => //; destruct PEND1 as [j3 [ARR3 [READY3 HEP3]]].
- move: (AHP pt) => /andP[HEP /negP NHEP]; eapply NHEP.
- eapply EDF_is_transitive; last by apply HEP3.
- eapply H_respects_policy; eauto 2.
- apply/andP; split; first by done.
- apply/negP; intros SCHED2.
- have EQ := ideal_proc_model_is_a_uniprocessor_model _ _ _ pt SCHED2 ALL_SCHED.
- subst j2; rename j3 into j.
- by specialize (AHP 0); destruct AHP; auto.
- Qed.
- (** Clearly, under the EDF priority policy, jobs satisfy the conditions
- described by the lemma above; hence EDF implies sequential tasks. *)
+ (** To prove sequentiality, we use lemma
+ [early_hep_job_is_scheduled]. Clearly, under the EDF priority
+ policy, jobs satisfy the conditions described by the lemma
+ (i.e., given two jobs [j1] and [j2] from the same task, if [j1]
+ arrives earlier than [j2], then [j1] always has a higher
+ priority than job [j2], and hence completes before [j2]);
+ therefore EDF implies sequential tasks. *)
Lemma EDF_implies_sequential_tasks:
sequential_tasks arr_seq sched.
Proof.
intros ? ? ? ARR1 ARR2 SAME LT.
- apply early_hep_job_is_scheduled => //.
+ eapply early_hep_job_is_scheduled => //; eauto 2.
+ - by auto with basic_facts.
- clear t; intros ?.
move: SAME => /eqP SAME.
apply /andP.
diff --git a/analysis/facts/priority/sequential.v b/analysis/facts/priority/sequential.v
new file mode 100644
index 000000000..790bf443d
--- /dev/null
+++ b/analysis/facts/priority/sequential.v
@@ -0,0 +1,94 @@
+Require Export prosa.analysis.definitions.always_higher_priority.
+Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+
+(** In this section, we prove that, given two jobs [j1] and [j2], if
+ job [j1] arrives earlier than job [j2] and [j1] always has higher
+ priority than [j2], then [j2] is scheduled only after [j1] is
+ completed. *)
+Section SequentialJLFP.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskDeadline Task}.
+
+ (** ... with a bound on the maximum non-preemptive segment length.
+ The bound is needed to ensure that, at any instant, it always
+ exists a subsequent preemption time in which the scheduler can,
+ if needed, switch to another higher-priority job. *)
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** Further, consider any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{Arrival : JobArrival Job}.
+ Context `{Cost : JobCost Job}.
+
+ (** Consider any arrival sequence. *)
+ Variable arr_seq : arrival_sequence Job.
+
+ (** Consider a JLFP-policy that indicates a higher-or-equal priority
+ relation, and assume that this relation is transitive. *)
+ Context `{JLFP_policy Job}.
+ Hypothesis H_priority_is_transitive : transitive_priorities.
+
+ (** Next, consider any ideal uni-processor schedule of this arrival sequence, ... *)
+ Variable sched : schedule (ideal.processor_state Job).
+
+ (** ... allow for any work-bearing notion of job readiness, ... *)
+ Context `{@JobReady Job (ideal.processor_state Job) _ Cost Arrival}.
+ Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
+
+ (** ... 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 with
+ bounded non-preemptive segments. *)
+ Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
+ valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+ (** Next, we assume that the schedule respects the policy defined by
+ the [job_preemptable] function (i.e., jobs have bounded
+ non-preemptive segments). *)
+ Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+
+ (** We show that, given two jobs [j1] and [j2], if job [j1] arrives
+ earlier than job [j2] and [j1] always has higher priority than
+ [j2], then [j2] is scheduled only after [j1] is completed. *)
+ Lemma early_hep_job_is_scheduled :
+ forall j1 j2,
+ arrives_in arr_seq j1 ->
+ job_arrival j1 < job_arrival j2 ->
+ always_higher_priority j1 j2 ->
+ forall t,
+ scheduled_at sched j2 t ->
+ completed_by sched j1 t.
+ Proof.
+ move=> j1 j2 ARR LE AHP t SCHED; apply/negPn/negP; intros NCOMPL.
+ move: H_sched_valid => [COARR MBR].
+ have ARR_EXEC := jobs_must_arrive_to_be_ready sched MBR.
+ edestruct scheduling_of_any_segment_starts_with_preemption_time
+ as [pt [LET [PT ALL_SCHED]]]; try eauto 2.
+ move: LET => /andP [LE1 LE2].
+ specialize (ALL_SCHED pt); feed ALL_SCHED; first by apply/andP; split.
+ have PEND1: pending sched j1 pt.
+ { apply/andP; split.
+ - by rewrite /has_arrived; ssrlia.
+ - by move: NCOMPL; apply contra, completion_monotonic.
+ }
+ apply H_job_ready in PEND1 => //; destruct PEND1 as [j3 [ARR3 [READY3 HEP3]]].
+ move: (AHP pt) => /andP[HEP /negP NHEP]; eapply NHEP.
+ eapply H_priority_is_transitive; last by apply HEP3.
+ eapply H_respects_policy; eauto 2.
+ apply/andP; split; first by done.
+ apply/negP; intros SCHED2.
+ have EQ := ideal_proc_model_is_a_uniprocessor_model _ _ _ pt SCHED2 ALL_SCHED.
+ subst j2; rename j3 into j.
+ by specialize (AHP 0); destruct AHP; auto.
+ Qed.
+
+End SequentialJLFP.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 372157f90..b2690aadf 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.facts.edf.
+Require Export prosa.analysis.facts.priority.edf.
Require Export prosa.analysis.definitions.schedulability.
Require Import prosa.model.priority.edf.
Require Import prosa.model.task.absolute_deadline.
--
GitLab