Library prosa.classic.model.schedule.global.jitter.constrained_deadlines

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

Module ConstrainedDeadlines.

  Import Job SporadicTaskset ScheduleOfSporadicTaskWithJitter SporadicTaskset
         TaskArrival 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_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.
    Variable job_jitter: Job time.

    (* 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.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched arr_seq.

    (* For simplicity, let's define some local names. *)
    Let job_is_pending := pending job_arrival job_cost job_jitter sched.
    Let job_is_backlogged := backlogged job_arrival job_cost job_jitter sched.

    (* Next, 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 the absence of multiple jobs of the same
       task when constrained deadlines are assumed.  *)

    Section NoMultipleJobs.

        (* Assume any work-conserving priority-based scheduler. *)
        Variable higher_eq_priority: JLDP_policy Job.
        Hypothesis H_work_conserving:
          work_conserving job_arrival job_cost job_jitter arr_seq sched.
        Hypothesis H_respects_JLDP_policy:
          respects_JLDP_policy job_arrival job_cost job_jitter arr_seq sched higher_eq_priority.

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

        (* Assume that all jobs come from the taskset. *)
        Hypothesis H_all_jobs_from_taskset:
           j,
            arrives_in arr_seq j
            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_arrival 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 job_arrival job_task arr_seq.

        (* 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: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_tsk: job_task j = tsk.

        (*... is backlogged at time t. *)
        Variable t: time.
        Hypothesis H_j_backlogged: job_is_backlogged j t.

        (* Assume that any previous jobs of tsk have completed by the period. *)
        Hypothesis H_all_previous_jobs_completed :
           j_other tsk_other,
            arrives_in arr_seq j_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,
            arrives_in arr_seq j1
            arrives_in arr_seq j2
            job_is_pending j1 t
            job_is_pending 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 NoMultipleJobs.

    (* In this section we also prove the absence of multiple jobs of the same
       task when constrained deadlines are assumed, but in the specific case
       of fixed-priority scheduling.  *)

    Section NoMultipleJobsFP.

      (* Assume any work-conserving priority-based scheduler. *)
      Variable higher_eq_priority: FP_policy sporadic_task.
      Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
      Hypothesis H_respects_JLDP_policy:
        respects_FP_policy job_arrival job_cost job_task job_jitter arr_seq sched higher_eq_priority.

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

      (* Assume that all jobs come from the taskset. *)
      Hypothesis H_all_jobs_from_taskset:
         j,
          arrives_in arr_seq j
          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_arrival 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 job_arrival job_task arr_seq.

      (* 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: Job.
      Hypothesis H_j_arrives: arrives_in arr_seq j.
      Hypothesis 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: job_is_backlogged j t.
      Hypothesis H_t_before_period: t < job_arrival j + task_period tsk.

      (* Recall the definition of a higher-priority task (with respect to tsk). *)
      Let is_hp_task := higher_priority_task higher_eq_priority tsk.

      (* Assume that any jobs of higher-priority tasks complete by their period. *)
      Hypothesis H_all_previous_jobs_completed :
         j_other tsk_other,
          arrives_in arr_seq j_other
          job_task j_other = tsk_other
          is_hp_task 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,
          arrives_in arr_seq j0
          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_other: sporadic_task) :=
        task_is_scheduled job_task sched tsk_other t &&
        is_hp_task 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,
          arrives_in arr_seq j1
          arrives_in arr_seq j2
          job_is_pending j1 t
          job_is_pending j2 t
          job_task j1 = job_task j2
          is_hp_task (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',
          arrives_in arr_seq j'
          job_is_pending 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 ts = num_cpus.

    End NoMultipleJobsFP.

  End Lemmas.

End ConstrainedDeadlines.