floating.v 987 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
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. *)
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.