Library rt.restructuring.model.preemption.rtc_threshold.instance.preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Import all.
From rt.restructuring.behavior Require Import all.
From rt.restructuring Require Import model.job model.task.
From rt.restructuring.model.preemption Require Import task.parameters.
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.