From f6c31ca076f3410eff692d32b4b18d0569df3f69 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Fri, 25 Sep 2020 13:08:21 +0200
Subject: [PATCH] adjust lemmas to work-bearing readiness
With some misc. cleanups and reorganization thrown in.
---
analysis/abstract/abstract_seq_rta.v | 14 +-
analysis/abstract/ideal_jlfp_rta.v | 29 ++--
analysis/definitions/task_schedule.v | 1 +
analysis/facts/busy_interval/busy_interval.v | 94 +++++++------
analysis/facts/busy_interval/carry_in.v | 105 ++++++++-------
.../facts/busy_interval/priority_inversion.v | 127 +++++++++---------
.../rtc_threshold/job_preemptable.v | 2 +-
analysis/facts/readiness/basic.v | 4 +
8 files changed, 198 insertions(+), 178 deletions(-)
diff --git a/analysis/abstract/abstract_seq_rta.v b/analysis/abstract/abstract_seq_rta.v
index 196493031..0217e3d95 100644
--- a/analysis/abstract/abstract_seq_rta.v
+++ b/analysis/abstract/abstract_seq_rta.v
@@ -231,13 +231,13 @@ Section Sequential_Abstract_RTA.
completed_by sched j2 t1.
Proof.
move => JA; move: (H_j2_from_tsk) => /eqP TSK2eq.
- move: (posnP (@job_cost _ H3 j2)) => [ZERO|POS].
- { by rewrite /completed_by /service.completed_by ZERO. }
- move: (H_interference_and_workload_consistent_with_sequential_tasks
- j1 t1 t2 H_j1_arrives H_j1_from_tsk H_j1_cost_positive H_busy_interval) => SWEQ.
- eapply all_jobs_have_completed_equiv_workload_eq_service
- with (j := j2) in SWEQ; eauto 2; try done.
- by apply arrived_between_implies_in_arrivals.
+ rewrite /completed_by.
+ move: (posnP (@job_cost _ H3 j2)) => [-> | POS]; first by done.
+ move: (H_interference_and_workload_consistent_with_sequential_tasks j1 t1 t2) => SWEQ.
+ feed_n 4 SWEQ; try by done.
+ apply all_jobs_have_completed_equiv_workload_eq_service with (j := j2) in SWEQ => //.
+ - by apply ideal_proc_model_provides_unit_service.
+ - by apply arrived_between_implies_in_arrivals.
Qed.
(** Next we prove that if a job is pending after the beginning
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index b963583f2..1eabeef9b 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -2,13 +2,9 @@ Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.abstract.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-(** In this file we consider an ideal uni-processor ... *)
+(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
-(** ... and classic model of readiness without jitter and no
- self-suspensions, where pending jobs are always ready. *)
-Require Import prosa.model.readiness.basic.
-
(** * JLFP instantiation of Interference and Interfering Workload for ideal uni-processor. *)
(** In this module we instantiate functions Interference and Interfering Workload
for an arbitrary JLFP-policy that satisfies the sequential tasks hypothesis.
@@ -372,9 +368,11 @@ Section JLFPInstantiation.
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (another_hep_job jo j) eqn:PRIO.
- - rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
- eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
- erewrite leq_sum; eauto 2.
+ - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between t1 t) _ x.
+ eapply leq_trans; last first.
+ + apply SCH; eauto using arrivals_uniq, ideal_proc_model_provides_unit_service,
+ ideal_proc_model_is_a_uniprocessor_model.
+ + by erewrite leq_sum.
- rewrite leqn0 big1 //; intros joo PRIO2.
apply/eqP; rewrite eqb0; apply/eqP; intros C.
inversion C; subst joo; clear C.
@@ -413,9 +411,11 @@ Section JLFPInstantiation.
{ ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
move: (Sched_jo); rewrite scheduled_at_def; move => /eqP EQ; rewrite EQ.
destruct (hep_job_from_another_task jo j) eqn:PRIO.
- - rewrite -EQ. have SCH := service_of_jobs_le_1 sched _ (arrivals_between t1 t) _ x.
- eapply leq_trans; last by apply SCH; eauto using arrivals_uniq.
- erewrite leq_sum; eauto 2.
+ - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between t1 t) _ x.
+ eapply leq_trans; last first.
+ + by apply SCH; eauto using arrivals_uniq, ideal_proc_model_provides_unit_service,
+ ideal_proc_model_is_a_uniprocessor_model.
+ + by erewrite leq_sum.
- rewrite leqn0 big1 //; intros joo PRIO2.
apply/eqP; rewrite eqb0; apply/eqP; intros C.
inversion C; subst joo; clear C.
@@ -455,8 +455,9 @@ Section JLFPInstantiation.
last by apply zero_is_quiet_time.
have L2 := instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs.
rewrite /cumulative_interfering_workload_of_hep_jobs in L2; rewrite L2; clear L2.
- rewrite eq_sym; apply/eqP.
- apply all_jobs_have_completed_equiv_workload_eq_service; try done.
+ rewrite eq_sym; apply/eqP.
+ apply all_jobs_have_completed_equiv_workload_eq_service;
+ eauto using ideal_proc_model_provides_unit_service.
intros; apply QT.
- by apply in_arrivals_implies_arrived in H4.
- by move: H5 => /andP [H6 H7].
@@ -479,7 +480,7 @@ Section JLFPInstantiation.
intros t [T0 T1]; intros jhp ARR HP ARB.
eapply all_jobs_have_completed_equiv_workload_eq_service with
(P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t);
- eauto 2; last eapply arrived_between_implies_in_arrivals; try done.
+ eauto using arrived_between_implies_in_arrivals, ideal_proc_model_provides_unit_service.
move: T0; rewrite /cumul_interference /cumul_interfering_workload.
rewrite CIS !big_split //=; move => /eqP; rewrite eqn_add2l.
rewrite IC1; last by apply zero_is_quiet_time.
diff --git a/analysis/definitions/task_schedule.v b/analysis/definitions/task_schedule.v
index 83065b17e..0838ff171 100644
--- a/analysis/definitions/task_schedule.v
+++ b/analysis/definitions/task_schedule.v
@@ -1,4 +1,5 @@
Require Export prosa.model.task.concept.
+Require Export prosa.analysis.facts.model.ideal_schedule.
(** Due to historical reasons this file defines the notion of a
schedule of a task for the ideal uni-processor model. This is not
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index ee074f832..fcf7a6af2 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -3,13 +3,11 @@ Require Export prosa.analysis.definitions.job_properties.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.facts.behavior.all.
Require Export prosa.analysis.facts.model.service_of_jobs.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
-
(** * Existence of Busy Interval for JLFP-models *)
(** In this module we derive a sufficient condition for existence of
busy intervals for uni-processor for JLFP schedulers. *)
@@ -22,8 +20,8 @@ Section ExistsBusyIntervalJLFP.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ Context {Arrival: JobArrival Job}.
+ Context {Cost : JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
@@ -39,8 +37,12 @@ Section ExistsBusyIntervalJLFP.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
(** Assume a given JLFP policy. *)
- Context `{JLFP_policy Job}.
-
+ Context `{JLFP_policy Job}.
+
+ (** Further, 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.
+
(** For simplicity, let's define some local names. *)
Let job_pending_at := pending sched.
Let job_completed_by := completed_by sched.
@@ -150,15 +152,15 @@ Section ExistsBusyIntervalJLFP.
Proof.
intros t IDLE jhp ARR HP AB.
apply negbNE; apply/negP; intros NCOMP.
- rewrite /arrived_before ltnS in AB.
- move:(H_work_conserving _ t ARR) => WC.
- feed WC.
- { apply/andP. split.
- - apply/negPn/negP; rewrite negb_and; intros COMP.
- move: COMP => /orP; rewrite Bool.negb_involutive; move => [/negP CON|COM]; auto.
- move: NCOMP => /negP NCOMP; apply: NCOMP.
- by apply completion_monotonic with t.
- - by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE.
+ have PEND : job_pending_at jhp t.
+ { apply/andP; split; first by done.
+ by move: NCOMP; apply contra, completion_monotonic.
+ }
+ apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+ move:(H_work_conserving j' t) => WC.
+ feed_n 2 WC; first by done.
+ { apply/andP; split; first by done.
+ by move: IDLE => /eqP IDLE; rewrite /scheduled_at scheduled_in_def IDLE.
}
move: IDLE WC => /eqP IDLE [jo SCHED].
by rewrite scheduled_at_def IDLE in SCHED.
@@ -224,8 +226,8 @@ Section ExistsBusyIntervalJLFP.
Proof.
intros t NEQ IDLE.
move: (pending_hp_job_exists _ NEQ) => [jhp [ARR [PEND HP]]].
- unfold work_conserving in *.
- feed (H_work_conserving _ t ARR).
+ apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+ feed (H_work_conserving _ t ARR').
apply/andP; split; first by done.
move: IDLE => /eqP IDLE; rewrite scheduled_at_def IDLE; by done.
move: (H_work_conserving) => [jo SCHED].
@@ -288,42 +290,38 @@ Section ExistsBusyIntervalJLFP.
- by eapply in_arrivals_implies_arrived; eauto 2.
- by eapply in_arrivals_implies_arrived_before; eauto 2.
Qed.
-
+
(** Next we prove that the total service within a "non-quiet"
- time interval <<[t1, t1 + Δ)>> is exactly Δ. *)
+ time interval <<[t1, t1 + Δ)>> is exactly [Δ]. *)
Lemma no_idle_time_within_non_quiet_time_interval:
service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
Proof.
- intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
+ intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs.
rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
apply/eqP; rewrite eqn_leq; apply/andP; split.
- { rewrite leq_sum //.
- move => t' _.
- have SCH := service_of_jobs_le_1 sched predT (arrivals_between 0 (t1 + Δ)) _ t'.
- by eauto using arrivals_uniq.
- }
- { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=; rewrite leq_sum //.
- move => t' /andP [/andP [LT GT] _].
- apply/sum_seq_gt0P.
+ { rewrite leq_sum // => t' _.
+ have SCH := @service_of_jobs_le_1 _ _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).
+ eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts.
+ by rewrite leq_sum // => i _; rewrite -scheduled_at_def service_at_is_scheduled_at. }
+ { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
+ leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
ideal_proc_model_sched_case_analysis_eq sched t' jo.
{ exfalso; move: LT; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT].
{ subst t'.
feed (H_no_quiet_time t1.+1); first by apply/andP; split.
- apply: H_no_quiet_time.
- by apply idle_time_implies_quiet_time_at_the_next_time_instant.
- }
+ by apply H_no_quiet_time, idle_time_implies_quiet_time_at_the_next_time_instant. }
{ feed (H_no_quiet_time t'); first by apply/andP; split; last rewrite ltnW.
apply: H_no_quiet_time; intros j_hp IN HP ARR.
- apply contraT; intros NOTCOMP.
- destruct (scheduled_at sched j_hp t') eqn:SCHEDhp;
- first by rewrite scheduled_at_def EqIdle in SCHEDhp.
- apply negbT in SCHEDhp.
- feed (H_work_conserving j_hp t' IN);
- first by repeat (apply/andP; split); first by apply ltnW.
+ apply contraT; intros NCOMP.
+ have PEND : job_pending_at j_hp t'.
+ { apply/andP; split.
+ - by rewrite /has_arrived ltnW.
+ - by move: NCOMP; apply contra, completion_monotonic. }
+ apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' _]]].
+ feed (H_work_conserving _ t' ARR').
+ { by apply/andP; split; last rewrite scheduled_at_def EqIdle. }
move: H_work_conserving => [j_other SCHEDother].
- by rewrite scheduled_at_def EqIdle in SCHEDother.
- }
- }
+ by rewrite scheduled_at_def EqIdle in SCHEDother. } }
{ exists jo; split.
- apply arrived_between_implies_in_arrivals; try done.
apply H_jobs_come_from_arrival_sequence with t'; try done.
@@ -472,12 +470,10 @@ Section ExistsBusyIntervalJLFP.
apply leq_trans with (cumulative_priority_inversion sched j t1 (t1 + delta) + hp_service t1 (t1 + delta)).
{ rewrite /hp_service hep_jobs_receive_no_service_before_quiet_time //.
rewrite /service_of_higher_or_equal_priority_jobs /service_of_jobs sum_pred_diff.
- rewrite addnBA; last first.
- { by rewrite big_mkcond //= leq_sum //; intros j' _; case (hep_job j' j). }
+ rewrite addnBA; last by rewrite big_mkcond //= leq_sum //; intros j' _; case (hep_job j' j).
rewrite addnC -addnBA.
- { intros. have TT := no_idle_time_within_non_quiet_time_interval.
- by unfold service_of_jobs in TT; rewrite TT // leq_addr.
- }
+ { have TT := no_idle_time_within_non_quiet_time_interval.
+ by unfold service_of_jobs in TT; rewrite TT // leq_addr. }
{ rewrite /cumulative_priority_inversion /is_priority_inversion exchange_big //=.
apply leq_sum_seq; move => t II _.
rewrite mem_index_iota in II; move: II => /andP [GEi LEt].
@@ -485,7 +481,9 @@ Section ExistsBusyIntervalJLFP.
{ by rewrite leqn0 big1_seq //. }
{ case PRIO1: (hep_job j1 j); simpl; first last.
- rewrite <- SCHED.
- have SCH := service_of_jobs_le_1 sched _ _ _ t; eauto using arrivals_uniq.
+ have SCH := @service_of_jobs_le_1 _ _ _ _ _ _ (fun i => ~~ hep_job i j) (arrivals_between 0 (t1 + delta)).
+ eapply leq_trans; last eapply SCH; eauto using arrivals_uniq with basic_facts.
+ by rewrite leq_sum // => i _; rewrite -scheduled_at_def service_at_is_scheduled_at.
- rewrite leqn0 big1_seq; first by done.
move => j2 /andP [PRIO2 ARRj2].
case EQ: (j1 == j2).
@@ -691,7 +689,7 @@ Section ExistsBusyIntervalJLFP.
job_completed_by j (job_arrival j + delta).
Proof.
have BUSY := exists_busy_interval priority_inversion_bound _ delta.
- move: (posnP (@job_cost _ H2 j)) => [ZERO|POS].
+ move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
{ by rewrite /job_completed_by /completed_by ZERO. }
feed_n 4 BUSY; try by done.
move: BUSY => [t1 [t2 [/andP [GE1 LT2] [GE2 BUSY]]]].
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 7074b8392..e4fe3aeff 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -5,14 +5,12 @@ Require Export prosa.analysis.facts.busy_interval.busy_interval.
(** Throughout this file, we assume ideal uniprocessor schedules. *)
Require Import prosa.model.processor.ideal.
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
-Require Import prosa.model.readiness.basic.
-
(** * Existence of No Carry-In Instant *)
-(** In this section, we derive an alternative condition for the existence of
- a busy interval. The new condition requires the total workload (instead
- of the high-priority workload) generated by the task set to be bounded. *)
+(** In this section, we derive an alternative condition for the
+ existence of a busy interval. The new condition requires the total
+ workload (instead of the high-priority workload) generated by the
+ task set to be bounded. *)
(** Next, we derive a sufficient condition for existence of
no carry-in instant for uniprocessor for JLFP schedulers *)
@@ -25,8 +23,8 @@ Section ExistsNoCarryIn.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ Context {Arrival: JobArrival Job}.
+ Context {Cost : JobCost Job}.
(** Consider any arrival sequence with consistent arrivals. *)
Variable arr_seq : arrival_sequence Job.
@@ -51,16 +49,10 @@ Section ExistsNoCarryIn.
Let no_carry_in := no_carry_in arr_seq sched.
Let quiet_time := quiet_time arr_seq sched.
- (** The fact that there is no carry-in at time instant t
- trivially implies that t is a quiet time. *)
- Lemma no_carry_in_implies_quiet_time :
- forall j t,
- no_carry_in t ->
- quiet_time j t.
- Proof.
- by intros j t FQT j_hp ARR HP BEF; apply FQT.
- Qed.
-
+ (** Further, 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.
+
(** Assume that the schedule is work-conserving, ... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
@@ -68,6 +60,17 @@ Section ExistsNoCarryIn.
Hypothesis H_arrival_sequence_is_a_set:
arrival_sequence_uniq arr_seq.
+ (** The fact that there is no carry-in at time instant [t] trivially
+ implies that [t] is a quiet time. *)
+ Lemma no_carry_in_implies_quiet_time :
+ forall j t,
+ no_carry_in t ->
+ quiet_time j t.
+ Proof.
+ by intros j t FQT j_hp ARR HP BEF; apply FQT.
+ Qed.
+
+
(** We show that an idle time implies no carry in at this time instant. *)
Lemma idle_instant_implies_no_carry_in_at_t :
forall t,
@@ -75,13 +78,18 @@ Section ExistsNoCarryIn.
no_carry_in t.
Proof.
intros ? IDLE j ARR HA.
- apply/negPn/negP; intros NCOMPL.
+ apply/negPn/negP; intros NCOMP.
+ have PEND : job_pending_at j t.
+ { apply/andP; split.
+ - by rewrite /has_arrived ltnW.
+ - by move: NCOMP; apply contra, completion_monotonic.
+ }
+ apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].
move: IDLE => /eqP IDLE.
- move: (H_work_conserving j t ARR) => NIDLE.
+ move: (H_work_conserving _ t ARRhp) => NIDLE.
feed NIDLE.
- { apply/andP; split; last first.
- { by rewrite scheduled_at_def IDLE. }
- { by apply/andP; split; [apply ltnW | done]. }
+ { apply/andP; split; first by done.
+ by rewrite scheduled_at_def IDLE.
}
move: NIDLE => [j' SCHED].
by rewrite scheduled_at_def IDLE in SCHED.
@@ -94,16 +102,18 @@ Section ExistsNoCarryIn.
no_carry_in t.+1.
Proof.
intros ? IDLE j ARR HA.
- apply/negPn/negP; intros NCOMPL.
+ apply/negPn/negP; intros NCOMP.
+ have PEND : job_pending_at j t.
+ { apply/andP; split.
+ - by rewrite /has_arrived.
+ - by move: NCOMP; apply contra, completion_monotonic.
+ }
+ apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [READYhp _]]].
move: IDLE => /eqP IDLE.
- move: (H_work_conserving j t ARR) => NIDLE.
+ move: (H_work_conserving _ t ARRhp) => NIDLE.
feed NIDLE.
- { apply/andP; split; last first.
- { by rewrite scheduled_at_def IDLE. }
- { apply/andP; split; first by done.
- move: NCOMPL => /negP NC1; apply/negP; intros NC2; apply: NC1.
- by apply completion_monotonic with t.
- }
+ { apply/andP; split; first by done.
+ by rewrite scheduled_at_def IDLE.
}
move: NIDLE => [j' SCHED].
by rewrite scheduled_at_def IDLE in SCHED.
@@ -120,14 +130,13 @@ Section ExistsNoCarryIn.
Let total_service t1 t2 :=
service_of_jobs sched predT (arrivals_between 0 t2) t1 t2.
- (** Assume that for some positive Δ, the sum of requested workload
- at time (t + Δ) is bounded by delta (i.e., the supply).
- Note that this assumption bounds the total workload of
- jobs released in a time interval [t, t + Δ) regardless of
- their priorities. *)
- Variable Δ: duration.
- Hypothesis H_delta_positive: Δ > 0.
- Hypothesis H_workload_is_bounded: forall t, total_workload t (t + Δ) <= Δ.
+ (** Assume that for some positive [Δ], the sum of requested workload
+ at time [t + Δ] is bounded by [Δ] (i.e., the supply). Note that
+ this assumption bounds the total workload of jobs released in a
+ time interval <<[t, t + Δ)>> regardless of their priorities. *)
+ Variable Δ : duration.
+ Hypothesis H_delta_positive : Δ > 0.
+ Hypothesis H_workload_is_bounded : forall t, total_workload t (t + Δ) <= Δ.
(** Next we prove that, since for any time instant [t] there is a
point where the total workload is upper-bounded by the supply,
@@ -162,8 +171,8 @@ Section ExistsNoCarryIn.
Proof.
unfold total_service.
rewrite -{3}[Δ]addn0 -{2}(subnn t) addnBA // [in X in _ <= X]addnC.
- apply service_of_jobs_le_length_of_interval'.
- by eapply arrivals_uniq; eauto 2.
+ apply service_of_jobs_le_length_of_interval'; auto with basic_facts.
+ by eapply arrivals_uniq; eauto 2.
Qed.
(** Next we consider two cases:
@@ -215,11 +224,11 @@ Section ExistsNoCarryIn.
have EQ: total_workload 0 (t + Δ) = service_of_jobs sched predT (arrivals_between 0 (t + Δ)) 0 (t + Δ).
{ intros.
have COMPL := all_jobs_have_completed_impl_workload_eq_service
- arr_seq H_arrival_times_are_consistent sched
+ _ arr_seq H_arrival_times_are_consistent sched
H_jobs_must_arrive_to_execute
H_completed_jobs_dont_execute
predT 0 t t.
- feed COMPL; try done.
+ feed_n 2 COMPL; auto with basic_facts.
{ intros j A B; apply H_no_carry_in.
- eapply in_arrivals_implies_arrived; eauto 2.
- eapply in_arrivals_implies_arrived_between in A; eauto 2.
@@ -238,8 +247,8 @@ Section ExistsNoCarryIn.
by apply H_workload_is_bounded.
}
intros s ARR BEF.
- eapply workload_eq_service_impl_all_jobs_have_completed; eauto 2; try done.
- by eapply arrived_between_implies_in_arrivals; eauto 2.
+ eapply workload_eq_service_impl_all_jobs_have_completed; eauto with basic_facts.
+ by eapply arrived_between_implies_in_arrivals.
Qed.
End ProcessorIsNotTooBusyInduction.
@@ -281,9 +290,9 @@ Section ExistsNoCarryIn.
Proof.
rename H_from_arrival_sequence into ARR, H_job_cost_positive into POS.
edestruct (exists_busy_interval_prefix
- arr_seq H_arrival_times_are_consistent sched j ARR H_priority_is_reflexive (job_arrival j))
- as [t1 [PREFIX GE]].
- apply job_pending_at_arrival; auto.
+ arr_seq H_arrival_times_are_consistent
+ sched j ARR H_priority_is_reflexive (job_arrival j))
+ as [t1 [PREFIX GE]]; first by apply job_pending_at_arrival; auto.
move: GE => /andP [GE1 _].
exists t1; move: (processor_is_not_too_busy t1.+1) => [δ [LE QT]].
apply no_carry_in_implies_quiet_time with (j := j) in QT.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index ae227fe67..ba5cf9dda 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -9,11 +9,6 @@ Require Export prosa.analysis.facts.busy_interval.busy_interval.
(** Throughout this file, we assume ideal uni-processor schedules. *)
Require Import prosa.model.processor.ideal.
-(** Throughout the file we assume for the classic Liu & Layland model
- of readiness without jitter and no self-suspensions, where
- pending jobs are always ready. *)
-Require Import prosa.model.readiness.basic.
-
(** In preparation of the derivation of the priority inversion bound, we
establish two basic facts on preemption times. *)
Section PreemptionTimes.
@@ -93,8 +88,8 @@ Section PriorityInversionIsBounded.
(** ... and any type of jobs associated with these tasks. *)
Context {Job : JobType}.
Context `{JobTask Job Task}.
- Context `{JobArrival Job}.
- Context `{JobCost Job}.
+ Context `{Arrival : JobArrival Job}.
+ Context `{Cost : JobCost Job}.
(** Consider any arrival sequence with consistent arrivals ... *)
Variable arr_seq : arrival_sequence Job.
@@ -129,6 +124,10 @@ Section PriorityInversionIsBounded.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+ (** Further, 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.
+
(** Next, we assume that the schedule is a work-conserving schedule... *)
Hypothesis H_work_conserving : work_conserving arr_seq sched.
@@ -221,29 +220,34 @@ Section PriorityInversionIsBounded.
scheduled_at sched jhp t ->
hep_job jhp j.
Proof.
- intros LTt2m1 jhp Sched_jhp.
- move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
- apply contraT; move => /negP NOTHP; exfalso.
- apply NOTQUIET with (t := t.+1).
+ intros LTt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+ move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
+ apply NOTQUIET with (t := t.+1).
{ apply/andP; split.
- by apply leq_ltn_trans with t1.
- rewrite -subn1 ltn_subRL addnC in LTt2m1.
- by rewrite -[t.+1]addn1.
+ by rewrite -[t.+1]addn1.
+ }
+ intros j_hp ARR HP BEF.
+ apply contraT => NCOMP'; exfalso.
+ have PEND : pending sched j_hp t.
+ { apply/andP; split.
+ - by rewrite /has_arrived.
+ - by move: NCOMP'; apply contra, completion_monotonic.
}
- intros j_hp' IN HP ARR.
- apply contraT; move => /negP NOTCOMP'; exfalso.
- have BACK: backlogged sched j_hp' t.
- { apply/andP; split; last first.
- { apply/negP; intro SCHED'.
- move: (ideal_proc_model_is_a_uniprocessor_model jhp j_hp' sched t Sched_jhp SCHED') => EQ; subst.
- by apply: NOTHP.
- }
- apply/andP; split. unfold arrived_before, has_arrived in *. by done.
- apply/negP; intro COMP; apply NOTCOMP'.
- by apply completion_monotonic with (t0 := t).
+ apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+ have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp).
+ clear HEP' NCOMP' BEF HP ARR j_hp.
+ have BACK: backlogged sched j' t.
+ { apply/andP; split; first by done.
+ apply/negP; intro SCHED'.
+ move: (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.
+ by subst; apply: NOTHP.
}
- apply NOTHP, (H_priority_is_transitive t j_hp'); eauto 2.
+ apply NOTHP, (H_priority_is_transitive t j'); last by eapply HEP.
+ by eapply H_respects_policy; eauto .
Qed.
+
(** In case when [t = t2 - 1], we cannot use the same proof
since [t+1 = t2], but [t2] is a quiet time. So we do a
@@ -254,43 +258,46 @@ Section PriorityInversionIsBounded.
scheduled_at sched jhp t ->
hep_job jhp j.
Proof.
- intros EQUALt2m1 jhp Sched_jhp.
- move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
- apply contraT; move => /negP NOTHP; exfalso.
+ intros EQUALt2m1 jlp Sched_jlp; apply contraT; move => /negP NOTHP; exfalso.
+ move: (H_t_in_busy_interval) (H_busy_interval_prefix) => /andP [GEt LEt] [SL [QUIET [NOTQUIET INBI]]].
rewrite leq_eqVlt in GEt; first move: GEt => /orP [/eqP EQUALt1 | LARGERt1].
- - subst t; clear LEt.
- rewrite -EQUALt1 in Sched_jhp; move: EQUALt1 => /eqP EQUALt1.
- destruct (job_scheduled_at j t1) eqn:SCHEDj.
- + apply NOTHP; erewrite (ideal_proc_model_is_a_uniprocessor_model j jhp); eauto.
- by apply (H_priority_is_reflexive 0).
- + eapply NOTHP, (H_respects_policy _ _ t2.-1); auto;
- last by rewrite -(eqbool_to_eqprop EQUALt1).
- apply/andP; split; last first.
- * by rewrite -(eqbool_to_eqprop EQUALt1); unfold job_scheduled_at in *; rewrite SCHEDj.
- * have EQ: t1 = job_arrival j.
- { rewrite -eqSS in EQUALt1.
- have EQ: t2 = t1.+1.
- { rewrite prednK in EQUALt1; first by apply/eqP; rewrite eq_sym.
- apply negbNE; rewrite -eqn0Ngt; apply/neqP; intros EQ0.
- move: INBI; rewrite EQ0; move => /andP [_ CONTR].
- by rewrite ltn0 in CONTR.
- } clear EQUALt1.
- by move: INBI; rewrite EQ ltnS -eqn_leq; move => /eqP INBI.
- }
- by rewrite -(eqbool_to_eqprop EQUALt1) EQ; eapply job_pending_at_arrival; eauto 2.
- - feed (NOTQUIET t); first by apply/andP; split.
+ { subst t t1; clear LEt SL.
+ have ARR : job_arrival j = t2.-1.
+ { apply/eqP; rewrite eq_sym eqn_leq.
+ destruct t2; first by done.
+ rewrite ltnS -pred_Sn in INBI.
+ now rewrite -pred_Sn.
+ }
+ have PEND := job_pending_at_arrival sched _ H_job_cost_positive H_jobs_must_arrive_to_execute.
+ rewrite ARR in PEND.
+ apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
+ eapply NOTHP, (H_priority_is_transitive 0); last by apply HEPhp.
+ apply (H_respects_policy _ _ t2.-1); auto.
+ apply/andP; split; first by done.
+ apply/negP; intros SCHED.
+ move: (ideal_proc_model_is_a_uniprocessor_model _ _ sched _ SCHED Sched_jlp) => EQ.
+ by subst; apply: NOTHP.
+ }
+ { feed (NOTQUIET t); first by apply/andP; split.
apply NOTQUIET; intros j_hp' IN HP ARR.
- apply contraT; move => /negP NOTCOMP'; exfalso.
- have BACK: backlogged sched j_hp' t.
+ apply contraT => NOTCOMP'; exfalso.
+ have PEND : pending sched j_hp' t.
{ apply/andP; split.
- - apply/andP; split. unfold arrived_before, has_arrived in *. by rewrite ltnW.
- apply/negP; intro COMP; apply NOTCOMP'.
- by apply completion_monotonic with (t0 := t).
- - apply/negP; intro SCHED'.
- move: (ideal_proc_model_is_a_uniprocessor_model jhp j_hp' sched t Sched_jhp SCHED') => EQ; subst.
- by apply: NOTHP.
- }
- apply NOTHP, (H_priority_is_transitive t j_hp'); eauto 2.
+ - by rewrite /has_arrived ltnW.
+ - by move: NOTCOMP'; apply contra, completion_monotonic.
+ }
+ apply H_job_ready in PEND => //; destruct PEND as [j' [ARR' [READY' HEP']]].
+ have HEP : hep_job j' j by apply (H_priority_is_transitive t j_hp').
+ clear ARR HP IN HEP' NOTCOMP' j_hp'.
+ have BACK: backlogged sched j' t.
+ { apply/andP; split; first by done.
+ apply/negP; intro SCHED'.
+ move: (ideal_proc_model_is_a_uniprocessor_model jlp j' sched t Sched_jlp SCHED') => EQ.
+ by subst; apply: NOTHP.
+ }
+ apply NOTHP, (H_priority_is_transitive t j'); last by eapply HEP.
+ by eapply H_respects_policy; eauto .
+ }
Qed.
(** By combining the above facts we conclude that a job that is
@@ -410,8 +417,8 @@ Section PriorityInversionIsBounded.
move: (H_respects_policy) => PRIO.
move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
ideal_proc_model_sched_case_analysis_eq sched t jhp.
- { exfalso; eapply not_quiet_implies_not_idle with (t0 := t); eauto 2.
- by apply/andP; split; first apply leq_trans with tp. }
+ { apply instant_t_is_not_idle in Idle; first by done.
+ by apply/andP; split; first apply leq_trans with tp. }
exists jhp.
have HP: hep_job jhp j.
{ intros.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 8efd14e73..269cf6477 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -13,7 +13,7 @@ Section RunToCompletionThreshold.
Context `{JobCost Job}.
(** In addition, we assume existence of a function
- mapping jobs to theirs preemption points. *)
+ mapping jobs to their preemption points. *)
Context `{JobPreemptable Job}.
(** Consider any kind of processor state model, ... *)
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index cd1458cb4..2c83ce771 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -67,3 +67,7 @@ Section LiuAndLaylandReadiness.
Qed.
End LiuAndLaylandReadiness.
+
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+ will be able to apply it automatically. *)
+Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_facts.
--
GitLab