Commit ba758466 authored by Björn Brandenburg's avatar Björn Brandenburg

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.
parent 73653440
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment