Library probsa.rt.model.axiomatic_pWCET

(* -------------------------------- ProBsa -------------------------------- *)
From probsa.rt.model Require Import task events.
From probsa Require Export probability.stochastic_order.

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

Axiomatic pWCET

In this file, we introduce the construction of the axiomatic pWCET described in the paper "What really is pWCET? A Rigorous Axiomatic Definition of pWCET" by Bozhko et al. (RTSS'23). The construction we provide ensures that the resulting pWCET is a sound IID upper-bound on the probabilistic execution time (pET), which is not necessarily (and even most likely not) IID.

Section AxiomaticPWCET.

Consider a probability space (Ω, μ).

Context {Ω} (μ : measure Ω).

Consider any type of tasks with costs defined by a pWCET pWCET. Please refer to the ProbWCET type-class to see how task costs are defined in this case. In this file, we only define the two additional assumptions about independence and boundedness.

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

Consider any finite type of jobs associated with these tasks. Assume that these jobs have probabilistic arrivals and costs defined by job_arrival and job_cost, respectively.

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

For simplicity, let ξ_pr denote Ω's probabilistic arrival sequence.

Let ξ_pr : pr_arrival_sequence μ Job := arr_seq.

The axiomatic pWCET definition consists of three parts: (i) partitions (defined in the file probsa/probability/partition.v for modularity reasons, see @Ω_partition Ω μ), (ii) partition independence, and (iii) partition dominance. We define the latter two concepts next.

Partition Independence

Consider a job j, a fixed arrival sequence ξ, and a partition S of Ω. We say that j's pET is partition-independent w.r.t. ξ and S, iff for (i) any subset S◁{i} of partition S with positive-probability intersection with an event ξ_fix ξ_pr ξ (represented by the term PosProb μ (ξ_fix ξ_pr ξ ∩ S◁{i})), (ii) any cost assignments 𝗖 : Job → option work, and (iii) any set of jobs jobs, an event where j's cost agrees with 𝗖 (denoted as 𝓒_fix [::j]) and an event where costs of jobs jobs agree with 𝗖 (denoted as 𝓒_fix jobs) are independent conditioned on (ξ_fix ξ_pr ξ) ∩ (S◁{i}).

  Definition job_cost_partition_independence
             (j : Job)
             (ξ : arrival_sequence Job)
             (S : @Ω_partition Ω μ) :=
    ∀ (i : I S) (ρ : PosProb μ (ξ_fix ξ_pr ξ ∩ S ◁{i })),
    ∀ (𝗖 : Job → option work) (jobs : seq Job),
      j \notin jobs →
      ℙ <μ , ρ >{[ (𝓒 _fix 𝗖 [::j ]) ∩ (𝓒 _fix 𝗖 jobs ) | ξ_fix ξ_pr ξ ∩ S ◁{i } ]}
      = ℙ <μ , ρ >{[ 𝓒 _fix 𝗖 [::j ] | (ξ_fix ξ_pr ξ ) ∩ S ◁{i } ]}
        × ℙ <μ , ρ >{[ 𝓒 _fix 𝗖 jobs | (ξ_fix ξ_pr ξ ) ∩ S ◁{i } ]}.

Partition Dominance

Next, consider a job j, an arrival sequence ξ, and a partition S of Ω. We say that j's cost is S-dominated by the CDF of task job_task j's pWCET, iff for any event S◁{i} of S with positive-probability intersection with ξ_fix ξ (i.e., PosProb μ (ξ_fix ξ_pr ξ ∩ S◁{i})) and any given value x : ℕ, the cumulative distribution function of the cost of the job j in the given subset (as represented by the expression 𝔽{[ job_cost j | ξ_fix ξ ∩ S◁{i}]}(x)) is greater than or equal to the pWCET of the task of the job j for the same value x (as represented by the function pWCET(job_task j)(x)).

Here, the statement uses the odflt0 function to safely extract the value of job_cost j, or fallback to zero if job_cost j is ⊥ for the given ω

  Definition job_cost_partition_dominated
             (j : Job)
             (ξ : arrival_sequence Job)
             (S : @Ω_partition Ω μ) :=
    ∀ (i : I S) (ρ : PosProb μ (ξ_fix ξ_pr ξ ∩ S ◁{i })),
      𝔽<μ , ρ >{[ odflt0 (job_cost j) | ξ_fix ξ_pr ξ ∩ S ◁{i } ]} ⪯ pWCET_cdf(job_task j).

Full Definition

We say that a pWCET is an axiomatic pWCET iff, for any job j and any arrival sequence ξ, there exists a partition S of Ω such that both conditional partition independence and partition dominance are satisfied.

Definition axiomatic_pWCET :=

For any a job j and any arrival sequence ξ...

∀ (j : Job) (ξ : arrival_sequence Job),

there exists a partition S such that the following two conditions hold:

      ∃ (S : @Ω_partition Ω μ ),
        job_cost_partition_independence j ξ S
        ∧ job_cost_partition_dominated j ξ S.

End AxiomaticPWCET.