Library prosa.analysis.facts.preemption.task.nonpreemptive

Platform for Fully Non-Preemptive Model

In this section, we prove that instantiation of functions job_preemptable and task_max_nonpreemptive_segment to the fully non-preemptive 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}.

Assume a fully non-preemptive task model.
  #[local] Existing Instance fully_nonpreemptive_job_model.
  #[local] Existing Instance fully_nonpreemptive_task_model.
  #[local] Existing Instance fully_nonpreemptive_rtc_threshold.

Consider any arrival sequence with consistent arrivals.
Next, consider any ideal non-preemptive uni-processor schedule of this arrival sequence...
... where jobs do not execute before their arrival or after completion.
Assume that a job cost cannot be larger than a task cost.
Then we prove that the fully_nonpreemptive_model function defines a model with bounded non-preemptive regions.
Which together with lemma valid_fully_nonpreemptive_model gives us the fact that fully_nonpreemptive_model defined 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_fully_nonpreemptive_model
     fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
     fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.