# Library prosa.analysis.facts.model.overheads.schedule

Require Import prosa.model.processor.overheads.
Require Export prosa.analysis.facts.busy_interval.pi.
In this section, we prove a few basic properties of the processor model with explicit overheads.
Section OverheadsProceProperties.
Local Transparent scheduled_in scheduled_on service_in service_on.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
First, we prove 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).
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).
We also show that the processor model is fully consuming. That is, if a job is scheduled at time t, then it receives the entire supply produced at that time as service.
Lemma overheads_proc_model_fully_consuming :
fully_consuming_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
overheads_proc_model_fully_consuming
: basic_rt_facts.
In this section, we prove basic properties of schedules with explicit overheads.
Section OverheadScheduleProperties.
Local Transparent scheduled_in scheduled_on.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
Consider any schedule with explicit overheads.
Variable sched : schedule (overheads.processor_state Job).
At any time t, either the processor is idle (no job is scheduled), or some job is scheduled at that time.
Lemma scheduled_job_dec :
∀ t,
scheduled_job sched t = None ∨ ∃ j, scheduled_job sched t = Some j.
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.
In this section, we show that, in the stated model with overheads, there are no idle times within a busy interval.
Section ScheduledInBusyPrefix.
Consider any type of jobs.
Context {Job : JobType}.
Context `{JobArrival Job}.
Context `{JobCost Job}.
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.
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.
Next, consider a schedule, ...
Variable sched : schedule (overheads.processor_state Job).
... allow for any work-bearing notion of job readiness, ...
Context {RM : JobReady Job (overheads.processor_state Job)}.
Hypothesis H_job_ready : work_bearing_readiness RM 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.
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.
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.
Then, we prove that, for every time instant within the busy interval prefix, some job is scheduled.
Lemma job_scheduled_in_busy_interval_prefix :
∀ t,
t1 ≤ t < t2 →
∃ jo,
scheduled_at sched jo t.
End ScheduledInBusyPrefix.