improve structure of FP response-time analysis results

results/fixed_priority/rta/floating_nonpreemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** * RTA for Model with Floating Non-Preemptive Regions *)
+(** In this module we prove the RTA theorem for floating non-preemptive regions FP model. *)
+
+(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.basic.
 
-(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
+(** Furthermore, we assume the task model with floating non-preemptive regions. *)
 Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.floating_nonpreemptive.
 
-(** * RTA for Model with Floating Non-Preemptive Regions *)
-(** In this module we prove the RTA theorem for floating
-    non-preemptive regions FP model. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFloatingModelwithArrivalCurves.
 
   (** Consider any type of tasks ... *)
@@ -89,12 +92,25 @@ Section RTAforFloatingModelwithArrivalCurves.
   (** ... and the schedule respects the policy defined by the [job_preemptable] 
      function (i.e., jobs have bounded non-preemptive 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.
+
+  (** ** Total Workload and Length of Busy Interval *)
+
+  (** We introduce the abbreviation [rbf] for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+  Let rbf := task_request_bound_function.
+
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
+  Let task_rbf := rbf tsk.
+
+  (** Using the sum of individual request bound functions, we define
+      the request bound function of all tasks with higher priority
+      ... *)
   Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+
+  (** ... and the request bound function of all tasks with higher
+      priority other than task [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 :=
@@ -107,11 +123,14 @@ Section RTAforFloatingModelwithArrivalCurves.
   Hypothesis H_L_positive : L > 0.
   Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
 
+  (** ** Response-Time Bound *)
+
   (** 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. *)    
+  (** 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),
@@ -120,8 +139,13 @@ Section RTAforFloatingModelwithArrivalCurves.
         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.  *)
+  (** 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.  *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
   Theorem uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions:
     response_time_bounded_by tsk R.  
   Proof.

results/fixed_priority/rta/fully_nonpreemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** * RTA for Fully Non-Preemptive FP Model *)
+(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
+
+(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.basic.
 
-(** Throughout this file, we assume the fully non-preemptive task model. *)
+(** Furthermore, we assume the fully non-preemptive task model. *)
 Require Import prosa.model.task.preemption.fully_nonpreemptive.
 
-(** * RTA for Fully Non-Preemptive FP Model *)
-(** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
 
   (** Consider any type of tasks ... *)
@@ -69,13 +73,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Context `{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.
@@ -88,6 +86,25 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
      segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.    
 
+  (** ** Total Workload and Length of Busy Interval *)
+
+  (** We introduce the abbreviation [rbf] for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+  Let rbf := task_request_bound_function.
+
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
+  Let task_rbf := rbf tsk.
+
+  (** Using the sum of individual request bound functions, we define
+      the request bound function of all tasks with higher priority
+      ... *)
+  Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+
+  (** ... and the request bound function of all tasks with higher
+      priority other than task [tsk]. *)
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
+  
   (** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
   Let blocking_bound :=
     \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk) (task_cost tsk_other - ε).
@@ -98,9 +115,11 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_L_positive : L > 0.
   Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
 
+  (** ** Response-Time Bound *)
+  
   (** 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.
@@ -117,6 +136,9 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
       bounded nonpreemptive segments to establish a response-time
       bound for the more concrete model of fully nonpreemptive
       scheduling. *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+  
   Theorem uniprocessor_response_time_bound_fully_nonpreemptive_fp:
     response_time_bounded_by tsk R.
   Proof.

results/fixed_priority/rta/fully_preemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** * RTA for Fully Preemptive FP Model *)
+(** In this section we prove the RTA theorem for the fully preemptive FP model *)
+
+(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.basic.
 
-(** Throughout this file, we assume the fully preemptive task model. *)
+(** Furthermore, we assume the fully preemptive task model. *)
 Require Import prosa.model.task.preemption.fully_preemptive.
 
-(** * RTA for Fully Preemptive FP Model *)
-(** In this module we prove the RTA theorem for fully preemptive FP model. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
 
   (** Consider any type of tasks ... *)
@@ -79,11 +83,24 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
      function (i.e., jobs have bounded non-preemptive 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.
+  (** ** Total Workload and Length of Busy Interval *)
+
+  (** We introduce the abbreviation [rbf] for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+  Let rbf := task_request_bound_function.
+
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
+  Let task_rbf := rbf tsk.
+
+  (** Using the sum of individual request bound functions, we define
+      the request bound function of all tasks with higher priority
+      ... *)
   Let total_hep_rbf := total_hep_request_bound_function_FP ts tsk.
+
+  (** ... and the request bound function of all tasks with higher
+      priority other than task [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. *)
@@ -91,11 +108,14 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_L_positive : L > 0.
   Hypothesis H_fixed_point : L = total_hep_rbf L.
 
+  (** ** Response-Time Bound *)
+  
   (** 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. *)
+  (** 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),
@@ -104,8 +124,13 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
         A + F = task_rbf (A + ε) + total_ohep_rbf (A + F) /\
         F <= R.
 
-  (** Now, we can leverage the results for the abstract model with bounded non-preemptive segments
-       to establish a response-time bound for the more concrete model of fully preemptive scheduling. *)
+  (** Now, we can leverage the results for the abstract model with
+      bounded non-preemptive segments to establish a response-time
+      bound for the more concrete model of fully preemptive
+      scheduling. *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+  
   Theorem uniprocessor_response_time_bound_fully_preemptive_fp:
     response_time_bounded_by tsk R.
   Proof.

results/fixed_priority/rta/limited_preemptive.v

 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
+
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Throughout this file, we assume ideal uni-processor schedules. *)
-Require Import prosa.model.processor.ideal.
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** * RTA for FP-schedulers with Fixed Preemption Points *)
+(** In this module we prove the RTA theorem for FP-schedulers with
+    fixed preemption points. *)
+
+(** Throughout this file, we assume the FP priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.processor.ideal.
 Require Import prosa.model.readiness.basic.
 
-(** Throughout this file, we assume the task model with fixed preemption points. *)
+(** Furthermore, we assume the task model with fixed preemption points. *)
 Require Import prosa.model.preemption.limited_preemptive.
 Require Import prosa.model.task.preemption.limited_preemptive.
 
+(** ** Setup and Assumptions *)
 
-(** * RTA for FP-schedulers with Fixed Preemption Points *)
-(** In this module we prove the RTA theorem for FP-schedulers with fixed preemption points. *)
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
 
   (** Consider any type of tasks ... *)
@@ -89,12 +93,25 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
      function (i.e., jobs have bounded non-preemptive 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.
+  (** ** Total Workload and Length of Busy Interval *)
+
+  (** We introduce the abbreviation [rbf] for the task request bound function,
+       which is defined as [task_cost(T) × max_arrivals(T,Δ)] for a task T. *)
+  Let rbf := task_request_bound_function.
+
+  (** Next, we introduce [task_rbf] as an abbreviation
+      for the task request bound function of task [tsk]. *)
+  Let task_rbf := rbf tsk.
+
+  (** Using the sum of individual request bound functions, we define
+      the request bound function of all tasks with higher priority
+      ... *)
   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.
 
+  (** ... and the request bound function of all tasks with higher
+      priority other than task [tsk]. *)
+  Let total_ohep_rbf := total_ohep_request_bound_function_FP ts tsk.
+  
   (** Next, we define a bound for the priority inversion caused by tasks of lower priority. *)
   Let blocking_bound :=
     \max_(tsk_other <- ts | ~~ hep_task tsk_other tsk)
@@ -105,7 +122,9 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Variable L : duration.
   Hypothesis H_L_positive : L > 0.
   Hypothesis H_fixed_point : L = blocking_bound + total_hep_rbf L.
-
+  
+  (** ** Response-Time Bound *)
+  
   (** 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 + ε)).
 
@@ -121,8 +140,12 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
                 + total_ohep_rbf (A + F) /\
         F + (task_last_nonpr_segment tsk - ε) <= R.
         
-  (** Now, we can reuse the results for the abstract model with bounded non-preemptive segments
-     to establish a response-time bound for the more concrete model of fixed preemption points. *)
+  (** Now, we can reuse the results for the abstract model with
+      bounded non-preemptive segments to establish a response-time
+      bound for the more concrete model of fixed preemption points. *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+    
   Theorem uniprocessor_response_time_bound_fp_with_fixed_preemption_points:
     response_time_bounded_by tsk R.  
   Proof.