Library prosa.classic.implementation.uni.susp.schedule

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

Module ConcreteScheduler.

  Import Job ArrivalSequence UniprocessorSchedule PlatformWithSuspensions Priority
         ScheduleConstruction.

  Section Implementation.

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

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.

    Variable next_suspension: job_suspension Job.

    Variable higher_eq_priority: JLDP_policy Job.

    Section ScheduleConstruction.

      Variable sched_prefix: schedule Job.
      Variable t: time.

      Let is_pending := pending job_arrival job_cost sched_prefix.
      Let is_suspended :=
        suspended_at job_arrival job_cost next_suspension sched_prefix.

      Definition pending_jobs :=
        [seq j <- jobs_arrived_up_to arr_seq t | is_pending j t && ~~ is_suspended j t].

      Definition highest_priority_job :=
        seq_min (higher_eq_priority t) pending_jobs.

    End ScheduleConstruction.

    Let empty_schedule : schedule Job := fun t ⇒ None.
    Definition scheduler :=
      build_schedule_from_prefixes highest_priority_job empty_schedule.

    Lemma scheduler_depends_only_on_prefix:
      ∀ sched1 sched2 t,
        (∀ t0, t0 < t → sched1 t0 = sched2 t0) →
        highest_priority_job sched1 t = highest_priority_job sched2 t.

    Corollary scheduler_uses_construction_function:
      ∀ t, scheduler t = highest_priority_job scheduler t.

  End Implementation.

  Section Proofs.

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

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_no_duplicate_arrivals: arrival_sequence_is_a_set arr_seq.

    Variable next_suspension: job_suspension Job.

    Variable higher_eq_priority: JLDP_policy Job.
    Hypothesis H_priority_is_transitive: JLDP_is_transitive higher_eq_priority.
    Hypothesis H_priority_is_total: JLDP_is_total arr_seq higher_eq_priority.

    Let sched := scheduler job_arrival job_cost arr_seq next_suspension higher_eq_priority.


      Lemma scheduler_jobs_come_from_arrival_sequence:
        jobs_come_from_arrival_sequence sched arr_seq.

    Theorem scheduler_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    Theorem scheduler_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    Theorem scheduler_work_conserving:
      work_conserving job_arrival job_cost next_suspension arr_seq sched.

    Theorem scheduler_respects_policy :
      respects_JLDP_policy job_arrival job_cost next_suspension arr_seq sched higher_eq_priority.

    Theorem scheduler_respects_self_suspensions:
      respects_self_suspensions job_arrival job_cost next_suspension sched.

  End Proofs.

End ConcreteScheduler.