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.

  Section WorkloadDef.

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

    Variable arr_seq: arrival_sequence Job.

    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    Variable tsk: sporadic_task.

    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.

    Definition workload (t1 t2: time) :=
      \sum_(t1 ≤ t < t2)
        \sum_(cpu < num_cpus)
          service_of_task cpu (sched cpu t).

    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.

    Lemma workload_eq_workload_joblist :
      ∀ t1 t2,
      workload t1 t2 = workload_joblist t1 t2.

  End WorkloadDef.

End Workload.