Library rt.model.schedule.uni.schedule

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.

Module UniprocessorSchedule.

  Import SporadicTaskset.
  Export Time ArrivalSequence.

  Section Schedule.

    (* We begin by defining a uniprocessor schedule. *)
    Section ScheduleDef.

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

      (* We define a uniprocessor schedule by mapping each point in time to either
         Some job that is scheduled or None, if the processor is idle. *)

      Definition schedule := time option Job.

    End ScheduleDef.

    (* In this section, we define properties of a schedule. *)
    Section ScheduleProperties.

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

      (* Consider any uniprocessor schedule. *)
      Variable sched: schedule Job.

      (* Let's define properties of the jobs to be scheduled. *)
      Section JobProperties.

        (* Let j be any job. *)
        Variable j: Job.

        (* First, we define whether a job j is scheduled at time t, ... *)
        Definition scheduled_at (t: time) := sched t == Some j.

        (* ...which also yields the instantaneous service received by
           job j at time t (i.e., either 0 or 1). *)

        Definition service_at (t: time) : time := scheduled_at t.

        (* Based on the notion of instantaneous service, we define the
           cumulative service received by job j during any interval [t1, t2). *)

        Definition service_during (t1 t2: time) :=
          \sum_(t1 t < t2) service_at t.

        (* Using the previous definition, we define the cumulative service
           received by job j up to time t, i.e., during interval [0, t). *)

        Definition service (t: time) := service_during 0 t.

        (* Next, we say that job j has completed by time t if it received enough
           service in the interval [0, t). *)

        Definition completed_by (t: time) := service t == job_cost j.

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

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

      End JobProperties.

      (* In this section, we define some properties of the processor. *)
      Section ProcessorProperties.

        (* We say that the processor is idle at time t iff there is no job being scheduled. *)
        Definition is_idle (t: time) := sched t == None.

        (* In addition, we define the total service performed by the processor in any interval
           [t1, t2) as the cumulative time in which the processor is not idle. *)

        Definition total_service_during (t1 t2: time) :=
          \sum_(t1 t < t2) ~~ is_idle t.

        (* Using the previous definition, we also define the total service up to time t2.*)
        Definition total_service (t2: time) := total_service_during 0 t2.

      End ProcessorProperties.

    End ScheduleProperties.

    (* 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 uniprocessor schedule. *)
      Variable sched: schedule Job.

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

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

      (* ... and whether a job cannot 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 schedules. *)
    Section Lemmas.

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

      (* Consider any uniprocessor schedule. *)
      Variable sched: schedule Job.

      (* Let's begin with lemmas about service. *)
      Section Service.

        (* Let j be any job that is to be scheduled. *)
        Variable j: Job.

        (* First, we prove that the instantaneous service cannot be greater than 1, ... *)
        Lemma service_at_most_one:
           t, service_at sched j t 1.

        (* ...which implies that the cumulative service received by job j in any
           interval of length delta is at most delta. *)

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

      End Service.

      (* Next, we prove properties related to job completion. *)
      Section Completion.

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

        (* Let j be any job that is to be scheduled. *)
        Variable j: Job.

        (* We prove that after job j completes, it remains completed. *)
        Lemma completion_monotonic:
           t t',
            t t'
            completed_by job_cost sched j t
            completed_by job_cost sched j t'.

        (* We also prove that a completed job cannot be scheduled. *)
        Lemma completed_implies_not_scheduled :
            completed_by job_cost sched j t
            ~~ scheduled_at sched j t.

        (* Next, we show that 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.

      (* In this section we prove properties related to job arrivals. *)
      Section Arrival.

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

        (* Let j be any job that is to be scheduled. *)
        Variable j: Job.

        (* First, we show that job j does not receive service at any time t
           prior to its arrival. *)

        Lemma service_before_job_arrival_zero :
            t < job_arrival j
            service_at sched j t = 0.

        (* Note that the same property applies to the cumulative service. *)
        Lemma cumulative_service_before_job_arrival_zero :
           t1 t2,
            t2 job_arrival j
            \sum_(t1 i < t2) service_at sched j i = 0.

        (* Hence, one can ignore the service received by a job before its arrival time. *)
        Lemma ignore_service_before_arrival:
           t1 t2,
            t1 job_arrival j
            t2 job_arrival j
            \sum_(t1 t < t2) service_at sched j t =
              \sum_(job_arrival j t < t2) service_at sched j t.

      End Arrival.

      (* In this section, we prove properties about pending jobs. *)
      Section Pending.

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

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

        (* Let j be any job. *)
        Variable j: Job.

        (* First, we show that if job j is scheduled, then it must be pending. *)
        Lemma scheduled_implies_pending:
            scheduled_at sched j t
            pending job_arrival job_cost sched j t.

      End Pending.

      (* In this section we show that the schedule is unique at any point. *)
      Section OnlyOneJobScheduled.

        (* Let j1 and j2 be any jobs. *)
        Variable j1 j2: Job.

        (* At any time t, if both j1 and j2 are scheduled, then they must be the same job. *)
        Lemma only_one_job_scheduled:
            scheduled_at sched j1 t
            scheduled_at sched j2 t
            j1 = j2.

      End OnlyOneJobScheduled.

      Section ServiceIsAStepFunction.

        (* First, we show that the service received by any job j
           is a step function. *)

        Lemma service_is_a_step_function:
            is_step_function (service sched j).

        (* Next, consider any job j at any time t... *)
        Variable j: Job.
        Variable t: time.

        (* ...and let s0 be any value less than the service received
           by job j by time t. *)

        Variable s0: time.
        Hypothesis H_less_than_s: s0 < service sched j t.

        (* Then, we show that there exists an earlier time t0 where
           job j had s0 units of service. *)

        Corollary exists_intermediate_service:
            t0 < t
            service sched j t0 = s0.

      End ServiceIsAStepFunction.

      Section ScheduledAtEarlierTime.

        (* Next, we show that if the service is positive,
           then the job is scheduled at some earlier time. *)

        Lemma scheduled_at_earlier_time:
           j t,
            service sched j t > 0
              t0 < t
              scheduled_at sched j t0.

      End ScheduledAtEarlierTime.

      Section ServiceNotZero.

        (* Let j be any job. *)
        Variable j: Job.

        (* Assume that the service received by j during [t1, t2) is not zero. *)
        Variable t1 t2: time.
        Hypothesis H_service_not_zero: service_during sched j t1 t2 > 0.

        (* Then, there must be a time t where job j is scheduled. *)
        Lemma cumulative_service_implies_scheduled :
            t1 t < t2
            scheduled_at sched j t.

      End ServiceNotZero.

      (* In this section, we prove some lemmas about time instants
         with same service. *)

      Section TimesWithSameService.

        (* Let j be any job. *)
        Variable j: Job.

        (* Consider any time instants t1 and t2... *)
        Variable t1 t2: time.

        (* ...where job j has received the same amount of service. *)
        Hypothesis H_same_service: service sched j t1 = service sched j t2.

        (* First, we show that job j is scheduled at some point t < t1 iff
           j is scheduled at some point t' < t2.  *)

        Lemma same_service_implies_scheduled_at_earlier_times:
          [ t: 'I_t1, scheduled_at sched j t] =
            [ t': 'I_t2, scheduled_at sched j t'].

      End TimesWithSameService.

    End Lemmas.

  End Schedule.

End UniprocessorSchedule.