Library prosa.classic.model.schedule.uni.service

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.time prosa.classic.model.arrival.basic.task prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.arrival_sequence
               prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.workload.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

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.

  (* In this section, we introduce some auxiliary definitions about the service. *)
  Section ExtraDefinitions.

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

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

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

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

    (* Recall the notion of a job of task tsk. *)
    Let of_task_tsk j := job_task j == tsk.

    (* We define the cumulative task service received by the jobs from the task
       that arrives in interval ta1, ta2) within time interval [t1, t2). *)

    Definition task_service_of_jobs_received_in ta1 ta2 t1 t2 :=
      service_of_jobs sched (jobs_arrived_between arr_seq ta1 ta2) of_task_tsk t1 t2.

    (* For simplicity, let's define a shorter version of task service 
       for jobs that arrive and execute in the same interval t1, t2). *)

    Definition task_service_between t1 t2 := task_service_of_jobs_received_in t1 t2 t1 t2.

  End ExtraDefinitions.

  (* In this section, we prove some auxiliary lemmas about the service. *)
  Section ExtraLemmas.

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

    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
    Variable sched: schedule Job.

    (* ... where jobs do not execute before their arrival or after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.

    (* For simplicity, let's define some local names. *)
    Let job_completed_by := completed_by job_cost sched.
    Let arrivals_between := jobs_arrived_between arr_seq.

    (* First, we prove that service is monotonic. *)
    Lemma service_monotonic:
       j t1 t2,
        t1 t2
        service sched j t1 service sched j t2.

    (* Next, we prove that service during can be splited into two parts. *)
    Lemma service_during_cat:
       j t t1 t2,
        t1 t t2
        service_during sched j t1 t2 =
        service_during sched j t1 t + service_during sched j t t2.

    (* We prove that if in some time interval t1,t2) a job j receives k units of service, then there time instant t in [t1,t2) such that job is scheduled at time t and service of job j within interval [t1,t) is equal to k. *)
    Lemma incremental_service_during:
       j t1 t2 k,
        service_during sched j t1 t2 > k
         t, t1 t < t2 scheduled_at sched j t service_during sched j t1 t = k.

    (* We prove that the overall service of jobs at each time instant is at most 1. *)
    Lemma service_of_jobs_le_1:
       (t1 t2 t: time) (P: Job bool),
        \sum_(j <- arrivals_between t1 t2 | P j) service_at sched j t 1.

    (* We prove that the overall service of jobs within 
       some time interval t, t + Δ) is at most Δ. *)

    Lemma total_service_of_jobs_le_delta:
       (t Δ: time) (P: Job bool),
        \sum_(j <- arrivals_between t (t + Δ) | P j)
         service_during sched j t (t + Δ) Δ.

    (* Next we prove that total service that is lower than the 
       range implies the existence of an idle time instant. *)

    Lemma low_service_implies_existence_of_idle_time :
       t1 t2,
        t1 t2
        service_of_jobs sched (arrivals_between 0 t2) predT t1 t2 < t2 - t1
         t, t1 t < t2 is_idle sched t.

    (* In this section we prove a few facts about splitting 
       the total service of a set of jobs. *)

    Section ServiceCat.

      (* We show that the total service of jobs released in a time interval t1,t2) during [t1,t2) is equal to the sum of: (1) the total service of jobs released in time interval [t1, t) during time [t1, t) (2) the total service of jobs released in time interval [t1, t) during time [t, t2) and (3) the total service of jobs released in time interval [t, t2) during time [t, t2). *)
      Lemma service_of_jobs_cat_scheduling_interval :
         P t1 t2 t,
          t1 t t2
          service_of_jobs sched (arrivals_between t1 t2) P t1 t2
          = service_of_jobs sched (arrivals_between t1 t) P t1 t
            + service_of_jobs sched (arrivals_between t1 t) P t t2
            + service_of_jobs sched (arrivals_between t t2) P t t2.

      (* We show that the total service of jobs released in a time interval t1,t2) during [t,t2) is equal to the sum of: (1) the total service of jobs released in a time interval [t1,t) during [t,t2) and (2) the total service of jobs released in a time interval [t,t2) during [t,t2). *)
      Lemma service_of_jobs_cat_arrival_interval :
         P t1 t2 t,
          t1 t t2
          service_of_jobs sched (arrivals_between t1 t2) P t t2 =
          service_of_jobs sched (arrivals_between t1 t) P t t2 +
          service_of_jobs sched (arrivals_between t t2) P t t2.

    End ServiceCat.

    (* In this section, we introduce a connection between the cumulative 
       service, cumulative workload, and completion of jobs. *)

    Section WorkloadServiceAndCompletion.

      (* Let P be an arbitrary predicate on jobs. *)
      Variable P: Job bool.

      (* Consider an arbitrary time interval t1, t2). *)
      Variables t1 t2: time.

      (* Let jobs be a set of all jobs arrived during t1, t2). *)
      Let jobs := arrivals_between t1 t2.

      (* Next, we consider some time instant t_compl. *)
      Variable t_compl: time.

      (* First, we prove that the fact that the workload of jobs is equal to the service 
         of jobs implies that any job in jobs is completed by time t_compl. *)

      Lemma workload_eq_service_impl_all_jobs_have_completed:
        workload_of_jobs job_cost jobs P =
        service_of_jobs sched jobs P t1 t_compl
        ( j, j \in jobs P j job_completed_by j t_compl).

      (* And vice versa, the fact that any job in jobs is completed by time t_compl 
         implies that the workload of jobs is equal to the service of jobs. *)

      Lemma all_jobs_have_completed_impl_workload_eq_service:
        ( j, j \in jobs P j job_completed_by j t_compl)
        workload_of_jobs job_cost jobs P =
        service_of_jobs sched jobs P t1 t_compl.

      (* Using the lemmas above, we prove equivalence. *)
      Lemma all_jobs_have_completed_equiv_workload_eq_service:
        ( j, j \in jobs P j job_completed_by j t_compl)
        workload_of_jobs job_cost jobs P =
        service_of_jobs sched jobs P t1 t_compl.

    End WorkloadServiceAndCompletion.

  End ExtraLemmas.

End Service.