Task Preemption Model

In this module, we define the abstract interface for task-level preemption models. Specific preemption models are instantiated in the sibling files in this directory.

Preemption-Related Task Parameters

We define three parameters to express the preemption behavior of a given task. First, we define task_max_nonpreemptive_segment to denote a bound on the maximum length of a task's non-preemptive segment.

Second, task_run_to_completion_threshold indicates a progress bound with the interpretation that, once a job of a task tsk has received at least task_run_to_completion_threshold 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.

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.

Preemption Model Validity

For analysis purposes, it is important that the distance between any two neighboring preemption points of a job is bounded. We define the validity criterion for the maximum non-preemptive segment length accordingly.

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.

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.

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

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.

Run-to-Completion Threshold Validity

Since a task model may not provide exact information about the preemption points of a task, a task's run-to-completion threshold generally cannot be defined in terms of the preemption points of a task (unlike a job's run-to-completion threshold, which can always be computed from a job's preemption points). Instead, we require each task-level preemption model to specify a task's run-to-completion threshold explicitly. We define its required properties in the following.

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.

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