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.

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.

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.

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.

  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.

  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.