Library rt.model.schedule.global.basic.platform

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

Module Platform.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask SporadicTaskset TaskArrival Interference Priority.

  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.

    (* Consider 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.

    Section Execution.

      (* A scheduler is work-conserving iff when a job j is backlogged,
         all processors are busy with other jobs. *)

      Definition work_conserving :=
         j t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
           cpu, j_other,
            scheduled_on sched j_other cpu t.

      (* We also provide an alternative, equivalent definition of work-conserving
         based on counting the number of scheduled jobs. *)

      Definition work_conserving_count :=
         j t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          size (jobs_scheduled_at sched t) = num_cpus.

    End Execution.

    Section FP.

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

      (* ... is respected by the scheduler iff every scheduled
         job has higher (or same) priority than (as) a backlogged job. *)

      Definition respects_FP_policy :=
         j j_hp t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled sched j_hp t
          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 the scheduler iff at any time t,
         a scheduled job has higher (or same) priority than (as)
         a backlogged job. *)

      Definition respects_JLFP_policy :=
         j j_hp t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled sched j_hp t
          higher_eq_priority j_hp j.

    End JLFP.

    Section JLDP.

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

      (* ... is respected by the scheduler iff at any time t,
         a scheduled job has higher (or same) priority than (as)
         a backlogged job. *)

      Definition respects_JLDP_policy :=
         j j_hp t,
          arrives_in arr_seq j
          backlogged job_arrival job_cost sched j t
          scheduled sched j_hp t
          higher_eq_priority t j_hp j.

    End JLDP.

    Section Lemmas.

      (* Assume all jobs have valid parameters, ...*)
      Hypothesis H_valid_job_parameters:
         j,
          arrives_in arr_seq j
          valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

      (* In this section, we prove that the two definitions of work-conserving are equivalent. *)
      Section EquivalentDefinitions.

        Lemma work_conserving_eq_work_conserving_count :
          work_conserving work_conserving_count.

      End EquivalentDefinitions.

    End Lemmas.

  End Properties.

End Platform.