Library prosa.analysis.facts.preemption.task.limited

Require Export prosa.analysis.facts.preemption.job.limited.
Require Export prosa.model.task.preemption.limited_preemptive.

Platform for Models with Limited Preemptions

In this section, we prove that instantiation of functions job_preemptable and task_preemption_points to the limited preemptions model indeed defines a valid preemption model with bounded non-preemptive regions.
Section LimitedPreemptionsModel.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

We assume that jobs are preemptable only at specific points during their execution, ...
  Context `{JobPreemptionPoints Job}.
  Context `{TaskPreemptionPoints Task}.
... i.e., we assume limited-preemptive jobs.
  #[local] Existing Instance limited_preemptive_job_model.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor preemption-aware 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.

... where jobs do not execute before their arrival or after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Consider an arbitrary task set ts.
  Variable ts : list Task.

Next, we assume that preemption points are defined by the model with fixed preemption points.
  Hypothesis H_valid_fixed_preemption_points_model:
    valid_fixed_preemption_points_model arr_seq ts.

Then we prove that functions job_preemptable and task_preemption_points define a model with bounded non-preemptive regions.
  Lemma fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions:
    model_with_bounded_nonpreemptive_segments arr_seq .

Which together with lemma valid_fixed_preemption_points_model gives us the fact that functions job_preemptable and task_preemption_points defines a valid preemption model with bounded non-preemptive regions.
  Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
    valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

End LimitedPreemptionsModel.

We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically.
Global Hint Resolve
     valid_fixed_preemption_points_model_lemma
     fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
     fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.