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.

    Variable sched: schedule Job.

    Let job_completed_by := completed_by job_cost sched.
    Let job_remaining_cost j t := remaining_cost job_cost sched j t.

    Definition is_nonpreemptive_schedule :=
      ∀ j t t',
        t ≤ t' →
        scheduled_at sched j t →
        ~~ job_completed_by j t' →
        scheduled_at sched j t'.

    Section Lemmas.

      Hypothesis H_nonpreemptive: is_nonpreemptive_schedule.

      Section BasicLemmas.

        Variable j: Job.

        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        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.

        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.

      Section CompletionUnderNonpreemptive.

        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        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.

      Section ExecutionInterval.

        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        Variable j: Job.
        Variable t: time.
        Hypothesis H_j_is_scheduled_at_t: scheduled_at sched j t.

        Section LeftBound.

          Lemma j_is_scheduled_at_t_minus_service:
            scheduled_at sched j (t - service sched j t).

          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).

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

        End LeftBound.

        Section RightBound.

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

          Lemma j_is_not_scheduled_after_t_plus_remaining_cost_minus_one:
            ∀ t',
              t + job_remaining_cost j t ≤ t' →
              ~~ scheduled_at sched j t'.

        End RightBound.

        Lemma nonpreemptive_executing_interval:
          ∀ t',
            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.