Library rt.restructuring.model.task.preemption.fully_preemptive
Platform for Fully Preemptive Model
In this section, we instantiate function task_max_nonpreemptive_segment for the fully preemptive model.
Consider any type of jobs.
In the fully preemptive model any job can be preempted at any time. Thus,
the maximal non-preemptive segment has length at most ε.
Global Program Instance fully_preemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := ε
}.
End FullyPreemptiveModel.
{
task_max_nonpreemptive_segment (tsk : Task) := ε
}.
End FullyPreemptiveModel.
Task's Run to Completion Threshold
In this section, we instantiate function task run to completion threshold for the fully preemptive model.
Consider any type of tasks.
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.
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFullyPreemptiveModel.