Library prosa.model.task.preemption.parameters

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.
  Context {Task : TaskType}.
  Context `{TaskPreemptionPoints Task}.

We define a function task_max_nonpr_segment that computes the length of the longest non-preemptive segment of a given task.
  Definition task_max_nonpr_segment (tsk : Task) :=
    max0 (distances (task_preemption_points tsk)).

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 ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.

Suppose we are given the maximum non-preemptive segment length for each task ...
... and a job-level preemption model.
  Context `{JobPreemptable Job}.

Consider any kind of processor state model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

... any job arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any given schedule.
  Variable sched : schedule PState.

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.
  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.

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 ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks ...
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

... where each job has an execution cost.
  Context `{JobCost Job}.

Suppose we are given a job-level preemption model ...
  Context `{JobPreemptable Job}.

...and the run-to-completion threshold for each task.
Further, consider any kind of processor model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

... any job arrival sequence, ...
  Variable arr_seq: arrival_sequence Job.

... and any given schedule.
  Variable sched: schedule PState.

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_task j = tsk
      job_run_to_completion_threshold j task_run_to_completion_threshold tsk.

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