Library rt.model.basic.schedule

Require Import rt.util.all
               rt.model.basic.job rt.model.basic.task rt.model.basic.arrival_sequence.

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

    Context {Job: eqType}.

    (* Given the number of processors and an arrival sequence, ...*)
    Variable num_cpus: nat.
    Variable arr_seq: arrival_sequence Job.

    (* ... 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 (JobIn arr_seq).

  End ScheduleDef.

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

    Context {Job: eqType}.

    (* 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 num_cpus arr_seq.
    Variable j: JobIn arr_seq.

    (* 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: 'I_(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 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 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 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}. (* Assume a job type with decidable equality, ...*)
    Context {arr_seq: arrival_sequence Job}. (* ..., an arrival sequence, ...*)

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

    (* ... and a schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

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

  End ValidSchedules.

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

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

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

    (* ..., and a particular schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

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

    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 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 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_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.

    (* Consider an arrival sequence ...*)
    Context {Job: eqType}.
    Context {arr_seq: arrival_sequence Job}.

    (* ... and some schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    Section Membership.

    (* A job is in the list of scheduled jobs iff it is scheduled. *)
      Lemma mem_scheduled_jobs_eq_scheduled :
         j t,
          j 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 schedule. *)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    (* 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 (j: JobIn arr_seq) ⇒ job_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 schedule. *)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

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

  End ScheduleProperties.

  Section BasicLemmas.

    (* Assume the job cost and task are known. *)
    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.

    (* Then, in a valid schedule of sporadic tasks ...*)
    Context {arr_seq: arrival_sequence Job}.
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

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

    Variable tsk: sporadic_task.

    Variable j: JobIn arr_seq.
    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.