Library probsa.rt.analysis.transformation_properties

From probsa.rt.model Require Export pRBF assumptions.basic.
From probsa.rt.analysis Require Export axiomatic_pWCET_full.

Local Open Scope nat_scope.


Properties of the Axiomatic-pWCET Transformation

This file proves that the system after replacing probabilistic execution times (pETs) with their axiomatic pWCETs satisfies key properties required for schedulability analysis.

Structure and Reading Guide

Each section follows a three-step pattern. Step 1: The property holds after one transformation step (single job). Step 2: The property holds after multiple transformation steps. Step 3: The property holds after the complete transformation (all jobs).
For understanding the main results, focus on the Step 3 lemmas in each section since they provide the final guarantees. The intermediate steps (1 and 2) are technical scaffolding for the inductive proof structure.

Preservation of the Sporadic Task Model

First, we prove that if the original system satisfies the sporadic task model, then the transformed system also satisfies the sporadic task model. Since the transformation only changes job costs and not arrival times, this property is preserved.
Section TransformationRespectsSporadicTaskModel.

Consider any type of tasks with a notion of pWCET ...
  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {T : SporadicModel Task}
          {pWCET_pmf : ProbWCET Task}.

...and their jobs.
  Context {Job : finType}
          {job_task : JobTask Job Task}.

Consider a scheduling algorithm ζ that receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.
  Variable ζ : @scheduler𝗔𝗖 Job.

Let sched denote a schedule generated by ζ for a given system S.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

First, we show that a single step of the transformation preserves the property in question.
  Section Step1.

Consider a system S.
    Variable S : @system Job.

Next, consider two arbitrary jobs: job j and job j_rep, whose pET we modify.
    Variable (j_rep : Job) (j : Job).

Suppose we use the construction replace_job_pET presented in probsa/rt/analysis/pETs_to_pWCETs to replace the execution cost of given job j_rep. Let S' denote the resulting system.
    Let S' : system := replace_job_pET j_rep S.

Then, given a task set ts, ...
    Variable ts : seq Task.

... if S respects the sporadic task model, then S' also satisfies the sporadic task model.
    Lemma sporadic_task_model_respected_step :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts .

  End Step1.

In the next step, we apply the transformation to an arbitrary subset of jobs jobs.
  Section Step2.

    Variables (ts : seq Task) (jobs : seq Job) (S : @system Job).
    Let S' : system := foldr replace_job_pET S jobs.

    Lemma sporadic_task_model_respected_steps :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.

  End Step2.

Finally, we apply the previous lemma to a set of jobs that coincides with the set of all jobs.
  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Variable ts : seq Task.

    Lemma sporadic_task_model_respected :
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S) ts →
      pr_taskset_respects_sporadic_task_model (job_arrival := 𝓐_of S') ts.

  End Step3.

End TransformationRespectsSporadicTaskModel.

Preservation of the Horizon Property

We prove that if all job deadlines fall before a horizon h in the original system, they also fall before h in the transformed system. Since the transformation does not modify arrival times or task deadlines, this property is trivially preserved.
Section TransformationRespectsBigHorizon.

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

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

  Let job_deadline (S : system) (j : Job) :=
    @job_deadline _ _ _ (@job_deadline_from_task_deadline _ _ _ _ D (𝓐_of S) _) j.

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Variable h : instant.
    Hypothesis BIG : ∀ (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon_step :
      ∀ (ω : Ω_of S'), odflt0 (job_deadline S' j) ω < h.

  End Step1.

  Section Step2.

    Variables (S : @system Job) (jobs : seq Job) (j : Job).
    Let S' : system := foldr replace_job_pET S jobs.

    Variable h : instant.
    Hypothesis H_horizon_big : ∀ (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon_steps :
      ∀ ω, odflt0 (job_deadline S' j) ω < h.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' : system := replace_all_pETs S.

    Variable h : instant.
    Hypothesis H_horizon_big : ∀ (j : Job) (ω : Ω_of S), odflt0 (job_deadline S j) ω < h.

    Lemma transformation_respects_big_horizon :
      ∀ (j : Job) (ω : Ω_of S'),
        odflt0 (job_deadline S' j) ω < h.

  End Step3.

End TransformationRespectsBigHorizon.

Preservation of Arrival-Cost Consistency

We prove that if arrivals and costs are consistent in the original system (i.e., jobs with no arrival have no cost), this consistency is preserved in the transformed system.
Section TransformationRespectsArrivalsCostConsistent.

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

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Lemma transformation_respects_consistent_arrivals_step :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').

  End Step1.

  Section Step2.

    Variables (jobs_rep : seq Job) (S : @system Job).
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Lemma transformation_respects_consistent_arrivals_steps :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Lemma transformation_respects_consistent_arrivals :
      arrivals_cost_consistent (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S) →
      arrivals_cost_consistent (job_arrival := 𝓐_of S') (job_cost := 𝓒_of S').

  End Step3.

End TransformationRespectsArrivalsCostConsistent.

Preservation of Arrival Sequences

We prove that the transformation preserves arrival sequences: every arrival sequence in the transformed system corresponds to an arrival sequence in the original system. Since the transformation only modifies costs and not arrivals, the set of possible arrival sequences remains unchanged.
Section TransformationPreservesArrivalSequence.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Variable (S : @system Job) (j_rep : Job).
  Let S' : system := replace_job_pET j_rep S.

  Lemma transformation_preserves_arr_seq :
    ∀ ξ' : imgT (arr_seq (job_arrival := 𝓐_of S')),
    ∃ ξ : imgT (arr_seq (job_arrival := 𝓐_of S)),
    ∀ t, proj1_sig ξ t = proj1_sig ξ' t.
End TransformationPreservesArrivalSequence.

Identical Distributions and Stochastic Bounds

We prove that after the transformation two new properties hold. (1) All jobs of the same task have identically distributed costs. And (2) job costs are stochastically dominated by (and dominate) their task's pWCET.
Section TransformationEnsuresIdenticalCosts.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' := replace_job_pET j_rep S.

    Section CostBoundedByPWCET.

      Variable tsk : Task.
      Hypothesis H_job_of_task : job_of_task tsk j_rep.

      Lemma replaced_pETs_bounded_by_pWCETs_step :
        odflt0 (𝓒_of S' j_rep) ⪯ to_distrib pWCET_pmf tsk.
      Lemma pWCETs_bounded_by_replaced_pETs_step :
        to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j_rep).
    End CostBoundedByPWCET.

    Section CostBounds.

      Hypothesis H_jobs_neq : j_rep != j.

      Lemma nonreplaced_pETs_dont_change_1_step :
        odflt0 (𝓒_of S' j) ⪯ odflt0 (𝓒_of S j).
      Lemma nonreplaced_pETs_dont_change_2_step :
        odflt0 (𝓒_of S j) ⪯ odflt0 (𝓒_of S' j).
    End CostBounds.

  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jobs_uniq : uniq jobs_rep.

    Variable S : @system Job.
    Let S' := foldr replace_job_pET S jobs_rep.

    Variables (j : Job) (tsk : Task).
    Hypothesis H_j_in_reps : j \in jobs_rep.
    Hypothesis H_job_of_task : job_of_task tsk j.

    Lemma replaced_pETs_bounded_by_pWCETs_steps :
      odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsk.

    Lemma pWCETs_bounded_by_replaced_pETs_steps :
      to_distrib pWCET_pmf tsk ⪯ odflt0 (𝓒_of S' j).

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Lemma replaced_pETs_bounded_by_pWCETs :
      ∀ (j : Job) (tsko : Task),
        job_of_task tsko j →
        odflt0 (𝓒_of S' j) ⪯ to_distrib pWCET_pmf tsko.

    Lemma pWCETs_bounded_by_replaced_pETs :
      ∀ (j : Job) (tsko : Task),
        job_of_task tsko j →
        to_distrib pWCET_pmf tsko ⪯ odflt0 (𝓒_of S' j).

    Lemma pETs_have_same_distribution :
      ∀ (j1 j2 : Job),
        job_task j1 = job_task j2 →
        odflt0 (𝓒_of S' j1) ⪯ odflt0 (𝓒_of S' j2).

  End Step3.

End TransformationEnsuresIdenticalCosts.

Independence of Job Costs

We prove that all job costs are jointly independent in the transformed system. This property is established by the transformation itself: since each job's cost is sampled independently from its task's pWCET distribution, the costs are independent regardless of whether the original pETs were independent.
Section TransformationEnsuresIndependentCosts.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Variable jobs : seq Job.
    Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

    Lemma replaced_pETs_are_independent_step :
      indep2 (𝓒_of S' j_rep) (rvar_list [seq 𝓒_of S' j | j <- jobs]).

    Lemma transformation_respects_independence_step :
      independent [seq 𝓒_of S j | j <- jobs] →
      independent [seq 𝓒_of S' j | j <- jobs].
  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jobs_uniq : uniq jobs_rep.

    Variable S : @system Job.
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Lemma replaced_pETs_are_independent_steps :
      independent [seq 𝓒_of S' j | j <- jobs_rep].

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' : system := replace_all_pETs S.

    Lemma replaced_pETs_are_independent :
      independent [seq 𝓒_of S' j | j <- index_enum Job].

  End Step3.

End TransformationEnsuresIndependentCosts.

Independence from Arrival Sequences and Conditional Independence

We prove that in the transformed system three new properties hold. (1) Job costs are independent of the arrival sequence. (2) Job costs are jointly independent when conditioned on any fixed arrival sequence. (3) Conditional job costs are bounded by pWCETs. These properties are established by the transformation: each job's cost is sampled from its task's pWCET distribution independently of arrivals.
Section TransformationEnsuresCostsIndependentFromArrivals.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Section Step1.

    Variable (S : @system Job) (j_rep : Job) (j : Job).
    Let S' : system := replace_job_pET j_rep S.

    Section IndependentArrSeq.

      Variable ξa : arrival_sequence Job.
      Let ξf := ξ_fix (arr_seq (job_arrival := 𝓐_of S)) ξa.
      Let ξf' := ξ_fix (arr_seq (job_arrival := 𝓐_of S')) ξa.

      Variable jobs : seq Job.
      Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

      Lemma transformation_respects_pET_indep_arr_seq_cons_step :
        @indep2 _ _ _ (μ_of S)
                {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
                {| rvar_fun := ξf |} →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- j_rep :: jobs] |}
                {| rvar_fun := ξf' |}.

      Lemma transformation_respects_pET_indep_arr_seq_eq_step :
        @indep2 _ _ _ (μ_of S)
                {| rvar_fun := λ ω, [seq 𝓒_of S j ω | j <- jobs] |}
                {| rvar_fun := ξf |} →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j ω | j <- jobs] |}
                {| rvar_fun := ξf' |}.
      Lemma transformation_respects_pET_indep_arr_seq_remove_step :
          @indep2 _ _ _ (μ_of S)
                  {| rvar_fun := λ ω, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
                  {| rvar_fun := ξf |} →
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := ξf' |}.

    End IndependentArrSeq.

    Section IndependentArrSeqPartition.

      Variable jobs : seq Job.
      Hypothesis H_jrep_notin_jobs : j_rep \notin jobs.

      Lemma transformation_respects_pET_indep_arr_seq_eq_part_step :
        (∀ (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
            @indep2 _ _ _ (μ_of S)
                    {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs] |}
                    {| rvar_fun := [eta ξpart◁{ξ}] |}
        ) →
        ∀ (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := [eta ξpart◁{ξ}] |}.

      Lemma transformation_respects_pET_indep_arr_seq_remove_part_step :
        (∀ (ξpart := @partition_on_ξ (Ω_of S) (μ_of S) Job (𝓐_of S)) (ξ : I ξpart),
            @indep2 _ _ _ (μ_of S)
                    {| rvar_fun := λ ω : Ω_of S, [seq 𝓒_of S j0 ω | j0 <- jobs & predC1 j0 j_rep] |}
                    {| rvar_fun := [eta ξpart◁{ξ}] |}
        ) →
        ∀ (ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S')) (ξ : I ξpart),
          @indep2 _ _ _ (μ_of S')
                  {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                  {| rvar_fun := [eta ξpart◁{ξ}] |}.

    End IndependentArrSeqPartition.

  End Step1.

  Section Step2.

    Variable jobs_rep : seq Job.
    Hypothesis H_jrep_notin_jobs : uniq jobs_rep.

    Variable S : @system Job.
    Let S' : system := foldr replace_job_pET S jobs_rep.

    Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
    Variable (ξ : I ξpart).

    Lemma replaced_pETs_are_independent_from_arr_seq_partition_steps :
      ∀ (jobs : seq Job),
        (∀ j, j \in jobs → j \in jobs_rep) →
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω : Ω_of S', [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                {| rvar_fun := [eta ξpart◁{ξ}] |}.

  End Step2.

  Section Step3.

    Variable S : @system Job.
    Let S' := replace_all_pETs S.

    Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
    Variable (ξ : I ξpart).
    Variable (ρ : PosProb (μ_of S') (ξpart◁{ξ})).

We prove that job costs (as a collection) are independent of the arrival sequence partition indicator. That is, knowing which arrival sequence ξ occurred doesn't provide information about job costs, and vice versa.
    Lemma replaced_pETs_are_independent_from_arr_seq_partition :
      ∀ (jobs : seq Job),
        @indep2 _ _ _ (μ_of S')
                {| rvar_fun := λ ω, [seq 𝓒_of S' j0 ω | j0 <- jobs] |}
                {| rvar_fun := [eta ξpart◁{ξ}] |}.

Job costs remain jointly independent when conditioned on a fixed arrival sequence ξ. That is, even after observing which arrival pattern occurred, the job costs are still independent of each other.
    Lemma replaced_pETs_are_cond_independent :
      @independent
        _ _ (restrict (μ_of S') (ξpart◁{ξ}))
        [seq mkRvar _ (𝓒_of S' j) | j <- index_enum Job].
  End Step3.

End TransformationEnsuresCostsIndependentFromArrivals.

Conditional Cost Bounds

In the last section, we prove that job costs conditioned on a fixed arrival sequence are still bounded by their task's pWCET distribution in the transformed system.
Section TransformationEnsuresCondCostsBounded.

  Context {Task : TaskType}
          {D : TaskDeadline Task}
          {pWCET_pmf : ProbWCET Task}.

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

  Variable ζ : @scheduler𝗔𝗖 Job.
  Let sched (S : system) := compute_pr_schedule ζ (job_arrival := 𝓐_of S) (job_cost := 𝓒_of S).

  Variable S : @system Job.
  Let S' := replace_all_pETs S.

  Let ξpart := @partition_on_ξ (Ω_of S') (μ_of S') Job (𝓐_of S').
  Variable (ξ : I ξpart).
  Variable (ρ : PosProb (μ_of S') (ξpart◁{ξ})).

The cost of job j, conditioned on arrival sequence ξ, is stochastically dominated by the pWCET of its task.
  Lemma replaced_cond_pETs_bounded_by_pWCETs :
    ∀ (j : Job) (tsk : Task),
      job_of_task tsk j →
      mkRvar (restrict (μ_of S') (ξpart◁{ξ})) [eta odflt0 (𝓒_of S' j)] ⪯ to_distrib pWCET_pmf tsk.

End TransformationEnsuresCondCostsBounded.