Library prosa.classic.model.schedule.global.workload

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.schedulability prosa.classic.model.schedule.global.response_time.
Require Import prosa.classic.model.schedule.global.basic.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq div fintype bigop path.

Module Workload.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask TaskArrival ResponseTime Schedulability.

  (* Let's define the workload. *)
  Section WorkloadDef.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_task: Job → sporadic_task.

    (* Consider any job arrival sequence ...*)
    Variable arr_seq: arrival_sequence Job.

    (* ...and any schedule of these jobs. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Let tsk be any task. *)
    Variable tsk: sporadic_task.

    (* First, we define a function that returns the amount of service
       received by this task in a particular processor. *)
    Definition service_of_task (cpu: processor num_cpus)
                               (scheduled_job: option Job) : time :=
      if scheduled_job is Some j' then
        (job_task j' == tsk)
      else 0.

    (* Next, workload is defined as the service received by jobs of
       the task in the interval t1,t2). *)
    Definition workload (t1 t2: time) :=
      \sum_(t1 ≤ t < t2)
        \sum_(cpu < num_cpus)
          service_of_task cpu (sched cpu t).

    (* Now, we define workload by summing up the cumulative service
       during t1,t2) of the scheduled jobs, but only those spawned by the task that we care about. *)
    Definition workload_joblist (t1 t2: time) :=
      \sum_(j <- jobs_of_task_scheduled_between job_task sched tsk t1 t2)
        service_during sched j t1 t2.

    (* Next, we show that the two definitions are equivalent. *)
    Lemma workload_eq_workload_joblist :
      ∀ t1 t2,
      workload t1 t2 = workload_joblist t1 t2.

  End WorkloadDef.

End Workload.