@bbb, here is a bound on a busy interval starting with priority inversion under the EDF scheduling policy.
It is intended to be used as follows
(** Let [L] be any positive fixed point of the busy interval
recurrence. *)
Variable L : duration.
Hypothesis H_L_positive : L > 0.
Hypothesis H_fixed_point : total_request_bound_function ts L <= SBF L.
Hypothesis H_L_bounds_bi_with_pi : longest_busy_interval_with_pi ts tsk <= SBF L.
Sergey Bozhko (94224a38) at 27 Mar 11:51
prosa.analysis.facts.busy_interval.pi
makes the assumption that the schedule is work-conserving (in the classic sense) Lemma scheduling_of_any_segment_starts_with_preemption_time_continuously_sched :
forall j t1 t2,
t1 <= t2 ->
preemption_time arr_seq sched t1 ->
scheduled_at sched j t2 ->
exists ptst,
t1 <= ptst <= t2
/\ preemption_time arr_seq sched ptst
/\ scheduled_at sched j ptst.
+ by apply IHt => ??; apply NPT; lia.
+ by apply NPT; lia.
Lemma preemption_time_exists_case1:
exists pr_t,
preemption_time arr_seq sched pr_t
/\ t1 <= pr_t <= t1 + max_lp_nonpreemptive_segment j t1.
Proof.
(** Thus, priority inversion takes place from the start of the busy interval
to the instant [t_pi], i.e., priority inversion takes place
continuously. *)
Lemma pi_continuous :
(** Next, we show that the same job will be scheduled from the start of the
busy interval to the priority inversion time [t_pi]. *)
(** First, we show that there is no preemption time in the interval <<[t1,t_pi]>>. *)
(** In this section, we prove that priority inversion only
occurs at the start of the busy window and occurs due to only
one job. *)
Section SingleJob.
(** * Lower Priority In Busy Intervals *)
prosa.analysis.facts.busy_interval.pi
makes the assumption that the schedule is work-conserving (in the classic sense)Doesn't this follow by definition?
Please format the statement properly
exists pt, preemption_time arr_seq sched pt /\
| t < pt <= t' /\
| scheduled_at sched j' pt.
^ ^ --- words do not align :(
Proof.
exists pt,
preemption_time arr_seq sched pt
/\ t < pt <= t'
/\ scheduled_at sched j' pt.
Proof.
I know why it is here, but such a hypothesis popping up here and there does not look good. I'm not sure that sections would help in this case, though.
(cc: @bbb)
Comment and the statement do not match
Please add a meaningful comment
Lemma lower_priority_job_scheduled_implies_job_sched_at_beginning:
scheduled_at sched jlp t1.
Proof.
^ --- `Proof` does no align with `Lemma`