From 540acffde3073de638d4e42ee8590ef4b115a3dc 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:08:49 +0100
Subject: [PATCH] model reorg: fold RTCT validity into
 task.preemption.parameters

No need to keep the two separate as they are tightly coupled anyway,
and the joint file doesn't become too long.
---
 .../analysis/abstract/core/abstract_rta.v     |  2 +-
 .../analysis/abstract/core/abstract_seq_rta.v |  2 +-
 .../basic_facts/preemption/job/limited.v      |  2 +-
 .../preemption/job/nonpreemptive.v            |  2 +-
 .../preemption/rtc_threshold/floating.v       |  2 +-
 .../preemption/rtc_threshold/limited.v        |  2 +-
 .../preemption/rtc_threshold/nonpreemptive.v  |  2 +-
 .../preemption/rtc_threshold/preemptive.v     |  2 +-
 .../basic_facts/preemption/task/floating.v    |  2 +-
 .../edf/rta/nonpr_reg/response_time_bound.v   |  2 +-
 .../analysis/edf/rta/response_time_bound.v    |  2 +-
 .../rta/nonpr_reg/response_time_bound.v       |  2 +-
 .../fixed_priority/rta/response_time_bound.v  |  2 +-
 .../preemption/rtc_threshold/valid_rtct.v     | 64 ------------------
 .../model/task/preemption/parameters.v        | 65 +++++++++++++++++++
 15 files changed, 78 insertions(+), 77 deletions(-)
 delete mode 100644 restructuring/model/preemption/rtc_threshold/valid_rtct.v

diff --git a/restructuring/analysis/abstract/core/abstract_rta.v b/restructuring/analysis/abstract/core/abstract_rta.v
index 68a2ebaa5..03df8f5ac 100644
--- a/restructuring/analysis/abstract/core/abstract_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_rta.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.schedulability.
 Require Import rt.restructuring.analysis.basic_facts.all.
diff --git a/restructuring/analysis/abstract/core/abstract_seq_rta.v b/restructuring/analysis/abstract/core/abstract_seq_rta.v
index 98c0f7ba9..350c71c37 100644
--- a/restructuring/analysis/abstract/core/abstract_seq_rta.v
+++ b/restructuring/analysis/abstract/core/abstract_seq_rta.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/job/limited.v b/restructuring/analysis/basic_facts/preemption/job/limited.v
index 4a4e11d94..255cd93ca 100644
--- a/restructuring/analysis/basic_facts/preemption/job/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/job/limited.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 
 (** * Platform for Models with Limited Preemptions *)
diff --git a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
index 727b6a712..efaaf78a2 100644
--- a/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/job/nonpreemptive.v
@@ -7,7 +7,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
index e02f73146..1bd61dbd6 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/floating.v
@@ -4,7 +4,7 @@ Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
index 4a4f9f54a..0535ccf6a 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/limited.v
@@ -3,7 +3,7 @@ Require Import rt.restructuring.behavior.job.
 Require Import rt.restructuring.behavior.schedule.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
index b3b14df8e..aa42896da 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/nonpreemptive.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.schedule.nonpreemptive.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
index 33e41a46f..59ffdcbb0 100644
--- a/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
+++ b/restructuring/analysis/basic_facts/preemption/rtc_threshold/preemptive.v
@@ -2,7 +2,7 @@ Require Import rt.util.all.
 Require Import rt.restructuring.behavior.all.
 Require Import rt.restructuring.analysis.definitions.job_properties.
 Require Import rt.restructuring.model.task.concept.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 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.
diff --git a/restructuring/analysis/basic_facts/preemption/task/floating.v b/restructuring/analysis/basic_facts/preemption/task/floating.v
index 9a918e50a..fd6ad2ea1 100644
--- a/restructuring/analysis/basic_facts/preemption/task/floating.v
+++ b/restructuring/analysis/basic_facts/preemption/task/floating.v
@@ -6,7 +6,7 @@ Require Import rt.restructuring.model.task.concept.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.preemption.job.instance.limited.
 Require Import rt.restructuring.model.schedule.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index d24bcd4ed..961efe2fb 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 Require Import rt.restructuring.model.schedule.work_conserving.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 23f6787d0..3f5bec3e2 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 54e45fcc7..48361205f 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_driven.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index b80e1ae55..7d97db5a0 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
 Require Import rt.restructuring.model.preemption.valid_model.
 Require Import rt.restructuring.model.preemption.job.parameters.
 Require Import rt.restructuring.model.task.preemption.parameters.
-Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
+
 Require Import rt.restructuring.model.schedule.work_conserving.
 Require Import rt.restructuring.model.priority.classes.
 Require Import rt.restructuring.model.schedule.priority_driven.
diff --git a/restructuring/model/preemption/rtc_threshold/valid_rtct.v b/restructuring/model/preemption/rtc_threshold/valid_rtct.v
deleted file mode 100644
index d3d4e8277..000000000
--- a/restructuring/model/preemption/rtc_threshold/valid_rtct.v
+++ /dev/null
@@ -1,64 +0,0 @@
-Require Export rt.restructuring.model.preemption.valid_model.
-
-(** * Task's Run-to-Completion Threshold *)
-(** Since a task model may not provide exact information about
-     preemption point of a task, task's run-to-completion threshold
-     cannot be defined in terms of preemption points of a task (unlike
-     job's run-to-completion threshold). Therefore, we can assume the
-     existence of a function that maps a task to its run-to-completion
-     threshold. In this section we define the notion of a valid
-     run-to-completion threshold of a task. *)
-Section ValidTaskRunToCompletionThreshold.
-  
-  (** 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 `{JobCost Job}.
-
-  (** In addition, we assume existence of a function
-     maping jobs to theirs preemption points ... *)
-  Context `{JobPreemptable Job}.
-
-  (** ...and a function mapping tasks to theirs
-     run-to-completion threshold. *)
-  Context `{TaskRunToCompletionThreshold Task}.
-
-  (** Consider any kind of processor state model, ... *)
-  Context {PState : Type}.
-  Context `{ProcessorState Job PState}.
-
-  (** ... any job arrival sequence, ... *)
-  Variable arr_seq: arrival_sequence Job.
-
-  (** ... and any given schedule. *)
-  Variable sched: schedule PState. 
-
-  (** A task's run-to-completion threshold should be at most the cost of the task. *)
-  Definition task_run_to_completion_threshold_le_task_cost tsk :=
-    task_run_to_completion_threshold tsk <= task_cost tsk.
-  
-  (** We say that the run-to-completion threshold of a task tsk bounds
-      the job run-to-completionthreshold iff for any job j of task tsk
-      the job run-to-completion threshold is less than or equal to the
-      task run-to-completion threshold. *) 
-  Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
-    forall j,
-      arrives_in arr_seq j ->
-      job_task j = tsk ->
-      job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
-
-  (** We say that task_run_to_completion_threshold is a valid task
-      run-to-completion threshold for a task tsk iff
-      [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. *)
-  Definition valid_task_run_to_completion_threshold tsk :=
-    task_run_to_completion_threshold_le_task_cost tsk /\
-    task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
-
-End ValidTaskRunToCompletionThreshold.
\ No newline at end of file
diff --git a/restructuring/model/task/preemption/parameters.v b/restructuring/model/task/preemption/parameters.v
index d4307eacd..7d3efc635 100644
--- a/restructuring/model/task/preemption/parameters.v
+++ b/restructuring/model/task/preemption/parameters.v
@@ -1,4 +1,5 @@
 Require Export rt.util.all.
+Require Export rt.restructuring.model.preemption.job.parameters.
 Require Export rt.restructuring.model.task.concept.
 (** * Static information about preemption points *)
 
@@ -48,3 +49,67 @@ Section MaxAndLastNonpreemptiveSegment.
     last0 (distances (task_preemption_points tsk)).
     
 End MaxAndLastNonpreemptiveSegment.
+
+
+(** * Task's Run-to-Completion Threshold *)
+(** Since a task model may not provide exact information about
+     preemption point of a task, task's run-to-completion threshold
+     cannot be defined in terms of preemption points of a task (unlike
+     job's run-to-completion threshold). Therefore, we can assume the
+     existence of a function that maps a task to its run-to-completion
+     threshold. In this section we define the notion of a valid
+     run-to-completion threshold of a task. *)
+Section ValidTaskRunToCompletionThreshold.
+  
+  (** 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 `{JobCost Job}.
+
+  (** In addition, we assume existence of a function
+     maping jobs to theirs preemption points ... *)
+  Context `{JobPreemptable Job}.
+
+  (** ...and a function mapping tasks to theirs
+     run-to-completion threshold. *)
+  Context `{TaskRunToCompletionThreshold Task}.
+
+  (** Consider any kind of processor state model, ... *)
+  Context {PState : Type}.
+  Context `{ProcessorState Job PState}.
+
+  (** ... any job arrival sequence, ... *)
+  Variable arr_seq: arrival_sequence Job.
+
+  (** ... and any given schedule. *)
+  Variable sched: schedule PState. 
+
+  (** A task's run-to-completion threshold should be at most the cost of the task. *)
+  Definition task_run_to_completion_threshold_le_task_cost tsk :=
+    task_run_to_completion_threshold tsk <= task_cost tsk.
+  
+  (** We say that the run-to-completion threshold of a task tsk bounds
+      the job run-to-completionthreshold iff for any job j of task tsk
+      the job run-to-completion threshold is less than or equal to the
+      task run-to-completion threshold. *) 
+  Definition task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk :=
+    forall j,
+      arrives_in arr_seq j ->
+      job_task j = tsk ->
+      job_run_to_completion_threshold j <= task_run_to_completion_threshold tsk.
+
+  (** We say that task_run_to_completion_threshold is a valid task
+      run-to-completion threshold for a task tsk iff
+      [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. *)
+  Definition valid_task_run_to_completion_threshold tsk :=
+    task_run_to_completion_threshold_le_task_cost tsk /\
+    task_run_to_completion_threshold_bounds_job_run_to_completion_threshold tsk.
+
+End ValidTaskRunToCompletionThreshold.
-- 
GitLab