Library prosa.analysis.facts.busy_interval.arrival
Require Export prosa.analysis.definitions.busy_interval.classical.
Require Export prosa.analysis.facts.busy_interval.hep_at_pt.
Require Export prosa.analysis.facts.busy_interval.hep_at_pt.
In this section, 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 BasicFacts.
∀ j t t',
busy_interval arr_seq sched j t t' →
t ≤ job_arrival j.
End BasicFacts.
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.
In the following section, we prove additional, more involved
properties about arrival times within busy intervals.
Consider any kind of jobs...
... and a reflexive JLFP policy defined on these jobs.
Consider any processor state model.
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 any schedule of this arrival sequence ...
Variable sched : schedule PState.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
... 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 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.