Library prosa.classic.implementation.apa.schedule

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.arrival_sequence prosa.classic.model.arrival.basic.task.
Require Import
Require Import prosa.classic.model.schedule.apa.affinity prosa.classic.model.schedule.apa.platform.
Require Import
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype bigop seq path.

Module ConcreteScheduler.

  Import SporadicTaskset ArrivalSequence Schedule Platform Priority Affinity ScheduleConstruction.

  (* In this section, we implement a concrete weak APA scheduler. *)
  Section Implementation.

    Context {Job: eqType}.
    Context {sporadic_task: eqType}.

    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_task: Job sporadic_task.

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

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

    (* Let alpha be an affinity associated with each task. *)
    Variable alpha: task_affinity sporadic_task num_cpus.

    (* 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 sched_prefix.
      Let actual_arrivals := jobs_arrived_up_to 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.

      (* Now we implement the algorithm that generates the APA schedule. *)

      (* Given a job j at time t, we first define a predicate that states
         whether j should preempt a mapping (cpu, x), where x is either Some j'
         that is currently mapped to cpu or None. *)

        Definition should_be_scheduled (j: Job) p :=
        let '(cpu, mapped_job) := p in
          if mapped_job is Some j' then (* If there is a job j', check the priority and affinity. *)
            (can_execute_on alpha (job_task j) cpu) &&
            ~~ (higher_eq_priority t j' j)
          else (* Else, if cpu is idle, check only the affinity. *)
            (can_execute_on alpha (job_task j) cpu).

      (* Next, using the "should_be_scheduled" predicate, we define a function
         that tries to schedule job j by updating a list of mappings.
         It does so by replacing the first pair (cpu, x) where j can be
         scheduled (if it exists). *)

      Definition update_available_cpu allocation j :=
        replace_first (should_be_scheduled j) (* search for processors that j can preempt *)
                      (set_pair_2nd (Some j)) (* replace the mapping in that processor with j *)
                      allocation. (* list of mappings *)

      (* Consider the empty mapping. *)
      Let empty_mapping : seq (processor num_cpus × option Job) :=
        (zip (enum (processor num_cpus)) (nseq num_cpus None)).

      (* Using the fuction "update_available_cpu", we now define an iteration
         that iteratively maps each pending job to a processor.

         Starting with an empty mapping,
         <(cpu0, None), (cpu1, None), (cpu2, None), ...>,
         it tries to schedule each job on some processor and yields an updated list: 
         <(cpu0, None), (cpu1, Some j5), (cpu2, Some j9), ...>. *)

      Definition schedule_jobs_from_list l :=
        foldl update_available_cpu empty_mapping l.

      (* To conclude, we take the list of pairs and convert to a function denoting
         the actual schedule. *)

      Definition apa_schedule :=
        pairs_to_function None (schedule_jobs_from_list 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 apa_schedule 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)
        apa_schedule sched1 cpu t = apa_schedule 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 = apa_schedule scheduler cpu t.

  End Implementation.

  (* In this section, we prove several properties about the scheduling algorithm we
     implemented. For example, we show that it is APA work conserving. *)

  Section Proofs.

    Context {Job: eqType}.
    Context {sporadic_task: eqType}.

    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_task: Job sporadic_task.

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

    (* Let alpha be an affinity associated with each task. *)
    Variable alpha: task_affinity sporadic_task num_cpus.

    (* 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_task num_cpus arr_seq alpha higher_eq_priority.

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

      (* To avoid many parameters, let's also rename the scheduling function.
         We make a generic version (for any list of jobs l), ... *)

      Let schedule_jobs t l := schedule_jobs_from_list job_task num_cpus alpha higher_eq_priority t l.
      (* ... and a specific version (for the pending jobs in sched). *)
      Let schedule_pending_jobs t :=
        schedule_jobs t (sorted_pending_jobs job_arrival job_cost num_cpus arr_seq
                                             higher_eq_priority sched t).

      (* Next, we show that there are no duplicate cpus in the mapping. *)
      Lemma scheduler_uniq_cpus :
         t l,
          uniq (unzip1 (schedule_jobs t l)).

      (* Next, we show that if a job j is in the mapping, then j must come from the list
         of jobs l used in the construction. *)

      Lemma scheduler_job_in_mapping :
         l j t cpu,
          (cpu, Some j) \in schedule_jobs t l j \in l.

      (* Next, we prove that if a pair (cpu, j) is in the mapping, then
         cpu must be part of j's affinity. *)

      Lemma scheduler_mapping_respects_affinity :
         j t cpu,
          (cpu, Some j) \in schedule_pending_jobs t
          can_execute_on alpha (job_task j) cpu.

      (* Next, we show that the mapping does not schedule the same job j in two
         different cpus. *)

      Lemma scheduler_has_no_duplicate_jobs :
         j t cpu1 cpu2,
          (cpu1, Some j) \in schedule_pending_jobs t
          (cpu2, Some j) \in schedule_pending_jobs t
          cpu1 = cpu2.

      (* Based on the definition of the schedule, a job j is scheduled on cpu
         iff (cpu, Some j) is the final mapping. *)

      Lemma scheduler_scheduled_on :
         j cpu t,
          scheduled_on sched j cpu t = ((cpu, Some j) \in schedule_pending_jobs t).

      (* Now we show that for every cpu, there is always a pair in the mapping. *)
      Lemma scheduler_has_cpus :
         cpu t l,
            (cpu, x) \in schedule_jobs t l.

      (* Next, consider a list of jobs l that is sorted by priority and does not have
         We prove that for any job j in l, if j is not scheduled at time t,
         then every cpu in j's affinity has some job mapped at time t.  *)

      Lemma scheduler_mapping_is_work_conserving :
         j cpu t l,
          j \in l
          sorted (higher_eq_priority t) l
          uniq l
          ( cpu, (cpu, Some j) \notin schedule_jobs t l)
          can_execute_on alpha (job_task j) cpu
            (cpu, Some j_other) \in schedule_jobs t l.

      (* Next, we prove that the mapping respects priority. *)
      Lemma scheduler_priority :
         j j_hp cpu t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          can_execute_on alpha (job_task j) cpu
          scheduled_on sched j_hp cpu t
          higher_eq_priority t j_hp j.

    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.

    (* Jobs do not execute before they arrive, ...*)
    Theorem scheduler_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.

    (* ..., jobs 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 APA work conserving, ... *)
    Theorem scheduler_apa_work_conserving:
      apa_work_conserving job_arrival job_cost job_task arr_seq sched alpha.

    (* ..., respects affinities, ... *)
    Theorem scheduler_respects_affinity:
      respects_affinity job_task sched alpha.

    (* ... and respects the JLDP policy under weak APA scheduling. *)
    Theorem scheduler_respects_policy :
      respects_JLDP_policy_under_weak_APA job_arrival job_cost job_task arr_seq
                                          sched alpha higher_eq_priority.

  End Proofs.

End ConcreteScheduler.