Project Page Index Table of Contents

# Library prosa.model.preemption.limited_preemptive

Require Export prosa.model.preemption.parameter.

# Job Model Parameter for Preemption Points

Under the limited-preemptive preemption model, jobs can be preempted only at a precise set of points during their execution. To allow such fixed, progress-dependent preemption points to be specified, we introduce a new job parameter job_preemptive_points that, for each job, yields the set of progress values at which the job can be preempted by the scheduler.
NB: the job parameter is called job_preemptive_points, rather than job_preemption_points, to avoid a name clash with the definition of the same name.
Class JobPreemptionPoints (Job : JobType) :=
{
job_preemptive_points : Job → seq work
}.

# Preemption Model: Limited-Preemptive Jobs

Based on the above definition of job_preemptive_points, in the following we instantiate job_preemptable for limited-preemptive jobs and introduce requirements that the function job_preemptive_points should satisfy to be coherent with the limited-preemptive preemption model.
Section LimitedPreemptions.
Consider any type of jobs with arrival times and execution costs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Given each job's preemption points, as determined by job_preemptive_points, ...
Context `{JobPreemptionPoints Job}.
...a job j is preemptable at a given point of progress ρ iff ρ is one of the preemption points of j.
#[local] Instance limited_preemptive_job_model : JobPreemptable Job :=
{
job_preemptable (j : Job) (ρ : work) := ρ \in job_preemptive_points j
}.

## Model Validity

Next, we introduce some structural properties that a valid sequence of preemption points must satisfy.
Section ValidLimitedPreemptiveModel.
Consider any arrival sequence.
Variable arr_seq : arrival_sequence Job.
We require the sequence of preemption points to contain the beginning ...
Definition beginning_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → 0 \in job_preemptive_points j.
... and the end of execution for any job j that arrives in the given arrival sequence arr_seq.
Definition end_of_execution_in_preemption_points :=
∀ j, arrives_in arr_seq j → last0 (job_preemptive_points j) = job_cost j.
We further require the sequence of preemption points to be a non-decreasing sequence.
Definition preemption_points_is_nondecreasing_sequence :=
∀ j, arrives_in arr_seq j → nondecreasing_sequence (job_preemptive_points j).
A job model is considered valid w.r.t. limited-preemptive preemption model if it satisfies each of the preceding definitions.
Definition valid_limited_preemptions_job_model :=
beginning_of_execution_in_preemption_points
∧ end_of_execution_in_preemption_points
∧ preemption_points_is_nondecreasing_sequence.
End ValidLimitedPreemptiveModel.
End LimitedPreemptions.