Library rt.restructuring.model.preemption.rtc_threshold.instance.floating
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.10.1 (October 2019)
----------------------------------------------------------------------------- *)
From rt.util Require Export 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 model with floating non-preemptive regions.
Consider any type of tasks.
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.
{
task_run_to_completion_threshold (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFloatingNonPreemptiveRegions.