Library rt.model.schedule.uni.susp.suspension_intervals

Require Import rt.util.all.
Require Import rt.model.suspension.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.arrival_sequence.
Require Import rt.model.schedule.uni.schedule.
Require Import rt.model.schedule.uni.susp.last_execution.

Module SuspensionIntervals.

  Export Job UniprocessorSchedule Suspension LastExecution.

  (* In this section we define job suspension intervals in a schedule. *)
  Section DefiningSuspensionIntervals.

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

    (* Consider any job suspension times... *)
    Variable next_suspension: job_suspension Job.

    (* ...and any uniprocessor schedule. *)
    (*Context {arr_seq: arrival_sequence Job}.*)
    Variable sched: schedule Job.

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

    (* Based on the time after the last execution of a job, we define next
       whether a job is suspended. *)

    Section JobSuspension.

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

      Section DefiningSuspension.

        (* We are going to define whether job j is suspended at time t. *)
        Variable t: time.

        (* First, we define the beginning of the latest self suspension as the
           time following the last execution of job j in the interval [0, t).
           (Note that suspension_start can return time t itself.) *)

        Let suspension_start := time_after_last_execution job_arrival sched j t.

        (* Next, using the service received by j in the interval [0, suspension_start),...*)
        Let current_service := service sched j suspension_start.

        (* ... we recall the duration of the suspension expected for job j after having
           received that amount of service. *)

        Definition suspension_duration := next_suspension j current_service.

        (* Then, we say that job j is suspended at time t iff j has not completed
           by time t and t lies in the latest suspension interval.
           (Also note that the suspension interval can have duration 0, in which
            case suspended_at will be trivially false.)                         *)

        Definition suspended_at :=
          ~~ completed_by job_cost sched j t &&
          (suspension_start t < suspension_start + suspension_duration).

      End DefiningSuspension.

      (* Based on the notion of suspension, we also define the cumulative
         suspension time of job j in any interval [t1, t2)... *)

      Definition cumulative_suspension_during (t1 t2: time) :=
        \sum_(t1 t < t2) (suspended_at t).

      (* ...and the cumulative suspension time in any interval [0, t). *)
      Definition cumulative_suspension (t: time) := cumulative_suspension_during 0 t.

    End JobSuspension.

    (* Next, we define whether the schedule respects self-suspensions. *)
    Section SuspensionAwareSchedule.

      (* We say that the schedule respects self-suspensions iff suspended
         jobs are never scheduled. *)

      Definition respects_self_suspensions :=
         j t,
          job_scheduled_at j t ¬ suspended_at j t.

    End SuspensionAwareSchedule.

    (* In this section, we prove several results related to job suspensions. *)
    Section Lemmas.

      (* First, we prove that at any time within any suspension interval, 
         a job is always suspended. *)

      Section InsideSuspensionInterval.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

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

        (* Consider any time t after the arrival of j... *)
        Variable t: time.
        Hypothesis H_has_arrived: has_arrived job_arrival j t.

        (* ...and recall the latest suspension interval of job j relative to time t. *)
        Let suspension_start := time_after_last_execution job_arrival sched j t.
        Let duration := suspension_duration j t.

        (* First, we analyze the service received during a suspension interval. *)
        Section SameService.

          (* Let t_in be any time in the suspension interval relative to time t. *)
          Variable t_in: time.
          Hypothesis H_within_suspension_interval:
            suspension_start t_in suspension_start + duration.

          (* Then, we show that the service received before time t_in
             equals the service received before the beginning of the
             latest suspension interval (if exists). *)

          Lemma same_service_in_suspension_interval:
            service sched j t_in = service sched j suspension_start.

        End SameService.

        (* Next, we infer that the job is suspended at all times during
           the suspension interval. *)

        Section JobSuspendedAtAllTimes.

          (* Let t_in be any time before the completion of job j. *)
          Variable t_in: time.
          Hypothesis H_not_completed: ~~ job_completed_by j t_in.

          (* If t_in lies in the suspension interval relative to time t, ...*)
          Hypothesis H_within_suspension_interval:
            suspension_start t_in < suspension_start + duration.

          (* ...then job j is suspended at time t_in. More precisely, the suspension
             interval relative to time t_in is included in the suspension interval
             relative to time t. *)

          Lemma suspended_in_suspension_interval:
            suspended_at j t_in.

        End JobSuspendedAtAllTimes.

      End InsideSuspensionInterval.

      (* Next, we prove lemmas about the state of a suspended job. *)
      Section StateOfSuspendedJob.

        (* Assume that jobs do not execute before they arrived. *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

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

        (* Assume that j is suspended at time t. *)
        Variable t: time.
        Hypothesis H_j_is_suspended: suspended_at j t.

        (* First, we show that j must have arrived by time t. *)
        Lemma suspended_implies_arrived: has_arrived job_arrival j t.

        (* By the definition of suspension, it also follows that j cannot
           have completed by time t. *)

        Corollary suspended_implies_not_completed:
          ~~ completed_by job_cost sched j t.

      End StateOfSuspendedJob.

      (* Next, we establish a bound on the cumulative suspension time of any job. *)
      Section BoundOnCumulativeSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

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

        (* Recall the total suspension of job j as given by the dynamic suspension model. *)
        Let cumulative_suspension_of_j :=
          cumulative_suspension_during j.
        Let total_suspension_of_j :=
          total_suspension job_cost next_suspension j.

        (* We prove that the cumulative suspension time of job j in any
           interval is upper-bounded by the total suspension time. *)

        Lemma cumulative_suspension_le_total_suspension:
           t1 t2,
            cumulative_suspension_of_j t1 t2 total_suspension_of_j.

      End BoundOnCumulativeSuspension.

      (* Next, we show that when a job completes, it must have suspended
         as long as the total suspension time. *)

      Section SuspendsForTotalSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

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

        (* Assume that j has completed by time t. *)
        Variable t: time.
        Hypothesis H_j_has_completed: completed_by job_cost sched j t.

        (* Then, we prove that the cumulative suspension time must be
           exactly equal to the total suspension time of the job. *)

        Lemma cumulative_suspension_eq_total_suspension:
          cumulative_suspension j t = total_suspension job_cost next_suspension j.

      End SuspendsForTotalSuspension.

      (* In this section, we prove that a job executes just before it starts suspending.  *)
      Section ExecutionBeforeSuspension.

        (* Assume that jobs do not execute before they arrive... *)
        Hypothesis H_jobs_must_arrive_to_execute:
          jobs_must_arrive_to_execute job_arrival sched.

        (* ...and nor after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule respects self-suspensions. *)
        Hypothesis H_respects_self_suspensions: respects_self_suspensions.

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

        (* ...that has arrived by some time t. *)
        Variable t: time.
        Hypothesis H_arrived: has_arrived job_arrival j t.

        (* If job j is not suspended at time t, but starts to suspend at time t + 1, ... *)
        Hypothesis H_not_suspended_at_t: ~~ suspended_at j t.
        Hypothesis H_begins_suspension: suspended_at j t.+1.

        (* ...then j must be scheduled at time t. *)
        Lemma executes_before_suspension:
          scheduled_at sched j t.

      End ExecutionBeforeSuspension.

    End Lemmas.

  End DefiningSuspensionIntervals.

End SuspensionIntervals.