Commit 7b64c4b0 authored by Björn Brandenburg's avatar Björn Brandenburg

model reorg: fold RTCT instances into task.preemption.*

The two concepts are tightly coupled and it does not make sense
to mix and match them. Therefore, it's cleaner and easier to
understand if both aspects of the preemption model are instantiated
in the same module next to each other.
parent 540acffd
......@@ -7,7 +7,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
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.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.floating.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -9,7 +9,6 @@ Require Import rt.restructuring.model.preemption.job.parameters.
Require Import rt.restructuring.model.task.preemption.parameters.
Require Import rt.restructuring.model.preemption.job.instance.limited.
Require Import rt.restructuring.model.task.preemption.limited_preemptive.
Require Import rt.restructuring.model.preemption.rtc_threshold.instance.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.task.limited.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
......
......@@ -9,7 +9,6 @@ Require Import rt.restructuring.model.task.preemption.parameters.
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.
Require Import rt.restructuring.analysis.basic_facts.preemption.job.nonpreemptive.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
......
......@@ -5,7 +5,6 @@ Require Import rt.restructuring.model.task.concept.
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.
Require Import rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.job_preemptable.
(** * Task's Run to Completion Threshold *)
......
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.floating_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.floating.
Require Export rt.restructuring.model.preemption.valid_model.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.task.preemption.limited_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.limited.
......@@ -3,4 +3,3 @@ Require Export rt.restructuring.model.schedule.nonpreemptive.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.nonpreemptive.
Require Export rt.restructuring.model.task.preemption.fully_nonpreemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.nonpreemptive.
Require Export rt.restructuring.model.schedule.limited_preemptive.
Require Export rt.restructuring.model.preemption.job.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.fully_preemptive.
Require Export rt.restructuring.model.preemption.rtc_threshold.instance.preemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the model with floating non-preemptive regions. *)
Section TaskRTCThresholdFloatingNonPreemptiveRegions.
(** Consider any type of tasks.*)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In the model with floating non-preemptive regions, task has to
static information about the placement of preemption
points. Thus, the only safe task's run to completion threshold
is [task cost]. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the limited preemptions model. *)
Section TaskRTCThresholdLimitedPreemptions.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskPreemptionPoints Task}.
(** In the model with limited preemptions, no job can be preempted after
a job reaches its last non-preemptive segment. Thus, we can
set task's run to completion threshold to [task_cost tsk -
(task_last_nonpr_seg tsk - ε)] which is always greater than
[job_cost j - (job_last_nonpr_seg j - ε)]. *)
Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) :=
task_cost tsk - (task_last_nonpr_segment tsk - ε)
}.
End TaskRTCThresholdLimitedPreemptions.
Require Export rt.restructuring.model.task.preemption.parameters.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the fully non-preemptive model. *)
Section TaskRTCThresholdFullyNonPreemptive.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In fully non-preemptive model no job can be preempted until its
completion. Thus, we can set task's run to completion threshold
to ε. *)
Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := ε
}.
End TaskRTCThresholdFullyNonPreemptive.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the fully preemptive model. *)
Section TaskRTCThresholdFullyPreemptiveModel.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In the fully preemptive model any job can be preempted at any time. Thus,
the only safe task's run to completion threshold is [task cost]. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFullyPreemptiveModel.
......@@ -39,3 +39,23 @@ Section ModelWithFloatingNonpreemptiveRegions.
job_max_np_segment_le_task_max_np_segment.
End ModelWithFloatingNonpreemptiveRegions.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the model with floating non-preemptive regions. *)
Section TaskRTCThresholdFloatingNonPreemptiveRegions.
(** Consider any type of tasks.*)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In the model with floating non-preemptive regions, task has to
static information about the placement of preemption
points. Thus, the only safe task's run to completion threshold
is [task cost]. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFloatingNonPreemptiveRegions.
......@@ -21,3 +21,25 @@ Section FullyNonPreemptiveModel.
}.
End FullyNonPreemptiveModel.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the fully non-preemptive model. *)
Section TaskRTCThresholdFullyNonPreemptive.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In fully non-preemptive model no job can be preempted until its
completion. Thus, we can set task's run to completion threshold
to ε. *)
Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := ε
}.
End TaskRTCThresholdFullyNonPreemptive.
......@@ -16,3 +16,23 @@ Section FullyPreemptiveModel.
}.
End FullyPreemptiveModel.
Require Export rt.restructuring.model.task.preemption.parameters.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the fully preemptive model. *)
Section TaskRTCThresholdFullyPreemptiveModel.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
(** In the fully preemptive model any job can be preempted at any time. Thus,
the only safe task's run to completion threshold is [task cost]. *)
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFullyPreemptiveModel.
......@@ -84,3 +84,27 @@ Section ModelWithFixedPreemptionPoints.
valid_fixed_preemption_points_task_model.
End ModelWithFixedPreemptionPoints.
(** * Task's Run to Completion Threshold *)
(** In this section, we instantiate function [task run to completion
threshold] for the limited preemptions model. *)
Section TaskRTCThresholdLimitedPreemptions.
(** Consider any type of tasks. *)
Context {Task : TaskType}.
Context `{TaskCost Task}.
Context `{TaskPreemptionPoints Task}.
(** In the model with limited preemptions, no job can be preempted after
a job reaches its last non-preemptive segment. Thus, we can
set task's run to completion threshold to [task_cost tsk -
(task_last_nonpr_seg tsk - ε)] which is always greater than
[job_cost j - (job_last_nonpr_seg j - ε)]. *)
Global Program Instance limited_preemptions : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) :=
task_cost tsk - (task_last_nonpr_segment tsk - ε)
}.
End TaskRTCThresholdLimitedPreemptions.
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