improve structure of EDF response-time analysis results

results/edf/rta/bounded_nps.v

@@ -10,7 +10,7 @@ Require Import prosa.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import prosa.model.readiness.basic.
 
-(** * RTA for EDF-schedulers with Bounded Non-Preemptive Segments *)
+(** * RTA for EDF  with Bounded Non-Preemptive Segments *)
 
 (** In this section we instantiate the Abstract RTA for EDF-schedulers
     with Bounded Priority Inversion to EDF-schedulers for ideal

results/edf/rta/floating_nonpreemptive.v

 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
-Require Import prosa.model.priority.edf.
 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.
+(** * RTA for EDF with Floating Non-Preemptive Regions *)
+(** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** Throughout this file, we assume the EDF priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.priority.edf.
+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 EDF model. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   
   (** Consider any type of tasks ... *)
@@ -28,12 +30,6 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
   
-  (** For clarity, let's denote the relative deadline of a task as D. *)
-  Let D tsk := task_deadline tsk.
-
-  (** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
-  Let EDF := EDF 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.
@@ -94,13 +90,8 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
       segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
 
-  (** Let's define some local names for clarity. *)
-  Let response_time_bounded_by :=
-    task_response_time_bound arr_seq sched.
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts 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.
@@ -115,21 +106,28 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   
   (** We define a bound for the priority inversion caused by jobs with lower priority. *)
   Definition blocking_bound :=
-    \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk_other > D tsk))
+    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
      (task_max_nonpreemptive_segment tsk_other - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
       of other tasks with higher-than-or-equal priority. *)
   Let bound_on_total_hep_workload A Δ :=
     \sum_(tsk_o <- ts | tsk_o != tsk)
-     rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+     rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
   
   (** 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 = total_rbf L.
 
+  (** ** Response-Time Bound *)
+  
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+
+  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
+  Let bound_on_total_hep_workload_changes_at :=
+    bound_on_total_hep_workload_changes_at ts tsk.  
+
   Let is_in_search_space (A : duration) :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
@@ -147,6 +145,9 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
       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_edf_with_floating_nonpreemptive_regions:
     response_time_bounded_by tsk R.  
   Proof.

results/edf/rta/fully_nonpreemptive.v

 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
-Require Import prosa.model.priority.edf.
+
 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 EDF *)
+(** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
+
+(** Throughout this file, we assume the EDF priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.priority.edf.
+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 EDF model. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   
   (** Consider any type of tasks ... *)
@@ -28,12 +32,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (** For clarity, let's denote the relative deadline of a task as D. *)
-  Let D tsk := task_deadline tsk.
-
-  (** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
-  Let EDF := EDF 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.
@@ -83,12 +81,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
       segments). *)
   Hypothesis H_respects_policy : respects_policy_at_preemption_point arr_seq sched.
 
-  (** Let's define some local names for clarity. *)
-  Let response_time_bounded_by :=
-    task_response_time_bound arr_seq sched.
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts 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. *)
@@ -104,21 +97,28 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   
   (** We also define a bound for the priority inversion caused by jobs with lower priority. *)
   Let blocking_bound :=
-    \max_(tsk_o <- ts | (tsk_o != tsk) && (D tsk_o > D tsk))
+    \max_(tsk_o <- ts | (tsk_o != tsk) && (task_deadline tsk_o > task_deadline tsk))
      (task_cost tsk_o - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
        of other tasks with higher-than-or-equal priority. *)
   Let bound_on_total_hep_workload A Δ :=
     \sum_(tsk_o <- ts | tsk_o != tsk)
-     rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+     rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
   
   (** 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 = total_rbf L.
-  
+
+  (** ** Response-Time Bound *)
+    
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+
+  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
+  Let bound_on_total_hep_workload_changes_at :=
+    bound_on_total_hep_workload_changes_at ts tsk.
+
   Let is_in_search_space A :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
@@ -135,6 +135,9 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
 
   (** 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. *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
   Theorem uniprocessor_response_time_bound_fully_nonpreemptive_edf:
     response_time_bounded_by tsk R.
   Proof.

results/edf/rta/fully_preemptive.v

 Require Import prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
-Require Import prosa.model.priority.edf.
 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.
+(** * RTA for Fully Preemptive EDF *)
+(** In this section we prove the RTA theorem for the fully preemptive EDF model *)
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** Throughout this file, we assume the EDF priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.priority.edf.
+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 EDF Model *)
-(** In this section we prove the RTA theorem for the fully preemptive EDF model *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
 
   (** Consider any type of tasks ... *)
@@ -28,12 +30,6 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
 
-  (** For clarity, let's denote the relative deadline of a task as D. *)
-  Let D tsk := task_deadline tsk.
-
-  (** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
-  Let EDF := EDF 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.
@@ -81,13 +77,8 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
       [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 response_time_bounded_by :=
-    task_response_time_bound arr_seq sched.
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts 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. *)
@@ -105,14 +96,21 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
       of other tasks with higher-than-or-equal priority. *)
   Let bound_on_total_hep_workload A Δ :=
     \sum_(tsk_o <- ts | tsk_o != tsk)
-     rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+     rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
 
   (** 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 = total_rbf L.
 
+  (** ** Response-Time Bound *)
+  
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+      
+  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
+  Let bound_on_total_hep_workload_changes_at :=
+    bound_on_total_hep_workload_changes_at ts tsk.
+
   Let is_in_search_space A :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A).
   
@@ -128,6 +126,9 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
 
   (** 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_edf:
     response_time_bounded_by tsk R.
   Proof.

results/edf/rta/limited_preemptive.v

 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
-Require Import prosa.model.priority.edf.
 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.
+(** * RTA for EDF with Fixed Preemption Points *)
+(** In this module we prove the RTA theorem for EDF-schedulers with
+    fixed preemption points. *)
 
-(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+(** Throughout this file, we assume the EDF priority policy, ideal uni-processor 
+    schedules, and the basic (i.e., Liu & Layland) readiness model. *)
+Require Import prosa.model.priority.edf.
+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.
 
-(** * RTA for EDF-schedulers with Fixed Preemption Points *)
-(** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
+(** ** Setup and Assumptions *)
+
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   
   (** Consider any type of tasks ... *)
@@ -27,13 +30,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Context `{JobTask Job Task}.
   Context `{JobArrival Job}.
   Context `{JobCost Job}.
-
-  (** For clarity, let's denote the relative deadline of a task as D. *)
-  Let D tsk := task_deadline tsk.
    
-  (** Consider the EDF policy that indicates a higher-or-equal priority relation. *)
-  Let EDF := EDF 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.
@@ -92,13 +89,9 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
       [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 response_time_bounded_by := task_response_time_bound arr_seq sched.
-  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
-  Let bound_on_total_hep_workload_changes_at :=
-    bound_on_total_hep_workload_changes_at ts 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.
@@ -113,21 +106,28 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
 
   (** We define a bound for the priority inversion caused by jobs with lower priority. *)
   Let blocking_bound :=
-    \max_(tsk_other <- ts | (tsk_other != tsk) && (D tsk_other > D tsk))
+    \max_(tsk_other <- ts | (tsk_other != tsk) && (task_deadline tsk_other > task_deadline tsk))
      (task_max_nonpreemptive_segment tsk_other - ε).
   
   (** Next, we define an upper bound on interfering workload received from jobs 
      of other tasks with higher-than-or-equal priority. *)
   Let bound_on_total_hep_workload A Δ :=
     \sum_(tsk_o <- ts | tsk_o != tsk)
-     rbf tsk_o (minn ((A + ε) + D tsk - D tsk_o) Δ).
+     rbf tsk_o (minn ((A + ε) + task_deadline tsk - task_deadline tsk_o) Δ).
   
   (** 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 = total_rbf L.
 
+  (** ** Response-Time Bound *)
+  
   (** To reduce the time complexity of the analysis, recall the notion of search space. *)
+  
+  Let task_rbf_changes_at A := task_rbf_changes_at tsk A.
+  Let bound_on_total_hep_workload_changes_at :=
+    bound_on_total_hep_workload_changes_at ts tsk.
+  
   Let is_in_search_space A :=
     (A < L) && (task_rbf_changes_at A || bound_on_total_hep_workload_changes_at A). 
   
@@ -145,6 +145,9 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   
   (** 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 fixed preemption points.  *)
+
+  Let response_time_bounded_by := task_response_time_bound arr_seq sched.
+
   Theorem uniprocessor_response_time_bound_edf_with_fixed_preemption_points:
     response_time_bounded_by tsk R.  
   Proof.