Library rt.model.schedule.uni.susp.last_execution

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

(* In this file, we show how to compute the time instant after the last
   execution of a job and prove several lemmas about that instant. This
   notion is crucial for defining suspension intervals. *)

Module LastExecution.

  Export Job UniprocessorSchedule.

  (* In this section we define the time after the last execution of a job (if exists). *)
  Section TimeAfterLastExecution.

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

    (* Consider any uniprocessor schedule. *)
    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.

    Section Defs.

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

      (* Next, we will show how to find the time after the most recent
         execution of a given job j in the interval [job_arrival j, t).
         (Note that this instant can be time t itself.) *)

      Variable t: time.

      (* Let scheduled_before denote whether job j was scheduled in the interval [0, t). *)
      Let scheduled_before :=
        [ t0: 'I_t, job_scheduled_at j t0].

      (* In case j was scheduled before, we define the last time in which j was scheduled. *)
      Let last_time_scheduled :=
        \max_(t_last < t | job_scheduled_at j t_last) t_last.

      (* Then, the time after the last execution of job j in the interval [0, t), if exists,
         occurs:
           (a) immediately after the last time in which job j was scheduled, or,
           (b) if j was never scheduled, at the arrival time of j. *)

      Definition time_after_last_execution :=
        if scheduled_before then
          last_time_scheduled + 1
        else job_arrival j.

    End Defs.

    (* Next, we prove lemmas about the time after the last execution. *)
    Section Lemmas.

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

      (* In this section, we show that the time after the last execution occurs
           no earlier than the arrival of the job. *)

      Section JobHasArrived.

        (* Then, the time following the last execution of job j in the
             interval [0, t) occurs no earlier than the arrival of j. *)

        Lemma last_execution_after_arrival:
           t,
            has_arrived job_arrival j (time_after_last_execution j t).

      End JobHasArrived.

      (* Next, we establish the monotonicity of the function. *)
      Section Monotonicity.

        (* Let t1 be any time no earlier than the arrival of job j. *)
        Variable t1: time.
        Hypothesis H_after_arrival: has_arrived job_arrival j t1.

        (* Then, (time_after_last_execution j) grows monotonically
             after that point. *)

        Lemma last_execution_monotonic:
           t2,
            t1 t2
            time_after_last_execution j t1 time_after_last_execution j t2.

      End Monotonicity.

      (* Next, we prove that the function is idempotent. *)
      Section Idempotence.

        (* The time after the last execution of job j is an idempotent function. *)
        Lemma last_execution_idempotent:
           t,
            time_after_last_execution j (time_after_last_execution j t)
            = time_after_last_execution j t.

      End Idempotence.

      (* Next, we show that time_after_last_execution is bounded by the identity function. *)
      Section BoundedByIdentity.

        (* Let t be any time no earlier than the arrival of j. *)
        Variable t: time.
        Hypothesis H_after_arrival: has_arrived job_arrival j t.

        (* Then, the time following the last execution of job j in the interval [0, t)
           occurs no later than time t. *)

        Lemma last_execution_bounded_by_identity:
          time_after_last_execution j t t.

      End BoundedByIdentity.

      (* In this section, we show that if the service received by a job
           remains the same, the time after last execution also doesn't change. *)

      Section SameLastExecution.

        (* Consider any time instants t and t'... *)
        Variable t t': time.

        (* ...in which job j has received the same amount of service. *)
        Hypothesis H_same_service: service sched j t = service sched j t'.

        (* Then, we prove that the times after last execution relative to
             instants t and t' are exactly the same. *)

        Lemma same_service_implies_same_last_execution:
          time_after_last_execution j t = time_after_last_execution j t'.

      End SameLastExecution.

      (* In this section, we show that the service received by a job
         does not change since the last execution. *)

      Section SameService.

        (* We prove that, for any time t, the service received by job j
           before (time_after_last_execution j t) is the same as the service
           by j before time t. *)

        Lemma same_service_since_last_execution:
           t,
            service sched j (time_after_last_execution j t) = service sched j t.

      End SameService.

      (* In this section, we show that for any smaller value of service, we can
         always find the last execution that corresponds to that service. *)

      Section ExistsIntermediateExecution.

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

        (* Then, for any value of service less than the cost of j, ...*)
        Variable s: time.
        Hypothesis H_less_than_cost: s < job_cost j.

        (* ...there exists a last execution where the service received
           by job j equals s. *)

        Lemma exists_last_execution_with_smaller_service:
           t0,
            service sched j (time_after_last_execution j t0) = s.

      End ExistsIntermediateExecution.

      (* In this section we prove that before the last execution the job
         must have received strictly less service. *)

      Section LessServiceBeforeLastExecution.

        (* Let t be any time... *)
        Variable t: time.

        (* ...and consider any earlier time t0 no earlier than the arrival of job j... *)
        Variable t0: time.
        Hypothesis H_no_earlier_than_arrival: has_arrived job_arrival j t0.

        (* ...and before the last execution of job j (with respect to time t). *)
        Hypothesis H_before_last_execution: t0 < time_after_last_execution j t.

        (* Then, we can prove that the service received by j before time t0
           is strictly less than the service received by j before time t. *)

        Lemma less_service_before_start_of_suspension:
          service sched j t0 < service sched j t.

      End LessServiceBeforeLastExecution.

    End Lemmas.

  End TimeAfterLastExecution.

End LastExecution.