Library rt.model.jitter.platform

Require Import rt.util.all.
Require Import rt.model.jitter.task rt.model.jitter.job rt.model.jitter.schedule
               rt.model.jitter.priority rt.model.jitter.task_arrival rt.model.jitter.interference.

Module Platform.

  Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset SporadicTaskArrival Interference Priority.

  Section SchedulingInvariants.

    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_cost: Job → time.
    Variable job_deadline: Job → time.
    Variable job_task: Job → sporadic_task.
    Variable job_jitter: Job → time.

    (* Assume any job arrival sequence... *)
    Context {arr_seq: arrival_sequence Job}.

    (* Consider any schedule. *)
    Context {num_cpus: nat}.
    Variable sched: schedule num_cpus arr_seq.

    Section WorkConserving.

      (* A scheduler is work-conserving iff when a job j is backlogged,
         all processors are busy with other jobs.
         NOTE: backlogged means that jitter has already passed. *)
      Definition work_conserving :=
        ∀ j t,
          backlogged job_cost job_jitter 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,
          backlogged job_cost job_jitter sched j t →
          size (jobs_scheduled_at sched t) = num_cpus.

    End WorkConserving.

    Section JLDP.

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

      (* ... is enforced by the scheduler iff at any time t,
         a scheduled job has higher (or same) priority than (as)
         a backlogged job. *)
      Definition enforces_JLDP_policy :=
        ∀ (j j_hp: JobIn arr_seq) t,
          backlogged job_cost job_jitter sched j t →
          scheduled sched j_hp t →
          higher_eq_priority t j_hp j.

    End JLDP.

    Section FP.

      (* Given an FP policy, ...*)
      Variable higher_eq_priority: FP_policy sporadic_task.

      (* ... this policy is enforced by the scheduler iff
         a corresponding JLDP policy is enforced by the scheduler. *)
      Definition enforces_FP_policy :=
        enforces_JLDP_policy (FP_to_JLDP job_task higher_eq_priority).

    End FP.

    Section Lemmas.

      (* Assume all jobs have valid parameters, ...*)
      Hypothesis H_valid_job_parameters:
        ∀ (j: JobIn arr_seq),
          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.

      Section JobInvariantAsTaskInvariant.

        (* Assume any work-conserving priority-based scheduler. *)
        Variable higher_eq_priority: JLDP_policy arr_seq.
        Hypothesis H_work_conserving: work_conserving.
        Hypothesis H_enforces_JLDP_policy: enforces_JLDP_policy higher_eq_priority.

        (* Consider task set ts. *)
        Variable ts: taskset_of sporadic_task.

        (* Assume the task set has no duplicates, ... *)
        Hypothesis H_ts_is_a_set: uniq ts.
        (* ... and all jobs come from the taskset. *)
        Hypothesis H_all_jobs_from_taskset:
          ∀ (j: JobIn arr_seq), job_task j \in ts.

        (* Suppose that jobs are sequential, ...*)
        Hypothesis H_sequential_jobs: sequential_jobs sched.
        (* ... jobs only execute after the jitter, ... *)
        Hypothesis H_jobs_execute_after_jitter:
          jobs_execute_after_jitter job_jitter sched.
        (* ... and jobs do not execute after completion. *)
        Hypothesis H_completed_jobs_dont_execute:
          completed_jobs_dont_execute job_cost sched.

        (* Assume that the schedule satisfies the sporadic task model ...*)
        Hypothesis H_sporadic_tasks:
          sporadic_task_model task_period arr_seq job_task.

        (* Consider a valid task tsk, ...*)
        Variable tsk: sporadic_task.
        Hypothesis H_valid_task: is_valid_sporadic_task task_cost task_period task_deadline tsk.

        (*... whose job j ... *)
        Variable j: JobIn arr_seq.
        Variable H_job_of_tsk: job_task j = tsk.

        (*... is backlogged at time t. *)
        Variable t: time.
        Hypothesis H_j_backlogged: backlogged job_cost job_jitter sched j t.

        (* Assume that any previous jobs of tsk have completed by the period. *)
        Hypothesis H_all_previous_jobs_completed :
          ∀ (j_other: JobIn arr_seq) tsk_other,
            job_task j_other = tsk_other →
            job_arrival j_other + task_period tsk_other ≤ t →
            completed job_cost sched j_other (job_arrival j_other + task_period (job_task j_other)).

        Let scheduled_task_other_than (tsk tsk_other: sporadic_task) :=
          task_is_scheduled job_task sched tsk_other t && (tsk_other != tsk).

        (* Then, there can be at most one pending job of each task at time t. *)
        Lemma platform_at_most_one_pending_job_of_each_task :
          ∀ j1 j2,
            pending job_cost job_jitter sched j1 t →
            pending job_cost job_jitter sched j2 t →
            job_task j1 = job_task j2 →
            j1 = j2.

        (* Therefore, all processors are busy with tasks other than tsk. *)
        Lemma platform_cpus_busy_with_interfering_tasks :
          count (scheduled_task_other_than tsk) ts = num_cpus.

      End JobInvariantAsTaskInvariant.

    End Lemmas.

  End SchedulingInvariants.

End Platform.