Library prosa.analysis.facts.model.overheads.schedule
Require Import prosa.model.processor.overheads.
Require Export prosa.analysis.facts.busy_interval.pi.
Require Export prosa.analysis.facts.busy_interval.pi.
In this section, we prove a few basic properties of the processor
model with explicit overheads.
Consider any type of jobs.
First, we prove that that the processor model with overheads is
a uni-processor model.
Lemma overheads_proc_model_is_a_uniprocessor_model :
uniprocessor_model (overheads.processor_state Job).
uniprocessor_model (overheads.processor_state Job).
The processor model with overheads is a unit-supply model.
Lemma overheads_proc_model_provides_unit_supply :
unit_supply_proc_model (overheads.processor_state Job).
End OverheadsProceProperties.
unit_supply_proc_model (overheads.processor_state Job).
End OverheadsProceProperties.
We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
will be able to apply them automatically.
Global Hint Resolve
overheads_proc_model_is_a_uniprocessor_model
overheads_proc_model_provides_unit_supply
: basic_rt_facts.
overheads_proc_model_is_a_uniprocessor_model
overheads_proc_model_provides_unit_supply
: basic_rt_facts.
In this section, we prove basic properties of schedules with
explicit overheads.
Consider any type of jobs.
Consider any schedule with explicit overheads.
At any time t, either the processor is idle (no job is
scheduled), or some job is scheduled at that time.
We next prove that the predicate scheduled_at and the function
scheduled_job agree.
Lemma scheduled_at_iff_scheduled_job :
∀ j t,
scheduled_at sched j t ↔ scheduled_job sched t = Some j.
End OverheadScheduleProperties.
∀ j t,
scheduled_at sched j t ↔ scheduled_job sched t = Some j.
End OverheadScheduleProperties.
In this section, we show that, in the stated model with overheads,
there are no idle times within a busy interval.
Consider any type of jobs.
Consider a JLFP-policy that indicates a higher-or-equal priority
relation, and assume that this relation is reflexive and
transitive.
Context {JLFP : JLFP_policy Job}.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
Hypothesis H_priority_is_reflexive : reflexive_job_priorities JLFP.
Hypothesis H_priority_is_transitive : transitive_job_priorities JLFP.
Consider any arrival sequence with consistent non-duplicate arrivals.
Variable arr_seq : arrival_sequence Job.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
Next, consider a schedule, ...
... allow for any work-bearing notion of job readiness, ...
Context `{!JobReady Job (overheads.processor_state Job)}.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
Hypothesis H_job_ready : work_bearing_readiness arr_seq sched.
... and assume that the schedule is valid and work-conserving.
Hypothesis H_sched_valid : valid_schedule sched arr_seq.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Hypothesis H_work_conserving : work_conserving arr_seq sched.
Consider an arbitrary job j with positive cost.
Variable j : Job.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Hypothesis H_from_arrival_sequence : arrives_in arr_seq j.
Hypothesis H_job_cost_positive : job_cost_positive j.
Consider any busy interval prefix
[t1, t2) of job j.
Variables t1 t2 : instant.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.
Hypothesis H_busy_interval_prefix : busy_interval_prefix arr_seq sched j t1 t2.
Then, we prove that, for every time instant within the busy
interval prefix, some job is scheduled.