Library prosa.classic.model.schedule.global.basic.schedule

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

(* Definition, properties and lemmas about schedules. *)
Module Schedule.

  Export ArrivalSequence.

  (* A processor is defined as a bounded natural number: 0, num_cpus). *)
  Definition processor (num_cpus: nat) := 'I_num_cpus.

  Section ScheduleDef.

    (* Consider any type of job. *)
    Variable Job: eqType.

    (* Given the number of processors... *)
    Variable num_cpus: nat.

    (* ... we define a schedule as a mapping such that each processor
       at each time contains either a job from the sequence or none. *)

    Definition schedule :=
      processor num_cpus time option Job.

  End ScheduleDef.

  (* Next, we define properties of jobs in a schedule. *)
  Section ScheduledJobs.

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

    (* Given an arrival sequence, ... *)
    Context {arr_seq: arrival_sequence Job}.

    Variable job_cost: Job time. (* ... a job cost function, ... *)

    (* ... and the number of processors, ...*)
    Context {num_cpus: nat}.

    (* ... we define the following properties for job j in schedule sched. *)
    Variable sched: schedule Job num_cpus.
    Variable j: Job.

    (* A job j is scheduled on processor cpu at time t iff such a mapping exists. *)
    Definition scheduled_on (cpu: processor num_cpus) (t: time) :=
      sched cpu t == Some j.

    (* A job j is scheduled at time t iff there exists a cpu where it is mapped.*)
    Definition scheduled (t: time) :=
      [ cpu, scheduled_on cpu t].

    (* A processor cpu is idle at time t if it doesn't contain any jobs. *)
    Definition is_idle (cpu: processor num_cpus) (t: time) :=
      sched cpu t = None.

    (* The instantaneous service of job j at time t is the number of cpus
       where it is scheduled on. Note that we use a sum to account for
       parallelism if required. *)

    Definition service_at (t: time) :=
      \sum_(cpu < num_cpus | scheduled_on cpu t) 1.

    (* The cumulative service received by job j during 0, t'). *)
    Definition service (t': time) := \sum_(0 t < t') service_at t.

    (* The cumulative service received by job j during t1, t2). *)
    Definition service_during (t1 t2: time) := \sum_(t1 t < t2) service_at t.

    (* Job j has completed at time t if it received enough service. *)
    Definition completed (t: time) := service t job_cost j.

    (* Job j is pending at time t iff it has arrived but has not completed. *)
    Definition pending (t: time) := has_arrived job_arrival j t && ~~completed t.

    (* Job j is backlogged at time t iff it is pending and not scheduled. *)
    Definition backlogged (t: time) := pending t && ~~scheduled t.

    (* Job j is carry-in in interval t1, t2) iff it arrives before t1 and is not complete at time t1 *)
    Definition carried_in (t1: time) := arrived_before job_arrival j t1 && ~~ completed t1.

    (* Job j is carry-out in interval t1, t2) iff it arrives after t1 and is not complete at time t2 *)
    Definition carried_out (t1 t2: time) := arrived_before job_arrival j t2 && ~~ completed t2.

    (* The list of scheduled jobs at time t is the concatenation of the jobs
       scheduled on each processor. *)

    Definition jobs_scheduled_at (t: time) :=
      \cat_(cpu < num_cpus) make_sequence (sched cpu t).

    (* The list of jobs scheduled during the interval t1, t2) is the the duplicate-free concatenation of the jobs scheduled at instant. *)
    Definition jobs_scheduled_between (t1 t2: time) :=
      undup (\cat_(t1 t < t2) jobs_scheduled_at t).

  End ScheduledJobs.

  (* In this section, we define properties of valid schedules. *)
  Section ValidSchedules.

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

    (* Consider any multiprocessor schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Next, we define whether job are sequential, ... *)
    Definition sequential_jobs :=
       j t cpu1 cpu2,
        sched cpu1 t = Some j sched cpu2 t = Some j cpu1 = cpu2.

    (* ... whether a job can only be scheduled if it has arrived, ... *)
    Definition jobs_must_arrive_to_execute :=
       j t,
        scheduled sched j t
        has_arrived job_arrival j t.

    (* ... whether a job can be scheduled after it completes. *)
    Definition completed_jobs_dont_execute :=
       j t, service sched j t job_cost j.

    (* We also define whether jobs come from some arrival sequence. *)
    Definition jobs_come_from_arrival_sequence (arr_seq: arrival_sequence Job) :=
       j t, scheduled sched j t arrives_in arr_seq j.

  End ValidSchedules.

  (* In this section, we prove some basic lemmas about a job. *)
  Section JobLemmas.

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

    (* Consider any multiprocessor schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Next, we prove some lemmas about the service received by a job j. *)
    Variable j: Job.

    Section Basic.

      (* At any time t, job j is not scheduled iff it doesn't get service. *)
      Lemma not_scheduled_no_service :
         t,
          ~~ scheduled sched j t = (service_at sched j t == 0).

      (* If the cumulative service during a time interval is not zero, there
         must be a time t in this interval where the service is not 0, ... *)

      Lemma cumulative_service_implies_service :
         t1 t2,
          service_during sched j t1 t2 != 0
           t,
            t1 t < t2
            service_at sched j t != 0.

      (* ... and vice versa. *)
      Lemma service_implies_cumulative_service:
         t t1 t2,
          t1 t < t2
          service_at sched j t != 0
          service_during sched j t1 t2 != 0.

    End Basic.

    Section SequentialJobs.

      (* If jobs are sequential, then... *)
      Hypothesis H_sequential_jobs: sequential_jobs sched.

      (* ..., the service received by job j at any time t is at most 1, ... *)
      Lemma service_at_most_one :
         t, service_at sched j t 1.

      (* ..., which implies that the service receive during a interval
         of length delta is at most delta. *)

      Lemma cumulative_service_le_delta :
         t delta, service_during sched j t (t + delta) delta.

    End SequentialJobs.

    Section Completion.

      (* Assume that completed jobs do not execute. *)
      Hypothesis H_completed_jobs:
        completed_jobs_dont_execute job_cost sched.

      (* Then, after job j completes, it remains completed. *)
      Lemma completion_monotonic :
         t t',
          t t'
          completed job_cost sched j t
          completed job_cost sched j t'.

      (* A completed job cannot be scheduled. *)
      Lemma completed_implies_not_scheduled :
         t,
          completed job_cost sched j t
          ~~ scheduled sched j t.

      (* The service received by job j in any interval is no larger than its cost. *)
      Lemma cumulative_service_le_job_cost :
         t t',
          service_during sched j t t' job_cost j.

    End Completion.

    Section Arrival.

      (* Assume that jobs must arrive to execute. *)
      Hypothesis H_jobs_must_arrive:
        jobs_must_arrive_to_execute job_arrival sched.

      (* Then, job j does not receive service at any time t prior to its arrival. *)
      Lemma service_before_job_arrival_zero :
         t,
          t < job_arrival j
          service_at sched j t = 0.

      (* The same applies for the cumulative service received by job j. *)
      Lemma cumulative_service_before_job_arrival_zero :
         t1 t2,
          t2 job_arrival j
          \sum_(t1 i < t2) service_at sched j i = 0.

      (* Hence, you can ignore the service received by a job before its arrival time. *)
      Lemma service_before_arrival_eq_service_during :
         t0 t,
          t0 job_arrival j
          \sum_(t0 t < job_arrival j + t) service_at sched j t =
          \sum_(job_arrival j t < job_arrival j + t) service_at sched j t.

    End Arrival.

    Section Pending.

      (* Assume that jobs must arrive to execute. *)
      Hypothesis H_jobs_must_arrive:
        jobs_must_arrive_to_execute job_arrival sched.

     (* Assume that completed jobs do not execute. *)
      Hypothesis H_completed_jobs:
        completed_jobs_dont_execute job_cost sched.

      (* Then, if job j is scheduled, it must be pending. *)
      Lemma scheduled_implies_pending:
         t,
          scheduled sched j t
          pending job_arrival job_cost sched j t.

    End Pending.

  End JobLemmas.

  (* In this section, we prove some lemmas about the list of jobs
     scheduled at time t. *)

  Section ScheduledJobsLemmas.

    Context {Job: eqType}.

    (* Consider any multiprocessor schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    Section Membership.

    (* A job is in the list of scheduled jobs iff it is scheduled. *)
      Lemma mem_scheduled_jobs_eq_scheduled :
         j t,
          j \in jobs_scheduled_at sched t = scheduled sched j t.

    End Membership.

    Section Uniqueness.

      (* Suppose that jobs are sequential. *)
      Hypothesis H_sequential_jobs : sequential_jobs sched.

      (* Then, the list of jobs scheduled at any time t has no duplicates. *)
      Lemma scheduled_jobs_uniq :
         t,
          uniq (jobs_scheduled_at sched t).

    End Uniqueness.

    Section NumberOfJobs.

      (* The number of scheduled jobs is no larger than the number of cpus. *)
      Lemma num_scheduled_jobs_le_num_cpus :
         t,
          size (jobs_scheduled_at sched t) num_cpus.

    End NumberOfJobs.

  End ScheduledJobsLemmas.

End Schedule.

(* Specific properties of a schedule of sporadic jobs. *)
Module ScheduleOfSporadicTask.

  Import SporadicTask Job.
  Export Schedule.

  Section ScheduledJobs.

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

    (* Consider any multiprocessor schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Given a task tsk, ...*)
    Variable tsk: sporadic_task.

    (* ..., we we can state that tsk is scheduled on cpu at time t as follows. *)
    Definition task_scheduled_on (cpu: processor num_cpus) (t: time) :=
      if (sched cpu t) is Some j then
        (job_task j == tsk)
      else false.

    (* Likewise, we can state that tsk is scheduled on some processor. *)
      Definition task_is_scheduled (t: time) :=
        [ cpu, task_scheduled_on cpu t].

    (* We also define the list of jobs scheduled during t1, t2). *)
    Definition jobs_of_task_scheduled_between (t1 t2: time) :=
      filter (fun jjob_task j == tsk)
             (jobs_scheduled_between sched t1 t2).

  End ScheduledJobs.

  Section ScheduleProperties.

    Context {sporadic_task: eqType}.
    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_task: Job sporadic_task.

    (* Consider any multiprocessor schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Next we define intra-task parallelism. *)
    Definition jobs_of_same_task_dont_execute_in_parallel :=
       j j' t,
        job_task j = job_task j'
        scheduled sched j t
        scheduled sched j' t
        j = j'.

  End ScheduleProperties.

  Section BasicLemmas.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Context {Job: eqType}.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Consider any valid schedule of sporadic tasks ...*)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

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

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

    (* ...and let j be any valid job of tsk. *)
    Variable j: Job.
    Hypothesis H_job_of_task: job_task j = tsk.
    Hypothesis valid_job:
      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* Remember that for any job of tsk, service <= task_cost tsk *)
    Lemma cumulative_service_le_task_cost :
         t t',
          service_during sched j t t' task_cost tsk.

  End BasicLemmas.

End ScheduleOfSporadicTask.