Library probsa.rt.analysis.axiomatic_pWCET_full

(* --------------------------------- 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
valid_pWCET_remains_valid axiomatic_pWCET_step.

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

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

In this file, we prove the correctness of 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).

Proof of Theorem 2

Section MainLemma.

Assume horizon defines (an upper bound on) the termination time of the system. If horizon = None, the system does not necessarily terminate. Note, however, that in either case our proof assumes there to be a finite number of jobs for technical reasons. As the horizon can be chosen to be arbitrarily large (the proof does not depend on its magnitude), e.g., hundreds of even thousands of years, assuming the existence of a finite horizon is not unreasonable for a computing system.

Variable horizon : option instant.

Initial System

Consider any type of tasks and their jobs.

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

Consider a system that is described by a ground truth sample space Ωg and a ground truth probability measure μg.

Variables (Ωg : _) (μg : measure Ωg).

Next, consider our two essential parameters — probabilistic job costs job_cost and probabilistic job arrivals job_arrival.

Context {job_cost : JobCostRV Job Ωg μg}
{job_arrival : JobArrivalRV Job Ωg μg}.

Ωg, μg, job_arrival, and job_cost together form a system that we call the initial system.

Let initial_system := Build_system Ωg μg job_arrival job_cost.

Let us assume that we are given an _axiomatic pWCET_ for the initial system.

Context {pWCET_pmf : ProbWCET Task}.
Hypothesis H_axiomatic_pWCET : axiomatic_pWCET μg.

Simplified System

We define the _simplified_ system as one in which the pETs have been replaced by pWCETs using the replace_all_pETs function defined in rt/analysis/pETs_to_pWCETs.v.

Let simplified_system : system := replace_all_pETs initial_system.

For convenience, we "unpack" the simplified system into its parameters: ... ... sample space Ωs, ...

Let Ωs : countType := Ω_of simplified_system.

... measure μs, ...

Let μs : measure Ωs := μ_of simplified_system.

... job arrivals job_arrival_s, ...

Instance job_arrival_s : JobArrivalRV Job Ωs μs := 𝓐 _of simplified_system.

... and job costs job_cost_s.

Instance job_cost_s : JobCostRV Job Ωs μs := 𝓒 _of simplified_system.

Theorem 2

Consider an RT-monotonic scheduler ζ ...

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

... and consider two (probabilistic) schedules computed with ζ for the initial system sched1 and for the simplified system sched2.

Let sched1 := @compute_pr_schedule Ωg μg Job _ _ ζ.
Let sched2 := @compute_pr_schedule Ωs μs Job _ _ ζ.

Then, for any job j, it is the case that the response-time distribution of j in sched1 is ⪯-dominated by the response-time distribution in sched2. In other words, by computing the response-time distribution of a given job in the simplified system, we obtain a safe upper bound on the response-time of the corresponding job in the initial system.

Theorem probabilistic_rt_monotonicity_of_iid_pWCET :
∀ j : Job , response_time sched1 horizon j ⪯ response_time sched2 horizon j.

In other words, the transformation is pRT-monotone.

  Corollary probabilistic_rt_monotonicity_of_iid_pWCET' :
    probabilistic_response_time_monotone_transformation
      horizon sched1 sched2.

End MainLemma.

Print Assumptions probabilistic_rt_monotonicity_of_iid_pWCET.