Library probsa.rt.analysis.valid_pWCET_remains_valid

(* --------------------------------- Prosa ---------------------------------- *)
From prosa.model Require Import processor.ideal.

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export misc bigop_inf.
From probsa.probability Require Export pred law_of_total_prob.
From probsa.rt.model Require Export task events axiomatic_pWCET scheduler rt_monotonic.
From probsa.rt.analysis Require Export pETs_to_pWCETs partition_transfer
axiomatic_pWCET_step.

(* -------------------------------- SSReflect ------------------------------- *)
From mathcomp Require Import finfun.

(* ---------------------------------- Main ---------------------------------- *)

Valid pWCET Remains Valid

We plan to replace every single job cost using the procedure replace_job_pET repeated for each job. However, note that the assumption axiomatic_pWCET (μ_of S) is stated only for the initial system S. After we apply the transformation, we create a new system S' := replace_job_pET j S. Thus, in order to be able to use axiomatic_pWCET again on S', we must ensure that the pWCET remains axiomatic in the new system S'. In this section, we show that this is indeed the case.

Section ValidpWCETRemainsValid.

Assume horizon defines the termination time of the system. If horizon = None, the system does not terminate; however, it still has a finite number of jobs.

Variable horizon : option instant.

Consider any type of tasks with a notion of pWCET ...

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

...and their jobs.

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

Consider a response-time monotonic scheduling algorithm ζ, where response-time monotonic means the following -- assuming that all arrival times are fixed, an increase of the execution cost of any job cannot cause a decrease of the response time of any job. Recall that ζ receives two vectors: a vector of arrival times 𝗔 and a vector of job costs 𝗖.

Variable ζ : @scheduler 𝗔𝗖 Job.
Hypothesis H_rt_monotonic : rt_monotonic_scheduler horizon ζ.

For simplicity, let 𝓡 denote a function that maps 𝗔 and 𝗖 to a function that computes the response time of any job ...

Let 𝓡 := scheduler 𝗔𝗖 _to_rt 𝗔𝗖 horizon ζ.

... and let sched denote a schedule generated by ζ for a given system S.

Let sched S := compute_pr_schedule ζ (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S).

Auxiliary Lemmas

When we talk about axiomatic pWCET, we are interested in two properties: partition-independentness and partition-dominance. In this section, we prove two auxiliary lemmas which state that after transforming a system into a new system via function replace_job_pET, both properties are satisfied in the new system.

Section ProofOfLemmas.

Consider four parameters that describe a system under analysis: Ω, μ, 𝓐, and 𝓒.

    Variable Ω : countType.
    Variable μ : measure Ω.
    Variable 𝓐 : JobArrivalRV Job Ω μ.
    Variable 𝓒 : JobCostRV Job Ω μ.

Let us use these parameters to construct a system S.

Let S := {| Ω_of := Ω; μ_of := μ; 𝓐 _of := 𝓐; 𝓒 _of := 𝓒 |}.

Next, consider two arbitrary jobs: job j, for which we compute the response time, 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' := replace_job_pET j_rep S.

Similar to probsa/rt/analysis/axiomatic_pWCET_step.v, consider an arrival sequence ξ and two events corresponding to ω that realize this arrival sequence in systems S and S', respectively.

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

Also, consider a partition P of Ω and its extension P' to Ω'.

Variable P : @Ω_partition (Ω_of S) (μ_of S).
Let P' := extend_partition S P j_rep.

In this section, we show that if partition-dominance holds for S w.r.t. partition P, then partition-dominance holds for S' w.r.t. partition P'.

    Section ConditionalBoundedness.

      Hypothesis H_job_cost_cond_bounded_by_pWCET :
        ∀ (i : I P) (ρ : PosProb (μ_of S) (ξf ∩ P ◁{i })),
          𝔽<μ_of S , ρ >{[ odflt0 (𝓒 _of S j) | ξf ∩ P ◁{i } ]} ⪯ pWCET_cdf (job_task j).

      Lemma job_cost_cond_bounded_by_pWCET_respected :
        ∀ (i : I P') (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i })),
          𝔽<μ_of S', ρ'>{[ odflt0 (𝓒 _of S' j) | ξf' ∩ P'◁{i } ]} ⪯ pWCET_cdf (job_task j).

    End ConditionalBoundedness.

In this section, we show that if partition-independentness holds for S w.r.t. partition P, then partition-independentness holds for S' w.r.t. partition P'.

Section ConditionalIndependence.

Consider an arbitrary vector of job costs 𝗖...

Variable (𝗖 : Job → option work).

... and two events corresponding to ωs that realize this vector of job costs in systems S and S', respectively.

      Let 𝓒 _fix := events .𝓒 _fix (job_cost := 𝓒 _of S) 𝗖.
      Let 𝓒 _fix' := events .𝓒 _fix (job_cost := 𝓒 _of S') 𝗖.

      Hypothesis H_job_cost_cond_independent :
        ∀ (i : I P) (jobs : seq Job) (ρ : PosProb (μ_of S) (ξf ∩ P ◁{i })),
          j \notin jobs →
          ℙ <μ_of S , ρ >{[ 𝓒 _fix [:: j ] ∩ 𝓒 _fix jobs | ξf ∩ P ◁{i } ]}
            = ℙ <μ_of S >{[ 𝓒 _fix [:: j ] | ξf ∩ P ◁{i } ]} × ℙ <μ_of S >{[ 𝓒 _fix jobs | ξf ∩ P ◁{i } ]}.

      Lemma job_cost_cond_independent_respected :
        ∀ (i : I P') (jobs : seq Job) (ρ' : PosProb (μ_of S') (ξf' ∩ P'◁{i })),
          j \notin jobs →
          ℙ <μ_of S', ρ'>{[ 𝓒 _fix' [:: j ] ∩ 𝓒 _fix' jobs | ξf' ∩ P'◁{i } ]}
            = ℙ <μ_of S'>{[ 𝓒 _fix' [:: j ] | ξf' ∩ P'◁{i } ]} × ℙ <μ_of S'>{[ 𝓒 _fix' jobs | ξf' ∩ P'◁{i } ]}.

    End ConditionalIndependence.

  End ProofOfLemmas.

Valid Axiomatic pWCET Remains Valid

We use the two auxiliary lemmas to prove a lemma that, given a system S, an axiomatic pWCET remains valid for a new system S' where pETs of an arbitrary set of jobs have been replaced by pWCETs.

  Lemma valid_axiomatic_pWCET_remains_valid :
    ∀ (S : system) (jobs : seq Job),
      let S' := foldr replace_job_pET S jobs in
      axiomatic_pWCET (μ_of S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S) →
      axiomatic_pWCET (μ_of S') (job_arrival := 𝓐 _of S') (job_cost := 𝓒 _of S').

Iterative Application of Theorem 1

Consequently, one can use Theorem 1 iteratively to replace the pETs of all jobs in the system.

  Theorem prob_rt_monotonic_axiomatic_pWCET_replace_all_pETs :
    ∀ (S : system),
      let S' := replace_all_pETs S in
      let sched S := compute_pr_schedule ζ (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S) in
      axiomatic_pWCET (μ_of S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S) →
      probabilistic_response_time_monotone_transformation horizon
        (sched S) (job_arrival := 𝓐 _of S) (job_cost := 𝓒 _of S)
        (sched S') (job_arrival_s := 𝓐 _of S') (job_cost_s := 𝓒 _of S').

End ValidpWCETRemainsValid.