Require Import rt.util.all.
Require Import rt.model.arrival.jitter.arrival_sequence rt.model.priority.
Require Import
Require Import

Module ConcreteScheduler.

  Import ArrivalSequenceWithJitter ScheduleWithJitter Platform Priority ScheduleConstruction.

  Section Implementation.

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

    (* Let num_cpus denote the number of processors, ...*)
    Variable num_cpus: nat.

    (* ...and let arr_seq be any job arrival sequence.*)
    Variable arr_seq: arrival_sequence Job.

    (* Assume a JLDP policy is given. *)
    Variable higher_eq_priority: JLDP_policy Job.

    (* Next, we show how to recursively construct the schedule. *)
    Section ScheduleConstruction.

      (* For any time t, suppose that we have generated the schedule prefix in the
         interval [0, t). Then, we must define what should be scheduled at time t. *)

      Variable sched_prefix: schedule Job num_cpus.
      Variable cpu: processor num_cpus.
      Variable t: time.

      (* For simplicity, let's use some local names. *)
      Let is_pending := pending job_arrival job_cost job_jitter sched_prefix.
      Let actual_arrivals := actual_arrivals_up_to job_arrival job_jitter arr_seq.

      (* Consider the list of pending jobs at time t, ... *)
      Definition pending_jobs :=
        [seq j <- actual_arrivals t | is_pending j t].

      (* ...which we sort by priority. *)
      Definition sorted_pending_jobs :=
        sort (higher_eq_priority t) pending_jobs.

      (* Then, we take the n-th highest-priority job from the list. *)
      Definition nth_highest_priority_job :=
        nth_or_none sorted_pending_jobs cpu.

    End ScheduleConstruction.

    (* Starting from the empty schedule, the final schedule is obtained by iteratively
       picking the highest-priority job. *)

    Let empty_schedule : schedule Job num_cpus := fun cpu tNone.
    Definition scheduler :=
      build_schedule_from_prefixes num_cpus nth_highest_priority_job empty_schedule.

    (* Then, by showing that the construction function depends only on the prefix, ... *)
    Lemma scheduler_depends_only_on_prefix:
       sched1 sched2 cpu t,
        ( t0 cpu0, t0 < t sched1 cpu0 t0 = sched2 cpu0 t0)
        nth_highest_priority_job sched1 cpu t = nth_highest_priority_job sched2 cpu t.

    (* ...we infer that the generated schedule is indeed based on the construction function. *)
    Corollary scheduler_uses_construction_function:
       t cpu, scheduler cpu t = nth_highest_priority_job scheduler cpu t.

  End Implementation.

  Section Proofs.

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

    (* Assume a positive number of processors. *)
    Variable num_cpus: nat.
    Hypothesis H_at_least_one_cpu: num_cpus > 0.

    (* Let arr_seq be any job arrival sequence with consistent, duplicate-free arrivals. *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arrival_sequence_is_a_set: arrival_sequence_is_a_set arr_seq.

    (* Consider any JLDP policy higher_eq_priority that is transitive and total. *)
    Variable higher_eq_priority: JLDP_policy Job.
    Hypothesis H_priority_transitive: JLDP_is_transitive higher_eq_priority.
    Hypothesis H_priority_total: t, total (higher_eq_priority t).

    (* Let sched denote our concrete scheduler implementation. *)
    Let sched := scheduler job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority.

    (* Next, we provide some helper lemmas about the scheduler construction. *)
    Section HelperLemmas.

      Let sorted_jobs :=
        sorted_pending_jobs job_arrival job_cost job_jitter num_cpus arr_seq higher_eq_priority sched.

      (* First, we recall that the schedule picks the nth highest-priority job. *)
      Corollary scheduler_nth_or_none_mapping :
         t cpu,
          sched cpu t = nth_or_none (sorted_jobs t) cpu.

      (* We also prove that a backlogged job has priority larger than or equal to the number
         of processors. *)

      Lemma scheduler_nth_or_none_backlogged :
         j t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost job_jitter sched j t
            nth_or_none (sorted_jobs t) i = Some j i num_cpus.

    End HelperLemmas.

    (* Now, we prove the important properties about the implementation. *)

    (* First, we show that scheduled jobs come from the arrival sequence. *)
      Lemma scheduler_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched arr_seq.

    (* Next, we show that jobs do not execute before the jitter has passed...*)
    Theorem scheduler_jobs_execute_after_jitter:
      jobs_execute_after_jitter job_arrival job_jitter sched.

    (* are sequential, ... *)
    Theorem scheduler_sequential_jobs: sequential_jobs sched.

    (* ... and jobs do not execute after completion. *)
    Theorem scheduler_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* In addition, the scheduler is (jitter-aware) work conserving, ... *)
    Theorem scheduler_work_conserving:
      work_conserving job_arrival job_cost job_jitter arr_seq sched.

    (* ...and respects the JLDP policy. *)
    Theorem scheduler_respects_policy :
      respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.

  End Proofs.

End ConcreteScheduler.