FP instantiations

Add instantiations of aRTA for
(1) fully preemptive,
(2) fully non-preemptive,
(3) limited preemptions,
(4) and floating non-preemptive regions FP models

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model Require Import preemption.floating.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for Model with Floating Non-Preemptive Regions *)
+(** In this module we prove the RTA theorem for floating
+    non-preemptive regions FP model. *)
+Section RTAforFloatingModelwithArrivalCurves.
+
+  (** 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 arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Assume we have the model with floating nonpreemptive regions. 
+      I.e., for each task only the length of the maximal nonpreemptive 
+      segment is known _and_ each job level is divided into a number of
+      nonpreemptive segments by inserting preemption points. *)
+  Context `{JobPreemptionPoints Job}
+          `{TaskMaxNonpreemptiveSegment Task}.
+  Hypothesis H_valid_task_model_with_floating_nonpreemptive_regions:
+    valid_model_with_floating_nonpreemptive_regions arr_seq.
+
+  (** Consider an arbitrary task set ts, ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  
+  (** ... and the cost of a job cannot be larger than the task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** 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.
+
+  (** Let tsk be any task in ts that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Next, consider any ideal uniprocessor schedule with limited preemptions 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.
+  Hypothesis H_schedule_with_limited_preemptions:
+    valid_schedule_with_limited_preemptions arr_seq sched.
+  
+  (** ... 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.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+      and assume that the relation is reflexive and transitive. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+
+  (** Assume we have sequential tasks, i.e, jobs from the 
+      same task execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+  
+  (** ... and the schedule respects the policy defined by thejob_preemptable 
+     function (i.e., jobs have bounded nonpreemptive segments). *)
+  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
+  (** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
+  Let blocking_bound :=
+    \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+     (task_max_nonpreemptive_segment tsk_other - ε).
+  
+  (** Let L be any positive fixed point of the busy interval recurrence, determined by 
+      the sum of blocking and higher-or-equal-priority workload. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+  Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
+
+  (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  
+  (** Next, consider any value R, and assume that for any given arrival A from search space
+     there is a solution of the response-time bound recurrence which is bounded by R. *)    
+  Variable R : duration.
+  Hypothesis H_R_is_maximum:
+    forall (A : duration),
+      is_in_search_space A ->
+      exists  (F : duration),
+        A + F = blocking_bound + task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+        F <= R.
+  
+  (** Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+     to establish a response-time bound for the more concrete model with floating nonpreemptive regions.  *)
+  Theorem uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions:
+    response_time_bounded_by tsk R.  
+  Proof.
+    move: (H_valid_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
+    move: (LIMJ) => [BEG [END _]].
+    eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
+    all: eauto 2 with basic_facts.
+    intros A SP.
+    rewrite subnn subn0.
+    destruct (H_R_is_maximum _ SP) as [F [EQ LE]].
+      by exists F; rewrite addn0; split.
+  Qed.
+
+End RTAforFloatingModelwithArrivalCurves.
\ No newline at end of file

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model Require Import preemption.limited.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for FP-schedulers with Fixed Premption Points *)
+(** In this module we prove the RTA theorem for FP-schedulers with fixed preemption points. *)
+Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
+
+  (** 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 arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Consider an arbitrary task set ts, ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  
+  (** ... and the cost of a job cannot be larger than the task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** First, we assume we have the model with fixed preemption points.
+      I.e., each task is divided into a number of nonpreemptive segments 
+      by inserting staticaly predefined preemption points. *)
+  Context `{JobPreemptionPoints Job}
+          `{TaskPreemptionPoints Task}.
+  Hypothesis H_valid_model_with_fixed_preemption_points:
+    valid_fixed_preemption_points_model arr_seq ts.
+
+  (** 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.
+
+  (** Let tsk be any task in ts that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Next, consider any ideal uniprocessor schedule  with limited preemptionsof 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.
+  Hypothesis H_valid_schedule_with_limited_preemptions:
+    valid_schedule_with_limited_preemptions arr_seq sched.
+
+  (** ... 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.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+     and assume that the relation is reflexive and transitive. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+  
+  (** Assume we have sequential tasks, i.e, jobs from the 
+     same task execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+  
+  (** ... and the schedule respects the policy defined by thejob_preemptable 
+     function (i.e., jobs have bounded nonpreemptive segments). *)
+  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
+  (** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
+  Let blocking_bound :=
+    \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+     (task_max_nonpreemptive_segment tsk_other - ε).
+
+  (** Let L be any positive fixed point of the busy interval recurrence, determined by 
+     the sum of blocking and higher-or-equal-priority workload. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+  Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
+
+  (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+  (** Next, consider any value R, and assume that for any given arrival A from search space
+      there is a solution of the response-time bound recurrence which is bounded by R. *)    
+  Variable R: nat.
+  Hypothesis H_R_is_maximum:
+    forall (A : duration),
+      is_in_search_space A ->
+      exists (F : duration),
+        A + F = blocking_bound
+                + (task_rbf (A + ε) - (task_last_nonpr_segment tsk - ε))
+                + total_ohep_rbf (A + F) /\
+        F + (task_last_nonpr_segment tsk - ε) <= R.
+        
+  (** Now, we can reuse the results for the abstract model with bounded nonpreemptive segments
+     to establish a response-time bound for the more concrete model of fixed preemption points. *)
+  Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
+    response_time_bounded_by tsk R.  
+  Proof.
+    move: (H_valid_model_with_fixed_preemption_points) => [MLP [BEG [END [INCR [HYP1 [HYP2 HYP3]]]]]].
+    move: (MLP) => [BEGj [ENDj _]].
+    edestruct (posnP (task_cost tsk)) as [ZERO|POSt].
+    { intros j ARR TSK.
+      move: (H_job_cost_le_task_cost _ ARR) => POSt.
+      move: POSt; rewrite /job_cost_le_task_cost TSK ZERO leqn0; move => /eqP Z.
+        by rewrite /job_response_time_bound /completed_by Z.
+    }
+    eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
+      with (L0 := L).
+    all: eauto 2 with basic_facts.
+    intros A SP.
+    destruct (H_R_is_maximum _ SP) as[FF [EQ1 EQ2]].
+    exists FF; rewrite subKn; first by done. 
+    rewrite /task_last_nonpr_segment  -(leq_add2r 1) subn1 !addn1 prednK; last first.
+    - rewrite /last0 -nth_last.
+      apply HYP3; try by done. 
+      rewrite -(ltn_add2r 1) !addn1 prednK //.
+      move: (number_of_preemption_points_in_task_at_least_two
+               _ _ H_valid_model_with_fixed_preemption_points _ H_tsk_in_ts POSt) => Fact2.
+      move: (Fact2) => Fact3.
+        by rewrite size_of_seq_of_distances // addn1 ltnS // in Fact2.
+    - apply leq_trans with (task_max_nonpreemptive_segment tsk).
+      + by apply last_of_seq_le_max_of_seq.
+      + rewrite -END; last by done.
+        apply ltnW; rewrite ltnS; try done.
+          by apply max_distance_in_seq_le_last_element_of_seq; eauto 2.
+  Qed.
+    
+End RTAforFixedPreemptionPointsModelwithArrivalCurves.

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
+
+(** Assume we have a fully non-preemptive model. *)
+From rt.restructuring.model Require Import preemption.nonpreemptive.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for Fully Non-Preemptive FP Model *)
+(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
+Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
+
+  (** 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 arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Consider an arbitrary task set ts, ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  
+  (** ... and the cost of a job cannot be larger than the task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** 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.
+
+  (** Let tsk be any task in ts that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Next, consider any ideal non-preemptive uniprocessor 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.
+  Hypothesis H_nonpreemptive_sched : is_nonpreemptive_schedule sched.
+
+  (** ... 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.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+     and assume that the relation is reflexive and transitive. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.  
+
+  (** Assume we have sequential tasks, i.e, tasks from the same task
+      execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Next, we assume that the schedule is a work-conserving schedule ... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+  
+  (** ... and the schedule respects the policy defined by the
+     [job_preemptable] function (i.e., jobs have bounded nonpreemptive
+     segments). *)
+  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.    
+
+  (** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
+  Let blocking_bound :=
+    \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk) (task_cost tsk_other - ε).
+  
+  (** Let L be any positive fixed point of the busy interval recurrence, determined by 
+      the sum of blocking and higher-or-equal-priority workload. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+  Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
+
+  (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  
+  (** Next, consider any value R, and assume that for any given arrival A from search space
+      there is a solution of the response-time bound recurrence which is bounded by R. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum:
+    forall (A : duration),
+      is_in_search_space A -> 
+      exists (F : duration),
+        A + F = blocking_bound
+                + (task_rbf (A + ε) - (task_cost tsk - ε))
+                + total_ohep_rbf (A + F) /\
+        F + (task_cost tsk - ε) <= R.
+  
+  (** Now, we can leverage the results for the abstract model with
+      bounded nonpreemptive segments to establish a response-time
+      bound for the more concrete model of fully nonpreemptive
+      scheduling. *)
+  Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp:
+    response_time_bounded_by tsk R.
+  Proof.
+    move: (posnP (@task_cost _ H tsk)) => [ZERO|POS].
+    { intros j ARR TSK.
+      have ZEROj: job_cost j = 0.
+      { move: (H_job_cost_le_task_cost j ARR) => NEQ.
+        rewrite /job_cost_le_task_cost TSK ZERO in NEQ.
+          by apply/eqP; rewrite -leqn0.
+      }
+        by rewrite /job_response_time_bound /completed_by ZEROj.
+    }
+    eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
+        (L0 := L).
+    all: eauto 2 with basic_facts. 
+  Qed.
+
+End RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
\ No newline at end of file

restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis.fixed_priority.rta Require Import nonpr_reg.response_time_bound.
+
+(** Assume we have a fully preemptive model. *)
+From rt.restructuring.model Require Import preemption.preemptive.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for Fully Preemptive FP Model *)
+(** In this module we prove the RTA theorem for fully preemptive FP model. *)
+Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
+
+  (** 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 arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Consider an arbitrary task set ts, ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  
+  (** ... and the cost of a job cannot be larger than the task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+
+  (** 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.
+
+  (** Let tsk be any task in ts that is to be analyzed. *)
+  Variable tsk : Task.
+  Hypothesis H_tsk_in_ts : tsk \in ts.
+
+  (** Next, consider any ideal uniprocessor 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 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.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+     and assume that the relation is reflexive and transitive. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+
+  (** Assume we have sequential tasks, i.e, tasks from the 
+     same task execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+  
+  (** ... and the schedule respects the policy defined by thejob_preemptable 
+     function (i.e., jobs have bounded nonpreemptive segments). *)
+  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.  
+
+  (** Let's define some local names for clarity. *)
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+  
+  (** Let L be any positive fixed point of the busy interval recurrence, determined by 
+      the sum of blocking and higher-or-equal-priority workload. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+  Hypothesis H_fixed_point : L = total_hep_rbf L.
+
+  (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+  Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+  
+  (** Next, consider any value R, and assume that for any given arrival A from search space
+       there is a solution of the response-time bound recurrence which is bounded by R. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum:
+    forall (A : duration),
+      is_in_search_space A -> 
+      exists (F : duration),
+        A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
+        F <= R.
+
+  (** Now, we can leverage the results for the abstract model with bounded nonpreemptive segments
+       to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
+  Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
+    response_time_bounded_by tsk R.
+  Proof.
+    have BLOCK: blocking_bound  higher_eq_priority ts tsk = 0.
+    { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
+               /preemptive.fully_preemptive_model subnn big1_eq. } 
+    eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.      
+    all: eauto 2 with basic_facts.
+    - by rewrite BLOCK add0n.
+    - move => A /andP [LT NEQ].
+      edestruct H_R_is_maximum as [F [FIX BOUND]].
+      { by apply/andP; split; eauto 2. }
+      exists F; split.
+      + by rewrite BLOCK add0n subnn subn0.
+      + by rewrite subnn addn0.
+  Qed.
+  
+End RTAforFullyPreemptiveFPModelwithArrivalCurves. 

restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model.preemption Require Import valid_model
+     job.parameters task.parameters rtc_threshold.valid_rtct.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis.fixed_priority Require Export rta.response_time_bound.
+From rt.restructuring.analysis.facts Require Import priority_inversion_is_bounded.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * RTA for FP-schedulers with Bounded Non-Preemprive Segments *)
+
+(** In this section we instantiate the Abstract RTA for FP-schedulers
+    with Bounded Priority Inversion to FP-schedulers for ideal
+    uni-processor model of real-time tasks with arbitrary
+    arrival models _and_ bounded non-preemprive segments. *)
+
+(** Recall that Abstract RTA for FP-schedulers with Bounded Priority
+    Inversion does not specify the cause of priority inversion. In
+    this section, we prove that the priority inversion caused by
+    execution of non-preemptive segments is bounded. Thus the Abstract
+    RTA for FP-schedulers is applicable to this instantiation. *)
+Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
+
+  (** Consider any type of tasks ... *)
+  Context {Task : TaskType}.
+  Context `{TaskCost Task}.
+  Context `{TaskRunToCompletionThreshold Task}. 
+  Context `{TaskMaxNonpreemptiveSegment 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 arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+
+  (** Next, consider any ideal uniprocessor 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 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.
+  
+  (** In addition, we assume the existence of a function maping jobs
+      to theirs preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (** ... and assume that it defines a valid preemption
+      model with bounded nonpreemptive segments. *)
+  Hypothesis H_valid_model_with_bounded_nonpreemptive_segments:
+    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+  (** Consider an FP policy that indicates a higher-or-equal priority
+      relation, and assume that the relation is reflexive and
+      transitive. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  Hypothesis H_priority_is_transitive : transitive_priorities.
+  
+  (** Assume we have sequential tasks, i.e, jobs from the same task
+      execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Next, we assume that the schedule is a work-conserving schedule... *)
+  Hypothesis H_work_conserving : work_conserving arr_seq sched.
+  
+  (** ... and the schedule respects the policy defined by thejob_preemptable 
+     function (i.e., jobs have bounded nonpreemptive segments). *)
+  Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
+  
+  (** Consider an arbitrary task set ts, ... *)
+  Variable ts : list Task.
+
+  (** ... assume that all jobs come from the task set, ... *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+  
+  (** ... and the cost of a job cannot be larger than the task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+  
+  (** 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.
+  
+  (** Let tsk be any task in 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_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
+     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     is bounded by task_run_to_completion_threshold. *)
+  Hypothesis H_valid_run_to_completion_threshold:
+    valid_task_run_to_completion_threshold arr_seq tsk.
+  
+  (** Let's define some local names for clarity. *)
+  Let max_length_of_priority_inversion :=
+    max_length_of_priority_inversion arr_seq _.
+  Let task_rbf := task_request_bound_function tsk.
+  Let total_hep_rbf := total_hep_request_bound_function_FP _ ts tsk.
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP _ ts tsk.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+  
+  (** We also define a bound for the priority inversion caused by jobs with lower priority. *)
+  Definition blocking_bound :=
+    \max_(tsk_other <- ts | ~~ higher_eq_priority tsk_other tsk)
+     (task_max_nonpreemptive_segment tsk_other - ε).
+  
+  (** ** Priority inversion is bounded *)
+  (** In this section, we prove that a priority inversion for task tsk is bounded by 
+      the maximum length of nonpreemtive segments among the tasks with lower priority. *)
+  Section PriorityInversionIsBounded.
+
+    (** First, we prove that the maximum length of a priority inversion of a job j is 
+       bounded by the maximum length of a nonpreemptive section of a task with 
+       lower-priority task (i.e., the blocking term). *)
+    Lemma priority_inversion_is_bounded_by_blocking:
+      forall j t, 
+        arrives_in arr_seq j ->
+        job_task j = tsk -> 
+        max_length_of_priority_inversion j t <= blocking_bound.
+    Proof.
+      intros j t ARR TSK.
+      rewrite /max_length_of_priority_inversion /blocking_bound /FP_to_JLFP
+              /priority_inversion_is_bounded.max_length_of_priority_inversion.
+      apply leq_trans with
+          (\max_(j_lp <- arrivals_between arr_seq 0 t
+                | ~~ higher_eq_priority (job_task j_lp) tsk)
+            (task_max_nonpreemptive_segment (job_task j_lp) - ε)).
+      { rewrite TSK.
+        apply leq_big_max.
+        intros j' JINB NOTHEP.
+        rewrite leq_sub2r //.
+        apply H_valid_model_with_bounded_nonpreemptive_segments.
+          by eapply in_arrivals_implies_arrived; eauto 2.
+      }
+      { apply /bigmax_leq_seqP. 
+        intros j' JINB NOTHEP.
+        apply leq_bigmax_cond_seq with
+            (i0 := (job_task j')) (F := fun tsk => task_max_nonpreemptive_segment tsk - 1); last by done.
+        apply H_all_jobs_from_taskset.
+        apply mem_bigcat_nat_exists in JINB.
+          by inversion JINB as [ta' [JIN' _]]; exists ta'.
+      }
+    Qed.
+    
+    (** Using the above lemma, we prove that the priority inversion of the task is bounded by blocking_bound. *) 
+    Lemma priority_inversion_is_bounded:
+      priority_inversion_is_bounded_by
+        arr_seq sched _ tsk blocking_bound.
+    Proof.
+      intros j ARR TSK POS t1 t2 PREF.
+      case NEQ: (t2 - t1 <= blocking_bound). 
+      { apply leq_trans with (t2 - t1); last by done.
+        rewrite /cumulative_priority_inversion /is_priority_inversion.
+        rewrite -[X in _ <= X]addn0 -[t2 - t1]mul1n -iter_addn -big_const_nat leq_sum //. 
+        intros t _; case: (sched t); last by done.
+          by intros s; case: (FP_to_JLFP Job Task s j). 
+      } 
+      move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
+      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2; move: NEQ => /andP [GE LE].
+      apply leq_trans with (cumulative_priority_inversion sched _ j t1 ppt);
+        last apply leq_trans with (ppt - t1); first last.
+      - rewrite leq_subLR.
+        apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+          by rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+      - rewrite /cumulative_priority_inversion /is_priority_inversion.
+        rewrite -[X in _ <= X]addn0 -[ppt - t1]mul1n -iter_addn -big_const_nat. 
+        rewrite leq_sum //; intros t _; case: (sched t); last by done.
+          by intros s; case: (FP_to_JLFP Job Task s j).
+      - rewrite /cumulative_priority_inversion /is_priority_inversion. 
+        rewrite (@big_cat_nat _ _ _ ppt) //=; last first.
+        { rewrite ltn_subRL in BOUND.
+          apply leq_trans with (t1 + blocking_bound); last by apply ltnW. 
+          apply leq_trans with (t1 + max_length_of_priority_inversion j t1); first by done.
+          rewrite leq_add2l; eapply priority_inversion_is_bounded_by_blocking; eauto 2.
+        }
+        rewrite -[X in _ <= X]addn0 leq_add2l leqn0.
+        rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ].
+        case SCHED: (sched t) => [s | ]; last by done.
+        edestruct (@not_quiet_implies_exists_scheduled_hp_job)
+          with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2.
+        { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. } 
+        { by rewrite subnKC //; apply/andP; split. }
+        apply/eqP; rewrite eqb0 Bool.negb_involutive.
+        enough (EQef : s = j_hp); first by subst;auto.
+        eapply ideal_proc_model_is_a_uniprocessor_model; eauto 2.
+          by rewrite scheduled_at_def SCHED.
+    Qed.
+    
+  End PriorityInversionIsBounded. 
+
+  (** ** Response-Time Bound *)
+  (** In this section, we prove that the maximum among the solutions of the response-time 
+      bound recurrence is a response-time bound for tsk. *)
+  Section ResponseTimeBound.
+
+    (** Let L be any positive fixed point of the busy interval recurrence. *)
+    Variable L : duration.
+    Hypothesis H_L_positive : L > 0.
+    Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
+
+    (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+    Let is_in_search_space (A : duration) := (A < L) && (task_rbf A != task_rbf (A + ε)).
+    
+    (** Next, consider any value R, and assume that for any given arrival offset A from the search 
+       space there is a solution of the response-time bound recurrence that is bounded by R. *)
+    Variable R : duration.
+    Hypothesis H_R_is_maximum:
+      forall (A : duration), 
+        is_in_search_space A -> 
+        exists (F : duration),
+          A + F = blocking_bound
+                  + (task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk))
+                  + total_ohep_rbf (A + F) /\
+          F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
+
+    (** Then, using the results for the general RTA for FP-schedulers, we establish a 
+       response-time bound for the more concrete model of bounded nonpreemptive segments. 
+       Note that in case of the general RTA for FP-schedulers, we just _assume_ that 
+       the priority inversion is bounded. In this module we provide the preemption model
+       with bounded nonpreemptive segments and _prove_ that the priority inversion is 
+       bounded. *)
+    Theorem uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments:
+      response_time_bounded_by tsk R.
+    Proof.
+      eapply uniprocessor_response_time_bound_fp;
+        eauto using priority_inversion_is_bounded. 
+    Qed.
+    
+  End ResponseTimeBound.
+  
+End RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.

restructuring/analysis/fixed_priority/rta/response_time_bound.v

+From rt.util Require Import all.
+From rt.restructuring.behavior Require Import all.
+From rt.restructuring.analysis.basic_facts Require Import all.
+From rt.restructuring.model Require Import job task workload processor.ideal readiness.basic.
+From rt.restructuring.model.arrival Require Import arrival_curves.
+From rt.restructuring.model.preemption Require Import valid_model
+     job.parameters task.parameters rtc_threshold.valid_rtct.
+From rt.restructuring.model.schedule Require Import
+     work_conserving priority_based.priorities priority_based.preemption_aware.
+From rt.restructuring.analysis.arrival Require Import workload_bound rbf.
+From rt.restructuring.analysis Require Export schedulability.
+From rt.restructuring.analysis.definitions Require Export busy_interval priority_inversion.
+From rt.restructuring.analysis.facts Require Export busy_interval_exists.
+From rt.restructuring.analysis.abstract Require Import
+     core.definitions core.abstract_seq_rta instantiations.ideal_processor.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
+(** In this module we instantiate the Abstract Response-Time analysis
+    (aRTA) to FP-schedulers for ideal uni-processor model of
+    real-time tasks with arbitrary arrival models. *)
+
+(** Given FP priority policy and an ideal uni-processor scheduler
+    model, we can explicitly specify [interference],
+    [interfering_workload], and [interference_bound_function]. In this
+    settings, we can define natural notions of service, workload, busy
+    interval, etc. The important feature of this instantiation is that
+    we can induce the meaningful notion of priority
+    inversion. However, we do not specify the exact cause of priority
+    inversion (as there may be different reasons for this, like
+    execution of a non-preemptive segment or blocking due to resource
+    locking). We only assume that that a priority inversion is
+    bounded. *)
+Section AbstractRTAforFPwithArrivalCurves.
+
+  (** 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 `{JobCost Job}.
+  Context `{JobPreemptable Job}.
+
+  (** Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+  Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.
+  
+  (** Next, consider any ideal uniprocessor 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 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.
+
+  (** Note that we differentiate between abstract and 
+     classical notions of work conserving schedule. *)
+  Let work_conserving_ab := definitions.work_conserving arr_seq sched.
+  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 we have sequential tasks, i.e, jobs from the 
+     same task execute in the order of their arrival. *)
+  Hypothesis H_sequential_tasks : sequential_tasks sched.
+
+  (** Assume that a job cost cannot be larger than a task cost. *)
+  Hypothesis H_job_cost_le_task_cost:
+    cost_of_jobs_from_arrival_sequence_le_task_cost arr_seq.
+  
+  (** Consider an arbitrary task set ts. *)    
+  Variable ts : list Task.
+
+  (** Next, we assume that all jobs come from the task set. *)
+  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.
+ 
+  (** 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.
+    
+  (** Let tsk be any task in 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_run_to_completion_threshold tsk] is (1) no bigger than tsk's 
+     cost, (2) for any job of task tsk job_run_to_completion_threshold 
+     is bounded by task_run_to_completion_threshold. *)
+  Hypothesis H_valid_run_to_completion_threshold:
+    valid_task_run_to_completion_threshold arr_seq tsk.
+  
+  (** Consider an FP policy that indicates a higher-or-equal priority relation,
+     and assume that the relation is reflexive. Note that we do not relate 
+     the FP policy with the scheduler. However, we define functions for 
+     Interference and Interfering Workload that actively use the concept of 
+     priorities. We require the FP policy to be reflexive, so a job cannot 
+     cause lower-priority interference (i.e. priority inversion) to itself. *)
+  Variable higher_eq_priority : FP_policy Task.
+  Hypothesis H_priority_is_reflexive : reflexive_priorities.
+  
+  (** For clarity, let's define some local names. *)
+  Let job_pending_at := pending sched.
+  Let job_scheduled_at := scheduled_at sched.
+  Let job_completed_by := completed_by sched.
+  Let job_backlogged_at := backlogged sched.
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
+  (** We introduce task_rbf as an abbreviation of the task request bound function,
+     which is defined as [task_cost(tsk) × max_arrivals(tsk,Δ)]. *)
+  Let task_rbf := task_request_bound_function tsk.
+
+  (** Using the sum of individual request bound functions, we define the request bound 
+     function of all tasks with higher-or-equal priority (with respect to tsk). *)
+  Let total_hep_rbf := total_hep_request_bound_function_FP higher_eq_priority ts tsk.
+ 
+  (** Similarly, we define the request bound function of all tasks other 
+     than tsk with higher-or-equal priority (with respect to tsk). *)
+  Let total_ohep_rbf :=
+    total_ohep_request_bound_function_FP higher_eq_priority ts tsk.
+  
+  (** Assume that there eixsts a constant priority_inversion_bound that bounds 
+     the length of any priority inversion experienced by any job of tsk. 
+     Sinse we analyze only task tsk, we ignore the lengths of priority 
+     inversions incurred by any other tasks. *)
+  Variable priority_inversion_bound : duration.
+  Hypothesis H_priority_inversion_is_bounded:
+    priority_inversion_is_bounded_by
+      arr_seq sched hep_job tsk priority_inversion_bound.
+
+  (** Let L be any positive fixed point of the busy interval recurrence. *)
+  Variable L : duration.
+  Hypothesis H_L_positive : L > 0.
+  Hypothesis H_fixed_point : L = priority_inversion_bound + total_hep_rbf L.
+
+  (** To reduce the time complexity of the analysis, recall the notion of search space.
+     Intuitively, this corresponds to all "interesting" arrival offsets that the job under
+     analysis might have with regard to the beginning of its busy-window. *)
+  Let is_in_search_space A := (A < L) && (task_rbf A != task_rbf (A + ε)).
+
+  (** Let R be a value 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 [F + (task cost - task lock-in service) <= R]. *)
+  Variable R : duration.
+  Hypothesis H_R_is_maximum : 
+    forall (A : duration),
+      is_in_search_space A -> 
+      exists (F : duration),
+        A + F = priority_inversion_bound
+                + (task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk))
+                + total_ohep_rbf (A + F) /\
+        F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
+
+  (** 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. *)
+  Let interference (j : Job) (t : instant) :=
+    ideal_processor.interference sched 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. *)
+  Let interfering_workload (j : Job) (t : instant) :=
+    ideal_processor.interfering_workload
+      arr_seq sched (@FP_to_JLFP Job Task H1 higher_eq_priority) j t.
+  
+  (** Finally, we define the interference bound function as the sum of the priority 
+      interference bound and the higher-or-equal-priority workload. *)
+  Let IBF (R : duration) := priority_inversion_bound + total_ohep_rbf R.
+
+  (** ** Filling Out Hypotheses Of Abstract RTA Theorem *)
+  (** In this section we prove that all preconditions necessary to use the abstract theorem are satisfied. *)
+  Section FillingOutHypothesesOfAbstractRTATheorem.
+
+    (** First, we prove that in the instantiation of interference and interfering workload, 
+       we really take into account everything that can interfere with tsk's jobs, and thus, 
+       the scheduler satisfies the abstract notion of work conserving schedule. *) 
+    Lemma instantiated_i_and_w_are_consistent_with_schedule:
+      work_conserving_ab tsk interference interfering_workload.
+    Proof.
+      intros j t1 t2 t ARR TSK POS BUSY NEQ; split; intros HYP.
+      - move: HYP => /negP.
+        rewrite negb_or /is_priority_inversion /is_priority_inversion
+                /is_interference_from_another_hep_job.
+        move => /andP [HYP1 HYP2].
+        case SCHED: (sched t) => [s | ].
+        + rewrite SCHED in HYP1, HYP2.
+          move: HYP1 HYP2. 
+          rewrite !Bool.negb_involutive negb_and Bool.negb_involutive.
+          move => HYP1 /orP [/negP HYP2| /eqP HYP2].
+          * by exfalso.
+          * by subst s; rewrite scheduled_at_def //; apply eqprop_to_eqbool.
+        + exfalso; clear HYP1 HYP2.
+          eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
+            by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
+                              eauto 2 using eqprop_to_eqbool.
+      - move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
+        rewrite /interference /ideal_processor.interference /is_priority_inversion
+                  /is_interference_from_another_hep_job HYP2 negb_or.
+         apply/andP; split.
+         + rewrite Bool.negb_involutive; eauto 2.
+             by eapply H_priority_is_reflexive with (t := 0).
+         + by rewrite negb_and Bool.negb_involutive; apply/orP; right.
+    Qed.
+
+    (** Next, we prove that the interference and interfering workload 
+       functions 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.
+      intros j t1 t2 ARR TSK POS BUSY. 
+      eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
+      eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2; intros s ARRs TSKs.
+      move: (BUSY) => [[_ [QT _]] _].
+      apply QT.
+      - by apply in_arrivals_implies_arrived in ARRs.
+      - move: TSKs => /eqP TSKs.
+        rewrite /FP_to_JLFP TSK -TSKs; eauto 2.
+          by eapply H_priority_is_reflexive with (t := 0).
+      - by eapply in_arrivals_implies_arrived_before; eauto 2.
+    Qed.
+
+    (** Recall that L is assumed to be a fixed point of the busy interval recurrence. Thanks to
+       this fact, we can prove that every busy interval (according to the concrete definition) 
+       is bounded. In addition, we know that the conventional concept of busy interval and the 
+       one obtained from the abstract definition (with the interference and interfering 
+       workload) coincide. Thus, it follows that any busy interval (in the abstract sense) 
+       is bounded. *)
+    Lemma instantiated_busy_intervals_are_bounded:
+      busy_intervals_are_bounded_by arr_seq sched tsk interference interfering_workload L.
+    Proof.
+      intros j ARR TSK POS.
+      edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2.
+      { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
+      exists t1, t2; split; first by done.
+      split.
+      - by done.
+      - by eapply instantiated_busy_interval_equivalent_edf_busy_interval; eauto 2 with basic_facts.
+    Qed.
+
+    (** Next, we prove that IBF is indeed an interference bound.
+
+       Recall that in module abstract_seq_RTA hypothesis task_interference_is_bounded_by expects 
+       to receive a function that maps some task t, the relative arrival time of a job j of task t, 
+       and the length of the interval to the maximum amount of interference (for more details see 
+       files limited.abstract_RTA.definitions and limited.abstract_RTA.abstract_seq_rta).
+
+       However, in this module we analyze only one task -- tsk, therefore it is “hardcoded” 
+       inside the interference bound function IBF. Moreover, in case of a model with fixed 
+       priorities, interference that some job j incurs from higher-or-equal priority jobs does not
+       depend on the relative arrival time of job j. Therefore, in order for the IBF signature to
+       match the required signature in module abstract_seq_RTA, we wrap the IBF function in a 
+       function that accepts, but simply ignores, the task and the relative arrival time. *)
+    Lemma instantiated_task_interference_is_bounded:
+      task_interference_is_bounded_by
+        arr_seq sched tsk interference interfering_workload (fun t A R => IBF R).
+    Proof.
+      intros ? ? ? ? ARR TSK ? NCOMPL BUSY; simpl.
+      move: (posnP (@job_cost _ H3 j)) => [ZERO|POS].
+      { by exfalso; rewrite /completed_by ZERO in  NCOMPL. }
+      eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto 2 with basic_facts.
+      rewrite /interference; erewrite cumulative_task_interference_split; eauto 2 with basic_facts; last first.
+      { move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
+          by eapply arrived_between_implies_in_arrivals; eauto 2. }
+      unfold IBF, interference.
+      apply respects_sequential_tasks; by done.
+      rewrite leq_add; try done. 
+      { move: (H_priority_inversion_is_bounded j ARR TSK) => BOUND.
+        apply leq_trans with (cumulative_priority_inversion sched _ j t1 (t1 + R0)); first by done.
+        apply leq_trans with (cumulative_priority_inversion sched _ j t1 t2); last first.
+        { by apply BOUND; move: BUSY => [PREF QT2]. }
+        rewrite [X in _ <= X](@big_cat_nat _ _ _ (t1 + R0)) //=.
+        - by rewrite leq_addr.
+        - by rewrite leq_addr.
+        - by rewrite ltnW.
+      }
+      { erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
+          eauto 2; last by unfold quiet_time; move: BUSY => [[_ [T1 T2]] _]. 
+        apply leq_trans with
+            (workload_of_jobs
+               (fun jhp : Job => (FP_to_JLFP _ _) jhp j && (job_task jhp != job_task j))
+               (arrivals_between arr_seq t1 (t1 + R0))
+            ).
+        { by apply service_of_jobs_le_workload; last apply ideal_proc_model_provides_unit_service.  }
+        { rewrite  /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
+            by rewrite -TSK; apply total_workload_le_total_rbf.
+        }
+      }
+    Qed.
+
+    (** Finally, we show that there exists a solution for the response-time recurrence. *)
+    Section SolutionOfResponseTimeReccurenceExists.
+
+      (** Consider any job j of tsk. *)
+      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 j.
+
+      (** Given any job j of task tsk that arrives exactly A units after the beginning of 
+         the busy interval, the bound of the total interference incurred by j within an 
+         interval of length Δ is equal to [task_rbf (A + ε) - task_cost tsk + IBF Δ]. *)
+      Let total_interference_bound tsk A Δ :=
+        task_rbf (A + ε) - task_cost tsk + IBF Δ.
+
+      (** Next, consider any A from the search space (in the abstract sence). *)
+      Variable A : duration.
+      Hypothesis H_A_is_in_abstract_search_space :
+        reduction_of_search_space.is_in_search_space tsk L total_interference_bound A. 
+      
+      (** We prove that A is also in the concrete search space. *)
+      Lemma A_is_in_concrete_search_space:
+        is_in_search_space A.
+      Proof.
+        move: H_A_is_in_abstract_search_space => [INSP | [/andP [POSA LTL] [x [LTx INSP2]]]].
+        - rewrite INSP.
+          apply/andP; split; first by done.
+          rewrite neq_ltn; apply/orP; left.
+          rewrite {1}/task_rbf; erewrite task_rbf_0_zero; eauto 2; try done.
+          rewrite add0n /task_rbf; apply leq_trans with (task_cost tsk).
+          + by apply leq_trans with (job_cost j); rewrite -?H_job_of_tsk; eauto 2.
+          + eapply task_rbf_1_ge_task_cost; eauto 2.
+        - apply/andP; split; first by done.
+          apply/negP; intros EQ; move: EQ => /eqP EQ.
+          apply INSP2.
+          unfold total_interference_bound in *.
+          rewrite subn1 addn1 prednK; last by done.              
+            by rewrite -EQ.
+      Qed.
+
+      (** Then, there exists a solution for the response-time recurrence (in the abstract sense). *)
+      Corollary correct_search_space:
+        exists (F : duration),
+          A + F = task_rbf (A + ε) - (task_cost tsk - task_run_to_completion_threshold tsk) + IBF (A + F) /\
+          F + (task_cost tsk - task_run_to_completion_threshold tsk) <= R.
+      Proof.
+        move: (H_R_is_maximum A) => FIX.
+        feed FIX; first by apply A_is_in_concrete_search_space. 
+        move: FIX => [F [FIX NEQ]].
+        exists F; split; last by done.
+        apply/eqP; rewrite {1}FIX.
+          by rewrite addnA [_ + priority_inversion_bound]addnC -!addnA.
+      Qed.
+
+    End SolutionOfResponseTimeReccurenceExists.
+
+  End FillingOutHypothesesOfAbstractRTATheorem.
+
+  (** ** Final Theorem *)
+  (** Based on the properties established above, we apply the abstract analysis 
+     framework to infer that R is a response-time bound for tsk. *) 
+  Theorem uniprocessor_response_time_bound_fp:
+    response_time_bounded_by tsk R.
+  Proof.
+    intros js ARRs TSKs.
+    move: (posnP (@job_cost _ H3 js)) => [ZERO|POS].
+    { by rewrite /job_response_time_bound /completed_by ZERO. }
+    eapply uniprocessor_response_time_bound_seq; eauto 3.
+    - by apply instantiated_i_and_w_are_consistent_with_schedule. 
+    - by apply instantiated_interference_and_workload_consistent_with_sequential_tasks. 
+    - by apply instantiated_busy_intervals_are_bounded.
+    - by apply instantiated_task_interference_is_bounded.
+    - by eapply correct_search_space; eauto 2. 
+  Qed.
+    
+End AbstractRTAforFPwithArrivalCurves.