Library probsa.rt.model.scheduler

From prosa.model Require Import processor.ideal.

From probsa.rt Require Import behavior.response_time.

Scheduler

Section SchedulerHardcoded.

  Variable horizon : option instant.

Consider any type of job.
  Context {Job : JobType}.

We define a scheduler with hardcoded arrivals and costs as a function that receives two functions -- one describing job arrivals 𝗔 : Job β†’ option instant and another describing job costs 𝗖 : Job β†’ option work -- and returns a schedule (which is a function that maps a time instant to a processor state at this time instant). Note that the functions do not depend on Ο‰ and, hence, are fixed. The motivation behind such a scheduler is to encode a scheduling algorithm that makes its decisions based only on the information provided by inputs from 𝗔 and 𝗖.
  Definition scheduler𝗔𝗖 : Type :=
    ( Job β†’ option instant) β†’ ( Job β†’ option work)
    β†’ instant β†’ ideal.processor_state Job.

The following definitions just mirror the existing definitions. The only difference is that the proposed definitions use the scheduler instead of a generic schedule.

  Definition service𝗔𝗖 : Type :=
    ( Job β†’ option instant) β†’ ( Job β†’ option work)
    β†’ Job β†’ instant β†’ work.

  Definition completed_by𝗔𝗖 : Type :=
    ( Job β†’ option instant) β†’ ( Job β†’ option work)
    β†’ Job β†’ instant β†’ bool.

  Definition response_time𝗔𝗖 : Type :=
    ( Job β†’ option instant) β†’ ( Job β†’ option work)
    β†’ Job β†’ etime.

  Definition scheduler𝗔𝗖_to_service𝗔𝗖 (ΞΆ : scheduler𝗔𝗖) : service𝗔𝗖 :=
    fun 𝗔 𝗖 j t β‡’ service (ΞΆ 𝗔 𝗖) j t.

  Definition scheduler𝗔𝗖_to_completed𝗔𝗖 (ΞΆ : scheduler𝗔𝗖) : completed_by𝗔𝗖 :=
    fun 𝗔 𝗖 j t β‡’ 𝗖 j ⟨<=⟩ service (ΞΆ 𝗔 𝗖) j t.

Given a scheduler, we define a function that maps 𝗔 : Job β†’ option instant and 𝗖 : Job β†’ option work to a function that can compute the response time of any given job.
  Section ResponseTimeFromScheduler.

    Variable ΞΆ : scheduler𝗔𝗖.
    Let completed_by := scheduler𝗔𝗖_to_completed𝗔𝗖 ΞΆ.

    Definition completed𝗔𝗖_is_dec :
      βˆ€ 𝗔 𝗖 (j : Job) (compl_time : instant),
        completed_by 𝗔 𝗖 j compl_time ∨ Β¬ completed_by 𝗔 𝗖 j compl_time.
    Proof.
      by intros Γ— β‡’ //=; elim (completed_by 𝗔 𝗖 j compl_time); auto.
    Defined.

    Definition min_completion_time 𝗔 𝗖 (j : Job) :=
      LPO_min (fun compl_time β‡’ completed_by 𝗔 𝗖 j compl_time) (completed𝗔𝗖_is_dec 𝗔 𝗖 j).

    Definition scheduler𝗔𝗖_to_rt𝗔𝗖 : response_time𝗔𝗖 :=
      fun 𝗔 𝗖 j β‡’
        match 𝗔 j with
        | None β‡’ Undef
        | Some ar β‡’
            match min_completion_time 𝗔 𝗖 j, horizon with
            | inright _, _ β‡’ Infty
            | inleft (exist compl_time _), None β‡’ Fin (compl_time - ar)
            | inleft (exist compl_time _), Some h β‡’
                if (compl_time β‰₯ h)%nat then Infty else Fin (compl_time - ar)
            end
        end.

  End ResponseTimeFromScheduler.

End SchedulerHardcoded.

Scheduler to Schedule

Section Schedule.

  Context {Ξ©} {ΞΌ : measure Ξ©}.
  Context {Job : JobType}
          {job_arrival : JobArrivalRV Job Ξ© ΞΌ}
          {job_cost : JobCostRV Job Ξ© ΞΌ}.

If we are given a scheduler sched, then a probabilistic schedule is defined as follows:
Ξ» (Ο‰ : Ξ©) (t : instant), sched (sample_arrivals Ο‰) (sample_costs Ο‰) t.
Here, sample_arrivals (sample_costs) is a function that maps Ο‰ ∈ Ξ© to a function with fixed arrivals (costs).
Similarly to arival_sequence, pr_schedule is an arrow type (instant β†’ PState), Coq cannot automatically derive the right type. Therefore, we need to steer Coq's coercion and type systems towards the right type via the annotation B := Equality.clone _ _.
  Definition compute_pr_schedule (sched : @scheduler𝗔𝗖 Job) : pr_schedule ΞΌ (ideal.processor_state Job) :=
    mkRvar _ (B := Equality.clone _ _)
           (fun Ο‰ t β‡’
              sched (sample_arrivals Ο‰) (sample_costs Ο‰) t
           ).

End Schedule.

RT-Monotonic Scheduler

Section RTMonotonicScheduler.

  Context {Ξ©} {ΞΌ : measure Ξ©}.
  Context {Job : JobType}
          {job_arrival : JobArrivalRV Job Ξ© ΞΌ}
          {job_cost : JobCostRV Job Ξ© ΞΌ}.

  Variable horizon : option instant.

Consider a scheduling algorithm ΞΆ.
  Variable ΞΆ : @scheduler𝗔𝗖 Job.

For convenience, let 𝓑 denote an algorithm that maps job arrivals, job costs, and a job to its response time.
  Let 𝓑 := scheduler𝗔𝗖_to_rt𝗔𝗖 horizon ΞΆ.

We let sched denote a schedule computed via ΞΆ.
  Let sched := @compute_pr_schedule Ξ© ΞΌ _ _ _ ΞΆ.

We prove that the response time of a job computed in sched is equal to the response time of the same job computed via 𝓑 if run with job arrivals equal to sample_arrivals Ο‰ and job costs equal to sample_costs Ο‰.
  Lemma valid_𝓑 :
    βˆ€ (j : Job) (Ο‰ : Ξ©),
      response_time sched horizon j Ο‰ = 𝓑 (sample_arrivals Ο‰) (sample_costs Ο‰) j.
  Proof.
    intros Γ—.
    rewrite /𝓑 /response_time /scheduler𝗔𝗖_to_rt𝗔𝗖 β‡’ //=.
    rewrite [sample_arrivals Ο‰ j]/sample_arrivals.
    elim JA: (job_arrival j Ο‰) β‡’ [a| ]; last by done.
    have EQU :
      βˆ€ i,
        pr_completed_by sched j i Ο‰
        = scheduler𝗔𝗖_to_completed𝗔𝗖 ΞΆ (sample_arrivals Ο‰) (sample_costs Ο‰) j i.
    { by intros t; rewrite /scheduler𝗔𝗖_to_completed𝗔𝗖 /pr_completed_by /sched β‡’ //=. }
    elim (response_time.min_completion_time sched Ο‰ j) β‡’ [[compl1 [COMPL1 MIN1]]|NCOMLP1].
    all: elim (min_completion_time ΞΆ (sample_arrivals Ο‰) (sample_costs Ο‰) j)
       β‡’ [[compl2 [COMPL2 MIN2]]|NCOMPL2].
    all: try done.
    { have ->: compl1 = compl2; last by done.
      apply/eqP; rewrite eqn_leq; apply/negbNE/negP.
      rewrite negb_and -!ltnNge β‡’ /orP [LT|LT].
      - by eapply MIN1; [apply/ltP; apply LT | apply COMPL2].
      - by eapply MIN2; [apply/ltP; apply LT | apply COMPL1].
    }
    { by exfalso; apply: (NCOMPL2 compl1); rewrite -EQU. }
    { by exfalso; eapply NCOMLP1; erewrite EQU; eapply COMPL2. }
  Qed.

To define RT-monotonicity, we define a function that updates a given vector with a new cost.
  Definition update (𝗖 : Job β†’ option work) (jo : Job) (c : option work) : (Job β†’ option work) :=
      fun j β‡’ if j == jo then c else 𝗖 j.

A scheduler ΞΆ is response-time monotonic if, given vectors of fixed arrival times 𝗔 and job costs 𝗖, an update of the cost of any job j_update from c1 to c2 : c1 βŸ¨β‰€βŸ© c2 cannot cause a decrease in response time of any job j.
  Definition rt_monotonic_scheduler :=
    βˆ€ 𝗔 𝗖 (j_update j : Job), βˆ€ (r : instant) (c1 c2 : option nat),
      is_true (c1 ⟨<=⟩ c2) β†’
      exceeds (𝓑 𝗔 (update 𝗖 j_update c1) j) r β†’
      exceeds (𝓑 𝗔 (update 𝗖 j_update c2) j) r.

End RTMonotonicScheduler.

Opaque scheduler𝗔𝗖_to_rt𝗔𝗖.