Library rt.model.schedule.uni.jitter.schedule

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

(* In this file, we prove additional definitions and lemmas about jitter-aware schedules. *)
Module UniprocessorScheduleWithJitter.

  (* To formalize jitter, we import the original uniprocessor schedule and
     redefine some of the properties. *)

  Export ArrivalSequenceWithJitter UniprocessorSchedule.

  (* In this section we redefine properties that depend on the arrival time. *)
  Section RedefiningProperties.

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

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

    (* First, we redefine some job properties. *)
    Section JobProperties.

      (* Let j be any job in the arrival sequence. *)
      Variable j: Job.

      (* Then, we say that job j is pending at time t iff the jitter has passed but
         j has not completed by time t. *)

      Definition pending (t: time) :=
        jitter_has_passed job_arrival job_jitter j t && ~~ completed_by job_cost sched j t.

      (* Finally, we say that job j is backlogged at time t iff it is pending and not scheduled. *)
      Definition backlogged (t: time) :=
        pending t && ~~ scheduled_at sched j t.

    End JobProperties.

    (* Next, we define properties of a valid jitter-aware schedule. *)
    Section ValidSchedules.

      (* In any jitter-aware schedule, a job can only be scheduled after
         the jitter has passed. *)

      Definition jobs_execute_after_jitter :=
         j t,
          scheduled_at sched j t jitter_has_passed job_arrival job_jitter j t.

    End ValidSchedules.

    (* In this section, we prove some basic lemmas about jitter-aware schedules. *)
    Section Lemmas.

      (* For simplicity, let's define some local names. *)
      Let has_actually_arrived := jitter_has_passed job_arrival job_jitter.
      Let actual_job_arrival := actual_arrival job_arrival job_jitter.

      (* We begin by proving properties related to job arrivals. *)
      Section Arrival.

        (* Assume that jobs only execute after the jitter has passed. *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* First, we show that every job in the schedule only executes after its arrival time. *)
        Lemma jobs_with_jitter_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* Now, let j be any job. *)
        Variable j: Job.

        (* First, we show that if the jitter has passed, then the job must have arrived. *)
        Lemma jitter_has_passed_implies_arrived:
           t,
            has_actually_arrived j t
            has_arrived job_arrival j t.

        (* Now we prove that job j does not receive service at any time t before
           its actual arrival time. *)

        Lemma service_before_jitter_is_zero :
           t,
            t < actual_job_arrival j
            service_at sched j t = 0.

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

        (* Hence, one can ignore the service received by a job before the jitter. *)
        Lemma ignore_service_before_jitter:
           t1 t2,
            t1 actual_job_arrival j t2
            \sum_(t1 t < t2) service_at sched j t =
            \sum_(actual_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 only execute after the jitter has passed... *)
        Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter.

        (* ...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:
           t,
            scheduled_at sched j t pending j t.

      End Pending.

    End Lemmas.

  End RedefiningProperties.

End UniprocessorScheduleWithJitter.