Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task_arrival
               prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
               prosa.classic.model.schedule.uni.schedule.
Require Import prosa.classic.model.schedule.uni.limited.platform.definitions
               prosa.classic.model.schedule.uni.limited.busy_interval.

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

Module PriorityInversionIsBounded.

  Import Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP.

  Section PriorityInversionIsBounded.

    Context {Task: eqType}.
    Variable task_max_nps task_cost: Task → time.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_max_nps job_cost: Job → time.
    Variable job_task: Job → Task.

    (* Consider any arrival sequence. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.

    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.

    (* ... where jobs do not execute before their arrival nor after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    (* Consider a JLFP policy that indicates a higher-or-equal priority relation,
       and assume that the relation is reflexive and transitive. *)
    Variable higher_eq_priority: JLFP_policy Job.
    Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.

    (* We consider an arbitrary function can_be_preempted which defines 
       a preemption model with bounded nonpreemptive segments. *)
    Variable can_be_preempted: Job → time → bool.
    Let preemption_time := preemption_time sched can_be_preempted.
    Hypothesis H_correct_preemption_model:
      correct_preemption_model arr_seq sched can_be_preempted.
    Hypothesis H_model_with_bounded_nonpreemptive_segments:
      model_with_bounded_nonpreemptive_segments
        job_cost job_task arr_seq can_be_preempted job_max_nps task_max_nps.

    (* Next, we assume that the schedule is a work-conserving schedule... *)
    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.

    (* ... and the schedule respects the policy defined by the 
       can_be_preempted function (i.e., bounded nonpreemptive segments). *)
    Hypothesis H_respects_policy:
      respects_JLFP_policy_at_preemption_point
        job_arrival job_cost arr_seq sched can_be_preempted higher_eq_priority.

    (* Let's define some local names for clarity. *)
    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.

    (* Finally, we introduce the notion of the maximal length of (potential) priority 
       inversion at a time instant t, which is defined as the maximum length of 
       nonpreemptive segments among all jobs that arrived so far. *)
    Definition max_length_of_priority_inversion (j: Job) (t: time) :=
      \max_(j_lp <- jobs_arrived_before arr_seq t | ~~ higher_eq_priority j_lp j)
       (job_max_nps j_lp - ε).

    (* Consider any job j of tsk with positive job cost. *)
    Variable j: Job.
    Hypothesis H_j_arrives: arrives_in arr_seq j.
    Hypothesis H_job_cost_positive: job_cost_positive job_cost j.

    (* Consider any busy interval prefix t1, t2) of job j. *)
    Variable t1 t2: time.
    Hypothesis H_busy_interval_prefix:
      busy_interval_prefix job_arrival job_cost arr_seq sched higher_eq_priority j t1 t2.

    (* In this section, we prove that at any time instant after any preemption point
       (inside the busy interval), the processor is always busy scheduling a 
       job with higher or equal priority. *)
    Section PreemptionTimeAndPriorityInversion.

      (* First, we show that the processor at any preemptive point is always 
         busy scheduling a job with higher or equal priority. *)
      Lemma not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
        ∀ t,
          t1 ≤ t < t2 →
          preemption_time t →
          ∃ j_hp,
            arrived_between job_arrival j_hp t1 t2 ∧
            higher_eq_priority j_hp j ∧
            job_scheduled_at j_hp t.

      (* In addition, we prove that every nonpreemptive segment 
         always begins with a preemption time. *)
      Lemma scheduling_of_any_segment_starts_with_preemption_time:
        ∀ j t,
          job_scheduled_at j t →
          ∃ pt,
            job_arrival j ≤ pt ≤ t ∧
            preemption_time pt ∧
            (∀ t', pt ≤ t' ≤ t → job_scheduled_at j t').

      (* Next we prove that at any time instant after a preemption point the
         processor is always busy with a job with higher or equal priority. *)
      Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
        ∀ tp t,
          preemption_time tp →
          t1 ≤ tp < t2 →
          tp ≤ t < t2 →
          ∃ j_hp,
            arrived_between job_arrival j_hp t1 t.+1 ∧
            higher_eq_priority j_hp j ∧
            job_scheduled_at j_hp t.

      (* Now, suppose there exists some constant K that bounds the distance to 
         a preemption time from the beginning of the busy interval. *)
      Variable K: time.
      Hypothesis H_preemption_time_exists:
        ∃ pr_t, preemption_time pr_t ∧ t1 ≤ pr_t ≤ t1 + K.

      (* Then we prove that the processor is always busy with a job with 
         higher-or-equal priority after time instant t1 + K. *)
      Lemma not_quiet_implies_exists_scheduled_hp_job:
        ∀ t,
          t1 + K ≤ t < t2 →
          ∃ j_hp,
            arrived_between job_arrival j_hp t1 t.+1 ∧
            higher_eq_priority j_hp j ∧
            job_scheduled_at j_hp t.

    End PreemptionTimeAndPriorityInversion.

    (* In this section we prove that the function max_length_of_priority_inversion 
       indeed upper bounds the priority inversion length. *)
    Section PreemprionTimeExists.

      (* First we prove that if a job with higher-or-equal priority is scheduled at 
         a quiet time t+1 then this is the first time when this job is scheduled. *)
      Lemma hp_job_not_scheduled_before_quiet_time:
        ∀ jhp t,
          quiet_time job_arrival job_cost arr_seq sched higher_eq_priority j t.+1 →
          job_scheduled_at jhp t.+1 →
          higher_eq_priority jhp j →
          ~~ job_scheduled_at jhp t.

      (* Also, we show that lower-priority jobs that are scheduled inside the
         busy-interval prefix t1,t2) must have arrived before that interval. *)
      Lemma low_priority_job_arrives_before_busy_interval_prefix:
        ∀ jlp t,
          t1 ≤ t < t2 →
          job_scheduled_at jlp t →
          ~~ higher_eq_priority jlp j →
          job_arrival jlp < t1.

      (* Moreover, we show that lower-priority jobs that are scheduled inside the
         busy-interval prefix t1,t2) must be scheduled before that interval. *)
      Lemma low_priority_job_scheduled_before_busy_interval_prefix:
        ∀ jlp t,
          t1 ≤ t < t2 →
          job_scheduled_at jlp t →
          ~~ higher_eq_priority jlp j →
          ∃ t', t' < t1 ∧ job_scheduled_at jlp t'.

      (* Thus, there must be a preemption time in the interval t1, t1 + max_priority_inversion t1. 
         That is, if a job with higher-or-equal priority is scheduled at time instant t1, then t1 is 
         a preemprion time. Otherwise, if a job with lower priority is scheduled at time t1, 
         then this jobs also should be scheduled before the beginning of the busy interval. So, the 
         next preemption time will be no more than max_priority_inversion t1 time units later. *)
      Lemma preemption_time_exists:
        ∃ pr_t,
          preemption_time pr_t ∧
          t1 ≤ pr_t ≤ t1 + max_length_of_priority_inversion j t1.

    End PreemprionTimeExists.

  End PriorityInversionIsBounded.

End PriorityInversionIsBounded.