Library prosa.classic.implementation.global.jitter.schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.jitter.arrival_sequence prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.jitter.schedule
               prosa.classic.model.schedule.global.jitter.platform.
Require Import prosa.classic.model.schedule.global.transformation.construction.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.

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.
    Proof.
      intros sched1 sched2 cpu t ALL.
      rewrite /nth_highest_priority_job.
      suff SAME: sorted_pending_jobs sched1 t = sorted_pending_jobs sched2 t by rewrite SAME.
      rewrite /sorted_pending_jobs; f_equal.
      apply eq_in_filter.
      intros j ARR.
      rewrite /pending; do 2 f_equal.
      rewrite /completed; f_equal.
      apply eq_big_nat; movei /= LTi.
      rewrite /service_at /scheduled_on; apply eq_bigl; movecpu'.
      by rewrite ALL.
    Qed.

    (* ...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.
    Proof.
      by ins; apply prefix_dependent_schedule_construction,
                    scheduler_depends_only_on_prefix.
    Qed.

  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.
      Proof.
        intros t cpu.
        by rewrite /sched scheduler_uses_construction_function.
      Qed.

      (* 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
           i,
            nth_or_none (sorted_jobs t) i = Some j i num_cpus.
      Proof.
        intros j t ARRj BACK.
        move: BACK ⇒ /andP [PENDING /negP NOTCOMP].
        assert (IN: j \in sorted_jobs t).
        {
          rewrite mem_sort mem_filter PENDING andTb.
          move: PENDING ⇒ /andP [ARRIVED _].
          try ( by apply arrived_between_implies_in_actual_arrivals with (job_arrival0 := job_arrival) ) ||
          by apply arrived_between_implies_in_actual_arrivals with (job_arrival := job_arrival).
        }
        apply nth_or_none_mem_exists in IN; des.
         n; split; first by done.
        rewrite leqNgt; apply/negP; red; intro LT.
        apply NOTCOMP; clear NOTCOMP PENDING.
        apply/existsP; (Ordinal LT); apply/eqP.
        by rewrite scheduler_nth_or_none_mapping.
      Qed.

    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.
      Proof.
        movej t /existsP [cpu /eqP SCHED].
        rewrite scheduler_nth_or_none_mapping in SCHED.
        apply nth_or_none_mem in SCHED.
        rewrite mem_sort mem_filter in SCHED.
        move: SCHED ⇒ /andP [_ ARR].
        rewrite /actual_arrivals_up_to in ARR.
        by eapply in_actual_arrivals_between_implies_arrived; eauto 1.
      Qed.

    (* 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.
    Proof.
      movej t /existsP [cpu /eqP SCHED].
      rewrite scheduler_nth_or_none_mapping in SCHED.
      apply nth_or_none_mem in SCHED.
      rewrite mem_sort mem_filter in SCHED.
      by move: SCHED ⇒ /andP [/andP [ARR _] _].
    Qed.

    (* ...jobs are sequential, ... *)
    Theorem scheduler_sequential_jobs: sequential_jobs sched.
    Proof.
      intros j t cpu1 cpu2 SCHED1 SCHED2.
      rewrite 2!scheduler_nth_or_none_mapping in SCHED1 SCHED2.
      set l := sorted_pending_jobs _ _ _ _ _ _ _ _ in SCHED1 SCHED2.
      try ( apply ord_inj, nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
      apply ord_inj, nth_or_none_uniq with (l := l) (x := j); try (by done).
      by rewrite sort_uniq filter_uniq // /actual_arrivals_up_to; apply actual_arrivals_uniq.
    Qed.

    (* ... and jobs do not execute after completion. *)
    Theorem scheduler_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.
    Proof.
      intros j t.
      induction t;
        first by rewrite /service /service_during big_geq //.
      rewrite /service /service_during big_nat_recr //=.
      rewrite leq_eqVlt in IHt; move: IHt ⇒ /orP [/eqP EQ | LT]; last first.
      {
        apply: leq_trans LT; rewrite -addn1.
        apply leq_add; first by done.
        rewrite /service_at.
        case (boolP ([ cpu, scheduled_on sched j cpu t])) ⇒ [EX | ALL]; last first.
        {
          rewrite negb_exists in ALL; move: ALL ⇒ /forallP ALL.
          rewrite big1 //; intros cpu SCHED.
          by specialize (ALL cpu); rewrite SCHED in ALL.
        }
        move: EX ⇒ /existsP [cpu SCHED].
        rewrite (bigD1 cpu) /=; last by done.
        rewrite big1; first by rewrite addn0.
        movecpu' /andP [SCHED' NEQ].
        move: NEQ ⇒ /eqP NEQ; exfalso; apply NEQ, ord_inj.
        move: SCHED SCHED' ⇒ /eqP SCHED /eqP SCHED'.
        rewrite 2!scheduler_nth_or_none_mapping in SCHED SCHED'.
        set l := sorted_pending_jobs _ _ _ _ _ _ _ _ in SCHED SCHED'.
        try ( apply nth_or_none_uniq with (l0 := l) (x := j); try (by done) ) ||
        apply nth_or_none_uniq with (l := l) (x := j); try (by done).
        by rewrite sort_uniq filter_uniq //; apply actual_arrivals_uniq.
      }
      rewrite -[job_cost _]addn0; apply leq_add; first by rewrite -EQ.
      rewrite leqn0 /service_at big1 // /scheduled_on.
      movecpu /eqP SCHED.
      rewrite scheduler_nth_or_none_mapping in SCHED.
      apply nth_or_none_mem in SCHED.
      rewrite mem_sort mem_filter in SCHED.
      move: SCHED ⇒ /andP [/andP [_ NOTCOMP] _].
      by rewrite /completed EQ leqnn in NOTCOMP.
    Qed.

    (* In addition, the scheduler is (jitter-aware) work conserving, ... *)
    Theorem scheduler_work_conserving:
      work_conserving job_arrival job_cost job_jitter arr_seq sched.
    Proof.
      intros j t ARRj BACK cpu.
      set jobs := sorted_pending_jobs job_arrival job_cost job_jitter num_cpus
                                      arr_seq higher_eq_priority sched t.
      destruct (sched cpu t) as [j0 |] eqn:SCHED; first by j0; apply/eqP.
      apply scheduler_nth_or_none_backlogged in BACK; last by done.
      destruct BACK as [cpu_out [NTH GE]].
      exfalso; rewrite leqNgt in GE; move: GE ⇒ /negP GE; apply GE.
      apply leq_ltn_trans with (n := cpu); last by done.
      rewrite scheduler_nth_or_none_mapping in SCHED.
      apply nth_or_none_size_none in SCHED.
      apply leq_trans with (n := size jobs); last by done.
      by apply nth_or_none_size_some in NTH; apply ltnW.
    Qed.

    (* ...and respects the JLDP policy. *)
    Theorem scheduler_respects_policy :
      respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.
    Proof.
      movej j_hp t ARRj BACK /existsP [cpu /eqP SCHED].
      apply scheduler_nth_or_none_backlogged in BACK; last by done.
      set jobs := sorted_pending_jobs _ _ _ _ _ _ _ _ in BACK.
      destruct BACK as [cpu_out [SOME GE]].
      rewrite scheduler_nth_or_none_mapping in SCHED.
      have EQ1 := nth_or_none_nth jobs cpu j_hp j SCHED.
      have EQ2 := nth_or_none_nth jobs cpu_out j j SOME.
      rewrite -EQ1 -{2}EQ2.
      apply sorted_lt_idx_implies_rel; try (by done); last 2 first.
      - by apply leq_trans with (n := num_cpus).
      - by apply nth_or_none_size_some in SOME.
      - by apply sort_sorted, H_priority_total.
    Qed.

  End Proofs.

End ConcreteScheduler.