Commit 540acffd authored by Björn Brandenburg's avatar Björn Brandenburg

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.
parent 4e9768b1
......@@ -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.
......
......@@ -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.
......
......@@ -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 *)
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
......@@ -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.
......
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
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.
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