# Library prosa.model.preemption.parameter

Require Export prosa.util.all.
Require Export prosa.behavior.all.
Require Export prosa.model.priority.classes.

# Job-Level Preemption Model

There are many equivalent ways to represent at which points in time a job is preemptable, i.e., where it can be forced to relinquish the processor on which it is executing. In Prosa, the various preemption models are represented with a single predicate job_preemptable that indicates, for given a job and a given degree of progress, whether the job is preemptable at its current point of execution.

# Maximum and Last Non-preemptive Segment of a Job

In the following section we define the notions of the maximal and the last non-preemptive segments.
Consider any type of jobs with arrival times and execution costs...
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.

... and consider any given preemption model.
Context `{JobPreemptable Job}.

It is useful to define a representation of the preemption points of a job as an actual sequence of points where this job can be preempted. To this end, we define job_preemption_points j as the sequence of all progress values at which job j is preemptable, according to job_preemptable.
Definition job_preemption_points (j : Job) : seq work :=
[seq ρ : work <- range 0 (job_cost j) | job_preemptable j ρ].

We observe that the conversion indeed is an equivalent way of representing the set of preemption points.
We further define a function that, for a given job, yields the sequence of lengths of its nonpreemptive segments.
Next, we define a function that determines the length of a job's longest nonpreemptive segment (or zero if the job is fully preemptive).
Similarly, we define a function that yields the length of a job's last nonpreemptive segment (or zero if the job is fully preemptive).

# Run-to-Completion Threshold of a Job

Finally, we define the notion of a job's run-to-completion threshold (RTCT): the run-to-completion threshold is the amount of service after which a job cannot be preempted until its completion.

# Model Validity

In the following, we define properties that any reasonable job preemption model must satisfy.
Section PreemptionModel.

Consider any type of jobs with arrival times and execution costs...
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.

... and any preemption model.
Context `{JobPreemptable Job}.

Consider any JLDP policy.
Context `{JLDP_policy Job}.

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

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

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

We say that a job is preempted_at t if the job is scheduled at t-1 and not scheduled at t, but not completed by t.
In the following, we define the notion of a valid preemption model. To begin with, we require that a job has to be executed at least one time instant in order to reach a nonpreemptive segment. In other words, a job must start execution to become non-preemptive.
And vice versa, a job cannot remain non-preemptive after its completion.
Next, if a job j is not preemptable at some time instant t, then j must be scheduled at time t.
A job can start its execution only from a preemption point.
We say that a preemption model is a valid preemption model if all assumptions given above are satisfied for any job.
We say that there are no superfluous preemptions if a job can only be preempted by another job having strictly higher priority.