analysis/abstract/iw_auxiliary.v

+Require Export prosa.analysis.definitions.interference.
+Require Export prosa.analysis.definitions.task_schedule.
+Require Export prosa.analysis.facts.priority.classes.
+Require Export prosa.analysis.abstract.restricted_supply.busy_prefix.
+Require Export prosa.model.aggregate.service_of_jobs.
+Require Export prosa.analysis.facts.model.service_of_jobs.
+
+
+(** * Auxiliary Lemmas About Interference and Interfering Workload. *)
+
+(** In this file we provide a set of auxiliary lemmas about generic
+    properties of Interference and Interfering Workload. *)
+Section InterferenceAndInterferingWorkloadAuxiliary.
+
+  (** 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}.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Consider any kind of fully supply-consuming uniprocessor model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** 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 uni-processor schedule of this arrival
+      sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence :
+    jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival or 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.
+
+  (** Let [tsk] be any task. *)
+  Variable tsk : Task.
+
+  (** For convenience, we define a function that "folds" cumulative
+      conditional interference with a predicate [fun _ _ => true] to
+      cumulative (unconditional) interference. *)
+  Lemma fold_cumul_interference :
+    forall j t1 t2,
+      cumul_cond_interference (fun _ _ => true) j t1 t2
+      = cumulative_interference j t1 t2.
+  Proof. by rewrite /cumulative_interference. Qed.
+
+  (** In this section, we prove a few basic properties of conditional
+      interference w.r.t. a generic predicate [P]. *)
+  Section CondInterferencePredicate.
+
+    (** In the following, consider a predicate [P]. *)
+    Variable P : Job -> instant -> bool.
+
+    (** First, we show that the cumulative conditional interference
+        within a time interval <<[t1, t2)>> can be rewritten as a sum
+        over all time instances satisfying [P j]. *)
+    Lemma cumul_cond_interference_alt :
+      forall j t1 t2,
+        cumul_cond_interference P j t1 t2 = \sum_(t1 <= t < t2 | P j t) interference j t.
+    Proof.
+      move=> j t1 t2; rewrite [RHS]big_mkcond //=; apply eq_big_nat => t _.
+      by rewrite /cond_interference; case: (P j t).
+    Qed.
+
+    (** Next, we show that cumulative interference on an interval
+        <<[al, ar)>> is bounded by the cumulative interference on an
+        interval <<[bl,br)>> if <<[al,ar)>> ⊆ <<[bl,br)>>. *)
+    Lemma cumulative_interference_sub :
+      forall (j : Job) (al ar bl br : instant),
+        bl <= al ->
+        ar <= br ->
+        cumul_cond_interference P j al ar <= cumul_cond_interference P j bl br.
+    Proof.
+      move => j al ar bl br LE1 LE2.
+      rewrite !cumul_cond_interference_alt.
+      case: (leqP al ar) => [LEQ|LT]; last by rewrite big_geq.
+      rewrite [leqRHS](@big_cat_nat _ _ _ al) //=; last by lia.
+      by rewrite [in X in _ <= _ + X](@big_cat_nat _ _ _ ar) //=; lia.
+    Qed.
+
+    (** We show that the cumulative interference of a job can be split
+        into disjoint intervals. *)
+    Lemma cumulative_interference_cat :
+      forall j t t1 t2,
+        t1 <= t <= t2 ->
+        cumul_cond_interference P j t1 t2
+        = cumul_cond_interference P j t1 t + cumul_cond_interference P j t t2.
+    Proof.
+      move => j t t1 t2 /andP [LE1 LE2].
+      by rewrite !cumul_cond_interference_alt {1}(@big_cat_nat _ _ _ t) //=.
+    Qed.
+
+  End CondInterferencePredicate.
+
+  (** Next, we show a few relations between interference functions
+      conditioned on different predicates. *)
+  Section CondInterferenceRelation.
+
+    (** Consider predicates [P1, P2]. *)
+    Variables P1 P2 : Job -> instant -> bool.
+
+    (** We introduce a lemma (similar to ssreflect's [bigID] lemma)
+        that allows us to split the cumulative conditional
+        interference w.r.t predicate [P1] into a sum of two cumulative
+        conditional interference w.r.t. predicates [P1 && P2] and [P1
+        && ~~ P2], respectively. *)
+    Lemma cumul_cond_interference_ID :
+      forall j t1 t2,
+        cumul_cond_interference P1 j t1 t2
+        = cumul_cond_interference (fun j t => P1 j t && P2 j t) j t1 t2
+          + cumul_cond_interference (fun j t => P1 j t && ~~ P2 j t) j t1 t2.
+    Proof.
+      move=> j t1 t2.
+      rewrite -big_split //=; apply eq_bigr => t _.
+      rewrite /cond_interference.
+      by case (P1 _ _), (P2 _ _ ), (interference _ _).
+    Qed.
+
+    (** If two predicates [P1] and [P2] are equivalent, then they can
+        be used interchangeably with [cumul_cond_interference]. *)
+    Lemma cumul_cond_interference_pred_eq :
+      forall (j : Job) (t1 t2 : instant),
+        (forall j t, P1 j t <-> P2 j t) ->
+        cumul_cond_interference P1 j t1 t2
+        = cumul_cond_interference P2 j t1 t2.
+    Proof.
+      move=> j t1 t2 EQU.
+      apply eq_bigr => t _; rewrite /cond_interference.
+      move: (EQU j t).
+      by case (P1 j t), (P2 j t), (interference _ _); move=> CONTR => //=; exfalso; apply notF, CONTR.
+    Qed.
+
+  End CondInterferenceRelation.
+
+End InterferenceAndInterferingWorkloadAuxiliary.

analysis/abstract/lower_bound_on_service.v

+Require Export prosa.analysis.facts.model.service_of_jobs.
+Require Export prosa.analysis.facts.preemption.rtc_threshold.job_preemptable.
+Require Export prosa.analysis.abstract.definitions.
+Require Export prosa.analysis.abstract.busy_interval.
+
+(** * Lower Bound On Job Service *)
+(** In this section we prove that if the cumulative interference
+    inside a busy interval is bounded by a certain constant then a job
+    executes long enough to reach a specified amount of service. *)
+Section LowerBoundOnService.
+
+  (** 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}.
+
+  (** In addition, we assume existence of a function mapping jobs to
+      their preemption points. *)
+  Context `{JobPreemptable Job}.
+
+  (** Consider _any_ kind of processor state model. *)
+  Context {PState : ProcessorState Job}.
+
+  (** Consider any arrival sequence with consistent arrivals ... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** ... and any schedule of this arrival sequence. *)
+  Variable sched : schedule PState.
+
+  (** Assume that the job costs are no larger than the task costs. *)
+  Hypothesis H_jobs_respect_taskset_costs : arrivals_have_valid_job_costs arr_seq.
+
+  (** Let [tsk] be any task that is to be analyzed. *)
+  Variable tsk : Task.
+
+  (** Assume we are provided with abstract functions for interference
+      and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the schedule is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Let [j] be any job of task [tsk] with positive cost. *)
+  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.
+
+  (** In this section, we show that the cumulative interference is a
+      complement to the total time where job [j] is scheduled inside a
+      busy interval prefix. *)
+  Section InterferenceIsComplement.
+
+    (** Consider any busy interval prefix <<[t1, t2)>> of job [j]. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
+
+    (** Consider any sub-interval <<[t, t + δ)>> inside the busy interval <<[t1, t2)>>. *)
+    Variables (t : instant) (δ : duration).
+    Hypothesis H_t1_le_t : t1 <= t.
+    Hypothesis H_tδ_le_t2 : t + δ <= t2.
+
+    (** We prove that sum of cumulative service and cumulative
+        interference in the interval <<[t, t + δ)>> is equal to
+        [δ]. *)
+    Lemma interference_is_complement_to_schedule :
+      service_during sched j t (t + δ) + cumulative_interference j t (t + δ) >= δ.
+    Proof.
+      rewrite /service_during /cumulative_interference /cumul_cond_interference /service_at.
+      rewrite -big_split //= -{1}(sum_of_ones t δ) big_nat [in X in _ <= X]big_nat leq_sum // => x /andP[Lo Hi].
+      move: (H_work_conserving j t1 t2 x) => Workj.
+      feed_n 4 Workj => //; first by lia.
+      rewrite /cond_interference //=.
+      case INT: interference; first by lia.
+      by rewrite // addn0; apply Workj; rewrite INT.
+    Qed.
+    
+    (** Also, note that under the unit-service processor model
+        assumption, the sum of service within the interval <<[t, t + δ)>> 
+        and the cumulative interference within the same interval
+        is bounded by the length of the interval (i.e., [δ]).  *) 
+    Remark service_and_interference_bounded :
+      unit_service_proc_model PState ->
+      service_during sched j t (t + δ) + cumulative_interference j t (t + δ) <= δ.
+    Proof.
+      move => UNIT.
+      rewrite /service_during /cumulative_interference/service_at -big_split //=.
+      rewrite -{2}(sum_of_ones t δ).
+      rewrite big_nat [in X in _ <= X]big_nat; apply leq_sum => x /andP[Lo Hi].
+      move: (H_work_conserving j t1 t2 x) => Workj.
+      feed_n 4 Workj => //.
+      { by apply/andP; split; lia. }
+      rewrite /cond_interference //=.
+      destruct interference.
+      - rewrite addn1 ltnS.
+        by move_neq_up NE; apply Workj.
+      - by rewrite addn0; apply UNIT.
+    Qed.
+    
+  End InterferenceIsComplement.
+
+  (** In this section, we prove a sufficient condition under which job
+      [j] receives enough service. *)
+  Section InterferenceBoundedImpliesEnoughService.
+
+    (** Consider any busy interval <<[t1, t2)>> of job [j]. *)
+    Variable t1 t2 : instant.
+    Hypothesis H_busy_interval : busy_interval sched j t1 t2.
+
+    (** Let [progress_of_job] be the desired service of job [j]. *)
+    Variable progress_of_job : duration.
+    Hypothesis H_progress_le_job_cost : progress_of_job <= job_cost j.
+
+    (** Assume that for some [δ] the sum of desired progress and
+        cumulative interference is bounded by [δ]. *)
+    Variable δ : duration.
+    Hypothesis H_total_workload_is_bounded :
+      progress_of_job + cumulative_interference j t1 (t1 + δ) <= δ.
+
+    (** Then, it must be the case that the job has received no less
+        service than [progress_of_job]. *)
+    Theorem j_receives_enough_service :
+      service sched j (t1 + δ) >= progress_of_job.
+    Proof.
+      destruct (leqP (t1 + δ) t2) as [NEQ|NEQ]; last first.
+      { move: (job_completes_within_busy_interval _ _ _ _ H_busy_interval) => COMPL.
+        apply leq_trans with (job_cost j) => [//|].
+        rewrite /service -(service_during_cat _ _ _ t2); last by apply/andP; split; last apply ltnW.
+        by apply leq_trans with (service_during sched j 0 t2); [| rewrite leq_addr].
+      }
+      { move: H_total_workload_is_bounded => BOUND.
+        rewrite addnC in BOUND; apply leq_subRL_impl in BOUND.
+        apply leq_trans with (δ - cumulative_interference j t1 (t1 + δ)) => [//|].
+        apply leq_trans with (service_during sched j t1 (t1 + δ)).
+        - eapply leq_trans.
+          + by apply leq_sub2r, (interference_is_complement_to_schedule t1 t2);
+              [apply H_busy_interval | apply leqnn | apply NEQ].
+          + by rewrite -addnBA // subnn addn0 //.
+        - rewrite /service -[X in _ <= X](service_during_cat _ _ _ t1); first by rewrite leq_addl //.
+          by apply/andP; split; last rewrite leq_addr.
+      }
+    Qed.
+
+  End InterferenceBoundedImpliesEnoughService.
+
+End LowerBoundOnService.

analysis/abstract/restricted_supply/abstract_rta.v

+Require Export prosa.analysis.facts.behavior.supply.
+Require Export prosa.analysis.facts.SBF.
+Require Export prosa.analysis.abstract.abstract_rta.
+Require Export prosa.analysis.abstract.iw_auxiliary.
+Require Export prosa.analysis.abstract.IBF.supply.
+Require Export prosa.analysis.abstract.restricted_supply.busy_sbf.
+
+(** * Abstract Response-Time Analysis for Restricted-Supply Processors (aRSA) *)
+(** In this section we propose a general framework for response-time
+    analysis ([RTA]) for real-time tasks with arbitrary arrival models
+    under uni-processor scheduling subject to supply restrictions,
+    characterized by a given [SBF]. *)
+
+(** We prove that the maximum (with respect to the set of offsets)
+    among the solutions of the response-time bound recurrence is a
+    response-time bound for [tsk]. Note that in this section we add
+    additional restrictions on the processor state. These assumptions
+    allow us to eliminate the second equation from [aRTA+]'s
+    recurrence since jobs experience delays only due to the lack of
+    supply while executing non-preemptively. *)
+Section AbstractRTARestrictedSupply.
+
+  (** Consider any type of tasks with a run-to-completion threshold ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of fully supply-consuming unit-supply
+      processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** Consider any restricted supply uniprocessor schedule of this
+      arrival sequence ...*)
+  Variable sched : schedule PState.
+  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 are given valid WCETs for all tasks.  *)
+  Hypothesis H_valid_job_cost :
+    arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider a task set [ts]... *)
+  Variable ts : list Task.
+
+  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model ... *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** ...and a valid task run-to-completion threshold function. That
+      is, [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2)
+      for any job [j] of task [tsk] [job_rtct j] is bounded by
+      [task_rtct tsk]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Assume we are provided with abstract functions for Interference
+      and Interfering Workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** We assume that the scheduler is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Next, we assume that [intra_IBF] is a bound on the intra-supply
+      interference incurred by task [tsk]. *)
+  Variable intra_IBF : duration -> duration -> duration.
+  Hypothesis H_intra_supply_interference_is_bounded :
+    intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
+
+  (** Given any job [j] of task [tsk] that arrives exactly [A] units
+      after the beginning of the busy interval, the bound on the
+      interference incurred by [j] within an interval of length [Δ] is
+      no greater than [(Δ - SBF Δ) + intra_IBF A Δ]. *)
+  Let IBF_P (A Δ : duration) :=
+    (Δ - SBF Δ) + intra_IBF A Δ.
+
+  (** Next, we instantiate function [IBF_NP], which is a function that
+      bounds interference in a non-preemptive stage of execution. We
+      prove that this function can be instantiated as [λ tsk F Δ ⟹ (F
+      - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F))]. *)
+
+  (** Let us reiterate on the intuitive interpretation of this
+      function. Since [F] is a solution to the first equation
+      [task_rtct tsk + IBF_P A F <= F], we know that by time
+      instant [t1 + F] a job receives [task_rtct tsk] units of service
+      and, hence, it becomes non-preemptive. Knowing this information,
+      how can we bound the job's interference in an interval <<[t1, t1
+      + Δ)>>?  Note that this interval starts with the beginning of
+      the busy interval. We know that the job receives [F - task_rtct
+      tsk] units of interference. In the non-preemptive mode, a job
+      under analysis can still experience some interference due to a
+      lack of supply. This interference is bounded by [(Δ - SBF Δ) -
+      (F - SBF F)] since part of this interference has already been
+      accounted for in the preemptive part of the execution ([F - SBF
+      F]). *)
+  Let IBF_NP (F Δ : duration) :=
+    (F - task_rtct tsk) + (Δ - SBF Δ - (F - SBF F)).
+
+  (** In the next section, we prove a few helper lemmas. *)
+  Section AuxiliaryLemmas.
+
+      (** 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.
+
+      (** Consider the busy interval <<[t1, t2)>> of job [j]. *)
+      Variable t1 t2 : instant.
+      Hypothesis H_busy_interval : busy_interval_prefix sched j t1 t2.
+
+      (** Let's define [A] as a relative arrival time of job [j] (with
+          respect to time [t1]). *)
+      Let A : duration := job_arrival j - t1.
+
+      (** Consider an arbitrary time [Δ] ... *)
+      Variable Δ : duration.
+      (** ... such that [t1 + Δ] is inside the busy interval... *)
+      Hypothesis H_inside_busy_interval : t1 + Δ < t2.
+      (** ... the job [j] is not completed by time [(t1 + Δ)]. *)
+      Hypothesis H_job_j_is_not_completed : ~~ completed_by sched j (t1 + Δ).
+
+      (** First, we show that blackout is counted as interference. *)
+      Lemma blackout_impl_interference :
+        forall t,
+          t1 <= t < t2 ->
+          is_blackout sched t ->
+          interference j t.
+      Proof.
+        move=> t /andP [LE1 LE2].
+        apply contraLR => /negP INT.
+        eapply H_work_conserving in INT =>//; last by lia.
+        by apply/negPn; eapply pos_service_impl_pos_supply.
+      Qed.
+
+      (** Next, we show that interference is equal to a sum of two
+          functions: [is_blackout] and [intra_interference]. *)
+      Lemma blackout_plus_local_is_interference :
+        forall t,
+          t1 <= t < t2 ->
+          is_blackout sched t + intra_interference sched j t
+          = interference j t.
+      Proof.
+        move=> t t_INT.
+        rewrite /intra_interference /cond_interference.
+        destruct (is_blackout sched t) eqn:BLACKOUT; rewrite (negbRL BLACKOUT) //.
+        by rewrite blackout_impl_interference.
+      Qed.
+
+      (** As a corollary, cumulative interference during a time
+          interval <<[t1, t1 + Δ)>> can be split into a sum of total
+          blackouts in <<[t1, t1 + Δ)>> and cumulative intra-supply
+          interference during <<[t1, t1 + Δ)>>. *)
+      Corollary blackout_plus_local_is_interference_cumul :
+        blackout_during sched t1 (t1 + Δ) + cumul_intra_interference sched j t1 (t1 + Δ)
+        = cumulative_interference j t1 (t1 + Δ).
+      Proof.
+        rewrite -big_split; apply eq_big_nat => //=.
+        move=> t /andP [t_GEQ t_LTN_td].
+        move: (ltn_trans t_LTN_td H_inside_busy_interval) => t_LTN_t2.
+        by apply blackout_plus_local_is_interference; apply /andP.
+      Qed.
+
+      (** Moreover, since the total blackout duration in an interval
+          of length [Δ] is bounded by [Δ - SBF Δ], the cumulative
+          interference during the time interval <<[t1, t1 + Δ)>> is
+          bounded by the sum of [Δ - SBF Δ] and cumulative
+          intra-supply interference during <<[t1, t1 + Δ)>>. *)
+      Corollary cumulative_job_interference_bound :
+        cumulative_interference j t1 (t1 + Δ)
+        <= (Δ - SBF Δ) + cumul_intra_interference sched j t1 (t1 + Δ).
+      Proof.
+        rewrite -blackout_plus_local_is_interference_cumul leq_add2r.
+        by eapply blackout_during_bound with (t2 := t2) => //.
+      Qed.
+
+      (** Next, consider a duration [F] such that [F <= Δ] and job [j]
+          has enough service to become non-preemptive by time instant
+          [t1 + F]. *)
+      Variable F : duration.
+      Hypothesis H_F_le_Δ : F <= Δ.
+      Hypothesis H_enough_service : task_rtct tsk <= service sched j (t1 + F).
+
+      (** Then, we show that job [j] does not experience any
+          intra-supply interference in the time interval <<[t1 + F, t1 +
+          Δ)>>. *)
+      Lemma no_intra_interference_after_F :
+        cumul_intra_interference sched j (t1 + F) (t1 + Δ) = 0.
+      Proof.
+        rewrite /cumul_intra_interference/ cumul_cond_interference big_nat.
+        apply big1; move => t /andP [GE__t LT__t].
+        apply/eqP; rewrite eqb0; apply/negP.
+        move => /andP [P /negPn /negP D]; apply: D; apply/negP.
+        eapply H_work_conserving with (t1 := t1) (t2 := t2); eauto 2.
+        { by apply/andP; split; lia. }
+        eapply progress_inside_supplies; eauto.
+        eapply job_nonpreemptive_after_run_to_completion_threshold; eauto 2.
+        - rewrite -(leqRW H_enough_service).
+          by apply H_valid_run_to_completion_threshold.
+        - move: H_job_j_is_not_completed; apply contra.
+          by apply completion_monotonic; lia.
+      Qed.
+
+  End AuxiliaryLemmas.
+
+  (** For clarity, let's define a local name for the search space. *)
+  Let is_in_search_space_rs := is_in_search_space L IBF_P.
+
+  (** We use the following equation to bound the response-time of a
+      job of task [tsk]. Consider any value [R] that upper-bounds the
+      solution of each response-time recurrence, i.e., for any
+      relative arrival time [A] in the search space, there exists a
+      corresponding solution [F] such that (1) [F <= A + R],
+      (2) [task_rtct tsk + intra_IBF tsk A F <= SBF F] and [SBF F +
+      (task_cost tsk - task_rtct tsk) <= SBF (A + R)].
+
+      Note that, compared to "ideal RTA," there is an additional requirement
+      [F <= A + R]. Intuitively, it is needed to rule out a nonsensical
+      situation when the non-preemptive stage completes earlier than
+      the preemptive stage.  *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_rs :
+    forall (A : duration),
+      is_in_search_space_rs A ->
+      exists (F : duration),
+        F <= A + R
+        /\ task_rtct tsk + intra_IBF A F <= SBF F
+        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+
+  (** In the following section we prove that all the premises of
+      abstract RTA are satisfied. *)
+  Section RSaRTAPremises.
+
+    (** First, we show that [IBF_P] correctly upper-bounds
+        interference in the preemptive stage of execution. *)
+    Lemma IBF_P_bounds_interference :
+      job_interference_is_bounded_by
+        arr_seq sched tsk IBF_P (relative_arrival_time_of_job_is_A sched).
+    Proof.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) => EQ.
+      rewrite fold_cumul_interference.
+      rewrite (leqRW (cumulative_job_interference_bound _ _ _ _ _ t2 _ _ _ _)) => //.
+      - rewrite leq_add2l /cumul_intra_interference.
+        by apply: H_intra_supply_interference_is_bounded => //.
+      - by eapply incomplete_implies_positive_cost => //.
+      - by apply BUSY.
+    Qed.
+
+    (** Next, we prove that [IBF_NP] correctly bounds interference in
+        the non-preemptive stage given a solution to the preemptive
+        stage [F]. *)
+    Lemma IBF_NP_bounds_interference :
+      job_interference_is_bounded_by
+        arr_seq sched tsk IBF_NP (relative_time_to_reach_rtct sched tsk IBF_P).
+    Proof.
+      have USER : unit_service_proc_model PState by apply unit_supply_is_unit_service.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM F RT.
+      have POS := incomplete_implies_positive_cost _ _ _ NCOM.
+      move: (RT _ _ BUSY) (BUSY) => [FIX RTC] [[/andP [LE1 LE2] _] _].
+      have RleF : task_rtct tsk <= F.
+      { apply cumulative_service_ge_delta with (j := j) (t := t1) (sched := sched) => //.
+        rewrite -[X in _ <= X]add0n.
+        by erewrite <-cumulative_service_before_job_arrival_zero;
+          first erewrite service_during_cat with (t1 := 0) => //; auto; lia. }
+      rewrite /IBF_NP addnBAC // leq_subRL_impl // addnC.
+      have [NEQ1|NEQ1] := leqP t2 (t1 + F); last have [NEQ2|NEQ2] := leqP F Δ.
+      { rewrite -leq_subLR in NEQ1.
+        rewrite -{1}(leqRW NEQ1) (leqRW RTC) (leqRW (service_at_most_cost _ _ _ _ _)) => //.
+        rewrite (leqRW (cumulative_interference_sub _ _ _ _ t1 t2 _ _)) => //.
+        rewrite (leqRW (service_within_busy_interval_ge_job_cost _ _ _ _ _ _ _)) => //.
+        have LLL : (t1 < t2) by lia.
+        interval_to_duration t1 t2 k.
+        by rewrite addnC (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) => //; lia. }
+      { rewrite addnC -{1}(leqRW FIX) -addnA leq_add2l /IBF_P.
+        rewrite (@addnC (_ - _) _) -addnA subnKC; last by apply complement_SBF_monotone.
+        rewrite -/(cumulative_interference _ _ _).
+        erewrite <-blackout_plus_local_is_interference_cumul with (t2 := t2) => //; last by apply BUSY. 
+        rewrite addnC leq_add //; last first.
+        { by eapply blackout_during_bound with (t2 := t2) => //; split; [ | apply BUSY]. }
+        rewrite /cumul_intra_interference (cumulative_interference_cat _ j (t1 + F)) //=; last by lia.
+        rewrite -!/(cumul_intra_interference _ _ _ _).
+        rewrite (no_intra_interference_after_F _ _ _ _ _ t2) //; last by move: BUSY => [].
+        rewrite addn0 //; eapply H_intra_supply_interference_is_bounded => //.
+        - by move : NCOM; apply contra, completion_monotonic; lia.
+        - move => t1' t2' BUSY'.
+          have [EQ1 E2] := busy_interval_is_unique _ _ _ _ _ _ BUSY BUSY'.
+          by subst; lia. }
+      { rewrite addnC (leqRW RTC); eapply leq_trans.
+        - by erewrite leq_add2l; apply cumulative_interference_sub with (bl := t1) (br := t1 + F); lia.
+        - erewrite no_service_before_busy_interval => //.
+          by rewrite (leqRW (service_and_interference_bound _ _ _ _ _ _ _ _ _ _ _ _)) => //; lia.  }
+    Qed.
+
+    (** Next, we prove that [F] is bounded by [task_cost tsk + IBF_NP
+        F Δ] for any [F] and [Δ]. As explained in file
+        [analysis/abstract/abstract_rta], this shows that the second
+        stage indeed takes into account service received in the first
+        stage. *)
+    Lemma IBF_P_sol_le_IBF_NP :
+      forall (F Δ : duration),
+        F <= task_cost tsk + IBF_NP F Δ.
+    Proof.
+      move=> F Δ.
+      have [NEQ|NEQ] := leqP F (task_rtct tsk).
+      - apply: leq_trans; [apply NEQ | ].
+        by apply: leq_trans; [apply H_valid_run_to_completion_threshold | lia].
+      - rewrite addnA (@addnBCA _ F _); try lia.
+        by apply H_valid_run_to_completion_threshold; lia.
+    Qed.
+
+    (** Next we prove that [H_R_is_maximum_rs] implies [H_R_is_maximum]. *)
+    Lemma max_in_rs_hypothesis_impl_max_in_arta_hypothesis :
+      forall (A : duration),
+        is_in_search_space L IBF_P A ->
+        exists (F : duration),
+          task_rtct tsk + (F - SBF F + intra_IBF A F) <= F
+          /\ task_cost tsk + (F - task_rtct tsk + (A + R - SBF (A + R) - (F - SBF F))) <= A + R.
+    Proof.
+      move=> A SP.
+      case: (H_R_is_maximum_rs A SP) => [F [EQ0 [EQ1 EQ2]]].
+      exists F; split.
+      { have -> : forall a b c, a + (b + c) = (a + c) + b by lia.
+        have -T : forall a b c, c >= b -> (a <= c - b) -> (a + b <= c); [by lia | apply: T; first by lia].
+        have LE : SBF F <= F by eapply sbf_bounded_by_duration; eauto.
+        by rewrite (leqRW EQ1); lia.
+      }
+      { have JJ := IBF_P_sol_le_IBF_NP F (A + R); rewrite /IBF_NP in JJ.
+        rewrite addnA; rewrite addnA in JJ.
+        have T: forall a b c, c >= b -> (a <= c - b) -> (a + b <= c); [by lia | apply: T; first by lia].
+        rewrite subnA; [ | by apply complement_SBF_monotone | by lia].
+        have LE : forall Δ, SBF Δ <= Δ by move => ?; eapply sbf_bounded_by_duration; eauto.
+        rewrite subKn; last by eauto.
+        have T: forall a b c d e, b >= e -> b >= c ->  e + (a - c) <= d -> a + (b - c) <= d + (b - e) by lia.
+        apply : T => //.
+        eapply leq_trans; last by apply LE.
+        by rewrite -(leqRW EQ1); lia.
+      }
+    Qed.
+
+  End RSaRTAPremises.
+
+  (** Finally, we apply the [uniprocessor_response_time_bound]
+      theorem, and using the lemmas above, we prove that all the
+      requirements are satisfied. So, [R] is a response time bound. *)
+  Theorem uniprocessor_response_time_bound_restricted_supply :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    eapply uniprocessor_response_time_bound => //.
+    { by apply IBF_P_bounds_interference. }
+    { by apply IBF_NP_bounds_interference. }
+    { by apply IBF_P_sol_le_IBF_NP. }
+    { by apply max_in_rs_hypothesis_impl_max_in_arta_hypothesis. }
+  Qed.
+
+End AbstractRTARestrictedSupply.

analysis/abstract/restricted_supply/abstract_seq_rta.v

+Require Export prosa.analysis.facts.model.rbf.
+Require Export prosa.analysis.abstract.IBF.supply_task.
+Require Export prosa.analysis.abstract.restricted_supply.abstract_rta.
+
+(** * Abstract Response-Time Analysis for Restricted-Supply Processors with Sequential Tasks *)
+(** In this section we propose a general framework for response-time
+    analysis (RTA) for real-time tasks with arbitrary arrival models
+    and _sequential_ _tasks_ under uni-processor scheduling subject to
+    supply restrictions, characterized by a given [SBF]. *)
+
+(** In this section, we assume tasks to be sequential. This allows us
+    to establish a more precise response-time bound, since jobs of the
+    same task will be executed strictly in the order they arrive. *)
+Section AbstractRTARestrictedSupplySequential.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (**  ... and any type of jobs associated with these tasks. *)
+  Context {Job : JobType}.
+  Context `{JobTask Job Task}.
+  Context `{JobArrival Job}.
+  Context {jc : JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any kind of fully-supply-consuming, unit-supply
+      processor state model. *)
+  Context `{PState : ProcessorState Job}.
+  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
+  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.
+  Hypothesis H_consumed_supply_proc_model : fully_consuming_proc_model PState.
+
+  (** Consider any valid arrival sequence. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_valid_arrivals : valid_arrival_sequence arr_seq.
+
+  (** Consider any restricted supply uniprocessor schedule of this
+      arrival sequence ... *)
+  Variable sched : schedule PState.
+  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 that the job costs are no larger than the task costs. *)
+  Hypothesis H_valid_job_cost :
+    arrivals_have_valid_job_costs arr_seq.
+
+  (** Consider a task set [ts] ... *)
+  Variable ts : list Task.
+
+  (** ... and a task [tsk] of [ts] that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Consider a valid preemption model ... *)
+  Hypothesis H_valid_preemption_model : valid_preemption_model arr_seq sched.
+
+  (** ... with valid task run-to-completion thresholds. That is,
+      [task_rtc tsk] is (1) no bigger than [tsk]'s cost and (2) for
+      any job [j] of task [tsk] [job_rtct j] is bounded by [task_rtct
+      tsk]. *)
+  Hypothesis H_valid_run_to_completion_threshold :
+    valid_task_run_to_completion_threshold arr_seq tsk.
+
+  (** Let [max_arrivals] be a family of valid arrival curves, i.e.,
+      for any task [tsk] in [ts], [max_arrival tsk] is (1) an arrival
+      bound of [tsk], and (2) it is a monotonic function that equals
+      [0] for the empty interval [delta = 0]. *)
+  Context `{MaxArrivals Task}.
+  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.
+  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.
+
+  (** Assume we are provided with functions characterizing
+      interference and interfering workload. *)
+  Context `{Interference Job}.
+  Context `{InterferingWorkload Job}.
+
+  (** Let's define a local name for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** We assume that the scheduler is work-conserving. *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+
+  (** Unlike the more general, underlying theorem
+      [uniprocessor_response_time_bound_restricted_supply], we assume
+      that tasks are sequential. *)
+  Hypothesis H_sequential_tasks : sequential_tasks arr_seq sched.
+  Hypothesis H_interference_and_workload_consistent_with_sequential_tasks :
+    interference_and_workload_consistent_with_sequential_tasks arr_seq sched tsk.
+
+  (** Let [L] be a constant that bounds any busy interval of task [tsk]. *)
+  Variable L : duration.
+  Hypothesis H_busy_interval_exists :
+    busy_intervals_are_bounded_by arr_seq sched tsk L.
+
+  (** Consider a unit SBF valid in busy intervals (w.r.t. task
+      [tsk]). That is, (1) [SBF 0 = 0], (2) for any duration [Δ], the
+      supply produced during a busy-interval prefix of length [Δ] is
+      at least [SBF Δ], and (3) [SBF] makes steps of at most one. *)
+  Context {SBF : SupplyBoundFunction}.
+  Hypothesis H_valid_SBF : valid_busy_sbf arr_seq sched tsk SBF.
+  Hypothesis H_unit_SBF : unit_supply_bound_function SBF.
+
+  (** Next, we assume that [task_intra_IBF] is a bound on intra-supply
+      interference incurred by task [tsk]. That is, [task_intra_IBF]
+      bounds interference ignoring interference due to lack of supply
+      _and_ due to self-interference. *)
+  Variable task_intra_IBF : duration -> duration -> duration.
+  Hypothesis H_interference_inside_reservation_is_bounded :
+    task_intra_interference_is_bounded_by arr_seq sched tsk task_intra_IBF.
+
+  (** We use the function [task_intra_IBF], which satisfies the
+      hypothesis [task_intra_interference_is_bounded_by], to construct
+      a new function [intra_IBF := (task_rbf (A + ε) - task_cost tsk)
+      + task_intra_IBF A Δ] that satisfies the hypothesis
+      [intra_interference_is_bounded_by]. This is needed to later
+      apply the lemma
+      [uniprocessor_response_time_bound_restricted_supply] from file
+      [restricted_supply/abstract_rta] (recall that it requires
+      [intra_IBF], not [task_intra_IBF]). *)
+
+  (** The logic behind [intra_IBF] is quite simple. Consider a job [j]
+      of task [tsk] that arrives exactly [A] units after the beginning
+      of the busy interval. Then the bound on the total interference
+      incurred by [j] within an interval of length [Δ] is no greater
+      than [task_rbf (A + ε) - task_cost tsk + task_intra_IBF A
+      Δ]. Note that, for sequential tasks, the bound consists of two
+      parts: (1) the part that bounds the interference received from
+      other jobs of task [tsk] -- [task_rbf (A + ε) - task_cost tsk]
+      -- and (2) any other interference that is bounded by
+      [task_intra_IBF(tsk, A, Δ)]. *)
+  Let intra_IBF (A Δ : duration) :=
+    (task_rbf (A + ε) - task_cost tsk) + task_intra_IBF A Δ.
+
+  (** For clarity, let's define a local name for the search space. *)
+  Let is_in_search_space_rs := is_in_search_space L intra_IBF.
+
+  (** We use the following equation to bound the response-time of a
+      job of task [tsk]. Consider any value [R] that upper-bounds the
+      solution of each response-time recurrence, i.e., for any
+      relative arrival time [A] in the search space, there exists a
+      corresponding solution [F] such that
+      (1) [F <= A + R],
+      (2) [(task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F],
+      (3) and [SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R)]. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum_seq_rs :
+    forall (A : duration),
+      is_in_search_space_rs A ->
+      exists (F : duration),
+        F <= A + R
+        /\ (task_rbf (A + ε) - (task_cost tsk - task_rtct tsk)) + task_intra_IBF A F <= SBF F
+        /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+
+  (** In the following section we prove that all the premises of
+      [aRSA] are satisfied. *)
+  Section aRSAPremises.
+
+    (** First, we show that [intra_IBF] correctly upper-bounds
+        interference in the preemptive stage of execution. *)
+    Lemma IBF_P_bounds_interference :
+      intra_interference_is_bounded_by arr_seq sched tsk intra_IBF.
+    Proof.
+      move=> t1 t2 Δ j ARR TSK BUSY LT NCOM A PAR; move: (PAR _ _ BUSY) => EQ.
+      have [ZERO|POS] := posnP (@job_cost _ jc j).
+      { exfalso; move: NCOM => /negP NCOM; apply: NCOM.
+        by rewrite /service.completed_by ZERO. }
+      rewrite (cumul_cond_interference_ID _ (nonself arr_seq sched)).
+      rewrite /intra_IBF addnC leq_add; first by done.
+      { rewrite -(leq_add2r (cumul_task_interference arr_seq sched j t1 (t1 + Δ))).
+        eapply leq_trans; first last.
+        { by rewrite EQ; apply: task.cumulative_job_interference_bound => //. }
+        { rewrite -big_split //= leq_sum // /cond_interference  => t _.
+          by case (interference j t), (has_supply sched t), (nonself arr_seq sched j t) => //. } }
+      { rewrite (cumul_cond_interference_pred_eq _ (nonself_intra arr_seq sched)) => //.
+        by move=> s t; split=> //; rewrite andbC. }
+    Qed.
+
+    (** To rule out pathological cases with the
+        [H_R_is_maximum_seq_rs] equation (such as [task_cost tsk]
+        being greater than [task_rbf (A + ε)]), we assume that the
+        arrival curve is non-pathological. *)
+    Hypothesis H_arrival_curve_pos : 0 < max_arrivals tsk ε.
+
+    (** To later apply the theorem
+        [uniprocessor_response_time_bound_restricted_supply], we need
+        to provide the IBF, which bounds the total interference. *)
+    Let IBF A Δ := Δ - SBF Δ + intra_IBF A Δ.
+
+    (** Next we prove that [H_R_is_maximum_seq_rs] implies
+        [H_R_is_maximum_rs] from file ([.../restricted_supply/abstract_rta.v]).
+        In other words, a solution to the response-time recurrence for
+        restricted-supply processor models with sequential tasks can
+        be translated to a solution for the same processor model with
+        non-necessarily sequential tasks. *)
+    Lemma sol_seq_rs_equation_impl_sol_rs_equation :
+      forall (A : duration),
+        is_in_search_space L IBF  A ->
+        exists F : duration,
+          F <= A + R
+          /\ task_rtct tsk + intra_IBF A F <= SBF F
+          /\ SBF F + (task_cost tsk - task_rtct tsk) <= SBF (A + R).
+    Proof.
+      rewrite /IBF; move=> A SP.
+      move: (H_R_is_maximum_seq_rs A) => T.
+      feed T.
+      { move: SP => [ZERO|[POS [x [LT NEQ]]]]; first by left.
+        by right; split => //; exists x; split => //. }
+      have [F [EQ0 [EQ1 EQ2]]] := T; clear T.
+      exists F; split => //; split => //.
+      rewrite /intra_IBF -(leqRW EQ1) addnA leq_add2r.
+      rewrite addnBA; last first.
+      { apply leq_trans with (task_rbf 1).
+        - by apply: task_rbf_1_ge_task_cost => //.
+        - by eapply task_rbf_monotone => //; rewrite addn1. }
+      { rewrite subnBA.
+        - by rewrite addnC.
+        - by apply H_valid_run_to_completion_threshold. }
+    Qed.
+
+  End aRSAPremises.
+
+  (** Finally, we apply the
+      [uniprocessor_response_time_bound_restricted_supply] theorem,
+      and using the lemmas above, prove that all its requirements are
+      satisfied. Hence, [R] is a response-time bound for task [tsk]. *)
+  Theorem uniprocessor_response_time_bound_restricted_supply_seq :
+    task_response_time_bound arr_seq sched tsk R.
+  Proof.
+    move => j ARR TSK.
+    eapply uniprocessor_response_time_bound_restricted_supply => //.
+    { exact: IBF_P_bounds_interference. }
+    { exact: sol_seq_rs_equation_impl_sol_rs_equation. }
+  Qed.
+
+End AbstractRTARestrictedSupplySequential.

analysis/definitions/always_higher_priority.v

+Require Export prosa.model.priority.classes.
+
+(** * Always Higher Priority *)
+(** In this section, we define what it means for a job to always have
+    a higher priority than another job. *)
+Section AlwaysHigherPriority.
+
+  (** Consider any type of jobs ... *)
+  Context {Job : JobType}.
+
+  (** ... and any JLDP policy. *)
+  Context `{JLDP_policy Job}.
+
+  (** We say that a job [j1] always has higher priority than job [j2]
+      if, at any time [t], the priority of job [j1] is strictly higher than
+      the priority of job [j2]. *)
+  Definition always_higher_priority (j1 j2 : Job) :=
+    forall t, hep_job_at t j1 j2 && ~~ hep_job_at t j2 j1.
+
+End AlwaysHigherPriority.
+
+(** We note that, under a job-level fixed-priority policy, the property is
+    trivial since job priorities by definition do not change in this case. *)
+Section UnderJLFP.
+  (** Consider any type of jobs ... *)
+  Context {Job : JobType}.
+
+  (** ... and any JLFP policy. *)
+  Context `{JLFP_policy Job}.
+
+  (** The property [always_higher_priority j j'] is equivalent to a statement
+      about [hep_job]. *)
+  Fact always_higher_priority_jlfp :
+    forall j j',
+      always_higher_priority j j' <-> (hep_job j j' && ~~ hep_job j' j).
+  Proof.
+    by move=> j j'; split => [|HP t]; [apply; exact: 0 | rewrite !hep_job_at_jlfp].
+  Qed.
+
+End UnderJLFP.