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

Require Export prosa.model.job.properties.
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.
Section RunToCompletionThreshold.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
In addition, we assume existence of a function mapping jobs to their preemption points.
Context `{JobPreemptable Job}.
Consider any kind of processor state model, ...
Context {PState : ProcessorState Job}.
... any job arrival sequence, ...
Variable arr_seq : arrival_sequence Job.
... and any given schedule.
Variable sched : schedule PState.
Assume that the preemption model is valid.
Hypothesis H_valid_preemption_model :
valid_preemption_model arr_seq sched.
Consider an arbitrary job j from the arrival sequence.
Variable j : Job.
Hypothesis H_j_arrives : arrives_in arr_seq j.
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.
Lemma preemption_points_of_zero_cost_job :
job_cost j = 0 →
job_preemption_points j = [::0].
For a positive-cost job, 0 ...
Lemma zero_in_preemption_points :
0 < job_cost j →
0 \in job_preemption_points j.
... and job_cost are in preemption points.
Lemma job_cost_in_preemption_points :
0 < job_cost j →
job_cost j \in job_preemption_points j.
Therefore, for a positive-cost job size of the sequence of preemption points is at least two.
Lemma size_of_preemption_points :
0 < job_cost j →
2 ≤ size (job_preemption_points j).
Next we show that the sequence of preemption points is a non-decreasing sequence.
Lemma preemption_points_nondecreasing :
nondecreasing_sequence (job_preemption_points j).
Next, we prove that the last element of the sequence of preemption points is job_cost.
Lemma job_cost_is_last_element_of_preemption_points :
job_cost j = last0 (job_preemption_points j).
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.
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.
Next we show that max nonpreemptive segment is at most the cost of a job.
Lemma job_max_nonpreemptive_segment_le_job_cost :
job_max_nonpreemptive_segment j ≤ job_cost j.
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.
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.
Lemma job_run_to_completion_threshold_positive :
job_cost_positive j →
0 < job_rtct j.
Next we show that the run-to-completion threshold is at most the cost of a job.
Lemma job_run_to_completion_threshold_le_job_cost :
job_rtct j ≤ job_cost j.
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 ρ.
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.
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.