Library prosa.classic.model.schedule.uni.nonpreemptive.schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job.
Require Import prosa.classic.model.schedule.uni.schedule.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module NonpreemptiveSchedule.

  Export UniprocessorSchedule.

  Section Definitions.

    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_completed_by := completed_by job_cost sched.
    Let job_remaining_cost j t := remaining_cost job_cost sched j t.

    (* We define schedule to be nonpreemptive iff every job remains scheduled until completion. *)
    Definition is_nonpreemptive_schedule :=
       j t t',
        t t'
        scheduled_at sched j t
        ~~ job_completed_by j t'
        scheduled_at sched j t'.

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

      (* Assume that we have a nonpreemptive schedule. *)
      Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.

      Section BasicLemmas.

        (* Consider any job j. *)
        Variable j: Job.

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

        (* First, we show that if j is scheduled at any two time instants, 
           then it is also scheduled at any time between them. *)

        Lemma continuity_of_nonpreemptive_scheduling:
           t t1 t2,
            t1 t t2
            scheduled_at sched j t1
            scheduled_at sched j t2
            scheduled_at sched j t.

        (* Next, we show that in any nonpreemptive schedule, once a job is scheduled, 
           it cannot be preempted until completion. *)

        Lemma in_nonpreemption_schedule_preemption_implies_completeness:
           t t' ,
            t t'
            scheduled_at sched j t
            ~~ scheduled_at sched j t'
            job_completed_by j t'.

      End BasicLemmas.

      (* In this section, we prove properties related to job completion. *)
      Section CompletionUnderNonpreemptive.

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

        (* If job j is scheduled at time t, then it must complete by (t + remaining_cost j t). *)
        Lemma job_completes_after_remaining_cost:
           j t,
            scheduled_at sched j t
            job_completed_by j (t + job_remaining_cost j t).

      End CompletionUnderNonpreemptive.

      (* In this section, we determine bounds on the length of the execution interval. *)
      Section ExecutionInterval.

        (* Assume that jobs do not execute after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Let j be any job scheduled at time t. *)
        Variable j: Job.
        Variable t: time.
        Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.

        (* Is this section we show that there is a bound for how early job j can start. *)
        Section LeftBound.

          (* We prove that job j is scheduled at time (t - service sched j t)... *)
          Lemma j_is_scheduled_at_t_minus_service:
            scheduled_at sched j (t - service sched j t).

          (* ... and it is not scheduled at time (t - service sched j t - 1). *)
          Lemma j_is_not_scheduled_at_t_minus_service_minus_one:
            t - service sched j t > 0
            ~~ scheduled_at sched j (t - service sched j t - 1).

          (* Using the previous lemma, we show that job j cannot be scheduled 
             before (t - service sched j t). *)

          Lemma j_is_not_scheduled_earlier_t_minus_service:
              t' < t - service sched j t
              ~~ scheduled_at sched j t'.

        End LeftBound.

        (* Is this section we prove that job j cannot be scheduled after (t + remaining_cost j t - 1). *)
        Section RightBound.

          (* We show that if job j is scheduled at time t, 
             then it is also scheduled at time (t + remaining_cost j t - 1)... *)

          Lemma j_is_scheduled_at_t_plus_remaining_cost_minus_one:
            scheduled_at sched j (t + job_remaining_cost j t - 1).

          (* ... and it is not scheduled after (t + remaining cost j t - 1). *)
          Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
              t + job_remaining_cost j t t'
              ~~ scheduled_at sched j t'.

        End RightBound.

        (* To conclude, we identify the interval where job j is scheduled. *)
        Lemma nonpreemptive_executing_interval:
            t - service sched j t t' < t + job_remaining_cost j t
            scheduled_at sched j t'.

      End ExecutionInterval.

    End Lemmas.

  End Definitions.

End NonpreemptiveSchedule.