# 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.

Proof.

move⇒ j t.

rewrite /job_meets_deadline ⇒ COMP SCHED.

case: (boolP (t < job_deadline j)) ⇒ //.

rewrite -leqNgt ⇒ AFTER_DL.

apply completion_monotonic with (t' := t) in COMP ⇒ //.

apply scheduled_implies_not_completed in SCHED ⇒ //.

move/negP in SCHED. contradiction.

Qed.

End IdealProgressSchedules.

∀ j t,

job_meets_deadline sched j →

scheduled_at sched j t →

t < job_deadline j.

Proof.

move⇒ j t.

rewrite /job_meets_deadline ⇒ COMP SCHED.

case: (boolP (t < job_deadline j)) ⇒ //.

rewrite -leqNgt ⇒ AFTER_DL.

apply completion_monotonic with (t' := t) in COMP ⇒ //.

apply scheduled_implies_not_completed in SCHED ⇒ //.

move/negP in SCHED. contradiction.

Qed.

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).

Proof.

move⇒ j SERVICE.

split;

by rewrite /job_meets_deadline /completed_by -SERVICE.

Qed.

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).

Proof.

move⇒ j SERVICE.

split;

by rewrite /job_meets_deadline /completed_by -SERVICE.

Qed.

End EqualProgress.

End DeadlineFacts.