# Library prosa.model.task.preemption.parameters

# Task Preemption Model

## Preemption-Related Task Parameters

Class TaskMaxNonpreemptiveSegment (Task : TaskType) :=

task_max_nonpreemptive_segment : Task → work.

task_max_nonpreemptive_segment : Task → work.

Second, run-to-completion threshold (RTCT) indicates a progress
bound with the interpretation that, once a job of a task tsk has
received at least task_rtct tsk time units of service, it will
remain nonpreemptive until the end and run to completion.

Third, the parameter task_preemption_points indicates the non-preemptive
segments of a task. Obviously, not all preemption models use this parameter.

## Derived Properties

In this section, we define the notions of the maximal and the last non-preemptive segments of a task.
Consider any type of tasks with fixed preemption points.

We define a function task_max_nonpr_segment that computes the length of
the longest non-preemptive segment of a given task.

Similarly, task_last_nonpr_segment is a function that computes the
length of the last non-preemptive segment.

Definition task_last_nonpr_segment (tsk : Task) :=

last0 (distances (task_preemption_points tsk)).

End MaxAndLastNonpreemptiveSegment.

last0 (distances (task_preemption_points tsk)).

End MaxAndLastNonpreemptiveSegment.

To avoid having to specify redundant information, we allow Coq to
automatically infer a task's maximum non-preemptive segment length if its
preemption points are known.

#[global]

Instance TaskPreemptionPoints_to_TaskMaxNonpreemptiveSegment_conversion

(Task : TaskType) `{TaskPreemptionPoints Task} : TaskMaxNonpreemptiveSegment Task := task_max_nonpr_segment.

Instance TaskPreemptionPoints_to_TaskMaxNonpreemptiveSegment_conversion

(Task : TaskType) `{TaskPreemptionPoints Task} : TaskMaxNonpreemptiveSegment Task := task_max_nonpr_segment.

## Preemption Model Validity

Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Suppose we are given the maximum non-preemptive segment length for each task ...

... and a job-level preemption model.

Consider any kind of processor state model, ...

... any job arrival sequence, ...

... and any given schedule.

First we require that task_max_nonpreemptive_segment gives an upper
bound on values of the function job_max_nonpreemptive_segment.

Definition job_respects_max_nonpreemptive_segment (j: Job) :=

job_max_nonpreemptive_segment j ≤ task_max_nonpreemptive_segment (job_task j).

job_max_nonpreemptive_segment j ≤ task_max_nonpreemptive_segment (job_task j).

Next, we require that all segments of a job j have bounded length. That
is, for any progress ρ of job j, there exists a preemption point pp
such that ρ ≤ pp ≤ ρ + (job_max_nps j - ε). That is, in any time
interval of length job_max_nps j during which a job is continuously
scheduled, there exists a preemption point that lies in this interval.

Definition nonpreemptive_regions_have_bounded_length (j : Job) :=

∀ (ρ : duration),

0 ≤ ρ ≤ job_cost j →

∃ (pp : duration),

ρ ≤ pp ≤ ρ + (job_max_nonpreemptive_segment j - ε) ∧

job_preemptable j pp.

∀ (ρ : duration),

0 ≤ ρ ≤ job_cost j →

∃ (pp : duration),

ρ ≤ pp ≤ ρ + (job_max_nonpreemptive_segment j - ε) ∧

job_preemptable j pp.

We say that the schedule exhibits bounded nonpreemptive segments iff the
predicate job_preemptable satisfies the two preceding conditions.

Definition model_with_bounded_nonpreemptive_segments :=

∀ j,

arrives_in arr_seq j →

job_respects_max_nonpreemptive_segment j

∧ nonpreemptive_regions_have_bounded_length j.

∀ j,

arrives_in arr_seq j →

job_respects_max_nonpreemptive_segment j

∧ nonpreemptive_regions_have_bounded_length j.

Finally, we say that the schedule exhibits

*valid*bounded nonpreemptive segments iff the predicate job_preemptable defines a valid preemption model and if this model has non-preemptive segments of bounded length.
Definition valid_model_with_bounded_nonpreemptive_segments :=

valid_preemption_model arr_seq sched ∧

model_with_bounded_nonpreemptive_segments.

End ValidPreemptionModel.

valid_preemption_model arr_seq sched ∧

model_with_bounded_nonpreemptive_segments.

End ValidPreemptionModel.

## Run-to-Completion Threshold Validity

Consider any type of tasks with bounded WCETs ...

... and any type of jobs associated with these tasks ...

... where each job has an execution cost.

Suppose we are given a job-level preemption model ...

...and the run-to-completion threshold for each task.

Further, consider any kind of processor model, ...

... any job arrival sequence, ...

... and any given schedule.

A task's run-to-completion threshold must not exceed the WCET of the
task.

We say that the run-to-completion threshold of a task tsk bounds the
job-level run-to-completion threshold iff, for any job j of task tsk,
the job's run-to-completion threshold is at most the task's
run-to-completion threshold.

Definition job_respects_task_rtc tsk :=

∀ j,

arrives_in arr_seq j →

job_of_task tsk j →

job_rtct j ≤ task_rtct tsk.

∀ j,

arrives_in arr_seq j →

job_of_task tsk j →

job_rtct j ≤ task_rtct tsk.

Finally, we require that a valid run-to-completion threshold parameter
will satisfy the two above definitions.