Library prosa.analysis.facts.busy_interval.ideal.priority_inversion_bounded_jlfp

Priority Inversion is Bounded

In this file, we prove that any priority inversion that occurs in a model with a given JLFP policy and bounded nonpreemptive segments is bounded.
Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

In addition, we assume that each task has a maximal non-preemptive segment ...
... and any type of preemptable jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{Arrival : JobArrival Job}.
  Context `{Cost : JobCost Job}.
  Context `{JobPreemptable Job}.

Consider any valid arrival sequence,...
... 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.
And assume that they define a valid preemption model with bounded nonpreemptive segments.
Further, allow for any work-bearing notion of job readiness.
We assume that the schedule is valid.
Next, we assume that the schedule is a work-conserving schedule...
...,it respects the scheduling policy at every preemption point,...
... and complies with the preemption model.
Now, we consider an arbitrary task set ts...
  Variable ts : seq Task.

... and assume that all jobs stem from tasks in this task set.
Let tsk be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Let blocking_bound be a bound on the priority inversion caused by jobs with lower priority.
First, we observe that the maximum non-preemptive segment length of any task that releases a job with lower priority (w.r.t. a given job j) and non-zero execution cost upper-bounds the maximum possible length of priority inversion (of said job j).
  Lemma priority_inversion_is_bounded_by_max_np_segment:
   j t1,
    max_length_of_priority_inversion arr_seq j t1
     \max_(j_lp <- arrivals_between arr_seq 0 t1 | (~~ JLFP j_lp j)
                                                     && (job_cost j_lp >0))
      (task_max_nonpreemptive_segment (job_task j_lp) - ε).
    movej t.
    rewrite /max_length_of_priority_inversion.
    apply: leq_big_maxj' JINB NOTHEP.
    rewrite leq_sub2r //.
    apply in_arrivals_implies_arrived in JINB.
    by apply H_valid_model_with_bounded_nonpreemptive_segments.

We show that, if the maximum length of a priority inversion of a given job j is bounded by the blocking bound,...
... then the priority inversion incurred by any job is bounded by the blocking bound.
  Lemma priority_inversion_is_bounded:
    priority_inversion_is_bounded_by arr_seq sched tsk blocking_bound.
    movej ARR TSK POS t1 t2 PREF.
    move: (PREF) ⇒ [_ [_ [_ /andP [T _]]]].
    move: H_valid_schedule ⇒ [COARR MBR].
    have [NEQ|NEQ] := boolP ((t2-t1) blocking_bound (job_arrival j - t1)).
    { apply leq_trans with (t2 -t1) ⇒ [|//].
      rewrite /cumulative_priority_inversion.
      rewrite -[X in _ X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat.
      by rewrite leq_sum //; movet _; destruct (priority_inversion). }
    have [ppt [PPT' /andP[GE LE]]]: ppt : instant,
                                      preemption_time arr_seq sched ppt
                                      t1 ppt
                                      t1 + max_length_of_priority_inversion arr_seq j t1.
    by apply /preemption_time_exists.
    apply leq_trans with (cumulative_priority_inversion arr_seq sched j t1 ppt);
      last apply leq_trans with (ppt - t1).
    apply: priority_inversion_occurs_only_till_preemption_point =>//.
    { rewrite /cumulative_priority_inversion -[X in _ X]addn0 -[ppt - t1]mul1n
              -iter_addn -big_const_nat.
      by rewrite leq_sum //; movet _; case: priority_inversion. }
    { rewrite leq_subLR; apply leq_trans with (t1 + max_length_of_priority_inversion arr_seq j t1) ⇒ [//|].
      by rewrite leq_add2l; apply: (H_priority_inversion_is_bounded_by_blocking j t1 t2). }

End PriorityInversionIsBounded.