# Library prosa.analysis.facts.preemption.rtc_threshold.job_preemptable

Require Export prosa.analysis.definitions.job_properties.

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

Require Export prosa.model.task.preemption.parameters.

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

Require Export prosa.model.task.preemption.parameters.

# Run-to-Completion Threshold

In this section, we provide a few basic properties of run-to-completion-threshold-compliant schedules.
Consider any type of jobs.

In addition, we assume existence of a function
mapping jobs to their preemption points.

Consider any kind of processor state model, ...

... any job arrival sequence, ...

... and any given schedule.

Assume that the preemption model is valid.

Consider an arbitrary job j from the arrival sequence.

First we prove a few auxiliary lemmas about
job_preemption_points.

We prove that the sequence of preemption points of a zero-cost
job consists of one element -- 0.

For a positive-cost job, 0 ...

... and job_cost are in preemption points.

Therefore, for a positive-cost job size of the sequence of
preemption points is at least two.

Next we show that the sequence of preemption points is a non-decreasing sequence.

Next, we prove that the last element of the sequence of
preemption points is job_cost.

Last non-preemptive segment of a positive-cost job has positive length.

Lemma job_last_nonpreemptive_segment_positive:

job_cost_positive j →

0 < job_last_nonpreemptive_segment j.

job_cost_positive j →

0 < job_last_nonpreemptive_segment j.

Max nonpreemptive segment of a positive-cost job has positive length.

Lemma job_max_nonpreemptive_segment_positive:

job_cost_positive j →

0 < job_max_nonpreemptive_segment j.

job_cost_positive j →

0 < job_max_nonpreemptive_segment j.

Next we show that max nonpreemptive segment is at most the
cost of a job.

We also show that last nonpreemptive segment is at most the
cost of a job.

Lemma job_last_nonpreemptive_segment_le_job_cost:

job_last_nonpreemptive_segment j ≤ job_cost j.

End AuxiliaryLemmas.

job_last_nonpreemptive_segment j ≤ job_cost j.

End AuxiliaryLemmas.

We prove that the run-to-completion threshold is positive for
any job with positive cost. I.e., in order to become
non-preemptive a job must receive at least one unit of
service.

Next we show that the run-to-completion threshold is at most
the cost of a job.

We prove that a job cannot be preempted
during execution of the last segment.

Lemma job_cannot_be_preempted_within_last_segment:

∀ (ρ : duration),

job_rtct j ≤ ρ < job_cost j →

~~ job_preemptable j ρ.

∀ (ρ : duration),

job_rtct j ≤ ρ < job_cost j →

~~ job_preemptable j ρ.

In order to get a consistent schedule, the scheduler should respect
the notion of run-to-completion threshold. We assume that, after
a job reaches its run-to-completion threshold, it cannot be preempted
until its completion.

Lemma job_nonpreemptive_after_run_to_completion_threshold:

∀ t t',

t ≤ t' →

job_rtct j ≤ service sched j t →

~~ completed_by sched j t' →

scheduled_at sched j t'.

End RunToCompletionThreshold.

∀ t t',

t ≤ t' →

job_rtct j ≤ service sched j t →

~~ completed_by sched j t' →

scheduled_at sched j t'.

End RunToCompletionThreshold.

We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically.

Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.