Library rt.model.basic.workload

Require Import rt.util.all.
Require Import rt.model.basic.job rt.model.basic.task rt.model.basic.schedule
               rt.model.basic.task_arrival rt.model.basic.response_time
               rt.model.basic.schedulability.

Module Workload.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask SporadicTaskArrival ResponseTime Schedulability.

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

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

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

    (* Consider some 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)
                               (j: option (JobIn arr_seq)) : time :=
      match j with
        | Some j' ⇒ (job_task j' = tsk)
        | None ⇒ 0
      end.

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