Commit 9933d50d authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: job.v is an analysis def; job_deadline a task property

parent 393d2007
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.valid_model.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.schedule.work_conserving.
......
Require Import rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.task_arrivals.
Require Import rt.restructuring.model.arrival.arrival_curves.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.preemption.task.parameters.
......
Require Import rt.util.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.preemption.valid_model.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.job.
Require Import rt.restructuring.behavior.schedule.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.valid_schedule.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.valid_model.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.rtc_threshold.valid_rtct.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
......
Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
Require Import rt.util.all.
Require Import rt.util.nondecreasing.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.parameters.
......
......@@ -2,7 +2,7 @@ Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.schedule.nonpreemptive.
Require Import rt.restructuring.model.preemption.job.instance.nonpreemptive.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.preemption.valid_model.
Require Import rt.restructuring.model.preemption.job.instance.preemptive.
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.schedule.work_conserving.
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......@@ -192,7 +192,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
{ have NINTSK: job_task j' != tsk.
{ apply/eqP; intros TSKj'.
rewrite /EDF -ltnNge in NOTHEP.
rewrite /job_deadline /job_deadline.job_deadline_from_task_deadline in NOTHEP.
rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
rewrite TSKj' TSK ltn_add2r in NOTHEP.
move: NOTHEP; rewrite ltnNge; move => /negP T; apply: T.
apply leq_trans with t; last by done.
......@@ -208,7 +208,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
eapply in_arrivals_implies_arrived_between in JINB; last by eauto 2.
by move: JINB; move => /andP [_ T].
}
rewrite /job_deadline /job_deadline.job_deadline_from_task_deadline in NOTHEP.
rewrite /job_deadline /absolute_deadline.job_deadline_from_task_deadline in NOTHEP.
rewrite /D; ssromega.
}
Qed.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
......
Require Export rt.util.all.
Require Export rt.restructuring.behavior.all.
Require Export rt.restructuring.analysis.basic_facts.all.
Require Export rt.restructuring.model.job.
Require Export rt.restructuring.analysis.definitions.job_properties.
Require Export rt.restructuring.model.task.
Require Export rt.restructuring.model.schedule.work_conserving.
Require Export rt.restructuring.model.priority.classes.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.all.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.analysis.definitions.job_properties.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.aggregate.workload.
Require Import rt.restructuring.model.processor.ideal.
......
Require Export rt.restructuring.model.job_deadline.
Require Export rt.restructuring.model.task.absolute_deadline.
Require Export rt.restructuring.analysis.basic_facts.completion.
Section Task.
......
Require Export rt.restructuring.model.job_deadline.
Require Export rt.restructuring.model.task.absolute_deadline.
Require Import rt.restructuring.model.priority.classes.
From mathcomp Require Export seq.
......
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