Library rt.model.basic.platform_fp

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

Module PlatformFP.

  Import Job SporadicTaskset Schedule ScheduleOfSporadicTask SporadicTaskset SporadicTaskArrival Interference Priority Platform.

  Section Lemmas.

    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.

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

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

    (* Assume that 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.

    Section JobInvariantAsTaskInvariant.

      (* Assume any work-conserving priority-based scheduler. *)
      Variable higher_eq_priority: FP_policy sporadic_task.
      Hypothesis H_work_conserving: work_conserving job_cost sched.
      Hypothesis H_enforces_JLDP_policy:
        enforces_FP_policy job_cost job_task sched higher_eq_priority.

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

      (* ... that has no duplicate tasks ... *)
      Hypothesis H_ts_is_a_set: uniq ts.
      (* ... and such that 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 must arrive to execute, ... *)
      Hypothesis H_completed_jobs_dont_execute:
        completed_jobs_dont_execute job_cost sched.
      (* ... and jobs do not execute after completion. *)
      Hypothesis H_jobs_must_arrive_to_execute:
        jobs_must_arrive_to_execute sched.

      (* Assume that jobs arrive sporadically. *)
      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 <= job_arrival j + task_period tsk. *)
      Variable t: time.
      Hypothesis H_j_backlogged: backlogged job_cost sched j t.
      Hypothesis H_t_before_period: t < job_arrival j + task_period tsk.

      Let can_interfere_with_tsk := fp_can_interfere_with higher_eq_priority tsk.

      (* Assume that any jobs of higher-priority tasks complete by their period. *)
      Hypothesis H_all_previous_jobs_completed :
         (j_other: JobIn arr_seq) tsk_other,
          job_task j_other = tsk_other
          can_interfere_with_tsk tsk_other
          completed job_cost sched j_other (job_arrival j_other + task_period tsk_other).

      (* Assume that any jobs of tsk prior to j complete by their period. *)
      Hypothesis H_all_previous_jobs_of_tsk_completed :
         j0 : JobIn arr_seq,
          job_task j0 = tsk
          job_arrival j0 < job_arrival j
          completed job_cost sched j0 (job_arrival j0 + task_period tsk).

      Definition scheduled_task_with_higher_eq_priority (tsk tsk_other: sporadic_task) :=
        task_is_scheduled job_task sched tsk_other t &&
        can_interfere_with_tsk tsk_other.

      (* Then, there can be at most one pending job of higher-priority tasks at time t. *)
      Lemma platform_fp_no_multiple_jobs_of_interfering_tasks :
           j1 j2,
            pending job_cost sched j1 t
            pending job_cost sched j2 t
            job_task j1 = job_task j2
            can_interfere_with_tsk (job_task j1)
            j1 = j2.

      (* Also, there can be at most one pending job of tsk at time t. *)
      Lemma platform_fp_no_multiple_jobs_of_tsk :
           j',
            pending job_cost sched j' t
            job_task j' = tsk
            j' = j.
      (* Therefore, all processors are busy with tasks other than tsk. *)
      Lemma platform_fp_cpus_busy_with_interfering_tasks :
        count (scheduled_task_with_higher_eq_priority tsk) ts = num_cpus.

    End JobInvariantAsTaskInvariant.

  End Lemmas.

End PlatformFP.