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

Print Assumptions probabilistic_rta_fp.