Library rt.model.schedule.apa.platform

Require Import rt.util.all.
Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task rt.model.priority rt.model.arrival.basic.task_arrival.
Require Import rt.model.schedule.global.basic.schedule.
Require Import rt.model.schedule.apa.interference rt.model.schedule.apa.affinity.

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.