Library prosa.model.task.preemption.limited_preemptive

Limited-Preemptive Task Model

In this module, we instantiate the task model in which jobs can be preempted only at certain preemption points.

Model Validity

To begin with, we introduce requirements that the function task_max_nonpr_segment must satisfy to be coherent with the limited-preemptive task model.
Consider any type of tasks with WCET bounds and given preemption points ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskPreemptionPoints Task}.

... and any type of jobs associated with these tasks, ...
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
... where each job has an arrival time, an execution cost, and some preemption points.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.
  Context `{JobPreemptionPoints Job}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Consider an arbitrary task set ts.
  Variable ts : TaskSet Task.

First, we describe structural properties that a sequence of preemption points of a task should satisfy.
(1) We require the sequence of preemption points to contain the beginning ...
... and (2) the end of execution.
(3) Furthermore, we require the sequence of preemption points to be a non-decreasing sequence.
(4) We also require the number of nonpreemptive segments of a job to be equal to the number of nonpreemptive segments of its task. Note that some of nonpreemptive segments of a job can have zero length; nonetheless the number of segments should match.
  Definition consistent_job_segment_count :=
     j,
      arrives_in arr_seq j
      size (job_preemptive_points j) = size (task_preemption_points (job_task j)).

(5) We require the lengths of the nonpreemptive segments of a job to be bounded by the lengths of the corresponding segments of its task.
  Definition job_respects_segment_lengths :=
     j n,
      arrives_in arr_seq j
      nth 0 (distances (job_preemptive_points j)) n
       nth 0 (distances (task_preemption_points (job_task j))) n.

(6) Lastly, we ban empty nonpreemptive segments at the task level.
  Definition task_segments_are_nonempty :=
     tsk n,
      (tsk \in ts)
      n < size (distances (task_preemption_points tsk))
      ε nth 0 (distances (task_preemption_points tsk)) n.

We define a valid task-level model with fixed preemption points as the conjunction of the hypotheses above.
Finally, a model with fixed preemption points is valid if it is both valid a the job and task levels.

Run-to-Completion Threshold

In this section, we instantiate the task-level run-to-completion threshold for the task model with fixed preemption points.
Consider any type of tasks with WCET bounds and fixed preemption points.
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{TaskPreemptionPoints Task}.

Given fixed preemption points, no job can be preempted after a job reaches its last non-preemptive segment. Thus, we can set the task-level run-to-completion threshold to task_cost tsk - (task_last_nonpr_seg tsk - ε), which safely bounds job_cost j - (job_last_nonpr_seg j - ε).