Library rt.model.schedule.uni.service

Require Import rt.util.all.
Require Import rt.model.time rt.model.arrival.basic.task rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence
               rt.model.priority.
Require Import rt.model.schedule.uni.schedule rt.model.schedule.uni.workload.

Module Service.

  Import UniprocessorSchedule Priority Workload.

  (* In this section, we define the more general notion of service received by sets of jobs. *)
  Section ServiceOverSets.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.

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

    (* ...and any uniprocessor schedule of these jobs. *)
    Variable sched: schedule Job.

    (* Let jobs denote any (finite) set of jobs. *)
    Variable jobs: seq Job.

    Section Definitions.

      (* First, we define the service received by a generic set of jobs. *)
      Section ServiceOfJobs.

        (* Then, given any predicate over jobs, ...*)
        Variable P: Job bool.

        (* ...we define the cumulative service received during [t1, t2)
           by the jobs that satisfy this predicate. *)

        Definition service_of_jobs (t1 t2: time) :=
          \sum_(j <- jobs | P j) service_during sched j t1 t2.

      End ServiceOfJobs.

      (* Next, we define the service received by tasks with higher-or-equal
         priority under a given FP policy. *)

      Section PerTaskPriority.

        Context {Task: eqType}.
        Variable job_task: Job Task.

        (* Consider any FP policy. *)
        Variable higher_eq_priority: FP_policy Task.

        (* Let tsk be the task to be analyzed. *)
        Variable tsk: Task.

        (* Based on the definition of jobs of higher or equal priority (with respect to tsk), ... *)
        Let of_higher_or_equal_priority j := higher_eq_priority (job_task j) tsk.

        (* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
        Definition service_of_higher_or_equal_priority_tasks (t1 t2: time) :=
          service_of_jobs of_higher_or_equal_priority t1 t2.

      End PerTaskPriority.

      (* Next, we define the service received by jobs with higher or equal priority
         under JLFP policies. *)

      Section PerJobPriority.

        (* Consider any JLDP policy. *)
        Variable higher_eq_priority: JLFP_policy Job.

        (* Let j be the job to be analyzed. *)
        Variable j: Job.

        (* Based on the definition of jobs of higher or equal priority, ... *)
        Let of_higher_or_equal_priority j_hp := higher_eq_priority j_hp j.

        (* ...we define the service received during [t1, t2) by jobs of higher or equal priority. *)
        Definition service_of_higher_or_equal_priority_jobs (t1 t2: time) :=
          service_of_jobs of_higher_or_equal_priority t1 t2.

      End PerJobPriority.

    End Definitions.

    Section Lemmas.

      (* Let P be any predicate over jobs. *)
      Variable P: Job bool.

      (* In this section, we prove that the service received by any set of jobs
         is upper-bounded by the corresponding workload. *)

      Section ServiceBoundedByWorkload.

        (* Recall the definition of workload. *)
        Let workload_of := workload_of_jobs job_cost.

        (* Assume that jobs do not execute after completion.*)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Then, we prove that the service received by those jobs is no larger than their workload. *)
        Lemma service_of_jobs_le_workload:
           t1 t2,
            service_of_jobs P t1 t2 workload_of jobs P.

      End ServiceBoundedByWorkload.

      (* In this section, we prove that the service received by any set of jobs
         is upper-bounded by the corresponding interval length. *)

      Section ServiceBoundedByIntervalLength.

        (* Assume that jobs do not execute after completion.*)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the sequence of jobs is a set. *)
        Hypothesis H_no_duplicate_jobs: uniq jobs.

        (* Then, we prove that the service received by those jobs is no larger than their workload. *)
        Lemma service_of_jobs_le_delta:
           t1 t2,
            service_of_jobs P t1 t2 t2 - t1.

      End ServiceBoundedByIntervalLength.

    End Lemmas.

  End ServiceOverSets.

End Service.