Library prosa.analysis.facts.behavior.deadlines
Consider any given type of jobs with costs and deadlines...
... any given type of processor states.
We begin with schedules / processor models in which scheduled jobs
always receive service.
Consider a given reference schedule...
...in which complete jobs don't execute...
...and scheduled jobs always receive service.
We observe that, if a job is known to meet its deadline, then
its deadline must be later than any point at which it is
scheduled. That is, if a job that meets its deadline is
scheduled at time t, we may conclude that its deadline is at a
time later than t.
Lemma scheduled_at_implies_later_deadline:
∀ j t,
job_meets_deadline sched j →
scheduled_at sched j t →
t < job_deadline j.
End IdealProgressSchedules.
∀ j t,
job_meets_deadline sched j →
scheduled_at sched j t →
t < job_deadline j.
End IdealProgressSchedules.
In the following section, we observe that it is sufficient to
establish that service is invariant across two schedules at a
job's deadline to establish that it either meets its deadline in
both schedules or none.
We observe that, if the service is invariant at the time of a
job's absolute deadline, and if the job meets its deadline in one of the schedules,
then it meets its deadline also in the other schedule.
Lemma service_invariant_implies_deadline_met:
∀ j,
service sched j (job_deadline j) = service sched' j (job_deadline j) →
(job_meets_deadline sched j ↔ job_meets_deadline sched' j).
End EqualProgress.
End DeadlineFacts.
∀ j,
service sched j (job_deadline j) = service sched' j (job_deadline j) →
(job_meets_deadline sched j ↔ job_meets_deadline sched' j).
End EqualProgress.
End DeadlineFacts.