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

Furthermore, we assume the task model with fixed preemption points.

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.
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}.

In addition, we assume the existence of functions mapping a job and task to the sequence of its preemption points.
  Context `{JobPreemptionPoints Job}.
  Context `{TaskPreemptionPoints Task}.

Consider any arrival sequence.
  Variable arr_seq : arrival_sequence Job.

Next, consider any ideal uni-processor preemption-aware schedule of this arrival sequence ...
... where jobs do not execute before their arrival or after completion.
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.
Then we prove that functions job_preemptable and task_preemption_points define a model with bounded non-preemptive regions.
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.
We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
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_facts.