Library prosa.model.task.preemption.fully_nonpreemptive
(* ----------------------------------[ coqtop ]---------------------------------
Welcome to Coq 8.11.2 (June 2020)
----------------------------------------------------------------------------- *)
Require Export prosa.model.task.preemption.parameters.
Fully Non-Preemptive Task Model
Consider any type of tasks with WCET bounds.
In the fully non-preemptive model, no job can be preempted until its
completion. The maximal non-preemptive segment of a job [j] has length
[job_cost j], which is bounded by [task_cost tsk].
Global Program Instance fully_nonpreemptive_model : TaskMaxNonpreemptiveSegment Task :=
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.
End FullyNonPreemptiveModel.
{
task_max_nonpreemptive_segment (tsk : Task) := task_cost tsk
}.
End FullyNonPreemptiveModel.
Run-to-Completion Threshold
Consider any type of tasks.
In the fully non-preemptive model, no job can be preempted prior to its
completion. In other words, once a job starts running, it is guaranteed
to finish. Thus, we can set the task-level run-to-completion threshold
to ε.
Global Program Instance fully_nonpreemptive : TaskRunToCompletionThreshold Task :=
{
task_run_to_completion_threshold (tsk : Task) := ε
}.
End TaskRTCThresholdFullyNonPreemptive.
{
task_run_to_completion_threshold (tsk : Task) := ε
}.
End TaskRTCThresholdFullyNonPreemptive.