Library prosa.classic.model.schedule.apa.platform

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority prosa.classic.model.arrival.basic.task_arrival.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.affinity.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.

Module Platform.

  Import Job SporadicTaskset ScheduleOfSporadicTask SporadicTaskset
         TaskArrival Interference Priority Affinity.

  Section Properties.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_period: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Assume any job arrival sequence ... *)
    Variable arr_seq: arrival_sequence Job.

    (* ... and any schedule of this arrival sequence. *)
    Context {num_cpus: nat}.
    Variable sched: schedule Job num_cpus.

    (* Assume that every task has a processor affinity alpha. *)
    Variable alpha: task_affinity sporadic_task num_cpus.

    Section Execution.

      (* A schedule is work-conserving iff when a job j is backlogged, all
         processors *on which j can be scheduled* are busy with other jobs. *)

      Definition apa_work_conserving :=
         j t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
           cpu,
            can_execute_on alpha (job_task j) cpu
             j_other,
              scheduled_on sched j_other cpu t.

      (* In a schedule that respects affinities, a job is scheduled
         only if its affinity allows it. *)

      Definition respects_affinity :=
         j cpu t,
          scheduled_on sched j cpu t
          can_execute_on alpha (job_task j) cpu.

    End Execution.

    Section FP.

      (* An FP policy ...*)
      Variable higher_eq_priority: FP_policy sporadic_task.

      (* ... is respected by a weak APA scheduler iff for any
         backlogged job j, if there is another job j_hp
         executing on j's affinity, then j_hp's task priority
         must be as high as j's task priority. *)

      Definition respects_FP_policy_under_weak_APA :=
         j j_hp cpu t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled_on sched j_hp cpu t
          can_execute_on alpha (job_task j) cpu
          higher_eq_priority (job_task j_hp) (job_task j).

    End FP.

    Section JLFP.

      (* A JLFP policy ...*)
      Variable higher_eq_priority: JLFP_policy Job.

      (* ... is respected by a weak APA scheduler iff for
         any backlogged job j, if there is another job j_hp
         executing on j's affinity, then j_hp's priority
         must be as high as j's priority. *)

      Definition respects_JLFP_policy_under_weak_APA :=
         j j_hp cpu t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled_on sched j_hp cpu t
          can_execute_on alpha (job_task j) cpu
          higher_eq_priority j_hp j.

    End JLFP.

    Section JLDP.

      (* A JLFP/JLDP policy ...*)
      Variable higher_eq_priority: JLDP_policy Job.

      (* ... is respected by a weak APA scheduler iff at any time t,
         for any backlogged job j, if there is another job j_hp
         executing on j's affinity, then j_hp's priority must be
         as high as j's priority. *)

      Definition respects_JLDP_policy_under_weak_APA :=
         j j_hp cpu t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled_on sched j_hp cpu t
          can_execute_on alpha (job_task j) cpu
          higher_eq_priority t j_hp j.

    End JLDP.

  End Properties.

End Platform.