# Library prosa.model.preemption.parameter

Require Export prosa.util.all.

Require Export prosa.behavior.all.

Require Export prosa.model.priority.classes.

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

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

Proof. by move⇒ j rho le; rewrite mem_filter mem_index_iota ltnS le/= andbT. Qed.

∀ (j : Job) (ρ : work),

ρ ≤ job_cost j →

job_preemptable j ρ ↔ ρ \in job_preemption_points j.

Proof. by move⇒ j rho le; rewrite mem_filter mem_index_iota ltnS le/= andbT. Qed.

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_rtct (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 JLDP policy.

Consider any kind of processor model, ...

... any job arrival sequence, ...

... and any given schedule.

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.

Definition preempted_at (j : Job) (t : instant) :=

scheduled_at sched j t.-1

&& ~~ completed_by sched j t

&& ~~ scheduled_at sched j t.

scheduled_at sched j t.-1

&& ~~ completed_by sched j t

&& ~~ scheduled_at sched j 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.

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.

Definition valid_preemption_model :=

∀ j,

arrives_in arr_seq j →

job_cannot_become_nonpreemptive_before_execution j

∧ job_cannot_be_nonpreemptive_after_completion j

∧ not_preemptive_implies_scheduled j

∧ execution_starts_with_preemption_point j.

∀ j,

arrives_in arr_seq j →

job_cannot_become_nonpreemptive_before_execution j

∧ job_cannot_be_nonpreemptive_after_completion j

∧ not_preemptive_implies_scheduled j

∧ execution_starts_with_preemption_point j.

We say that there are no superfluous preemptions if a job can
only be preempted by another job having strictly higher priority.

Definition no_superfluous_preemptions :=

∀ t j j_hp,

preempted_at j t →

scheduled_at sched j_hp t →

~~ hep_job_at t j j_hp.

End PreemptionModel.

∀ t j j_hp,

preempted_at j t →

scheduled_at sched j_hp t →

~~ hep_job_at t j j_hp.

End PreemptionModel.