From ba7584666bf4b08c861319e5b1548cbe88db427b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Fri, 22 Nov 2019 16:47:22 +0100
Subject: [PATCH] model reorg: have only one notion of priority-driven
schedules
The Prosa notion of priority-driven scheduling depends on the
preemption model. That is ok; any theory that doesn't want to deal
with non-preemptive sections can simply Require Export the fully
preemptive model and be done with it.
---
.../rta/nonpr_reg/concrete_models/floating.v | 2 +-
.../rta/nonpr_reg/concrete_models/limited.v | 2 +-
.../nonpr_reg/concrete_models/nonpreemptive.v | 2 +-
.../nonpr_reg/concrete_models/preemptive.v | 2 +-
.../edf/rta/nonpr_reg/response_time_bound.v | 2 +-
.../analysis/edf/rta/response_time_bound.v | 2 +-
.../facts/priority_inversion_is_bounded.v | 2 +-
.../rta/nonpr_reg/concrete_models/floating.v | 2 +-
.../rta/nonpr_reg/concrete_models/limited.v | 2 +-
.../nonpr_reg/concrete_models/nonpreemptive.v | 2 +-
.../nonpr_reg/concrete_models/preemptive.v | 2 +-
.../rta/nonpr_reg/response_time_bound.v | 2 +-
.../fixed_priority/rta/response_time_bound.v | 2 +-
.../schedule/priority_based/preemptive.v | 28 -------------------
.../preemption_aware.v => priority_driven.v} | 0
15 files changed, 13 insertions(+), 41 deletions(-)
delete mode 100644 restructuring/model/schedule/priority_based/preemptive.v
rename restructuring/model/schedule/{priority_based/preemption_aware.v => priority_driven.v} (100%)
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 719cb129f..36179365d 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.preemption.floating.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index 23893b26d..1d743f001 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -11,7 +11,7 @@ Require Import rt.restructuring.model.preemption.limited.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 80a489504..e5536a880 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index d8d5d1e7e..a01366022 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
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 55ecf77dc..e44a589f4 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -16,7 +16,7 @@ Require Import rt.restructuring.analysis.facts.priority_inversion_is_bounded.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 4c5a3284f..5eb78f449 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -16,7 +16,7 @@ Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.jo
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
Require Import rt.restructuring.model.priority.edf.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.schedulability.
diff --git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 9e7880b56..771e3324d 100644
--- a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ -5,7 +5,7 @@ Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.preemption_time.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Export rt.restructuring.analysis.definitions.no_carry_in.
Require Export rt.restructuring.analysis.definitions.busy_interval.
Require Export rt.restructuring.analysis.definitions.priority_inversion.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 3f15c28b0..1a61e9aff 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.floating.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index fe73e59a1..05213cf7e 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -10,7 +10,7 @@ Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.preemption.limited.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 78c93cd06..58a8bbad0 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index 565952da9..70cefe5ca 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -9,7 +9,7 @@ Require Import rt.restructuring.model.readiness.basic.
Require Import rt.restructuring.model.arrival.arrival_curves.
Require Import rt.restructuring.model.schedule.work_conserving.
Require Import rt.restructuring.model.priority.classes.
-Require Import rt.restructuring.model.schedule.priority_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Import rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
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 1b91e8ccf..ffec52ae6 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
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.preemption.task.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_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index b1ed59948..facdb26cd 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -13,7 +13,7 @@ Require Import rt.restructuring.model.preemption.task.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_based.preemption_aware.
+Require Import rt.restructuring.model.schedule.priority_driven.
Require Import rt.restructuring.analysis.arrival.workload_bound.
Require Import rt.restructuring.analysis.arrival.rbf.
Require Export rt.restructuring.analysis.schedulability.
diff --git a/restructuring/model/schedule/priority_based/preemptive.v b/restructuring/model/schedule/priority_based/preemptive.v
deleted file mode 100644
index d41123a36..000000000
--- a/restructuring/model/schedule/priority_based/preemptive.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Require Export rt.restructuring.model.priority.classes.
-
-(** We now define what it means for a schedule to respect a priority *)
-(** We only define it for a JLDP policy since the definitions for JLDP and JLFP are the same
- and can be used through the conversions *)
-Section Priority.
- Context {Job: JobType} {Task: TaskType}.
- Context `{JobCost Job} `{JobArrival Job}.
-
- Context `{JLDP_policy Job}.
-
- Variable arr_seq : arrival_sequence Job.
-
- Context {PState : Type}.
- Context `{ProcessorState Job PState}.
-
- Context `{JobReady Job PState}.
-
- Variable sched : schedule PState.
-
- Definition respects_preemptive_priorities :=
- forall j j_hp t,
- arrives_in arr_seq j ->
- backlogged sched j t ->
- scheduled_at sched j_hp t ->
- hep_job_at t j_hp j.
-
-End Priority.
diff --git a/restructuring/model/schedule/priority_based/preemption_aware.v b/restructuring/model/schedule/priority_driven.v
similarity index 100%
rename from restructuring/model/schedule/priority_based/preemption_aware.v
rename to restructuring/model/schedule/priority_driven.v
--
GitLab