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

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.
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

In addition, we assume existence of a function mapping jobs to theirs preemption points.
  Context `{JobPreemptable Job}.

Consider any kind of processor state model, ...
  Context {PState : Type}.
  Context `{ProcessorState Job PState}.

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

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.
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.
Max nonpreemptive segment of a positive-cost job has positive length.
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.
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.
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.
We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.