Library prosa.analysis.facts.preemption.task.floating
Furthermore, we assume the task model with floating non-preemptive regions.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Require Import prosa.model.task.preemption.floating_nonpreemptive.
Platform for Floating Non-Preemptive Regions Model
In this section, we prove that instantiation of functions job_preemptable and task_max_nonpreemptive_segment to the model with floating non-preemptive regions indeed defines a valid preemption model with bounded non-preemptive regions.
Consider any type of tasks ...
... and any type of jobs associated with these tasks.
Context {Job : JobType}.
Context `{JobTask Job Task}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
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.
Consider any arrival sequence.
Next, consider any ideal uni-processor preemption-aware schedule
of this arrival sequence ...
Variable sched : schedule (ideal.processor_state Job).
Hypothesis H_preemption_aware_schedule:
schedule_respects_preemption_model arr_seq sched.
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.
Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
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.
valid_model_with_floating_nonpreemptive_regions arr_seq.
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.
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.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
End FloatingNonPreemptiveRegionsModel.
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
floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
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_facts.