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

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

# 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.
Section FloatingNonPreemptiveRegionsModel.
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 ...
Context `{TaskMaxNonpreemptiveSegment Task}.
.. 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 preemption-aware schedule of this arrival sequence...
Context {PState : ProcessorState Job}.
Variable sched : schedule PState.
Hypothesis H_preemption_aware_schedule :
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 : seq Task.
Next, we assume that preemption points are defined by the model with floating non-preemptive regions.
Hypothesis H_valid_model_with_floating_nonpreemptive_regions :
valid_model_with_floating_nonpreemptive_regions arr_seq ts.
Then, we prove that the job_preemptable and task_max_nonpreemptive_segment functions define a model with bounded non-preemptive regions.
Lemma floating_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_max_nonpreemptive_segment define a valid preemption model with bounded non-preemptive regions.
Corollary floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions :
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
End FloatingNonPreemptiveRegionsModel.
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.