Library prosa.classic.model.schedule.uni.limited.jlfp_instantiation

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task_arrival
               prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.service
               prosa.classic.model.schedule.uni.workload
               prosa.classic.model.schedule.uni.schedule_of_task.
Require Import prosa.classic.model.schedule.uni.limited.busy_interval
               prosa.classic.model.schedule.uni.limited.abstract_RTA.definitions
               prosa.classic.model.schedule.uni.limited.abstract_RTA.abstract_seq_rta.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.

JLFP instantiation of Interference and Interfering Workload

In this module we instantiate functions Interference and Interfering Workload for an arbitrary JLFP-policy that satisfies the sequential jobs hypothesis. We also prove equivalence of Interference and Interfering Workload to the more conventional notions of service or workload.
Module JLFPInstantiation.

  Import Job TaskArrival ScheduleOfTask Priority Workload Service BusyIntervalJLFP.

  Section Instantiation.

    Context {Task: eqType}.
    Variable task_cost: Task → time.

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_task: Job → Task.

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.

    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    Hypothesis H_sequential_jobs: sequential_jobs job_arrival job_cost sched job_task.

    Variable higher_eq_priority: JLFP_policy Job.
    Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.

    Hypothesis H_JLFP_respects_sequential_jobs:
      JLFP_respects_sequential_jobs
        job_task job_arrival higher_eq_priority.

    Variable tsk: Task.

    Let job_scheduled_at := scheduled_at sched.
    Let job_completed_by := completed_by job_cost sched.
    Let arrivals_between := jobs_arrived_between arr_seq.
    Let quiet_time := quiet_time job_arrival job_cost arr_seq sched higher_eq_priority.
    Let cumulative_task_interference :=
      AbstractSeqRTA.cumul_task_interference job_task arr_seq sched.

Interference and Interfering Workload

In this section, we introduce definitions of interference, interfering workload and a function that bounds cumulative interference.

    Let another_job_with_higher_eq_priority: JLFP_policy Job :=
      fun j1 j2 ⇒ higher_eq_priority j1 j2 && (j1 != j2).

    Let job_from_another_task_with_higher_eq_priority: JLFP_policy Job :=
      fun j1 j2 ⇒ higher_eq_priority j1 j2 && (job_task j1 != job_task j2).

    Let is_priority_inversion (j: Job) (t: time) :=
      is_priority_inversion sched higher_eq_priority j t.

    Definition is_interference_from_another_job_with_higher_eq_priority (j: Job) (t: time) :=
      if sched t is Some jhp then
        another_job_with_higher_eq_priority jhp j
      else false.

    Definition is_interference_from_another_task_with_higher_eq_priority (j: Job) (t: time) :=
      if sched t is Some jhp then
        job_from_another_task_with_higher_eq_priority jhp j
      else false.

    Definition interfering_workload_of_jobs_with_hep_priority (j: Job) (t: time) :=
      \sum_(jhp <- jobs_arriving_at arr_seq t |
            another_job_with_higher_eq_priority jhp j) job_cost jhp.

    Definition interference j t :=
      is_priority_inversion j t || is_interference_from_another_job_with_higher_eq_priority j t.

    Definition interfering_workload j t :=
      is_priority_inversion j t + interfering_workload_of_jobs_with_hep_priority j t.

    Let cumulative_priority_inversion j t1 t2 :=
      \sum_(t1 ≤ t < t2) is_priority_inversion j t.

    Let cumulative_interference_from_other_jobs j t1 t2 :=
      \sum_(t1 ≤ t < t2) is_interference_from_another_job_with_higher_eq_priority j t.

    Let cumulative_interference_from_other_tasks j t1 t2 :=
      \sum_(t1 ≤ t < t2) is_interference_from_another_task_with_higher_eq_priority j t.

    Let cumulative_interference j t1 t2 := \sum_(t1 ≤ t < t2) interference j t.

    Let cumulative_interfering_workload_of_jobs_with_hep_priority j t1 t2 :=
      \sum_(t1 ≤ t < t2) interfering_workload_of_jobs_with_hep_priority j t.

    Let cumulative_interfering_workload j t1 t2 := \sum_(t1 ≤ t < t2) interfering_workload j t.


    Let workload_of_other_jobs_with_hep_priority j t1 t2 :=
      workload_of_jobs job_cost (arrivals_between t1 t2)
                       (fun jhp ⇒ another_job_with_higher_eq_priority jhp j).

    Let service_of_jobs_from_other_tasks_with_hep_priority j t1 t2 :=
      service_of_jobs sched (arrivals_between t1 t2)
                      (fun jhp ⇒ job_from_another_task_with_higher_eq_priority jhp j) t1 t2.

    Let service_of_other_jobs_with_hep_priority j t1 t2 :=
      service_of_jobs sched (arrivals_between t1 t2)
                      (fun jhp ⇒ another_job_with_higher_eq_priority jhp j) t1 t2.

Equivalences

In this section we prove a few equivalences between the definitions obtained by instantiation of definitions from the Abstract RTA module (interference and interfering workload) and definitions corresponding to the conventional concepts.
As it was mentioned previously, instantiated functions of interference and interfering workload usually do not have any useful lemmas about them. Hovewer, it is possible to prove their equivalence to the more conventional notions like service or workload. Next we prove the equivalence between the instantiations and conventional notions.
    Section Equivalences.

      Lemma cumulative_interference_split:
        ∀ j t1 t2,
          cumulative_interference j t1 t2
          = cumulative_priority_inversion j t1 t2 + cumulative_interference_from_other_jobs j t1 t2.

      Lemma cumulative_task_interference_split:
        ∀ j t1 t2 upp_t,
          job_task j = tsk →
          j \in jobs_arrived_before arr_seq upp_t →
          ~~ job_completed_by j t2 →
          cumulative_task_interference interference tsk upp_t t1 t2 =
          cumulative_priority_inversion j t1 t2 +
          cumulative_interference_from_other_tasks j t1 t2.

      Section InstantiatedWorkloadEquivalence.

        Variables t1 t2: time.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_tsk: job_task j = tsk.

        Lemma instantiated_cumulative_workload_of_hep_jobs_equal_total_workload_of_hep_jobs:
          cumulative_interfering_workload_of_jobs_with_hep_priority j t1 t2
          = workload_of_other_jobs_with_hep_priority j t1 t2.

      End InstantiatedWorkloadEquivalence.

      Section InstantiatedServiceEquivalences.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_tsk: job_task j = tsk.

        Variable t1 t: time.
        Hypothesis H_quiet_time: quiet_time j t1.

        Lemma instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs:
          cumulative_interference_from_other_jobs j t1 t = service_of_other_jobs_with_hep_priority j t1 t.

        Lemma instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks:
          cumulative_interference_from_other_tasks j t1 t = service_of_jobs_from_other_tasks_with_hep_priority j t1 t.

      End InstantiatedServiceEquivalences.

      Section BusyIntervalEquivalence.

        Variable j: Job.
        Hypothesis H_j_arrives: arrives_in arr_seq j.
        Hypothesis H_job_of_tsk: job_task j = tsk.
        Hypothesis H_job_cost_positive: job_cost_positive job_cost j.

        Lemma instantiated_quiet_time_equivalent_edf_quiet_time:
          ∀ t,
            quiet_time j t ↔
            AbstractRTADefinitions.quiet_time job_arrival job_cost sched interference interfering_workload j t.

        Lemma instantiated_busy_interval_equivalent_busy_interval:
          ∀ t1 t2,
            busy_interval job_arrival job_cost arr_seq sched higher_eq_priority j t1 t2 ↔
            AbstractRTADefinitions.busy_interval job_arrival job_cost sched interference interfering_workload j t1 t2.

      End BusyIntervalEquivalence.

    End Equivalences.

  End Instantiation.

End JLFPInstantiation.