Library probsa.rt.analysis.scheduler_properties

From prosa Require Export model.preemption.fully_preemptive.
From prosa.implementation Require Import facts.ideal_uni.prio_aware.

From probsa.util Require Export seq prosa.prio_aware.
From probsa.rt.model Require Export scheduler abort_readiness.
From probsa.rt.model.assumptions
Require Export basic pr_respects_policy pr_must_be_ready pr_work_conserving.

Local Open Scope nat_scope.

Sustainability and Properties of Fixed-Priority Fully-Preemptive Scheduling

This file establishes two key results: (1) Sustainability: Under a fully-preemptive fixed priority schedule, if job costs decrease, completion times can only improve. (2) Scheduler properties: The FP_FP_sched implementation satisfies all required properties (work conservation, policy compliance, etc.)

These results enable the pRT-monotonicity proof, allowing us to safely replace pETs with upper bounds (pWCETs, losely speaking) in schedulability analysis.

Section SustainableUniFPFP.

  Context {Job : finType}
          {job_arrival : JobArrival Job}
          {job_deadline : JobDeadline Job}
          {JLDP : JLDP_policy Job}.

Consider two job cost functions where job_cost2 is pointwise smaller than job_cost1 (i.e., costs have been reduced).

  Context {job_cost1 : JobCost Job}
          {job_cost2 : JobCost Job}.
  Hypothesis H_cost_monotone : ∀ j, job_cost1 j ≥ job_cost2 j.

  Let job_ready1 := @abort_ready_instance Job _ job_arrival job_cost1 job_deadline.
  Let job_ready2 := @abort_ready_instance Job _ job_arrival job_cost2 job_deadline.

  Variable arr_seq : arrival_sequence Job.

We consider two schedules: sched1 with higher costs and sched2 with lower costs.

  Let sched1 := @uni_schedule Job job_cost1 job_arrival arr_seq job_ready1 fully_preemptive_model JLDP.
  Let sched2 := @uni_schedule Job job_cost2 job_arrival arr_seq job_ready2 fully_preemptive_model JLDP.

  Hypothesis H_consistent_arrival_times : consistent_arrival_times arr_seq.
  Hypothesis H_arrival_sequence_uniq : arrival_sequence_uniq arr_seq.

  Hypothesis H_total : total_priorities.
  Hypothesis H_reflexive : reflexive_priorities.
  Hypothesis H_transitive : transitive_priorities.

  Section ScheduledAtMonotone.

    Variables j : Job.
    Variables t : instant.

    Hypothesis H_j_sched1 : scheduled_at sched1 j t.
    Hypothesis H_j_not_completed_sched2 : ~~ completed_by sched2 j t.

    Hypothesis H_service_monotone_wrt_schedules :
      ∀ (j : Job),
        ~~ completed_by sched2 j t →
        service sched1 j t ≤ service sched2 j t.

If job j is scheduled at time t in sched1 (with higher costs) and hasn't completed by t in sched2 (with lower costs), then j must also be scheduled at t in sched2. Intuition: With lower costs, other jobs complete faster, freeing the processor for j at least as early as before.

    Local Lemma j_scheduled_at_t_in_sched2 :
      scheduled_at sched2 j t.

  End ScheduledAtMonotone.

Jobs receive at least as much service with lower costs, since other jobs finish faster and consume less processor time.

  Local Lemma service_monotone_wrt_sched :
    ∀ (j : Job) (t : instant),
      ~~ completed_by sched2 j t →
      service sched1 j t ≤ service sched2 j t.

Main sustainability result: Reducing job costs cannot delay completion. If a job completes by time t in a schedule with larger costs job_cost1, it will also complete by t in a schedule with smaller costs job_cost2.

  Lemma sustainable_uni_fp_fp :
    ∀ t j,
      completed_by (H := job_cost1) sched1 j t →
      completed_by (H := job_cost2) sched2 j t.

End SustainableUniFPFP.

Scheduler Definition and Properties

We define FP_FP_sched, a fully-preemptive fixed-priority scheduler with job abortion. Later in this file, we prove that it satisfies all required properties for probabilistic schedulability analysis.

Section UniScheduleAsSchedulerAC.

  Context {Task : TaskType}
          {FP : FP_policy Task}
          {D : TaskDeadline Task}.

  Context {Job : finType}
          {job_task : JobTask Job Task}.

  Let arr_seq (A : Job → option instant) : arrival_sequence Job :=
    fun t ⇒
      [seq j <- index_enum Job |
        if A j is Some ta
        then t == ta
        else false
      ].

  Let job_deadline (A : Job → option nat) : JobDeadline Job :=
    fun (j : Job) ⇒
      odflt 0 (match A j with Some a ⇒ Some (a + D (job_task j)) | None ⇒ None end).

  Let readiness (A C : Job → option nat) :=
    @abort_ready_instance
      _ _ (fun j ⇒ odflt 0 (A j)) (fun j ⇒ odflt 0 (C j)) (job_deadline A).

  Let JLDP : JLDP_policy Job :=
    @JLFP_to_JLDP _ (@FP_to_JLFP Job Task _ FP).

Given vectors A and C describing job arrivals and job costs respectively, the scheduler FP_FP_sched defined below implements fully-preemptive fixed-priority scheduling using uni_schedule.

  Definition FP_FP_sched : @scheduler 𝗔𝗖 Job :=
    fun (A C : Job → option nat) t ⇒
      @uni_schedule
        Job
        (fun j ⇒ odflt 0 (C j)) (fun j ⇒ odflt 0 (A j))
        (arr_seq A)
        (readiness A C)
        fully_preemptive_model
        JLDP
        t.

End UniScheduleAsSchedulerAC.

Verification of Scheduler Properties

We prove that FP_FP_sched satisfies all properties required for probabilistic response-time analysis.

Section SchedulerProperties.

  Context {Task : TaskType}
          {FP : FP_policy Task}
          {D : TaskDeadline Task}.

  Context {Ω} {μ : measure Ω}.
  Context {Job : finType}
          {job_cost : JobCostRV Job Ω μ}
          {job_arrival : JobArrivalRV Job Ω μ}
          {job_task : JobTask Job Task}.

  Hypothesis H_total : total_priorities.
  Hypothesis H_reflexive : reflexive_priorities.
  Hypothesis H_transitive : transitive_priorities.

  Let pr_sched := @compute_pr_schedule Ω μ Job job_arrival job_cost FP_FP_sched.

  Lemma abortion_readiness_is_nonclairvoyant :
    ∀ ω, @nonclairvoyant_readiness _ _ _ _ (pr_abort_ready_instance ω).

  Lemma FP_FP_sched_respects_completed_jobs_dont_execute :
    pr_completed_jobs_dont_execute pr_sched.
  Lemma FP_FP_sched_respects_jobs_must_arrive_to_execute :
    pr_jobs_must_arrive_to_execute pr_sched.
  Lemma FP_FP_sched_respects_jobs_come_from_arrival_sequence :
    pr_jobs_come_from_arrival_sequence pr_sched.
  Lemma FP_FP_sched_is_work_conserving :
    pr_work_conserving pr_sched pr_abort_ready_instance.
  Lemma FP_FP_sched_respects_policy_at_preemption_point :
    pr_respects_policy_at_preemption_point
      pr_sched pr_abort_ready_instance fully_preemptive_model.
  Lemma FP_FP_sched_respects_jobs_must_be_ready_to_execute :
    pr_jobs_must_be_ready_to_execute pr_sched pr_abort_ready_instance.

We prove that the scheduler is RT-monotonic. That is, reducing a job's cost can only improve (or maintain) its completion time.

  Lemma FP_FP_sched_is_rt_monotonic :
    ∀ horizon,
      rt_monotonic_scheduler (Some horizon) FP_FP_sched.

End SchedulerProperties.