Library probsa.rt.analysis.WCET_is_pWCET

(* --------------------------------- ProBsa --------------------------------- *)
From probsa.util Require Export bigop_inf.
From probsa.probability Require Export pred.
From probsa.rt.model Require Export task WCET events axiomatic_pWCET .

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

WCET is Axiomatic pWCET

Section WCETisAxiomaticPWCET.

Consider a probability space (Ω, μ), ...

Context {Ω} {μ : measure Ω}.

... any type of tasks with costs defined by a function task_cost, ...

Context {Task : TaskType}
{task_cost : TaskCost Task}.

... and any finite type of jobs associated with these tasks. Assume that the 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 Ω μ}.

Let us assume that task_cost is a WCET in the system (Ω,μ).

Hypothesis H_task_cost_is_valid_WCET : task_cost_is_WCET.

Here we state that WCET might be interpreted as a pWCET. For this, we define a degenerate distribution with one step at workload task_cost tsk, which represents the WCET of a task tsk.

  Program Instance WCET_pmf : ProbWCET Task :=
    {|
      pWCET_pmf (tsk : Task) (c : work) := if task_cost tsk == c then 1%R else 0%R
    |}.

Next, we prove that partition_into_singletons trivially ensures the job_cost_partition_independence. The idea here is that conditioned on a singleton {ω} (for ω ∈ Ω), any random variable becomes a constant. But constants are always independent. Hence, the conditional independence holds.

  Lemma partition_into_singletons_partition_intependent :
    ∀ j ξ,
      job_cost_partition_independence μ j ξ (partition_into_singletons μ).

Next, we prove that conditioned on a singleton {ω}, any job cost is still bounded by WCET. This follows from the fact that we simply assume WCET is valid. The rest of the proof just connects the probabilistic interpretation of WCET with job costs.

  Lemma partition_into_singletons_partition_dominated :
    ∀ j ξ,
      job_cost_partition_dominated μ j ξ (partition_into_singletons μ).

Since both conditions hold, we can conclude that WCET is an axiomatic pWCET. Note, however, that here we only prove that WCET could be interpreted as an axiomatic pWCET, not that this is the ony possible pWCET.

Lemma WCET_is_axiomatic_pWCET :
axiomatic_pWCET μ.

End WCETisAxiomaticPWCET.

Print Assumptions WCET_is_axiomatic_pWCET.