Library prosa.analysis.definitions.service_inversion.pred

Require Export prosa.model.priority.classes.
Require Export prosa.analysis.facts.behavior.completion.
Require Export prosa.analysis.definitions.service.

Service Inversion

In this section, we define the notion of service inversion for arbitrary processors.
Section ServiceInversion.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Next, consider any kind of processor state model, ...
  Context {PState : ProcessorState Job}.

... any arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule of this arrival sequence.
  Variable sched : schedule PState.

Assume a given JLDP policy.
  Context `{JLDP_policy Job}.

Consider an arbitrary predicate on time intervals.
  Variable P : Job → instant → instant → Prop.

Consider a job j.
  Variable j : Job.

We say that the job incurs service inversion if it has higher priority than the job receiving service. Note that this definition is oblivious to whether job j is ready. Therefore, it may not apply as intuitively expected in models with jitter or self-suspensions. Further generalization of the concept is likely necessary to efficiently analyze models in which jobs may be pending without being ready.
  Definition service_inversion (t : instant) :=
    (j \notin served_jobs_at arr_seq sched t)
    && has (fun jlp ⇒ ~~ hep_job_at t jlp j) (served_jobs_at arr_seq sched t).

Then we compute the cumulative service inversion incurred by a job within some time interval [t1, t2).
  Definition cumulative_service_inversion (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) service_inversion t.

For proof purposes, it is often useful to bound the cumulative service interference in a time interval [t1, t2) that satisfies a given predicate (e.g., [t1, t2) is a busy interval prefix). To this end, we say that the cumulative service inversion of job j is bounded by a function B : duration → duration w.r.t. to predicate P iff, for any interval [t1, t2) that satisfies P j, the cumulative priority inversion in [t1, t2) is bounded by B (job_arrival j - t1).
  Definition pred_service_inversion_of_job_is_bounded_by (B : duration → duration) :=
    ∀ (t1 t2 : instant),
      P j t1 t2 →
      cumulative_service_inversion t1 t2 ≤ B (job_arrival j - t1).

End ServiceInversion.

In this section, we define a notion of the bounded service inversion for tasks.
Section TaskServiceInversionBound.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost 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 processor state model, ...
  Context {PState : ProcessorState Job}.

... any arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any schedule.
  Variable sched : schedule PState.

Assume a given JLDP policy.
  Context `{JLDP_policy Job}.

Consider an arbitrary predicate on jobs and time intervals.
  Variable P : Job → instant → instant → Prop.

Consider an arbitrary task tsk.
  Variable tsk : Task.

We say that task tsk has bounded service inversion if all its jobs have cumulative service inversion bounded by function B : duration → duration.
  Definition pred_service_inversion_is_bounded_by (B : duration → duration) :=
    ∀ (j : Job),
      arrives_in arr_seq j →
      job_of_task tsk j →
      job_cost j > 0 →
      pred_service_inversion_of_job_is_bounded_by arr_seq sched P j B.

End TaskServiceInversionBound.