Library prosa.analysis.facts.busy_interval.arrival
In this module we collect some basic facts about arrival times in busy
windows. These are primarily useful for proof automation.
Consider any kind of jobs...
... and a JLFP policy defined on these jobs.
Consider any processor state model.
Consider any schedule and arrival sequence.
We note the trivial fact that, by definition, a job arrives after the
beginning of its busy-interval prefix ...
Fact busy_interval_prefix_job_arrival :
∀ j t t',
busy_interval_prefix arr_seq sched j t t' →
t ≤ job_arrival j.
∀ j t t',
busy_interval_prefix arr_seq sched j t t' →
t ≤ job_arrival j.
... and hence also after the beginning of its busy interval.
Fact busy_interval_job_arrival :
∀ j t t',
busy_interval arr_seq sched j t t' →
t ≤ job_arrival j.
End Facts.
∀ j t t',
busy_interval arr_seq sched j t t' →
t ≤ job_arrival j.
End Facts.
We add the above facts into the "Hint Database" basic_rt_facts, so Coq will
be able to apply them automatically where needed.
Global Hint Resolve
busy_interval_prefix_job_arrival
busy_interval_job_arrival
: basic_rt_facts.
busy_interval_prefix_job_arrival
busy_interval_job_arrival
: basic_rt_facts.