Library prosa.analysis.facts.preemption.task.floating

Platform for Floating Non-Preemptive Regions Model

In this section, we prove that instantiation of functions job_preemptable and task_max_nonpreemptive_segment for the model with floating non-preemptive regions 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 a function mapping a task to its maximal non-preemptive segment ...
.. and the existence of functions mapping a job to the sequence of its preemption points, ...
  Context `{JobPreemptionPoints Job}.
... 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 ...
... where jobs do not execute before their arrival or after completion.
Next, we assume that preemption points are defined by the model with floating non-preemptive regions.
Then, we prove that the job_preemptable and task_max_nonpreemptive_segment functions 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_max_nonpreemptive_segment define a valid preemption model with bounded non-preemptive regions.
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
     floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
     floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.