Library prosa.analysis.facts.busy_interval.ideal.priority_inversion_bounded
Require Export prosa.model.task.preemption.parameters.
Require Export prosa.analysis.facts.model.preemption.
Require Export prosa.analysis.facts.model.preemption.
Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.
Require Export prosa.analysis.facts.busy_interval.ideal.hep_job_scheduled.
Require Export prosa.analysis.facts.busy_interval.ideal.hep_job_scheduled.
Priority inversion is bounded
In this file, we prove that any priority inversion that occurs in the model with bounded nonpreemptive segments is bounded.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
Context `{JobTask Job Task}.
Context `{Arrival : JobArrival Job}.
Context `{Cost : JobCost Job}.
Consider any arrival sequence with consistent arrivals ...
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
... and any ideal uniprocessor schedule of this arrival sequence.
Consider a 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.
Hypothesis H_priority_is_reflexive: reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive: transitive_job_priorities JLFP.
Consider a valid preemption model with known maximum non-preemptive
segment lengths.
Context `{TaskMaxNonpreemptiveSegment Task} `{JobPreemptable Job}.
Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
Hypothesis H_valid_preemption_model : valid_preemption_model 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.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
We assume that the schedule is valid.
Next, we assume that the schedule is a work-conserving schedule...
... and the schedule respects the scheduling policy at every preemption point.
Finally, we introduce the notion of the maximal length of
(potential) priority inversion at a time instant t, which is
defined as the maximum length of nonpreemptive segments among
all jobs that arrived so far.
Definition max_length_of_priority_inversion (j : Job) (t : instant) :=
\max_(j_lp <- arrivals_before arr_seq t | (~~ hep_job j_lp j) && (job_cost j_lp > 0))
(job_max_nonpreemptive_segment j_lp - ε).
\max_(j_lp <- arrivals_before arr_seq t | (~~ hep_job j_lp j) && (job_cost j_lp > 0))
(job_max_nonpreemptive_segment j_lp - ε).
Next we prove that a priority inversion of a job is bounded by
function max_length_of_priority_inversion.
Note that any bound on function
max_length_of_priority_inversion will also be a bound on the
maximal priority inversion. This bound may be different for
different scheduler and/or task models. Thus, we don't define
such a bound in this module.
Consider any job j of tsk with positive job cost.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_j_arrives : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider any busy interval prefix
[t1, t2)
of job j.
Variable t1 t2 : instant.
Hypothesis H_busy_interval_prefix:
busy_interval_prefix arr_seq sched j t1 t2.
Hypothesis H_busy_interval_prefix:
busy_interval_prefix arr_seq sched j t1 t2.
Processor Executes HEP jobs after Preemption Point
In this section, we prove that at any time instant after any preemption point (inside the busy interval), the processor is always busy scheduling a job with higher or equal priority.
First, recall from file busy_interval/ideal/hep_job_scheduled
we already know that the processor at any preemptive point is always
busy scheduling a job with higher or equal priority.
We show that at any time instant after a preemption point the
processor is always busy with a job with higher or equal
priority.
Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
∀ tp t,
preemption_time arr_seq sched tp →
t1 ≤ tp < t2 →
tp ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
∀ tp t,
preemption_time arr_seq sched tp →
t1 ≤ tp < t2 →
tp ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
Now, suppose there exists some constant K that bounds the
distance to a preemption time from the beginning of the busy
interval.
Variable K : duration.
Hypothesis H_preemption_time_exists :
∃ pr_t, preemption_time arr_seq sched pr_t ∧ t1 ≤ pr_t ≤ t1 + K.
Hypothesis H_preemption_time_exists :
∃ pr_t, preemption_time arr_seq sched pr_t ∧ t1 ≤ pr_t ≤ t1 + K.
Then we prove that the processor is always busy with a job
with higher-or-equal priority after time instant t1 + K.
Lemma not_quiet_implies_exists_scheduled_hp_job:
∀ t,
t1 + K ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
End PreemptionTimeAndPriorityInversion.
∀ t,
t1 + K ≤ t < t2 →
∃ j_hp,
arrived_between j_hp t1 t.+1 ∧
hep_job j_hp j ∧
scheduled_at sched j_hp t.
End PreemptionTimeAndPriorityInversion.
Preemption Time Exists
In this section we prove that the function max_length_of_priority_inversion indeed upper-bounds the priority inversion length.
In this section, we require the jobs to have valid bounded
non-preemptive segments.
Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
First, we prove that, if a job with higher-or-equal priority is scheduled at
a quiet time t+1, then this is the first time when this job is scheduled.
Lemma hp_job_not_scheduled_before_quiet_time:
∀ jhp t,
quiet_time arr_seq sched j t.+1 →
scheduled_at sched jhp t.+1 →
hep_job jhp j →
~~ scheduled_at sched jhp t.
∀ jhp t,
quiet_time arr_seq sched j t.+1 →
scheduled_at sched jhp t.+1 →
hep_job jhp j →
~~ scheduled_at sched jhp t.
Also, we show that lower-priority jobs that are scheduled inside the
busy-interval prefix
[t1,t2)
must arrive before that interval.
Lemma low_priority_job_arrives_before_busy_interval_prefix:
∀ jlp t,
t1 ≤ t < t2 →
scheduled_at sched jlp t →
~~ hep_job jlp j →
job_arrival jlp < t1.
∀ jlp t,
t1 ≤ t < t2 →
scheduled_at sched jlp t →
~~ hep_job jlp j →
job_arrival jlp < t1.
Moreover, we show that lower-priority jobs that are scheduled
inside the busy-interval prefix
[t1,t2)
must be scheduled
before that interval.
Lemma low_priority_job_scheduled_before_busy_interval_prefix:
∀ jlp t,
t1 ≤ t < t2 →
scheduled_at sched jlp t →
~~ hep_job jlp j →
∃ t', t' < t1 ∧ scheduled_at sched jlp t'.
∀ jlp t,
t1 ≤ t < t2 →
scheduled_at sched jlp t →
~~ hep_job jlp j →
∃ t', t' < t1 ∧ scheduled_at sched jlp t'.
Thus, there must be a preemption time in the interval t1, t1
+ max_priority_inversion t1. That is, if a job with
higher-or-equal priority is scheduled at time instant t1, then
t1 is a preemption time. Otherwise, if a job with lower
priority is scheduled at time t1, then this job also should
be scheduled before the beginning of the busy interval. So,
the next preemption time will be no more than
max_priority_inversion t1 time units later.
We proceed by doing a case analysis.
(1) Case when the schedule is idle at time t1.
Assume that the schedule is idle at time t1.
Then time instant t1 is a preemption time.
Lemma preemption_time_exists_case1:
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case1.
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case1.
(2) Case when a job with higher-or-equal priority is scheduled at time t1.
Variable jhp : Job.
Hypothesis H_jhp_is_scheduled : scheduled_at sched jhp t1.
Hypothesis H_jhp_hep_priority : hep_job jhp j.
Hypothesis H_jhp_is_scheduled : scheduled_at sched jhp t1.
Hypothesis H_jhp_hep_priority : hep_job jhp j.
Then time instant t1 is a preemption time.
Lemma preemption_time_exists_case2:
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case2.
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case2.
(3) Case when a job with lower priority is scheduled at time t1.
Variable jlp : Job.
Hypothesis H_jlp_is_scheduled : scheduled_at sched jlp t1.
Hypothesis H_jlp_low_priority : ~~ hep_job jlp j.
Hypothesis H_jlp_is_scheduled : scheduled_at sched jlp t1.
Hypothesis H_jlp_low_priority : ~~ hep_job jlp j.
To prove the lemma in this case we need a few auxiliary
facts about the first preemption point of job jlp.
Variable fpt : instant.
Hypothesis H_fpt_is_preemptio_point : job_preemptable jlp (progr_t1 + fpt).
Hypothesis H_fpt_is_first_preemption_point:
∀ ρ,
progr_t1 ≤ ρ ≤ progr_t1 + (job_max_nonpreemptive_segment jlp - ε) →
job_preemptable jlp ρ →
service sched jlp t1 + fpt ≤ ρ.
Hypothesis H_fpt_is_preemptio_point : job_preemptable jlp (progr_t1 + fpt).
Hypothesis H_fpt_is_first_preemption_point:
∀ ρ,
progr_t1 ≤ ρ ≤ progr_t1 + (job_max_nonpreemptive_segment jlp - ε) →
job_preemptable jlp ρ →
service sched jlp t1 + fpt ≤ ρ.
For correctness, we also assume that fpt does not
exceed the length of the maximum non-preemptive
segment.
Lemma no_intermediate_preemption_point:
∀ ρ,
progr_t1 ≤ ρ < progr_t1 + fpt →
~~ job_preemptable jlp ρ.
∀ ρ,
progr_t1 ≤ ρ < progr_t1 + fpt →
~~ job_preemptable jlp ρ.
Thanks to the fact that the scheduler respects the notion of preemption points
we show that jlp is continuously scheduled in time interval
[t1, t1 + fpt)
.
Lemma continuously_scheduled_between_preemption_points:
∀ t',
t1 ≤ t' < t1 + fpt →
scheduled_at sched jlp t'.
∀ t',
t1 ≤ t' < t1 + fpt →
scheduled_at sched jlp t'.
Thus, job jlp reaches its preemption point at time instant t1 + fpt,
which implies that time instant t1 + fpt is a preemption time.
And since fpt ≤ max_length_of_priority_inversion j t1,
t1 ≤ t1 + fpt ≤ t1 + max_length_of_priority_inversion j t1.
Lemma preemption_time_le_max_len_of_priority_inversion:
t1 ≤ t1 + fpt ≤ t1 + max_length_of_priority_inversion j t1.
End FirstPreemptionPointOfjlp.
t1 ≤ t1 + fpt ≤ t1 + max_length_of_priority_inversion j t1.
End FirstPreemptionPointOfjlp.
Next, we combine the above facts to conclude the lemma.
Lemma preemption_time_exists_case3:
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case3.
End CaseAnalysis.
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End Case3.
End CaseAnalysis.
By doing the case analysis, we show that indeed there is a
preemption time in the time interval [t1, t1 +
max_length_of_priority_inversion j t1].
Lemma preemption_time_exists:
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End PreemptionTimeExists.
∃ pr_t,
preemption_time arr_seq sched pr_t ∧
t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.
End PreemptionTimeExists.
In this section we prove that if a preemption point ppt exists in a job's busy window,
it suffers no priority inversion after ppt. Equivalently the cumulative_priority_inversion
of the job in the busy window t1,t2 is bounded by the cumulative_priority_inversion
of the job in the time window t1,[ppt]).
Consider the preemption point ppt.
Variable ppt: instant.
Hypothesis H_preemption_point : preemption_time arr_seq sched ppt.
Hypothesis H_after_t1 : t1 ≤ ppt.
Hypothesis H_preemption_point : preemption_time arr_seq sched ppt.
Hypothesis H_after_t1 : t1 ≤ ppt.
We first establish the aforementioned result by showing that j cannot
suffer priority inversion after the preemption time ppt ...
Lemma no_priority_inversion_after_preemption_point :
∀ t,
ppt ≤ t < t2 →
~~ priority_inversion arr_seq sched j t.
∀ t,
ppt ≤ t < t2 →
~~ priority_inversion arr_seq sched j t.
... and then lift this fact to cumulative priority inversion.
Lemma priority_inversion_occurs_only_till_preemption_point :
cumulative_priority_inversion arr_seq sched j t1 t2 ≤
cumulative_priority_inversion arr_seq sched j t1 ppt.
End NoPriorityInversionAfterPreemptionPoint.
Section SingleJob.
cumulative_priority_inversion arr_seq sched j t1 t2 ≤
cumulative_priority_inversion arr_seq sched j t1 ppt.
End NoPriorityInversionAfterPreemptionPoint.
Section SingleJob.
Here, we will prove that priority inversion only occurs at the start of
the busy window and occurs due to only one job.
Suppose job j incurs priority inversion at a time t_pi in its busy window.
Variable t_pi : instant.
Hypothesis H_from_t1_before_t2 : t1 ≤ t_pi < t2.
Hypothesis H_PI_occurs : priority_inversion arr_seq sched j t_pi.
Hypothesis H_from_t1_before_t2 : t1 ≤ t_pi < t2.
Hypothesis H_PI_occurs : priority_inversion arr_seq sched j t_pi.
First, we show that there is no preemption time in the interval
[t1,
t_pi]>>.
Next, we show that the same job will be scheduled from the start of the
busy interval to the priority inversion time t_pi.
Lemma pi_job_remains_scheduled :
∀ jlp,
scheduled_at sched jlp t_pi →
∀ t,
t1 ≤ t ≤ t_pi → scheduled_at sched jlp t.
∀ jlp,
scheduled_at sched jlp t_pi →
∀ t,
t1 ≤ t ≤ t_pi → scheduled_at sched jlp t.
Thus, priority inversion takes place from the start of the busy interval
to the instant t_pi, i.e., priority inversion takes place
continuously.