Library probsa.rt.analysis.pRTA.pRTA_full

From probsa.rt.analysis Require Export transformation_properties.
From probsa.rt.analysis Require Export scheduler_properties.
From probsa.rt.analysis.pRTA Require Export pRTA.

Probabilistic Response-Time Analysis for Fixed-Priority Scheduling

This file proves the correctness of probabilistic response-time analysis (pRTA) for fixed-priority preemptive scheduling with constrained deadlines.

We provide a machine-checked proof that verifies and slightly generalizes Theorem 11 from: Chen et al., "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited." RTSS 2022.

Section ProbabilisticRTA.

Model and Assumptions

Consider any type of tasks with deadlines, minimum inter-arrival times, probabilistic WCET, and a total, reflexive, and transitive priority policy hep_task (also denoted FP).

  Context {Task : TaskType}
          {FP : FP_policy Task}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {pWCET_pmf : ProbWCET Task}.
  Hypothesis H_priority_is_total : total hep_task.
  Hypothesis H_priority_is_reflexive : reflexive hep_task.
  Hypothesis H_priority_is_transitive : transitive hep_task.

Consider an arbitrary task set ts.

Variable ts : seq Task.
Hypothesis H_ts_uniq : uniq ts.

We assume constrained deadlines and valid sporadic task parameters.

Hypothesis H_constrained_deadlines : constrained_deadlines ts.
Hypothesis H_valid_sporadic : valid_taskset_inter_arrival_times ts.

Consider a task tsk ∈ ts.

Variable tsk : Task.
Hypothesis H_tsk_in_ts : tsk \in ts.

Consider a probability space with sample space Ω and measure μ.

Context {Ω} {μ : measure Ω}.

Consider a set of jobs with probabilistic job arrivals and costs that are consistent (jobs that do not arrive have no cost).

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

Assume a finite horizon h that extends beyond all job deadlines.

  Variable h : instant.
  Hypothesis H_horizon_after_deadlines :
    ∀ j ω, (odflt0 (job_deadline j) ω < h)%nat.

We assume all jobs come from the task set and respect the sporadic model.

Hypothesis H_all_jobs_from_ts : ∀ j, job_task j \in ts.
Hypothesis H_sporadic : pr_taskset_respects_sporadic_task_model ts.

We assume the pWCET satisfies the axiomatic pWCET definition.

Hypothesis H_axiomatic_pWCET : axiomatic_pWCET μ.

Here, FP_FP_sched is an implementation of a fully preemptive FP scheduler with the classical notion of readiness and where jobs are terminated if a deadline is missed. The theorem below makes use of several properties of the scheduler, such as work conservation. All necessary properties (work conservation, policy compliance, etc.) are proven in probsa.rt.analysis.scheduler_properties.

Let 𝓡 j := response_time (compute_pr_schedule FP_FP_sched) (Some h) j.

Consider a job of task tsk.

Variable j : Job.
Hypothesis H_job_of_task : job_of_task tsk j.

Main Theorem

The probability that job j's response time exceeds the task deadline is bounded by Λ ts tsk. The proof applies pRT-monotonicity to replace probabilistic execution times with IID-pETs (creating a pessimistic simplified system), then derives the bound by analyzing this simplified system.

  Theorem probabilistic_rta_fp_fp :
    ℙ <μ >{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ ts tsk.
  Proof.
    have TOT : total_priorities
      by intros ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP.
    have REF : reflexive_priorities
      by intros ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP.
    have TRN : transitive_priorities
      by intros ? ? ? ?; unfold hep_job_at, JLFP_to_JLDP, hep_job, FP_to_JLFP;
      apply H_priority_is_transitive.
    apply: Rle_trans.
    { by apply probabilistic_rt_monotonicity_of_iid_pWCET ⇒ //; apply FP_FP_sched_is_rt_monotonic ⇒ //. }
    { apply: probabilistic_rta_fp; eauto 1; try set (S := replace_all_pETs _).
      { by apply: transformation_respects_big_horizon; intros; apply H_horizon_after_deadlines. }
      { by unfold pr_work_conserving; apply FP_FP_sched_is_work_conserving. }
      { by apply FP_FP_sched_respects_policy_at_preemption_point. }
      { by apply FP_FP_sched_respects_jobs_come_from_arrival_sequence. }
      { by apply FP_FP_sched_respects_completed_jobs_dont_execute. }
      { by apply FP_FP_sched_respects_jobs_must_arrive_to_execute. }
      { by apply FP_FP_sched_respects_jobs_must_be_ready_to_execute. }
      { by intros; apply transformation_respects_consistent_arrivals ⇒ //; apply H_arrivals_agree_with_costs. }
      { by intros ? ? ?; apply H_all_jobs_from_ts. }
      { by apply: sporadic_task_model_respected. }
      { by apply: replaced_pETs_are_independent. }
      { intros ? ?; unfold nth_cost.
        destruct pWCET_pmf as [pWCET nonneg sum1]; simpl.
        destruct task_job eqn:TSK; last first.
        { intros ?; apply Rge_trans with 1%R.
          { by rewrite pr_xpredT_ext //; apply Rge_refl. }
          { by apply Rle_ge, pr_le_1. }
        }
        { intros ?; apply: Rge_trans.
          { apply replaced_pETs_bounded_by_pWCETs with (tsko := tsk0).
            by move: TSK; intros EQ; apply nth_mem_o in EQ; apply EQ. }
          { by apply Rle_refl. }
        }
      }
      { by apply: pETs_have_same_distribution. }
      { by apply: replaced_pETs_are_cond_independent. }
      { unfold job_costs_independent_of_arrival_sequence; intros.
        by apply: replaced_pETs_are_independent_from_arr_seq_partition.
      }
      { by intros ? ? ? ? ? ?; apply: replaced_cond_pETs_bounded_by_pWCETs. }
    }
  Qed.

End ProbabilisticRTA.

Print Assumptions probabilistic_rta_fp.