Project Page Index Table of Contents

# Library prosa.analysis.facts.busy_interval.service_inversion

Require Export prosa.analysis.definitions.service_inversion.busy_prefix.
Require Export prosa.analysis.facts.busy_interval.pi.

# Service Inversion Lemmas

In this section, we prove a few lemmas about service inversion.
Section ServiceInversion.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any kind of fully supply-consuming uniprocessor state model.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Consider any arrival sequence with consistent, non-duplicate arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any uni-processor schedule of this arrival sequence...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence :
jobs_come_from_arrival_sequence sched arr_seq.
... 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.
In this section, we prove a few basic lemmas about priority inversion.
Section BasicLemmas.
Consider an JLDP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive.
Context {JLDP : JLDP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_priorities JLDP.
First, we show that a blackout at a time instant t implies that there is no service inversion at time t.
Lemma blackout_implies_no_service_inversion :
∀ (j : Job) (t : instant),
is_blackout sched t →
~~ service_inversion arr_seq sched j t.
Proof.
move⇒ j t SUP.
apply/negP ⇒ /andP [_ /hasP [s IN LP]].
move: (SUP) ⇒ /negP NSUP; apply: NSUP.
by apply: receives_service_implies_has_supply.
Qed.
Similarly, there is no service inversion at an idle time instant.
Lemma idle_implies_no_service_inversion :
∀ (j : Job) (t : instant),
is_idle arr_seq sched t →
~~ service_inversion arr_seq sched j t.
Proof.
move⇒ j t IDLE; rewrite /service_inversion.
rewrite negb_and negbK; apply/orP; right.
apply/hasPn ⇒ [s A].
apply served_at_and_receives_service_consistent in A.
exfalso.
by apply/negP; first apply: no_service_received_when_idle ⇒ //.
Qed.
Next, we prove that if a job j receives service at time t, job j does not incur service inversion at time t.
Lemma receives_service_implies_no_service_inversion :
∀ (j : Job) (t : instant),
receives_service_at sched j t →
~~ service_inversion arr_seq sched j t.
Proof.
move⇒ j t RSERV; apply/negP ⇒ /andP [_ /hasP [s IN LP]].
have EQ: j = s by apply: only_one_job_receives_service_at_uni ⇒ //.
subst; move: LP ⇒ /negP NHEP; apply: NHEP.
by apply H_priority_is_reflexive.
Qed.
We show that cumulative service inversion received during an interval `[t1, t2)` can be split into the sum of cumulative service inversion `[t1, t)` and `[t, t2)` for any `t2 \in [t1, t3]`.
Lemma service_inversion_cat :
∀ (j : Job) (t1 t2 t : instant),
t1 ≤ t →
t ≤ t2 →
cumulative_service_inversion arr_seq sched j t1 t2
= cumulative_service_inversion arr_seq sched j t1 t
+ cumulative_service_inversion arr_seq sched j t t2.
Proof. by move⇒ j t1 t2 t LE1 LE2; rewrite -big_cat_nat //=. Qed.
Next, we show that cumulative service inversion on an interval `[al, ar)` is bounded by the cumulative service inversion on an interval `[bl,br)` if `[al,ar)` ⊆ `[bl,br)`.
Lemma service_inversion_widen :
∀ (j : Job) (al ar bl br : instant),
bl ≤ al →
ar ≤ br →
cumulative_service_inversion arr_seq sched j al ar
≤ cumulative_service_inversion arr_seq sched j bl br.
Proof.
move⇒ j al ar bl br LE1 LE2.
rewrite /cumulative_service_inversion.
have [NEQ1|NEQ1] := leqP al ar; last by rewrite big_geq //.
rewrite (big_cat_nat LE1) //=; last by lia.
by rewrite (big_cat_nat _ LE2) //= addnC -addnA leq_addr //=.
Qed.
End BasicLemmas.
In the following section, we prove one rewrite rule about service inversion.
Section ServiceInversionRewrite.
Consider a reflexive JLDP policy.
Context {JLDP : JLDP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_priorities JLDP.
Consider a time instant t ...
Variable t : instant.
... and assume that there is supply at t.
Hypothesis H_supply : has_supply sched t.
Consider two (not necessarily distinct) jobs j and j' and assume that job j is scheduled at time t.
Variables j j' : Job.
Hypothesis H_sched : scheduled_at sched j t.
Then the predicate "is there service inversion for job j' at time t?" is equal to the predicate "is job j has lower priority than job j'?"
Lemma service_inversion_supply_sched :
service_inversion arr_seq sched j' t = ~~ hep_job_at t j j'.
Proof.
have RSERV : receives_service_at sched j t by apply ideal_progress_inside_supplies.
apply/idP/idP.
{ move ⇒ /andP [IN /hasP [s SE LP]].
have EQj: s = j by apply: only_one_job_receives_service_at_uni.
by subst. }
{ move ⇒ NHEP; apply/andP; split.
- move: NHEP; apply contra ⇒ SERV.
have EQj: j = j' by apply: only_one_job_receives_service_at_uni.
by subst; apply H_priority_is_reflexive.
- apply/hasP; ∃ j ⇒ //.
by apply: receives_service_and_served_at_consistent. }
Qed.
End ServiceInversionRewrite.
In the last section, we prove that cumulative service inversion is bounded by cumulative priority inversion.
Section PriorityInversion.
Consider a reflexive JLFP policy.
Note that, unlike the other sections, this section assumes a JLFP policy. This is due to the fact that priority inversion is defined in terms of JLFP policies. This is not a fundamental assumption and may be relaxed in the future.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
We prove that service inversion implies priority inversion ...
Lemma service_inv_implies_priority_inv :
∀ (j : Job) (t : instant),
service_inversion arr_seq sched j t →
priority_inversion arr_seq sched j t.
Proof.
move⇒ j t.
move⇒ /andP [NSERV /hasP [s IN LP]]; apply/andP; split.
{ apply/negP ⇒ INj; rewrite scheduled_jobs_at_iff in INj ⇒ //.
have EQ : s = j.
{ apply: H_uniprocessor_proc_model ⇒ //.
by eapply service_at_implies_scheduled_at, served_at_and_receives_service_consistent. }
by subst; move: LP ⇒ /negP LP; apply: LP; apply H_priority_is_reflexive. }
{ apply/hasP; ∃ s ⇒ //.
rewrite scheduled_jobs_at_iff ⇒ //.
by apply service_at_implies_scheduled_at; apply: served_at_and_receives_service_consistent. }
Qed.
... and, as a corollary, it is easy to see that cumulative service inversion is bounded by cumulative priority inversion.
Corollary cumul_service_inv_le_cumul_priority_inv :
∀ (j : Job) (t1 t2 : instant),
cumulative_service_inversion arr_seq sched j t1 t2
≤ cumulative_priority_inversion arr_seq sched j t1 t2.
Proof.
move⇒ j t1 t2; apply leq_sum ⇒ t _.
have L : ∀ (a b : bool), (a → b) → a ≤ b by move ⇒ [] [].
by apply L, service_inv_implies_priority_inv.
Qed.
End PriorityInversion.
End ServiceInversion.
In the following, we prove that the cumulative service inversion in a busy interval prefix is bounded.
Section ServiceInversionIsBounded.
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}.
Consider any kind of fully supply-consuming unit-supply uniprocessor state model.
Context `{PState : ProcessorState Job}.
Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
Consider an JLFP policy that indicates a higher-or-equal priority relation, and assume that the relation is reflexive and transitive.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
Consider any arrival sequence with consistent, non-duplicate arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
... and any uni-processor schedule of this arrival sequence.
Variable sched : schedule PState.
Next, allow for any work-bearing notion of job readiness ...
Context {RM : JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness RM 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_preemption_model : valid_preemption_model arr_seq sched.
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 scheduling policy.
Hypothesis H_respects_policy : respects_JLFP_policy_at_preemption_point arr_seq sched JLFP.
In the following section, we prove that cumulative service inversion in a busy-interval prefix is necessarily caused by one lower-priority job.
Section CumulativeServiceInversionFromOneJob.
Consider any job j with a positive job cost.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Let `[t1, t2)` be a busy-interval prefix.
Variable t1 t2 : instant.
Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
Consider a time instant t : t ≤ t2 such that ...
Variable t : instant.
Hypothesis H_t_le_t2 : t ≤ t2.
... the cumulative service inversion is positive in `[t1, t)`.
Hypothesis H_service_inversion_positive : 0 < cumulative_service_inversion arr_seq sched j t1 t.
First, note that there is a lower-priority job that receives service at some time during the time interval `[t1, t)`.
Local Lemma lower_priority_job_receives_service :
∃ (jlp : Job) (to : instant),
t1 ≤ to < t
∧ ~~ hep_job jlp j
∧ receives_service_at sched jlp to.
Proof.
move: H_service_inversion_positive; rewrite sum_nat_gt0 filter_predT ⇒ /hasP [t' IN POS].
rewrite mem_index_iota in IN; rewrite lt0b in POS.
move: POS ⇒ /andP [NIN /hasP [jlp INlp LP]].
∃ jlp, t'.
by rewrite IN LP.
Qed.
Then we prove that the service inversion incurred by job j can only be caused by one lower priority job.
Lemma cumulative_service_inversion_from_one_job :
∃ (jlp : Job),
job_arrival jlp < t1
∧ ~~ hep_job jlp j
∧ cumulative_service_inversion arr_seq sched j t1 t = service_during sched jlp t1 t.
Proof.
have [jlp [to [NEQ [LP SERV]]]] := lower_priority_job_receives_service.
∃ jlp; split; last split ⇒ //.
- apply: low_priority_job_arrives_before_busy_interval_prefix ⇒ //=.
+ by instantiate (1 := to); lia.
+ by apply service_at_implies_scheduled_at.
- apply: eq_sum_seq ⇒ t'; rewrite mem_index_iota ⇒ NEQt' _.
have [ZERO | POS] := unit_supply_proc_service_case H_unit_supply_proc_model sched jlp t'.
+ rewrite ZERO eqb0; apply/negP ⇒ /andP [_ /hasP [joo SERVoo LPoo]].
have EQ : jlp = joo.
{ apply: only_one_pi_job ⇒ //=.
× by instantiate (1 := to); lia.
× by apply service_at_implies_scheduled_at.
× by instantiate (1 := t'); lia.
× apply: service_at_implies_scheduled_at.
by apply: served_at_and_receives_service_consistent.
}
subst joo.
apply served_at_and_receives_service_consistent in SERVoo.
by move: SERVoo; rewrite /receives_service_at ZERO.
+ rewrite POS eqb1; apply/andP; split.
× apply/negP ⇒ IN; apply served_at_and_receives_service_consistent in IN.
have EQ: j = jlp by apply: only_one_job_receives_service_at_uni ⇒ //; rewrite /receives_service_at.
by subst jlp; move: LP ⇒ /negP LP; apply: LP; apply H_priority_is_reflexive.
× apply/hasP; ∃ jlp; last by apply: LP.
apply receives_service_and_served_at_consistent ⇒ //.
by rewrite /receives_service_at POS.
Qed.
End CumulativeServiceInversionFromOneJob.
In this section, we prove that, given a job j with a busy interval prefix `[t1, t2)` and a lower-priority job jlp, the service of jlp within the busy interval prefix is bounded by the maximum non-preemptive segment of job jlp.
Section ServiceOfLowPriorityJobIsBounded.
Consider an arbitrary job j with positive cost ...
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_j_job_cost_positive : job_cost_positive j.
... and a lower-priority job jlp.
Variable jlp : Job.
Hypothesis H_jlp_arrives : arrives_in arr_seq jlp.
Hypothesis H_jlp_lp : ~~ hep_job jlp j.
Let `[t1, t2)` be a busy interval prefix of job j.
Variable t1 t2 : instant.
Hypothesis H_busy_prefix : busy_interval_prefix arr_seq sched j t1 t2.
First, we consider a scenario when there is no preemption time inside of the busy interval prefix but there is a time instant where jlp is scheduled. In this case, the cumulative service inversion of job j in the time interval `[t1, t2)` is bounded by the total service of job jlp received in the interval `[t1, t2)`.
Local Lemma no_preemption_impl_service_inv_bounded :
(∀ t, t1 ≤ t < t2 → ~~ preemption_time arr_seq sched t) →
(∃ t, t1 ≤ t < t2 ∧ scheduled_at sched jlp t) →
cumulative_service_inversion arr_seq sched j t1 t2 ≤ service_during sched jlp t1 t2.
Proof.
move⇒ NPT SCHED.
rewrite [leqLHS]big_seq [leqRHS]big_seq; apply leq_sum ⇒ t.
rewrite mem_index_iota ⇒ /andP [LE LT].
have F : ∀ (b : bool) (n : nat), (b → 0 < n) → b ≤ n by lia.
apply: F ⇒ /andP [ZE /hasP [h IN LPh]].
have EQ: h = jlp; last by subst; apply: served_at_and_receives_service_consistent.
apply: H_uniprocessor_proc_model.
{ by apply served_at_and_receives_service_consistent in IN; apply: service_at_implies_scheduled_at. }
{ move: SCHED ⇒ [t' [/andP [LE' LT'] SCHED]].
unshelve apply: neg_pt_scheduled_continuous ⇒ //.
- by generalize dependent t'; clear; lia.
- by generalize dependent t; clear; lia.
}
Qed.
In this section, we assume that jlp is scheduled inside of the busy interval prefix and prove that its service is bounded by jlp's maximum non-preemptive segment.
Section ServiceOfLPJobIsBounded.
Consider an arbitrary time instant t such that t ≤ t2.
Variables t : instant.
Hypothesis H_t_le_t2 : t ≤ t2.
Consider a second time instant st such that t1 ≤ st < t and jlp is scheduled at time st.
Variable st : instant.
Hypothesis H_t1_le_st_lt_t : t1 ≤ st < t.
Hypothesis H_jlp_sched : scheduled_at sched jlp st.
Consider a preemption point σ of job jlp such that ...
Variable σ : duration.
Hypothesis H_σ_is_pt : job_preemptable jlp σ.
... σ is greater than or equal to the service of jlp at time t1 but exceeds the service by at most job_max_nonpreemptive_segment jlp - ε.
Hypothesis H_σ_constrained :
service sched jlp t1
≤ σ
≤ service sched jlp t1 + (job_max_nonpreemptive_segment jlp - ε).
Next, we perform case analysis on whether job jlp has reached σ units of service by time t.
First, assume that the service of jlp at time t is smaller than σ. In this case, it is easy to see from the hypothesis H_σ_constrained that the service received by jlp within time interval `[t1, t)` is bounded by job_max_nonpreemptive_segment jlp - ε.
Local Lemma small_service_implies_bounded_service :
service sched jlp t < σ →
service_during sched jlp t1 t ≤ job_max_nonpreemptive_segment jlp - ε.
Proof.
move ⇒ B; move_neq_up CO.
have E : σ ≤ service sched jlp t1 + service_during sched jlp t1 t by lia.
by move: B E; rewrite service_cat /service; lia.
Qed.
Next, assume that σ ≤ service sched jlp t. In this case, we can show that jlp is preempted after it reaches σ units of service and hence, again, the service during `[t1, t)` is bounded by job_max_nonpreemptive_segment jlp - ε.
Local Lemma big_service_implies_bounded_service :
σ ≤ service sched jlp t →
service_during sched jlp t1 t ≤ job_max_nonpreemptive_segment jlp - ε.
Proof.
rewrite -[service_during _ _ _ _ ≤ _](leq_add2l (service sched jlp t1)).
rewrite leq_eqVlt ⇒ /orP [/eqP EQ|GT].
{ by rewrite service_cat; [ rewrite -EQ; move: H_σ_constrained ⇒ /andP [A B] | lia]. }
exfalso.
have [pt [LTpt EQ]] : ∃ pt, pt < t ∧ service sched jlp pt = σ.
{ by apply exists_intermediate_service ⇒ //; apply unit_supply_is_unit_service. }
have NPT : ~~ preemption_time arr_seq sched t1.
{ by eapply lower_priority_job_scheduled_implies_no_preemption_time
with (t1 := t1) (t2:= t2) (t := st) (jlp := jlp) (j := j)=> //; lia. }
have LEpt: t1 ≤ pt.
{ move_neq_up LEpt.
have EQ1: service sched jlp t1 = σ.
{ apply/eqP; rewrite eqn_leq; apply/andP; split;
first by move: H_σ_constrained ⇒ /andP [A B].
by rewrite -EQ; apply: service_monotonic; lia. }
have PT : preemption_time arr_seq sched t1.
{ rewrite /preemption_time.
have ->: scheduled_job_at arr_seq sched t1 = Some jlp.
{ apply/eqP; rewrite scheduled_job_at_scheduled_at ⇒ //.
eapply lower_priority_job_continuously_scheduled
with (t1 := t1) (t2:= t2) (t := st) (jlp := jlp) (j := j)=> //=; lia. }
by rewrite EQ1.
}
by rewrite PT in NPT. }
have [t' [NEQ' [SERV' SCHED']]] := kth_scheduling_time sched _ _ _ _ EQ GT.
have PT : preemption_time arr_seq sched t'.
{ move: SCHED'; erewrite <-scheduled_job_at_scheduled_at ⇒ //.
by rewrite /preemption_time ⇒ /eqP ->; rewrite SERV'. }
move: H_jlp_lp ⇒ /negP LP2; apply: LP2.
apply: scheduled_at_preemption_time_implies_higher_or_equal_priority ⇒ //.
by move: NEQ' LEpt H_t_le_t2; clear; lia.
Qed.
Either way, the service of job jlp during the time interval `[t1, t)` is bounded by job_max_nonpreemptive_segment jlp - ε.
Local Lemma lp_job_bounded_service_aux :
service_during sched jlp t1 t ≤ job_max_nonpreemptive_segment jlp - ε.
Proof.
have [B|S] := leqP σ (service sched jlp t); last first.
- by apply small_service_implies_bounded_service.
- by apply big_service_implies_bounded_service.
Qed.
End ServiceOfLPJobIsBounded.
Note that the preemption point σ assumed in the previous section always exists.
Local Remark preemption_point_of_jlp_exists :
∃ σ,
service sched jlp t1 ≤ σ ≤ service sched jlp t1 + (job_max_nonpreemptive_segment jlp - ε)
∧ job_preemptable jlp σ.
Proof.
move: (proj2 (H_valid_model_with_bounded_nonpreemptive_segments) jlp H_jlp_arrives) =>[_ EXPP].
have T: 0 ≤ service sched jlp t1 ≤ job_cost jlp.
{ by apply/andP; split⇒ [//|]; apply service_at_most_cost, unit_supply_is_unit_service ⇒ //. }
by move: (EXPP (service sched jlp t1) T) ⇒ [pt [NEQ2 PP]]; ∃ pt.
Qed.
We strengthen the lemma lp_job_bounded_service_aux by removing the assumption that jlp is scheduled somewhere in the busy interval prefix.
Lemma lp_job_bounded_service :
∀ t,
t ≤ t2 →
service_during sched jlp t1 t ≤ job_max_nonpreemptive_segment jlp - ε.
Proof.
move⇒ t LT.
have [ZE|POS] := posnP (service_during sched jlp t1 t); first by rewrite ZE.
have [st [NEQ SCHED]] := cumulative_service_implies_scheduled _ _ _ _ POS.
have [σ [EX PTσ]] := preemption_point_of_jlp_exists.
by apply: lp_job_bounded_service_aux.
Qed.
Finally, we remove jlp from the RHS of the inequality by taking the maximum over all jobs that arrive before time t1.
Lemma lp_job_bounded_service_max :
∀ t,
t ≤ t2 →
service_during sched jlp t1 t ≤ max_lp_nonpreemptive_segment arr_seq j t1.
Proof.
move⇒ t LT.
have [ZE|POS] := posnP (service_during sched jlp t1 t); first by rewrite ZE.
have [st [NEQ SCHED]] := cumulative_service_implies_scheduled _ _ _ _ POS.
rewrite (leqRW (lp_job_bounded_service _ _)) //.
rewrite /max_lp_nonpreemptive_segment -(leqRW (leq_bigmax_cond_seq _ _ _ jlp _ _)) //.
{ apply: arrived_between_implies_in_arrivals ⇒ //.
apply/andP; split ⇒ //.
by (apply: low_priority_job_arrives_before_busy_interval_prefix; try apply: H_busy_prefix) ⇒ //; lia.
}
{ by rewrite H_jlp_lp andTb; apply: scheduled_implies_positive_cost. }
Qed.
End ServiceOfLowPriorityJobIsBounded.
Let tsk be any task to be analyzed.
Variable tsk : Task.
Let blocking_bound be a bound on the maximum length of a nonpreemptive segment of a lower-priority job.
Variable blocking_bound : duration → duration.
We show that, if the maximum length of a nonpreemptive segment is bounded by the blocking bound, ...
Hypothesis H_priority_inversion_is_bounded_by_blocking :
∀ j t1 t2,
arrives_in arr_seq j →
job_of_task tsk j →
busy_interval_prefix arr_seq sched j t1 t2 →
max_lp_nonpreemptive_segment arr_seq j t1 ≤ blocking_bound (job_arrival j - t1).
... then the service inversion incurred by any job is bounded by the blocking bound.
Lemma service_inversion_is_bounded :
service_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
Proof.
move⇒ j ARR TSK POS t1 t2 BUSY.
rewrite -(leqRW (H_priority_inversion_is_bounded_by_blocking _ _ _ _ _ _ )) //.
edestruct busy_interval_pi_cases as [CPI|PI]; (try apply BUSY) ⇒ //.
{ by rewrite (leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _)) //. }
{ move: (PI) ⇒ /andP [_ /hasP [jlp INjlp LPjlp]].
have SCHEDjlp : scheduled_at sched jlp t1 by erewrite <-scheduled_jobs_at_iff ⇒ //.
have [NPT| [pt [/andP [LE1 LE2] [PT MIN]]]] := preemption_time_interval_case arr_seq sched t1 t2.
{ rewrite (leqRW (no_preemption_impl_service_inv_bounded j _ jlp _ _ _ _ _ )) //.
- by apply: lp_job_bounded_service_max.
- by ∃ t1; split ⇒ //; apply/andP; split; [ | move: BUSY ⇒ [T _]]; lia. }
{ have LEQ : cumulative_service_inversion arr_seq sched j t1 t2
≤ cumulative_service_inversion arr_seq sched j t1 pt.
{ have [LE|WF] := leqP t2 pt.
{ by rewrite (leqRW (service_inversion_widen arr_seq sched j t1 _ _ pt _ _ )) ⇒ //. }
{ rewrite (service_inversion_cat _ _ _ _ _ pt) //
-{2}[_ _ _ j t1 pt]addn0 leq_add2l
(leqRW (cumul_service_inv_le_cumul_priority_inv _ _ _ _ _ _ _ _ _ _))// leqn0.
rewrite /cumulative_priority_inversion big_nat_cond; apply/eqP; apply big1 ⇒ t /andP [NEQ3 _]; apply/eqP.
by rewrite eqb0; apply: no_priority_inversion_after_preemption_point ⇒ //; lia. } }
rewrite (leqRW LEQ) (leqRW (no_preemption_impl_service_inv_bounded j _ jlp _ _ _ _ _ )) //; clear LEQ.
{ by apply: lp_job_bounded_service_max ⇒ //; lia. }
{ move⇒ t /andP [NEQ1 NEQ2]; apply/negP ⇒ PTt.
by specialize (MIN _ NEQ1 PTt); move: MIN NEQ2; clear; lia. }
{ ∃ t1; split ⇒ //.
apply/andP; split ⇒ //.
move_neq_up LE; have EQ: pt = t1; [by lia | subst].
eapply no_preemption_time_before_pi with (t := t1) in PI ⇒ //.
- by rewrite PT in PI.
- by move: LE2; clear; lia.
- by clear; lia. }
}
}
Qed.
End ServiceInversionIsBounded.