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.

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.

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.

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.

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.

  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'.
  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.

... 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.

  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 `{!JobReady Job PState}.
Hypothesis H_job_ready : work_bearing_readiness 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.

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.

  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.

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 - ε.

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 - ε.

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 - ε.

    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 σ.

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 - ε.

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.
  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.
End ServiceInversionIsBounded.