Library prosa.analysis.abstract.ideal_jlfp_rta

Require Export prosa.analysis.abstract.abstract_seq_rta.
Require Export prosa.analysis.definitions.priority_inversion.
Require Export prosa.analysis.definitions.work_bearing_readiness.
Require Export prosa.analysis.facts.busy_interval.carry_in.

Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.
Require Export prosa.analysis.facts.busy_interval.ideal.priority_inversion.

JLFP instantiation of Interference and Interfering Workload for ideal uni-processor.

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

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Consider any valid arrival sequence with consistent arrivals...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

... and any ideal uni-processor schedule of this arrival sequence...
  Variable sched : schedule (ideal.processor_state Job).
  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.

... where jobs do not execute before their arrival nor after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Assume we have sequential tasks, i.e., jobs of the same task execute in the order of their arrival.
  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.

Consider a JLFP-policy that indicates a higher-or-equal priority relation, and assume that this relation is reflexive and transitive.
  Context `{JLFP_policy Job}.
  Hypothesis H_priority_is_reflexive : reflexive_priorities.
  Hypothesis H_priority_is_transitive : transitive_priorities.

We also assume that the policy respects sequential tasks, meaning that later-arrived jobs of a task don't have higher priority than earlier-arrived jobs of the same task.
  Hypothesis H_JLFP_respects_sequential_tasks : policy_respects_sequential_tasks.

Let tsk be any task to be analyzed.
  Variable tsk : Task.

For simplicity, let's define some local names.
  Let job_scheduled_at := scheduled_at sched.
  Let job_completed_by := completed_by sched.
  Let cumulative_task_interference := cumul_task_interference arr_seq sched.

Interference and Interfering Workload

In this section, we introduce definitions of interference, interfering workload, and a function that bounds cumulative interference.
In order to introduce the interference, first we need to recall the definition of priority inversion. We say that job j is incurring a priority inversion at time t if there exists a job with lower priority that executes at time t. In order to simplify things, we ignore the fact that according to this definition a job can incur priority inversion even before its release (or after completion). All such (potentially bad) cases do not cause problems, as each job is analyzed only within the corresponding busy interval where the priority inversion behaves in the expected way.
  Let is_priority_inversion (j : Job) (t : instant) :=
    priority_inversion_dec arr_seq sched j t.

Next, we say that job j is incurring interference from another job with higher or equal priority at time t, if there exists a job jhp (different from j) with higher or equal priority that executes at time t.
  Definition is_interference_from_another_hep_job (j : Job) (t : instant) :=
    if sched t is Some jhp then
      another_hep_job jhp j
    else false.

Similarly, we say that job j is incurring interference from a job with higher or equal priority of another task at time t, if there exists a job jhp (of a different task) with higher or equal priority that executes at time t.
  Definition is_interference_from_hep_job_from_another_task (j : Job) (t : instant) :=
    if sched t is Some jhp then
      another_task_hep_job jhp j
    else false.

Now, we define the notion of cumulative interference, called interfering_workload_of_hep_jobs, that says how many units of workload are generated by jobs with higher or equal priority released at time t.
  Definition interfering_workload_of_hep_jobs (j : Job) (t : instant) :=
    \sum_(jhp <- arrivals_at arr_seq t | another_hep_job jhp j) job_cost jhp.

Instantiation of Interference We say that job j incurs interference at time t iff it cannot execute due to a higher-or-equal-priority job being scheduled, or if it incurs a priority inversion.
  Definition interference (j : Job) (t : instant) :=
    is_priority_inversion j t || is_interference_from_another_hep_job j t.

Instantiation of Interfering Workload The interfering workload, in turn, is defined as the sum of the priority inversion function and interfering workload of jobs with higher or equal priority.
  Definition interfering_workload (j : Job) (t : instant) :=
    is_priority_inversion j t + interfering_workload_of_hep_jobs j t.

For each of the concepts defined above, we introduce a corresponding cumulative function: (a) cumulative priority inversion...
  Definition cumulative_priority_inversion (j : Job) (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) is_priority_inversion j t.

... (b) cumulative interference from other jobs with higher or equal priority...
  Let cumulative_interference_from_other_hep_jobs (j : Job) (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) is_interference_from_another_hep_job j t.

... (c) and cumulative interference from jobs with higher or equal priority from other tasks...
  Definition cumulative_interference_from_hep_jobs_from_other_tasks (j : Job) (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) is_interference_from_hep_job_from_another_task j t.

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

... (e) cumulative workload from jobs with higher or equal priority...
  Let cumulative_interfering_workload_of_hep_jobs (j : Job) (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) interfering_workload_of_hep_jobs j t.

... (f) and cumulative interfering workload.
  Let cumulative_interfering_workload (j : Job) (t1 t2 : instant) :=
    \sum_(t1 ≤ t < t2) interfering_workload j t.

Instantiated functions usually do not have any useful lemmas about them. In order to reuse existing lemmas, we need to prove equivalence of the instantiated functions to some conventional notions. The instantiations given in this file are equivalent to service and workload. Further, we prove these equivalences formally.
In order to avoid confusion, we denote the notion of a quiet time in the classical sense as quiet_time_cl, and the notion of quiet time in the abstract sense as quiet_time_ab.
    Let quiet_time_cl := busy_interval.quiet_time arr_seq sched.
    Let quiet_time_ab := definitions.quiet_time sched interference interfering_workload.

Same for the two notions of a busy interval.
    Let busy_interval_cl := busy_interval.busy_interval arr_seq sched.
    Let busy_interval_ab := definitions.busy_interval sched interference interfering_workload.

Before we present the formal proofs of the equivalences, we recall the notion of workload of higher or equal priority jobs.
  Let workload_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
    workload_of_jobs (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2).

Similarly, we recall notions of service of higher or equal priority jobs from other tasks...
  Let service_of_hep_jobs_from_other_tasks (j : Job) (t1 t2 : instant) :=
    service_of_jobs sched (fun jhp ⇒ another_task_hep_job jhp j)
                    (arrivals_between arr_seq t1 t2) t1 t2.

... and service of all other jobs with higher or equal priority.
  Let service_of_other_hep_jobs (j : Job) (t1 t2 : instant) :=
    service_of_jobs sched (fun jhp ⇒ another_hep_job jhp j) (arrivals_between arr_seq t1 t2) t1 t2.

Equivalences

In this section we prove useful 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. However, 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.

In the following subsection, we prove properties of the introduced functions under the assumption that the schedule is idle.
    Section IdleSchedule.

Consider a time instant t ...
      Variable t : instant.

... and assume that the schedule is idle at t.
      Hypothesis H_idle : is_idle sched t.

We prove that in this case: ...
... interference from higher-or-equal priority jobs from another task is equal to false, ...
      Lemma idle_implies_no_hep_task_interference :
        ∀ j, is_interference_from_hep_job_from_another_task j t = false.
      Proof.
        intros j.
        unfold is_interference_from_hep_job_from_another_task.
        by move: (H_idle) ⇒ /eqP →.
      Qed.

... and interference for a task is equal to false as well.
      Lemma idle_implies_no_task_interference :
        ∀ upp, task_interference_received_before arr_seq sched interference tsk upp t = false.
      Proof.
        intros ?.
        apply/negP/negP.
        rewrite negb_and; apply/orP; right.
        rewrite -all_predC; apply /allP; intros s IN.
        rewrite //= /interference /is_priority_inversion.
        rewrite idle_implies_no_priority_inversion //.
        unfold is_interference_from_another_hep_job.
        by move: (H_idle) ⇒ /eqP →.
      Qed.

    End IdleSchedule.

Next, we prove properties of the introduced functions under the assumption that the scheduler is not idle.
    Section ScheduledJob.

Consider a job j of task tsk. In this subsection, job j is deemed to be the main job with respect to which the functions are computed.
      Variable j : Job.
      Hypothesis H_j_tsk : job_of_task tsk j.

Consider a time instant t.
      Variable t : instant.

First, consider a case when some jobs is scheduled at time t.
      Section SomeJobIsScheduled.

Consider a job j' (not necessarily distinct from job j) that is scheduled at time t.
        Variable j' : Job.
        Hypothesis H_sched : scheduled_at sched j' t.

Under the stated assumptions, we show that the interference from another higher-or-equal priority job is equal to the relation another_hep_job.
        Lemma interference_ahep_eq_ahep :
          is_interference_from_another_hep_job j t = another_hep_job j' j.
        Proof.
          unfold is_interference_from_another_hep_job.
          by move: (H_sched); rewrite scheduled_at_def; move ⇒ /eqP →.
        Qed.

      End SomeJobIsScheduled.

Next, consider a case when j itself is scheduled at t.
      Section JIsScheduled.

Assume that j is scheduled at time t.
        Hypothesis H_j_sched : scheduled_at sched j t.

Then there is no interference from higher-or-equal priority jobs at time t.
        Lemma interference_ahep_job_eq_false :
          is_interference_from_another_hep_job j t = false.
        Proof.
          erewrite interference_ahep_eq_ahep; last by eassumption.
          by rewrite /another_hep_job eq_refl //= Bool.andb_false_r.
        Qed.

      End JIsScheduled.

In the next subsection, we consider a case when a job j' from the same task (as job j) is scheduled.
      Section FromSameTask.

Consider a job j' that comes from task tsk and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_tsk : job_of_task tsk j'.
        Hypothesis H_j'_sched : scheduled_at sched j' t.

Then we show that interference from higher-or-equal priority jobs from another task is false.
        Lemma interference_athep_eq_false :
          is_interference_from_hep_job_from_another_task j t = false.
        Proof.
          apply/eqP; rewrite eqbF_neg.
          unfold is_interference_from_hep_job_from_another_task.
          move: (H_j'_sched); rewrite scheduled_at_def; move ⇒ /eqP →.
          rewrite negb_and; apply/orP; right.
          by move: (H_j_tsk) (H_j'_tsk) ⇒ /eqP → /eqP ->; rewrite eq_refl.
        Qed.

Similarly, task interference is equal to false, since in order to incur the task interference, a job from a distinct task must be scheduled.
        Lemma task_interference_eq_false :
          ∀ upp,
            task_interference_received_before arr_seq sched interference tsk upp t = false.
        Proof.
          intros ?; unfold task_interference_received_before.
          apply/eqP; rewrite eqbF_neg negb_and Bool.negb_involutive; apply/orP; left.
          rewrite /task_scheduled_at.
          by move: (H_j'_sched); rewrite scheduled_at_def ⇒ /eqP →.
        Qed.

      End FromSameTask.

In the next subsection, we consider a case when a job j' from a task other than j's task is scheduled.
      Section FromDifferentTask.

Consider a job j' that does _not comes from task tsk and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_not_tsk : ~~ job_of_task tsk j'.
        Hypothesis H_j'_sched : scheduled_at sched j' t.

We prove that then j incurs higher-or-equal priority interference from another task iff j' has higher-or-equal priority than j.
        Lemma sched_at_implies_interference_athep_eq_hep :
          is_interference_from_hep_job_from_another_task j t = hep_job j' j.
        Proof.
          unfold is_interference_from_hep_job_from_another_task.
          move: (H_j'_sched); rewrite scheduled_at_def; move ⇒ /eqP →.
          apply/andP; destruct (hep_job).
          - by move: (H_j_tsk) ⇒ /eqP ->; rewrite H_j'_not_tsk.
          - by intros [F _].
        Qed.

Hence, if we assume that j' has higher-or-equal priority, ...
        Hypothesis H_j'_hep : hep_job j' j.

... we will be able to show that j incurs higher-or-equal priority interference from another task.
        Lemma sched_athep_implies_interference_athep :
          is_interference_from_hep_job_from_another_task j t.
        Proof.
          unfold is_interference_from_hep_job_from_another_task.
          move: (H_j'_sched); rewrite scheduled_at_def ⇒ /eqP →.
          rewrite /another_task_hep_job H_j'_hep.
          by move: (H_j_tsk) ⇒ /eqP →.
        Qed.

Moreover, in this case, task tsk also incurs interference.
        Lemma sched_athep_implies_task_interference :
          ∀ upp,
            j \in arrivals_between arr_seq 0 upp →
            task_interference_received_before arr_seq sched interference tsk upp t.
        Proof.
          intros ? IN.
          apply/andP; split.
          - by move: (H_j'_sched); rewrite /task_scheduled_at scheduled_at_def ⇒ /eqP →.
          - apply/hasP; ∃ j.
            + rewrite mem_filter; apply/andP; split; last by done.
              by rewrite H_j_tsk.
            + apply/orP; right.
              move: (H_j'_sched); rewrite /is_interference_from_another_hep_job scheduled_at_def ⇒ /eqP →.
              apply/andP; split; first by done.
              apply/negP; move ⇒ /eqP EQ; subst.
              by move: (H_j'_not_tsk); rewrite H_j_tsk.
        Qed.

      End FromDifferentTask.

In the last subsection, we consider a case when the scheduled job j' has lower priority than job j.
      Section LowerPriority.

Consider a job j' that has lower priority than job j and is scheduled at time instant t.
        Variable j' : Job.
        Hypothesis H_j'_sched : scheduled_at sched j' t.
        Hypothesis H_j'_lp : ~~ hep_job j' j.

        Lemma sched_alp_implies_interference_ahep_false :
          is_interference_from_another_hep_job j t = false.
        Proof.
          apply/eqP; rewrite eqbF_neg.
          unfold is_interference_from_another_hep_job.
          move: (H_j'_sched); rewrite scheduled_at_def; move ⇒ /eqP →.
          apply/negP; move ⇒ /andP [HEP _].
          by move: H_j'_lp ⇒ /negP T; apply: T.
        Qed.

      End LowerPriority.

    End ScheduledJob.

We prove that we can split cumulative interference into two parts: (1) cumulative priority inversion and (2) cumulative interference from jobs with higher or equal priority.
    Lemma cumulative_interference_split :
      ∀ j t1 t2,
        cumulative_interference j t1 t2
        = cumulative_priority_inversion j t1 t2
          + cumulative_interference_from_other_hep_jobs j t1 t2.
    Proof.
      rewrite /cumulative_interference /interference.
      intros; rewrite -big_split //=.
      rewrite /is_priority_inversion.
      apply/eqP; rewrite eqn_leq; apply/andP; split; rewrite leq_sum; try done.
      { intros t _.
        destruct (ideal_proc_model_sched_case_analysis sched t) as [IDLE | [s SCHED]].
        - rewrite idle_implies_no_priority_inversion //.
        - destruct (hep_job s j) eqn:PRIO.
          + by destruct (priority_inversion_dec _ _ _), (is_interference_from_another_hep_job _ _).
          + erewrite sched_lp_implies_priority_inversion; rt_eauto.
            by rewrite PRIO.
      }
      { intros t _.
        destruct (ideal_proc_model_sched_case_analysis sched t) as [IDLE | [s SCHED]].
        - rewrite idle_implies_no_priority_inversion //.
        - destruct (hep_job s j) eqn:PRIO.
          + erewrite sched_hep_implies_no_priority_inversion; eauto 2.
          + erewrite sched_lp_implies_priority_inversion; rt_eauto.
            erewrite sched_alp_implies_interference_ahep_false; rt_eauto.
            all: by rewrite PRIO.
      }
    Qed.

Similarly, we prove that we can split cumulative interfering workload into two parts: (1) cumulative priority inversion and (2) cumulative interfering workload from jobs with higher or equal priority.
    Lemma cumulative_interfering_workload_split :
      ∀ j t1 t2,
        cumul_interfering_workload interfering_workload j t1 t2 =
          cumulative_priority_inversion j t1 t2 + cumulative_interfering_workload_of_hep_jobs j t1 t2.
    Proof.
      rewrite /cumul_interfering_workload
              /cumulative_priority_inversion
              /cumulative_interfering_workload_of_hep_jobs.
      by intros; rewrite -big_split //=.
    Qed.

Let j be any job of task tsk, and let upp_t be any time instant after job j's arrival. Then for any time interval lying before upp_t, the cumulative interference received by tsk is equal to the sum of the cumulative priority inversion of job j and the cumulative interference incurred by task tsk due to other tasks.
    Lemma cumulative_task_interference_split :
      ∀ j t1 t2 upp_t,
        arrives_in arr_seq j →
        job_of_task tsk j →
        j \in arrivals_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_hep_jobs_from_other_tasks j t1 t2.
    Proof.
      rewrite /cumulative_task_interference /cumul_task_interference; intros j t1 R upp ARRin TSK ARR NCOMPL.
      rewrite -big_split //= big_seq_cond [in X in _ = X]big_seq_cond; apply eq_bigr; move ⇒ t /andP [IN _].
      apply/eqP; rewrite eqn_leq; apply/andP; split.
      - unfold is_priority_inversion.
        ideal_proc_model_sched_case_analysis_eq sched t s; first by rewrite idle_implies_no_task_interference //=.
        destruct (hep_job s j) eqn:HP, (job_task s == tsk) eqn:TSKs.
        + by erewrite task_interference_eq_false; eauto 1.
        + move: TSKs ⇒ /eqP/eqP TSKs; erewrite sched_athep_implies_task_interference, sched_athep_implies_interference_athep; eauto 1.
          by destruct (priority_inversion_dec).
        + erewrite sched_lp_implies_priority_inversion; rt_eauto; last by rewrite HP.
          by destruct (task_interference_received_before), (is_interference_from_hep_job_from_another_task).
        + erewrite sched_lp_implies_priority_inversion; rt_eauto; last by rewrite HP.
          by destruct (task_interference_received_before), (is_interference_from_hep_job_from_another_task).
      - rewrite /is_priority_inversion; ideal_proc_model_sched_case_analysis_eq sched t s;
          first by rewrite idle_implies_no_priority_inversion //= idle_implies_no_hep_task_interference.
        destruct (job_task s == job_task j) eqn:TSKEQ.
        + erewrite priority_inversion_equiv_sched_lower_priority; rt_eauto.
          erewrite interference_athep_eq_false with (j' := s),
              ?task_interference_eq_false with (j' := s), leqn0, addn0, eqb0; eauto 2; try by move: TSK ⇒ /eqP <-.
          apply/negP; intros NEQ; move: NCOMPL ⇒ /negP NCOMPL; apply: NCOMPL.
          apply completion_monotonic with t; first by rewrite mem_iota in IN; apply ltnW; lia.
          apply/negP; intros NCOMPL; move: NCOMPL ⇒ /negP NCOMPL.
          move: NEQ ⇒ /negP NEQ; apply: NEQ; apply H_JLFP_respects_sequential_tasks; rt_eauto.
          by eapply scheduler_executes_job_with_earliest_arrival; rt_eauto.
        + erewrite priority_inversion_equiv_sched_lower_priority; rt_eauto.
          have TSKn : ~~ job_of_task tsk s.
            by apply/negP; intros ?; move: TSKEQ ⇒ /eqP TSKEQ; apply:TSKEQ; move: (H4) (TSK) ⇒ /eqP → /eqP →.
          erewrite sched_at_implies_interference_athep_eq_hep with (j' := s); eauto 2.
          have F: ∀ b, ~~ b + b = true; [ by intros b; destruct b | rewrite F lt0b; clear F ].
          apply/andP; split.
          × by move: (Sched_s); rewrite /task_scheduled_at scheduled_at_def ⇒ /eqP →.
          × apply/hasP; ∃ j.
            -- rewrite mem_filter; apply/andP; split; first by done.
               by exact: arrivals_between_sub ARR.
            -- rewrite /interference /is_priority_inversion; erewrite priority_inversion_equiv_sched_lower_priority; rt_eauto.
              rewrite /is_interference_from_another_hep_job.
              destruct (hep_job s j) eqn:HP; apply/orP; [right| by left].
              move: (Sched_s); rewrite /task_scheduled_at scheduled_at_def ⇒ /eqP →.
              rewrite /another_hep_job HP Bool.andb_true_l.
              by apply/eqP; intros EQ; subst s; rewrite TSK in TSKn.
    Qed.

In this section we prove that the (abstract) cumulative interfering workload is equivalent to conventional workload, i.e., the one defined with concrete schedule parameters.
    Section InstantiatedWorkloadEquivalence.

Let [t1,t2) be any time interval.
      Variables t1 t2 : instant.

Consider any job j of tsk.
      Variable j : Job.
      Hypothesis H_j_arrives : arrives_in arr_seq j.
      Hypothesis H_job_of_tsk : job_of_task tsk j.

Then for any job j, the cumulative interfering workload is equal to the conventional workload.
      Lemma cumulative_iw_hep_eq_workload_of_ohep :
        cumulative_interfering_workload_of_hep_jobs j t1 t2
        = workload_of_other_hep_jobs j t1 t2.
      Proof.
        intros.
        rewrite /cumulative_interfering_workload_of_hep_jobs
                /workload_of_other_hep_jobs.
        case NEQ: (t1 < t2); last first.
        { move: NEQ ⇒ /negP /negP; rewrite -leqNgt; move ⇒ NEQ.
          rewrite big_geq; last by done.
          rewrite /arrivals_between /arrival_sequence.arrivals_between big_geq; last by done.
            by rewrite /workload_of_jobs big_nil.
        }
        { unfold interfering_workload_of_hep_jobs, workload_of_jobs.
          interval_to_duration t1 t2 k.
          induction k.
          - rewrite !addn0.
            rewrite big_geq; last by done.
            rewrite /arrivals_between /arrival_sequence.arrivals_between big_geq; last by done.
              by rewrite /workload_of_jobs big_nil.
          - rewrite addnS big_nat_recr //=; last by rewrite leq_addr.
            rewrite IHk.
            rewrite /arrivals_between /arrival_sequence.arrivals_between big_nat_recr //=;
                    last by rewrite leq_addr.
              by rewrite big_cat //=.
        }
      Qed.

    End InstantiatedWorkloadEquivalence.

In this section we prove that the (abstract) cumulative interference of jobs with higher or equal priority is equal to total service of jobs with higher or equal priority.
    Section InstantiatedServiceEquivalences.

Consider any job j of tsk.
      Variable j : Job.
      Hypothesis H_j_arrives : arrives_in arr_seq j.
      Hypothesis H_job_of_tsk : job_of_task tsk j.

We consider an arbitrary time interval [t1, t) that starts with a quiet time.
      Variable t1 t : instant.
      Hypothesis H_quiet_time : quiet_time_cl j t1.

Then for any job j, the (abstract) instantiated function of interference is equal to the total service of jobs with higher or equal priority.
      Lemma cumulative_i_ohep_eq_service_of_ohep :
        cumulative_interference_from_other_hep_jobs j t1 t
        = service_of_other_hep_jobs j t1 t.
      Proof.
        rewrite /service_of_other_hep_jobs /service_of_jobs.
        rewrite /cumulative_interference_from_other_hep_jobs
                /is_interference_from_another_hep_job.
        rewrite exchange_big //= big_nat_cond [in X in _ = X]big_nat_cond.
        all: apply/eqP; rewrite eqn_leq; apply/andP; split.
        all: rewrite leq_sum //; move ⇒ x /andP [/andP [Ge Le] _].
        { ideal_proc_model_sched_case_analysis_eq sched x jo; first by done.
          move: (Sched_jo); rewrite scheduled_at_def; move ⇒ /eqP EQ; rewrite EQ.
          destruct (another_hep_job jo j) eqn:PRIO; last by done.
          rewrite (big_rem jo) /=; first by rewrite PRIO service_at_def EQ eq_refl.
          apply arrived_between_implies_in_arrivals; try done; rt_eauto.
          - rewrite /arrived_between; apply/andP; split.
            + move: PRIO ⇒ /andP [PRIO1 PRIO2].
              rewrite leqNgt; apply/negP; intros AB.
              move: (Sched_jo). rewrite -[scheduled_at _ _ _]Bool.negb_involutive;
                                  move ⇒ /negP SCHED2; apply: SCHED2.
              apply completed_implies_not_scheduled; rt_eauto.
              apply completion_monotonic with t1; try done.
              by apply H_quiet_time; try done; rt_eauto.
              move : EQ ⇒ /eqP EQ.
              rewrite -scheduled_at_def in EQ.
              eapply has_arrived_scheduled in EQ; rt_eauto.
              apply leq_ltn_trans with x; rt_eauto. }
        { erewrite eq_bigr; last by move⇒ i _; rewrite service_at_def /=.
          ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
          move: (Sched_jo); rewrite scheduled_at_def; move ⇒ /eqP EQ; rewrite EQ.
          destruct (another_hep_job jo j) eqn:PRIO.
          - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between arr_seq t1 t) _ x.
            eapply leq_trans; last first.
            + apply SCH; rt_eauto.
            + rewrite /service_of_jobs_at; erewrite leq_sum ⇒ // i _.
              by rewrite service_at_def.
          - rewrite leqn0 big1 //; intros joo PRIO2.
            apply/eqP; rewrite eqb0; apply/eqP; intros C.
            inversion C; subst joo; clear C.
            by rewrite PRIO2 in PRIO. }
      Qed.

The same applies to the alternative definition of interference.
      Lemma cumulative_i_thep_eq_service_of_othep :
        cumulative_interference_from_hep_jobs_from_other_tasks j t1 t
        = service_of_hep_jobs_from_other_tasks j t1 t.
      Proof.
        rewrite /service_of_hep_jobs_from_other_tasks /service_of_jobs.
        rewrite /cumulative_interference_from_hep_jobs_from_other_tasks
                /is_interference_from_hep_job_from_another_task.
        rewrite exchange_big //= big_nat_cond [in X in _ = X]big_nat_cond.
        all: apply/eqP; rewrite eqn_leq; apply/andP; split.
        all: rewrite leq_sum //; move ⇒ x /andP [/andP [Ge Le] _].
        { ideal_proc_model_sched_case_analysis_eq sched x jo; first by done.
          move: (Sched_jo); rewrite scheduled_at_def; move ⇒ /eqP EQ; rewrite EQ.
          destruct (another_task_hep_job jo j) eqn:PRIO; last by done.
          rewrite (big_rem jo) /=; first by rewrite PRIO service_at_def EQ eq_refl.
          apply arrived_between_implies_in_arrivals; try done; rt_eauto.
          - rewrite /arrived_between; apply/andP; split.
            + move: PRIO ⇒ /andP [PRIO1 PRIO2].
              rewrite leqNgt; apply/negP; intros AB.
              move: (Sched_jo). rewrite -[scheduled_at _ _ _]Bool.negb_involutive;
                                  move ⇒ /negP SCHED2; apply: SCHED2.
              apply completed_implies_not_scheduled; rt_eauto.
              apply completion_monotonic with t1; try done.
              apply H_quiet_time; try done; rt_eauto.
            + move : EQ ⇒ /eqP EQ; rewrite -scheduled_at_def in EQ.
              eapply has_arrived_scheduled in EQ; rt_eauto.
              by apply leq_ltn_trans with x; rt_eauto.

        }
        { erewrite eq_bigr; last by move⇒ i _; rewrite service_at_def /=.
          ideal_proc_model_sched_case_analysis_eq sched x jo; first by rewrite big1_eq.
          move: (Sched_jo); rewrite scheduled_at_def; move ⇒ /eqP EQ; rewrite EQ.
          destruct (another_task_hep_job jo j) eqn:PRIO.
          - rewrite -EQ. have SCH := service_of_jobs_le_1 _ _ sched _ (arrivals_between arr_seq t1 t) _ x.
            eapply leq_trans; last first.
            + by apply SCH; rt_eauto.
            + rewrite /service_of_jobs_at; erewrite leq_sum ⇒ // i _.
              by rewrite service_at_def.
          - rewrite leqn0 big1 //; intros joo PRIO2.
            apply/eqP; rewrite eqb0; apply/eqP; intros C.
            inversion C; subst joo; clear C.
              by rewrite PRIO2 in PRIO.
        }
      Qed.

      End InstantiatedServiceEquivalences.

In this section we prove that the abstract definition of busy interval is equivalent to the conventional, concrete definition of busy interval for JLFP scheduling.
      Section BusyIntervalEquivalence.

Consider any job j of tsk.
        Variable j : Job.
        Hypothesis H_j_arrives : arrives_in arr_seq j.
        Hypothesis H_job_of_tsk : job_of_task tsk j.
        Hypothesis H_job_cost_positive : job_cost_positive j.

To show the equivalence of the notions of busy intervals we first show that the notions of quiet time are also equivalent.

        Lemma quiet_time_cl_implies_quiet_time_ab:
          ∀ t, quiet_time_cl j t → quiet_time_ab j t.
        Proof.
          have zero_is_quiet_time: ∀ j, quiet_time_cl j 0.
          { by intros jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
          intros t QT; split; last first.
          { rewrite negb_and Bool.negb_involutive; apply/orP.
            by case ARR: (arrived_before j t); [right | left]; [apply QT | ]; eauto.
          }
          { erewrite cumulative_interference_split, cumulative_interfering_workload_split; apply/eqP; rewrite eqn_add2l.
            rewrite cumulative_i_ohep_eq_service_of_ohep //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
            apply all_jobs_have_completed_equiv_workload_eq_service;
              rt_eauto.
            intros j0 IN HEP; apply QT.
            - by apply in_arrivals_implies_arrived in IN.
            - by move: HEP ⇒ /andP [H6 H7].
            - by apply in_arrivals_implies_arrived_between in IN; rt_eauto.
          }
        Qed.

        Lemma quiet_time_ab_implies_quiet_time_cl:
          ∀ t, quiet_time_ab j t → quiet_time_cl j t.
        Proof. clear H_job_of_tsk.
          have zero_is_quiet_time: ∀ j, quiet_time_cl j 0.
          { by intros jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
          intros t [T0 T1] jhp ARR HP ARB.
          eapply all_jobs_have_completed_equiv_workload_eq_service with
              (P := fun jhp ⇒ hep_job jhp j) (t1 := 0) (t2 := t); rt_eauto.
          erewrite service_of_jobs_case_on_pred with (P2 := fun j' ⇒ j' != j); rt_eauto.
          erewrite workload_of_jobs_case_on_pred with (P' := fun j' ⇒ j' != j); rt_eauto.
          replace ((fun j0 : Job ⇒ hep_job j0 j && (j0 != j))) with (another_hep_job^~j); last by rewrite /another_hep_job.
          rewrite -/(service_of_other_hep_jobs j 0 t) -cumulative_i_ohep_eq_service_of_ohep; eauto.
          rewrite -/(workload_of_other_hep_jobs j 0 t) -cumulative_iw_hep_eq_workload_of_ohep; eauto.
          move: T1; rewrite negb_and ⇒ /orP [NA | /negPn COMP].
          { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j__copy : Job ⇒ hep_job j__copy j && ~~ (j__copy != j)) =1 pred0}.
            { intros j__copy IN; apply negbTE.
              rewrite negb_and; apply/orP; right; apply/negPn/eqP ⇒ EQ; subst j__copy.
              move: NA ⇒ /negP CONTR; apply: CONTR.
              by apply in_arrivals_implies_arrived_between in IN; rt_eauto. }
            erewrite service_of_jobs_equiv_pred with (P2 := pred0); last by done.
            erewrite workload_of_jobs_equiv_pred with (P' := pred0); last by done.
            move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split ⇒ /eqP; rewrite eqn_add2l ⇒ /eqP EQ.
            rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
            by erewrite workload_of_jobs_pred0, service_of_jobs_pred0.
          }
          { have PRED__eq: {in arrivals_between arr_seq 0 t, (fun j0 : Job ⇒ hep_job j0 j && ~~ (j0 != j)) =1 eq_op j}.
            { intros j__copy IN.
              replace (~~ (j__copy != j)) with (j__copy == j); last by case: (j__copy == j).
              rewrite eq_sym; destruct (j == j__copy) eqn:EQ; last by rewrite Bool.andb_false_r.
              move: EQ ⇒ /eqP EQ; rewrite Bool.andb_true_r; apply/eqP; rewrite eqb_id; subst.
              by eapply (H_priority_is_reflexive 0). }
            erewrite service_of_jobs_equiv_pred with (P2 := eq_op j); last by done.
            erewrite workload_of_jobs_equiv_pred with (P' := eq_op j); last by done.
            move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split ⇒ /eqP; rewrite eqn_add2l ⇒ /eqP EQ.
            rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
            apply/eqP; eapply all_jobs_have_completed_equiv_workload_eq_service with
              (P := eq_op j) (t1 := 0) (t2 := t); rt_eauto.
            by move ⇒ j__copy _ /eqP EQ; subst j__copy. }
        Qed.

The equivalence trivially follows from the lemmas above.
        Corollary instantiated_quiet_time_equivalent_quiet_time:
          ∀ t,
            quiet_time_cl j t ↔ quiet_time_ab j t.
        Proof.
          clear H_job_of_tsk.
          intros ?; split.
          - apply quiet_time_cl_implies_quiet_time_ab.
          - apply quiet_time_ab_implies_quiet_time_cl.
        Qed.

Based on that, we prove that the concept of busy interval obtained by instantiating the abstract definition of busy interval coincides with the conventional definition of busy interval.
        Lemma instantiated_busy_interval_equivalent_busy_interval:
          ∀ t1 t2,
            busy_interval_cl j t1 t2 ↔ busy_interval_ab j t1 t2.
        Proof.
          clear H_job_of_tsk.
          split.
          { move ⇒ [[NEQ [QTt1 [NQT REL]] QTt2]].
            split; [split; [ |split] | ].
            - by done.
            - by apply instantiated_quiet_time_equivalent_quiet_time in QTt1.
            - by intros t NE QT; eapply NQT; eauto 2; apply instantiated_quiet_time_equivalent_quiet_time.
            - by eapply instantiated_quiet_time_equivalent_quiet_time in QTt2.
          }
          { move ⇒ [[/andP [NEQ1 NEQ2] [QTt1 NQT] QTt2]].
            split; [split; [ | split; [ |split] ] | ].
            - by apply leq_ltn_trans with (job_arrival j).
            - by eapply instantiated_quiet_time_equivalent_quiet_time; eauto 2.
            - by intros t NEQ QT; eapply NQT; eauto 2; eapply instantiated_quiet_time_equivalent_quiet_time in QT; eauto 2.
            - by apply/andP; split.
            - by eapply instantiated_quiet_time_equivalent_quiet_time; eauto 2.
          }
        Qed.

      End BusyIntervalEquivalence.

  End Equivalences.

In this section we prove some properties about the interference and interfering workload as defined in this file.
  Section I_IW_correctness.

Consider work-bearing readiness.
    Context `{@JobReady Job (ideal.processor_state Job) _ _}.
    Hypothesis H_work_bearing_readiness : work_bearing_readiness arr_seq sched.

Assume that the schedule is valid and work-conserving.
    Hypothesis H_sched_valid : @valid_schedule Job (ideal.processor_state Job) sched _ _ _ arr_seq.

Note that we differentiate between abstract and classical notions of work conserving schedule.
    Let work_conserving_ab := definitions.work_conserving arr_seq sched interference interfering_workload.
    Let work_conserving_cl := work_conserving.work_conserving arr_seq sched.

We assume that the schedule is a work-conserving schedule in the classical sense, and later prove that the hypothesis about abstract work-conservation also holds.
    Hypothesis H_work_conserving : work_conserving_cl.

Assume the scheduling policy under consideration is reflexive.
    Hypothesis policy_reflexive : reflexive_priorities.

In this section, we prove the correctness of interference inside the busy interval, i.e., we prove that if interference for a job is false then the job is scheduled and vice versa. This property is referred to as abstract work conservation.

    Section Abstract_Work_Conservation.

Consider a job j that is in the arrival sequence and has a positive job cost.
      Variable j : Job.
      Hypothesis H_arrives : arrives_in arr_seq j.
      Hypothesis H_job_cost_positive : 0 < job_cost j.

Let the busy interval of the job be [t1,t2).
      Variable t1 t2 : instant.
      Hypothesis H_busy_interval : busy_interval_ab j t1 t2.

Consider a time t inside the busy interval of the job.
      Variable t : instant.
      Hypothesis H_t_in_busy_interval : t1 ≤ t < t2.

First, we prove that if interference is false at a time t then the job is scheduled.
    Lemma not_interference_implies_scheduled :
      ¬ interference j t → scheduled_at sched j t.
    Proof.
      move ⇒ /negP HYP; move : HYP.
      rewrite negb_or !/is_priority_inversion
        /is_interference_from_another_hep_job.
      move ⇒ /andP [HYP1 HYP2].
      ideal_proc_model_sched_case_analysis_eq sched t jo.
      { exfalso; clear HYP1 HYP2.
        eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; rt_eauto.
        move: H_busy_interval ⇒ [PREF _].
        eapply not_quiet_implies_not_idle; rt_eauto. }
      {
        clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move ⇒ /eqP EqSched_jo.
        rewrite EqSched_jo in HYP1, HYP2.
        move: HYP2; rewrite /another_hep_job negb_and ⇒ /orP [NHEP| EQ].
        { eapply sched_lp_implies_priority_inversion in NHEP; rt_eauto.
          - by rewrite NHEP in HYP1.
          - by erewrite scheduled_at_def, EqSched_jo.
        }
        { move: EQ; rewrite -Bool.negb_involutive_reverse ⇒ /eqP EQ.
          by subst jo; rewrite scheduled_at_def EqSched_jo.
        }
      }
    Qed.

Conversely, if the job is scheduled at t then interference is false.
    Lemma scheduled_implies_no_interference :
      scheduled_at sched j t → ¬ interference j t.
    Proof.
      rewrite scheduled_at_def ⇒ /eqP HYP.
      apply /negP.
      rewrite /interference /is_priority_inversion
        /is_interference_from_another_hep_job
        HYP negb_or.
      apply/andP; split.
      - erewrite sched_hep_implies_no_priority_inversion; first by done.
      - by erewrite scheduled_at_def, HYP; apply/eqP; reflexivity.
        by apply (policy_reflexive 0).
      - rewrite negb_and.
        by apply /orP; right; apply /negPn.
    Qed.

    End Abstract_Work_Conservation.

Using the above two lemmas, we can prove that abstract work conservation always holds for these instantiations of I and IW.
    Corollary instantiated_i_and_w_are_coherent_with_schedule :
      work_conserving_ab.
    Proof.
      move ⇒ j t1 t2 t ARR POS BUSY NEQ; split.
      + by apply (not_interference_implies_scheduled j ARR POS t1 t2); try done.
      + by apply (scheduled_implies_no_interference j t ); try done.
    Qed.

Next, in order to prove that these definitions of I and IW are consistent with sequential tasks, we need to assume that the policy under consideration respects sequential tasks.
    Hypothesis H_policy_respects_sequential_tasks : policy_respects_sequential_tasks.

We prove that these definitions of I and IW are consistent with sequential tasks.
    Lemma instantiated_interference_and_workload_consistent_with_sequential_tasks :
      interference_and_workload_consistent_with_sequential_tasks
        arr_seq sched tsk interference interfering_workload.
    Proof.
      move ⇒ j t1 t2 ARR /eqP TSK POS BUSY.
      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
      eapply all_jobs_have_completed_equiv_workload_eq_service; rt_eauto.
      move ⇒ s INs /eqP TSKs.
      move: (INs) ⇒ NEQ.
      eapply in_arrivals_implies_arrived_between in NEQ; rt_eauto.
      move: NEQ ⇒ /andP [_ JAs].
      move: (BUSY) ⇒ [[ _ [QT [_ /andP [JAj _]]] _]].
      apply QT; try done; first by eapply in_arrivals_implies_arrived; eauto 2.
      apply H_policy_respects_sequential_tasks; first by rewrite TSK TSKs.
      by apply leq_trans with t1; [lia | done].
    Qed.

Since interfering and interfering workload are sufficient to define the busy window, next, we reason about the bound on the length of the busy window.
    Section BusyWindowBound.

Consider an arrival curve.
      Context `{MaxArrivals Task}.

Consider a set of tasks that respects the arrival curve.
      Variable ts : list Task.
      Hypothesis H_taskset_respects_max_arrivals : taskset_respects_max_arrivals arr_seq ts.

Assume that all jobs come from this task set.
      Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

Consider a constant L such that...
      Variable L : duration.
... L is greater than 0, and...
      Hypothesis H_L_positive : L > 0.

L is the fixed point of the following equation.
      Hypothesis H_fixed_point : L = total_request_bound_function ts L.

Assume all jobs have a valid job cost.
      Hypothesis H_arrivals_have_valid_job_costs : arrivals_have_valid_job_costs arr_seq.

Then, we prove that L is a bound on the length of the busy window.
      Lemma instantiated_busy_intervals_are_bounded:
        busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
      Proof.
        move ⇒ j ARR TSK POS.
        edestruct exists_busy_interval_from_total_workload_bound
          with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
        { intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf; try by done. }
        ∃ t1, t2; split; first by done.
        by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
      Qed.

    End BusyWindowBound.

  End I_IW_correctness.

End JLFPInstantiation.

Global Opaque is_interference_from_another_hep_job.