Library prosa.model.task.preemption.fully_preemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.preemption.parameters.
Fully Preemptive Task 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 ε
(i.e., one time unit such as a processor cycle).
Global Program Instance fully_preemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := ε
}.
End FullyPreemptiveModel.
{
task_max_nonpreemptive_segment (tsk : Task) := ε
}.
End FullyPreemptiveModel.
Run-to-Completion Threshold
Consider any type of tasks with WCETs.
In the fully preemptive model, any job can be preempted at any
time. Thus, the only safe run-to-completion threshold for a task
is its WCET.
Global Program Instance fully_preemptive : TaskRunToCompletionThreshold Task :=
{
task_rtct (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFullyPreemptiveModel.
{
task_rtct (tsk : Task) := task_cost tsk
}.
End TaskRTCThresholdFullyPreemptiveModel.