Library probsa.rt.model.task

From prosa.model Require Export task.concept.

From probsa.probability Require Export nrvar.
From probsa.rt.behavior Require Export job.

PMF of pWCET

In this file, we define pWCET's probability mass function. The typeclass contains three elements: (1) a function called pWCET_pmf that takes a Task and a work as input and returns a value in R that is supposed to denote the "probability" of a task to take a certain value, (2) a proof term that pWCET_pmf is non negative for any task and any work value, and (3) a proof term that pWCET_pmf sums up to 1.

It is important to note that even though R represents the set of real numbers, in the context of probability theory, probabilities are always represented by values between 0 and 1. Therefore, the pWCET_pmf function actually returns a value within the closed interval [0,1], representing the probability of a given Task completing after consuming work time units of processor service.

Class ProbWCET (Task : TaskType) := {
    pWCET_pmf : Task → (work → R );
    pWCET_nonnegative : ∀ (tsk : Task), ∀ (w : work ), pWCET_pmf tsk w ≥ 0;
    pWCET_sum1 : ∀ (tsk : Task), is_series (countable_sum (pWCET_pmf tsk)) 1
  }.

CDF of pWCET

Section CDFPWCET.

  Context {Ω} (μ : measure Ω).

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

Next, we define a more common form of pWCET as a CDF. Note that since pWCET_pmf is not an actual random variable, we cannot re-use the existing definition of CDF. Hence, we simply define pWCET_cdf tsk w0 as a sum of pWCET_pmf tsk w of all w ≤ w0.

Definition pWCET_cdf (tsk : Task) (w0 : nat) :=
∑[∞]_{w <- nat } if (w ≤ w0)%nat then pWCET_pmf tsk w else 0.

End CDFPWCET.

Given a job j and its task tsk with deadline D tsk, we define the probabilistic job deadline as Some (A + D tsk) if job_arrival j ω = Some A in an evolution ω and None otherwise.

Instance job_deadline_from_task_deadline
         (Job : JobType) (Task : TaskType)
         `{Ω : _} `{μ : measure Ω}
         `{TaskDeadline Task} `{job_arrival : JobArrivalRV Job Ω μ} `{JobTask Job Task}
  : JobDeadlineRV Job Ω μ :=
  { job_deadline j :=
        mkRvar
          μ
          (fun ω ⇒
             match job_arrival j ω with
             | Some A ⇒ Some(A + task_deadline (job_task j))%nat
             | None ⇒ None end
          )
  }.