# Library prosa.analysis.facts.preemption.job.limited

Require Export prosa.model.schedule.limited_preemptive.

Require Export prosa.analysis.definitions.job_properties.

Require Export prosa.analysis.facts.behavior.all.

Require Export prosa.analysis.facts.model.sequential.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.model.preemption.limited_preemptive.

Require Export prosa.analysis.definitions.job_properties.

Require Export prosa.analysis.facts.behavior.all.

Require Export prosa.analysis.facts.model.sequential.

Require Export prosa.analysis.facts.model.ideal.schedule.

Require Export prosa.model.preemption.limited_preemptive.

# Platform for Models with Limited Preemptions

In this section, we prove that instantiation of predicate job_preemptable to the model with limited preemptions indeed defines a valid preemption model.
Consider any type of tasks ...

... and any type of jobs associated with these tasks.

Context {Job : JobType}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

Context `{JobTask Job Task}.

Context `{JobArrival Job}.

Context `{JobCost Job}.

In addition, assume the existence of a function that maps a job
to the sequence of its preemption points...

..., i.e., we assume limited-preemptive jobs.

#[local] Existing Instance limited_preemptive_job_model.

Consider any arrival sequence.

Next, consider any limited ideal uni-processor schedule of this arrival sequence ...

Variable sched : schedule (ideal.processor_state Job).

Hypothesis H_schedule_respects_preemption_model:

schedule_respects_preemption_model arr_seq sched.

Hypothesis H_schedule_respects_preemption_model:

schedule_respects_preemption_model arr_seq sched.

...where jobs do not execute after their completion.

Next, we assume that preemption points are defined by the
job-level model with limited preemptions.

First, we prove a few auxiliary lemmas.

Consider a job j.

Recall that 0 is a preemption point.

Using the fact that job_preemptive_points is a
non-decreasing sequence, we prove that the first element of
job_preemptive_points is 0.

We prove that the list of preemption points is not empty.

Next, we prove that the cost of a job is a preemption point.

As a corollary, we prove that the sequence of non-preemptive
points of a job with positive cost contains at least 2
points.

Corollary number_of_preemption_points_at_least_two:

job_cost_positive j →

2 ≤ size (job_preemptive_points j).

job_cost_positive j →

2 ≤ size (job_preemptive_points j).

Next we prove that "anti-density" property (from
preemption.util file) holds for job_preemption_point j.

Lemma antidensity_of_preemption_points:

∀ (ρ : work),

ρ ≤ job_cost j →

~~ (ρ \in job_preemptive_points j) →

first0 (job_preemptive_points j) ≤ ρ < last0 (job_preemptive_points j).

∀ (ρ : work),

ρ ≤ job_cost j →

~~ (ρ \in job_preemptive_points j) →

first0 (job_preemptive_points j) ≤ ρ < last0 (job_preemptive_points j).

We also prove that any work that doesn't belong to
preemption points of job j is placed strictly between two
neighboring preemption points.

Lemma work_belongs_to_some_nonpreemptive_segment:

∀ (ρ : work),

ρ ≤ job_cost j →

~~ (ρ \in job_preemptive_points j) →

∃ n,

n.+1 < size (job_preemptive_points j) ∧

nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1.

∀ (ρ : work),

ρ ≤ job_cost j →

~~ (ρ \in job_preemptive_points j) →

∃ n,

n.+1 < size (job_preemptive_points j) ∧

nth 0 (job_preemptive_points j) n < ρ < nth 0 (job_preemptive_points j) n.+1.

Recall that the module prosa.model.preemption.parameters also defines
a notion of preemption points, namely job_preemption_points, which
cannot have duplicated preemption points. Therefore, we need additional
lemmas to relate job_preemption_points and job_preemptive_points.
First we show that the length of the last non-preemptive segment in
job_preemption_points is equal to the length of the last non-empty
non-preemptive segment of job_preemptive_points.

Lemma job_parameters_last_np_to_job_limited:

last0 (distances (job_preemption_points j)) =

last0 (filter (fun x ⇒ 0 < x) (distances (job_preemptive_points j))).

last0 (distances (job_preemption_points j)) =

last0 (filter (fun x ⇒ 0 < x) (distances (job_preemptive_points j))).

Next we show that the length of the max non-preemptive segment of
job_preemption_points is equal to the length of the max non-preemptive
segment of job_preemptive_points.

Lemma job_parameters_max_np_to_job_limited:

max0 (distances (job_preemption_points j)) =

max0 (distances (job_preemptive_points j)).

End AuxiliaryLemmas.

max0 (distances (job_preemption_points j)) =

max0 (distances (job_preemptive_points j)).

End AuxiliaryLemmas.

We prove that the fixed_preemption_point_model function
defines a valid preemption model.

Lemma valid_fixed_preemption_points_model_lemma:

valid_preemption_model arr_seq sched.

End ModelWithLimitedPreemptions.

Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.

valid_preemption_model arr_seq sched.

End ModelWithLimitedPreemptions.

Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.