In this file, we define the response-time monotonic transformation presented in the paper "What really is pWCET? A Rigorous Axiomatic Definition of pWCET" by Bozhko et al. (RTSS'23).

Transformation

As discussed in the paper, there are potentially many different response-time monotonic transformations (e.g., one can imagine a trivial transformation that simply maps probabilistic job costs to WCETs). However, we are interested in one specific transformation that decouples job-cost dependencies, thus turning job costs into IID random variables. In this section, we define a response-time monotonic transformation of the probability space that ensures the validity of axiomatic pWCET (defined in rt.model.axiomatic_pWCET).

Consider any type of tasks with a notion of pWCET.

Consider a finite set of jobs associated with the tasks.

System

For the sake of construction, we introduce a concept of a "system" S, which is a record type containing a sample space Ω_of S, a measure μ_of S, arrival times 𝓐_of S, and execution costs 𝓒_of S.

pWCET to Job Cost Random Variable

Given a pWCET, we can construct a new random variable describing a job's cost with the same distribution as its task's pWCET's probability mass function (PMF) pWCET_pmf. Note that this procedure involves defining a new sample space (the set of natural numbers), a new measure (that coincides with the pWCET's PMF), and a new job-cost function. The definition might seem a bit involved, so one might think about this function as follows. The pWCET of a task assigns a probability to each natural number. We can take these probabilities and construct a new probability space where Ω = nat and μ c = pWCET_pmf c. Next, we can define a random variable on this space as fun c ⇒ Some c; all this variable does is convert a natural number c to Some c, which is Coq's way of constructing the type 𝕎 ∪ ⊥. Note that fun c ⇒ Some c is a pET on Ω = nat. Indeed, its type is Ω → 𝕎 ∪ ⊥. Next, we use this random variable to construct pETs on the initial sample space Ω_of S.

Destruct pWCET_pmf into its constituent parts pWCET, nonneg, and sum1.

Replace pET of a Job

Suppose we are given a system S = (Ω, μ, 𝓐, 𝓒) and a job j. To construct a new system S' with j's pET replaced with its task's pWCET, we define (Ω', μ', 𝓐', 𝓒') as follows. Let (Ωj, μj, Cj) := pWCET_to_RVpWCET(job_task j). Then, the new system is defined as follows:

1. Ω' := Ω × Ωj — the new sample space is a cross product of Ω and Ωj.

2. μ' := fun (ω, ωj) ⇒ (μ ω) × (μj ωj) — the new measure on Ω' is defined as a product of μ and μj.

3. 𝓐'(jo) := 𝓐(jo) — arrival times remain the same.

4. 𝓒'(jo) := fun (ω, ωj) ⇒ if (j == jo) then (Cj jo ωj) else (𝓒 jo ω) — given a job jo: jo != j, its cost is defined on Ω and does not change, for job j the cost is redefined as Cj j ωj.

Replace pETs of a Set of Jobs

We can iteratively apply the function replace_job_pET for each job in a given set of jobs simply via foldr.

Replace pETs of All Jobs

To replace all job pETs, we simply need to repeat the procedure for all jobs (i.e., index_enum Job).