Library probsa.rt.analysis.pRTA.pRTA

From probsa.util.prosa Require Export sporadic_as_curve.
From probsa.rt.model Require Export axiomatic_pWCET scheduler rt_monotonic pRBF assumptions.pr_cost.
From probsa.rt.analysis Require Export work_bound.
From probsa.rt.analysis.independent Require Export cost_and_workload task_workload.

TDFP ≤ WCA-TDFP

In this section, we prove that if the worst-case-arrival TDFP is bounded by a constant Λ, then TDFP is bounded by Λ as well.

Section WCATDFPtoTDFP.

  Context {Ω} {μ : measure Ω}.

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

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

  Variable h : instant.

Consider any scheduler.

  Variable ζ : @scheduler 𝗔𝗖 Job.
  Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
  Let 𝓡 j := response_time sched (Some h) j.

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

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

  Variable Λ : R.
  Hypothesis H_Λ_bounded : 0 ≤ Λ ≤ 1.

We assume that the TDFP is bounded by Λ for every possible arrival sequence ξ. The conditioning on ξpart◁{ξ} represents fixing a specific arrival pattern. Worst-case arrival (WCA-TDFP) means this bound holds for all possible arrival patterns, not just on average.

  Hypothesis H_WCA_TDFP_bounded :
    let ξpart := partition_on_ξ μ in
    ∀ (ξ : I ξpart) (ρ : PosProb μ (ξpart ◁{ξ })),
      ℙ <μ ,ρ >{[ D tsk ⟨<⟩ 𝓡 j | ξpart ◁{ξ } ]} ≤ Λ.

If WCA-TDFP is bounded by Λ for every arrival sequence, then the unconditional TDFP (averaging over all possible arrival sequences) is also bounded by Λ. This holds because the unconditional probability is a weighted average of the conditional probabilities, where each conditional probability is at most Λ. Therefore, their average cannot exceed Λ.

Lemma WCA_TDFP_bounded_implies_TDFP_bounded :
ℙ <μ >{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ.

End WCATDFPtoTDFP.

TDFP Bound

In this section, we define a constant Λ that bounds TDFP.

Section TDFPBound.

  Context {Task : TaskType}
          {pWCET_pmf : ProbWCET Task}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {FP : FP_policy Task}.

  Variables (ts : seq Task) (tsk : Task).

The interference distribution for task tsk in an interval of length t is the convolution of workload distributions from all tasks with higher-or-equal priority to tsk, excluding tsk itself. Each task tsko contributes workload over the interval t + D tsko.

  Definition interference_distrib (t : nat) : distrib [countType of nat] :=
    ⨁_{tsko <- ts | (hep_task tsko tsk ) && (tsko != tsk )}
     pRBF tsko (t + D tsko)%nat.

The total demand distribution in an interval of length t combines the job's own cost with interference from higher-or-equal priority tasks.

Definition demand_distrib (t : nat) : distrib [countType of nat] :=
to_distrib pWCET_pmf tsk ⊕ interference_distrib t.

The TDFP bound Λ is the minimum probability, over all interval lengths t ∈ [1, D tsk], that the total workload of higher-or-equal priority jobs exceeds the length t of the interval.

The key insight: ℙ{demand_distrib t > t} gives the probability that workload generated in an interval of length t exceeds t itself, meaning the work cannot be completed within the interval. Taking the minimum over all t identifies the interval length where the workload is most likely to be consumed, thereby providing an upper bound on the deadline miss probability.

  Definition Λ : R :=
    min1 [ seq ℙ <demand_distrib t >{[ltn t ]}
         | t <- index_iota 1 (D tsk + 1) ].

  Remark lims_Λ : 0 ≤ Λ ≤ 1.

End TDFPBound.

Step-by-Step Proof of Probabilistic Response-Time Analysis: TDFP Bound

This section proves the main result of probabilistic response-time analysis proven in Chen et al., "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited."

Section TDFPIsBounded.

  Context {Ω} {μ : measure Ω}.

  Context {Task : TaskType}
          {pWCET_pmf : ProbWCET Task}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {FP : FP_policy Task}.

  Hypothesis H_priority_is_reflexive : reflexive hep_task.
  Hypothesis H_transitive_priorities : transitive hep_task.

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

Let us assume that the pWCET is axiomatic.

Hypothesis H_axiomatic_pWCET : axiomatic_pWCET μ.

Assume the system terminates at some distant time h.

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

Consider a scheduler ...

  Variable ζ : @scheduler 𝗔𝗖 Job.
  Let sched := @compute_pr_schedule Ω μ Job _ _ ζ.
  Let 𝓡 j := response_time sched (Some h) j.

... and assume that it is work conserving and respects the FP-FP policy.

  Hypothesis H_work_conserving : pr_work_conserving sched pr_abort_ready_instance.
  Hypothesis H_respects_policy_at_preemption_point :
    pr_respects_policy_at_preemption_point sched pr_abort_ready_instance fully_preemptive_model.

  Hypothesis H_jobs_come_from_arrival_sequence : pr_jobs_come_from_arrival_sequence sched.
  Hypothesis H_completed_jobs_dont_execute : pr_completed_jobs_dont_execute sched.
  Hypothesis H_jobs_must_arrive_to_execute : pr_jobs_must_arrive_to_execute sched.
  Hypothesis H_jobs_must_be_ready_to_execute :
    pr_jobs_must_be_ready_to_execute sched pr_abort_ready_instance.

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

  Hypothesis H_jobs_from_ts : ∀ (j : Job), job_task j \in ts.
  Hypothesis H_arrivals_and_costs_consistent : arrivals_cost_consistent.
  Hypothesis H_arrivals_from_ts : arrivals_from_task_set ts.
  Hypothesis H_sporadic_arrivals : pr_taskset_respects_sporadic_task_model ts.
  Hypothesis H_task_min_inter_arrival_time_valid : valid_taskset_inter_arrival_times ts.
  Hypothesis H_constrained_deadlines : constrained_deadlines ts.

The sporadic task model implies that the task set respects arrival curves.

  Local Remark respects_arrival_curve :
    ∀ ω,
      taskset_respects_max_arrivals (arr_seq ω) ts.
  Local Remark valid_arrival_curve :
    valid_taskset_arrival_curve ts max_arrivals.

In this proof, we assume the job cost properties established by the axiomatic-pWCET transformation.

  Hypothesis H_job_costs_independent : job_costs_independent.
  Hypothesis H_job_costs_bounded_by_pWCET : job_costs_bounded_by_pWCET.
  Hypothesis H_job_costs_identically_distr : job_costs_identically_distributed.
  Hypothesis H_job_costs_independent_cond_arr_seq : job_costs_independent_cond_arr_seq.
  Hypothesis H_job_costs_independent_arr_seq : job_costs_independent_of_arrival_sequence.
  Hypothesis H_conditional_cost_bounded_by_pWCET : conditional_cost_bounded_by_pWCET.

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

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

Step-by-Step Proof Sketch

This section establishes the key steps of the proof, all conditioned on a fixed arrival sequence ξ. The main theorem later combines these steps and lifts the bound to the unconditional case via the law of total probability.

  Section StepByStep.

    Let ξpart := partition_on_ξ μ : Ω_partition.
    Let V := pr_carry_in_workload_of_hep_jobs sched tsk : instant → rvar μ [eqType of work].

Consider an arbitrary arrival sequence that has positive probability.

Variable ξ : I ξpart.
Hypothesis ρ : PosProb μ (ξpart ◁{ξ }).

Step 1: Handle the case where job j doesn't arrive.

For a fixed arrival sequence ξ, either job j arrives at some time A in all outcomes with that sequence ξpart◁{ξ}, or j doesn't arrive in any outcome with that sequence.

    Local Lemma job_either_arrives_or_not :
      (∀ ω, (ξpart ◁{ξ }) ω → job_arrival j ω = None )
      ∨ (∃ A , ∀ ω, (ξpart ◁{ξ }) ω → job_arrival j ω = Some A ).

If job j doesn't arrive in arrival sequence ξ, then the conditional TDFP is 0 (no deadline to miss).

    Lemma tdfp_zero_when_job_does_not_arrive :
      (∀ ω , (ξpart ◁{ξ }) ω → job_arrival j ω = None ) →
      ℙ <μ >{[ D tsk ⟨<⟩ response_time (compute_pr_schedule ζ) (Some h) j | ξpart ◁{ξ } ]} = 0.

Step 2: Relate deadline miss to workload demand

Since the partition element ξ has positive probability, there exists at least one outcome ω where ξ is sampled. We fix such an ω and observe that job j arrives at time A in this outcome. By the property of arrival sequences within a partition element, j arrives at A in all outcomes with arrival sequence ξ.

    Variable ω : Ω.
    Hypothesis H_ω _in_ξ : ξpart ◁{ξ } ω.

    Variable A : nat.
    Hypothesis H_job_arrives_at :
      ∀ ω , ξpart ◁{ξ } ω → job_arrival j ω = Some A.

We consider interval lengths from 1 to the task deadline.

Let lengths := index_iota 1 (D tsk + 1).

Next, we define a predicate that is true iff the workload demand exceeds available time in an interval of length Δ in an evolution ω.

Let workload_exceeds_time (ω : Ω) (Δ : duration) :=
(V A ω + pr_workload_of_hep_tasks tsk A (A + Δ) ω > Δ)%nat.

We prove a probabilistic version of an intuitive statement: if the response time exceeds the deadline, then workload demand must exceed the available time in ALL intervals of length Δ ∈ [1, D tsk].

    Lemma deadline_miss_implies_workload_exceeds_time :
      ℙ <μ >{[ D tsk ⟨<⟩ 𝓡 j | ξpart ◁{ξ } ]}
      ≤ ℙ <μ >{[ λ ω , all (workload_exceeds_time ω) lengths | ξpart ◁{ξ } ]}.

By Fréchet's inequality, the probability that workload exceeds time in ALL intervals is bounded by the minimum probability across intervals. This allows us to focus on a single interval length at a time.

    Lemma frechet_bound_on_all_intervals :
      ℙ <μ >{[ λ ω , all (workload_exceeds_time ω) lengths | ξpart ◁{ξ } ]}
      ≤ min1 [
            seq ℙ <μ >{[ λ ω , workload_exceeds_time ω t | ξpart ◁{ξ } ]}
          | t <- lengths].

Step 3: Bound workload for a single interval

We now focus on a single interval of length Δ and show that the probability of workload exceeding Δ is bounded by the corresponding term in the Λ computation.

Variable Δ : nat.
Hypothesis H_Δ_in_range : (0 < Δ < D tsk + 1)%N.

Define random variables for the workload components (conditioned on ξ)...

    Let interfering_workload :=
      mkRvar
        (restrict μ (ξpart ◁{ξ }))
        (fun ω ⇒
           \sum_(tsko <- ts | (hep_task tsko tsk ) && (tsko != tsk ))
            pr_workload_of_task (μ := μ) tsko (A - D tsko) (A + Δ) ω
        ).

... and j's cost conditioned on arrival sequence ξ.

    Let cond_cost_j :=
      mkRvar (restrict μ (ξpart ◁{ξ })) (fun ω ⇒ odflt0 (job_cost j) ω).

    Hypothesis H_arrivals_consistent : arr_seq_job_arrival_consistent.
    Hypothesis H_arrivals_unique : pr_arrival_sequence_uniq.

The probability that the total workload exceeds Δ is bounded by the probability that the sum of job j's cost and interference exceeds Δ.

This uses the carry-in workload decomposition and properties of the abort-ready model (at most one job of each task is pending).

    Lemma workload_bounded_by_cost_plus_interference :
      ℙ <μ >{[ λ ω , workload_exceeds_time ω Δ | ξpart ◁{ξ } ]}
      ≤ ℙ <μ >{[ λ ω , (Δ < cond_cost_j ω + interfering_workload ω)%nat | ξpart ◁{ξ } ]}.

Define workload random variable for a single higher-priority task.

    Let task_workload : Task → rvar (restrict μ (ξpart ◁{ξ })) [eqType of work] :=
      λ tsko ,
        mkRvar (restrict μ (ξpart ◁{ξ }))
               [eta pr_workload_of_task tsko (A - D tsko)%N (A + Δ)%N].

The sum of task workloads (as random variables) stochastically dominates the interference workload (monotonicity of sums).

    Lemma interference_bounded_by_task_workload_sum :
      interfering_workload
        ⪯ ∑[rv ]_{tsko <- ts | hep_task tsko tsk && (tsko != tsk )} task_workload tsko .

Step 4: Bound each task's workload by a sum of job costs

For each higher-priority task, we bound its workload by the sum of costs of its jobs using the arrival curve and nth_cost construction.

    Variable tsko : Task.
    Hypothesis H_tsko_in_ts : tsko \in ts.
    Hypothesis H_tsko_hep : hep_task tsko tsk.
    Hypothesis H_neq : tsko != tsk.

Task workload is bounded by the sum of nth_cost over the maximum number of arrivals in the interval (given by the arrival curve).

    Lemma task_workload_bounded_by_nth_cost_sum :
      task_workload tsko
      ⪯ ∑[rv ]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i.

Technical lemma: rewrite sum using iota notation.

    Lemma nth_cost_sum_rewrite :
      ∑[rv ]_{i < max_arrivals tsko (Δ + D tsko)%nat} nth_cost tsko i
       ⪯ ∑[rv ]_{x <-iota 0 (max_arrivals tsko (Δ + D tsko)%nat)|xpredT x } nth_cost tsko x.

Step 5: Bound individual job costs by pWCET

Finally, we show that each individual job cost (the i-th job of task tsko) is bounded by the pWCET distribution of that task.

Variable i : nat.

The cost of the i-th job of task tsko is stochastically dominated by the pWCET distribution of tsko. This is the leaf-level bound that allows us to "replace" random job costs with deterministic pWCET distributions.

    Lemma nth_job_cost_bounded_by_pWCET :
      nth_cost tsko i ⪯ to_distrib pWCET_pmf tsko.

  End StepByStep.

Main Theorem

We prove that TDFP is bounded by Λ ts tsk.

Theorem probabilistic_rta_fp :
ℙ <μ >{[ D tsk ⟨<⟩ 𝓡 j ]} ≤ Λ ts tsk.

End TDFPIsBounded.