Library prosa.analysis.facts.preemption.task.limited
Furthermore, we assume the task model with fixed preemption points.
Require Import prosa.model.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.
Require Import prosa.model.task.preemption.limited_preemptive.
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 ...
... 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 functions mapping a
job and task 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_schedule_respects_preemption_model:
schedule_respects_preemption_model arr_seq sched.
Hypothesis H_schedule_respects_preemption_model:
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.
Consider an arbitrary task set ts.
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.
Lemma fixed_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_preemption_points defines a valid preemption model with
bounded non-preemptive regions.
Corollary fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions:
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
End LimitedPreemptionsModel.
valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
End LimitedPreemptionsModel.
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.
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.