Library prosa.model.preemption.parameter
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...
... and consider any given preemption model.
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 ρ].
[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.
Remark conversion_preserves_equivalence:
∀ (j : Job) (ρ : work),
ρ ≤ job_cost j →
job_preemptable j ρ ↔ ρ \in job_preemption_points j.
∀ (j : Job) (ρ : work),
ρ ≤ job_cost j →
job_preemptable j ρ ↔ ρ \in job_preemption_points j.
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
Definition job_run_to_completion_threshold (j : Job) :=
job_cost j - (job_last_nonpreemptive_segment j - ε).
End MaxAndLastNonpreemptiveSegment.
job_cost j - (job_last_nonpreemptive_segment j - ε).
End MaxAndLastNonpreemptiveSegment.
Model Validity
In the following, we define properties that any reasonable job preemption model must satisfy.
Consider any type of jobs with arrival times and execution costs...
... and any preemption model.
Consider any kind of processor model, ...
... any job arrival sequence, ...
... and any given schedule.
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.
Definition job_cannot_be_nonpreemptive_after_completion (j : Job) :=
job_preemptable j (job_cost j).
job_preemptable j (job_cost j).
Definition not_preemptive_implies_scheduled (j : Job) :=
∀ t,
~~ job_preemptable j (service sched j t) →
scheduled_at sched j t.
∀ t,
~~ job_preemptable j (service sched j t) →
scheduled_at sched j t.
A job can start its execution only from a preemption point.
Definition execution_starts_with_preemption_point (j : Job) :=
∀ prt,
~~ scheduled_at sched j prt →
scheduled_at sched j prt.+1 →
job_preemptable j (service sched j prt.+1).
∀ prt,
~~ scheduled_at sched j prt →
scheduled_at sched j prt.+1 →
job_preemptable j (service sched j prt.+1).
We say that a preemption model is a valid preemption model if
all assumptions given above are satisfied for any job.