From 7b64c4b0f275de7c850af1a37494e73eb4e12487 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 19:15:38 +0100
Subject: [PATCH] model reorg: fold RTCT instances into task.preemption.*
The two concepts are tightly coupled and it does not make sense
to mix and match them. Therefore, it's cleaner and easier to
understand if both aspects of the preemption model are instantiated
in the same module next to each other.
---
.../preemption/rtc_threshold/floating.v | 1 -
.../preemption/rtc_threshold/limited.v | 1 -
.../preemption/rtc_threshold/nonpreemptive.v | 1 -
.../preemption/rtc_threshold/preemptive.v | 1 -
restructuring/model/preemption/floating.v | 1 -
restructuring/model/preemption/limited.v | 2 +-
.../model/preemption/nonpreemptive.v | 1 -
restructuring/model/preemption/preemptive.v | 1 -
.../rtc_threshold/instance/floating.v | 21 ----------------
.../rtc_threshold/instance/limited.v | 24 -------------------
.../rtc_threshold/instance/nonpreemptive.v | 22 -----------------
.../rtc_threshold/instance/preemptive.v | 19 ---------------
.../task/preemption/floating_nonpreemptive.v | 20 ++++++++++++++++
.../task/preemption/fully_nonpreemptive.v | 22 +++++++++++++++++
.../model/task/preemption/fully_preemptive.v | 20 ++++++++++++++++
.../task/preemption/limited_preemptive.v | 24 +++++++++++++++++++
16 files changed, 87 insertions(+), 94 deletions(-)
delete mode 100644 restructuring/model/preemption/rtc_threshold/instance/floating.v
delete mode 100644 restructuring/model/preemption/rtc_threshold/instance/limited.v
delete mode 100644 restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
delete mode 100644 restructuring/model/preemption/rtc_threshold/instance/preemptive.v
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index 1bd61dbd6..e3e91e0cf 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -7,7 +7,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 0535ccf6a..cebdf4816 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -9,7 +9,6 @@ Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index aa42896da..b90c5e803 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -9,7 +9,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 59ffdcbb0..4c2d58e60 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -5,7 +5,6 @@ Require Import rt.restructuring.model.task.concept.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
Require Import rt.restructuring.model.task.preemption.fully_preemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
diff --git a/restructuring/model/preemption/floating.v b/restructuring/model/preemption/floating.v
index a44335562..4f8f8b04c 100644
--- a/restructuring/model/preemption/floating.v
+++ b/restructuring/model/preemption/floating.v
@@ -1,4 +1,3 @@
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
-Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
diff --git a/restructuring/model/preemption/limited.v b/restructuring/model/preemption/limited.v
index fad9bf13e..a1f943c35 100644
--- a/restructuring/model/preemption/limited.v
+++ b/restructuring/model/preemption/limited.v
@@ -1,4 +1,4 @@
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.limited_preemptive.
-Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
+
diff --git a/restructuring/model/preemption/nonpreemptive.v b/restructuring/model/preemption/nonpreemptive.v
index b213f9636..e3b6368e7 100644
--- a/restructuring/model/preemption/nonpreemptive.v
+++ b/restructuring/model/preemption/nonpreemptive.v
@@ -3,4 +3,3 @@ Require Export rt.restructuring.model.schedule.nonpreemptive.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.task.preemption.fully_nonpreemptive.
-Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
diff --git a/restructuring/model/preemption/preemptive.v b/restructuring/model/preemption/preemptive.v
index 4a081def8..3f5028e7e 100644
--- a/restructuring/model/preemption/preemptive.v
+++ b/restructuring/model/preemption/preemptive.v
@@ -1,4 +1,3 @@
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.fully_preemptive.
-Require Export rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/floating.v b/restructuring/model/preemption/rtc_threshold/instance/floating.v
deleted file mode 100644
index 4b87a208c..000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/floating.v
+++ /dev/null
@@ -1,21 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
- threshold] for the model with floating non-preemptive regions. *)
-Section TaskRTCThresholdFloatingNonPreemptiveRegions.
-
- (** Consider any type of tasks.*)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** In the model with floating non-preemptive regions, task has to
- static information about the placement of preemption
- points. Thus, the only safe task's run to completion threshold
- is [task cost]. *)
- Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
- {
- task_run_to_completion_threshold (tsk : Task) := task_cost tsk
- }.
-
-End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/limited.v b/restructuring/model/preemption/rtc_threshold/instance/limited.v
deleted file mode 100644
index 14efa2870..000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/limited.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
- threshold] for the limited preemptions model. *)
-Section TaskRTCThresholdLimitedPreemptions.
-
- (** Consider any type of tasks. *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
- Context `{TaskPreemptionPoints Task}.
-
- (** In the model with limited preemptions, no job can be preempted after
- a job reaches its last non-preemptive segment. Thus, we can
- set task's run to completion threshold to [task_cost tsk -
- (task_last_nonpr_seg tsk - ε)] which is always greater than
- [job_cost j - (job_last_nonpr_seg j - ε)]. *)
- Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
- {
- task_run_to_completion_threshold (tsk : Task) :=
- task_cost tsk - (task_last_nonpr_segment tsk - ε)
- }.
-
-End TaskRTCThresholdLimitedPreemptions.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v b/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
deleted file mode 100644
index 271f11b4a..000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/nonpreemptive.v
+++ /dev/null
@@ -1,22 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
- threshold] for the fully non-preemptive model. *)
-Section TaskRTCThresholdFullyNonPreemptive.
-
- (** Consider any type of tasks. *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** In fully non-preemptive model no job can be preempted until its
- completion. Thus, we can set task's run to completion threshold
- to ε. *)
- Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
- {
- task_run_to_completion_threshold (tsk : Task) := ε
- }.
-
-End TaskRTCThresholdFullyNonPreemptive.
diff --git a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v b/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
deleted file mode 100644
index 30459d065..000000000
--- a/restructuring/model/preemption/rtc_threshold/instance/preemptive.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Export rt.restructuring.model.task.preemption.parameters.
-
-(** * Task's Run to Completion Threshold *)
-(** In this section, we instantiate function [task run to completion
- threshold] for the fully preemptive model. *)
-Section TaskRTCThresholdFullyPreemptiveModel.
-
- (** Consider any type of tasks. *)
- Context {Task : TaskType}.
- Context `{TaskCost Task}.
-
- (** In the fully preemptive model any job can be preempted at any time. Thus,
- the only safe task's run to completion threshold is [task cost]. *)
- Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
- {
- task_run_to_completion_threshold (tsk : Task) := task_cost tsk
- }.
-
-End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 6b3837b8d..61eff9396 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -39,3 +39,23 @@ Section ModelWithFloatingNonpreemptiveRegions.
job_max_np_segment_le_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+ threshold] for the model with floating non-preemptive regions. *)
+Section TaskRTCThresholdFloatingNonPreemptiveRegions.
+
+ (** Consider any type of tasks.*)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** In the model with floating non-preemptive regions, task has to
+ static information about the placement of preemption
+ points. Thus, the only safe task's run to completion threshold
+ is [task cost]. *)
+ Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+ {
+ task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+ }.
+
+End TaskRTCThresholdFloatingNonPreemptiveRegions.
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index ced8e61be..c470b16c5 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ -21,3 +21,25 @@ Section FullyNonPreemptiveModel.
}.
End FullyNonPreemptiveModel.
+
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+ threshold] for the fully non-preemptive model. *)
+Section TaskRTCThresholdFullyNonPreemptive.
+
+ (** Consider any type of tasks. *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** In fully non-preemptive model no job can be preempted until its
+ completion. Thus, we can set task's run to completion threshold
+ to ε. *)
+ Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
+ {
+ task_run_to_completion_threshold (tsk : Task) := ε
+ }.
+
+End TaskRTCThresholdFullyNonPreemptive.
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index fba328695..a8f0f210c 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ -16,3 +16,23 @@ Section FullyPreemptiveModel.
}.
End FullyPreemptiveModel.
+
+Require Export rt.restructuring.model.task.preemption.parameters.
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+ threshold] for the fully preemptive model. *)
+Section TaskRTCThresholdFullyPreemptiveModel.
+
+ (** Consider any type of tasks. *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+
+ (** In the fully preemptive model any job can be preempted at any time. Thus,
+ the only safe task's run to completion threshold is [task cost]. *)
+ Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
+ {
+ task_run_to_completion_threshold (tsk : Task) := task_cost tsk
+ }.
+
+End TaskRTCThresholdFullyPreemptiveModel.
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 380996b0e..194ceb278 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -84,3 +84,27 @@ Section ModelWithFixedPreemptionPoints.
valid_fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
+
+
+(** * Task's Run to Completion Threshold *)
+(** In this section, we instantiate function [task run to completion
+ threshold] for the limited preemptions model. *)
+Section TaskRTCThresholdLimitedPreemptions.
+
+ (** Consider any type of tasks. *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskPreemptionPoints Task}.
+
+ (** In the model with limited preemptions, no job can be preempted after
+ a job reaches its last non-preemptive segment. Thus, we can
+ set task's run to completion threshold to [task_cost tsk -
+ (task_last_nonpr_seg tsk - ε)] which is always greater than
+ [job_cost j - (job_last_nonpr_seg j - ε)]. *)
+ Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
+ {
+ task_run_to_completion_threshold (tsk : Task) :=
+ task_cost tsk - (task_last_nonpr_segment tsk - ε)
+ }.
+
+End TaskRTCThresholdLimitedPreemptions.
--
GitLab