From bac8ebeaaa6df93ecc7fd82197922124ed6a4098 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Wed, 18 Dec 2019 22:27:44 +0100
Subject: [PATCH] improve structure of FP response-time analysis results
---
.../rta/floating_nonpreemptive.v | 54 +++++++++++++------
.../fixed_priority/rta/fully_nonpreemptive.v | 50 ++++++++++++-----
results/fixed_priority/rta/fully_preemptive.v | 51 +++++++++++++-----
.../fixed_priority/rta/limited_preemptive.v | 49 ++++++++++++-----
4 files changed, 149 insertions(+), 55 deletions(-)
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 2132f463c..ca36e3af9 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,20 +1,23 @@
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.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 931ae85d1..a3b95d652 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,19 +1,23 @@
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.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 528b717ad..8144eb552 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,19 +1,23 @@
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.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index acc6a3972..37576d9c5 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,20 +1,24 @@
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.
--
GitLab