# Library prosa.analysis.facts.behavior.deadlines

Consider any given type of jobs with costs and deadlines...

... any given type of processor states.

First, we derive two properties from the fact that a job is incomplete at
some point in time.

Consider any given schedule.

Trivially, a job that both meets its deadline and is incomplete at a
time t must have a deadline later than t.

Lemma incomplete_implies_later_deadline:

∀ j t,

job_meets_deadline sched j →

~~ completed_by sched j t →

t < job_deadline j.

Proof.

move⇒ j t MET INCOMP; apply: contraT; rewrite -leqNgt ⇒ PAST_DL.

have /negP// : ~~ completed_by sched j (job_deadline j).

exact: incompletion_monotonic INCOMP.

Qed.

∀ j t,

job_meets_deadline sched j →

~~ completed_by sched j t →

t < job_deadline j.

Proof.

move⇒ j t MET INCOMP; apply: contraT; rewrite -leqNgt ⇒ PAST_DL.

have /negP// : ~~ completed_by sched j (job_deadline j).

exact: incompletion_monotonic INCOMP.

Qed.

Furthermore, a job that both meets its deadline and is incomplete at a
time t must be scheduled at some point between t and its
deadline.

Lemma incomplete_implies_scheduled_later:

∀ j t,

job_meets_deadline sched j →

~~ completed_by sched j t →

∃ t', t ≤ t' < job_deadline j ∧ scheduled_at sched j t'.

Proof.

move⇒ j t MET INCOMP.

apply: cumulative_service_implies_scheduled.

rewrite -(ltn_add2l (service sched j t)) addn0.

rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline.

by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete.

Qed.

End Incompletion.

∀ j t,

job_meets_deadline sched j →

~~ completed_by sched j t →

∃ t', t ≤ t' < job_deadline j ∧ scheduled_at sched j t'.

Proof.

move⇒ j t MET INCOMP.

apply: cumulative_service_implies_scheduled.

rewrite -(ltn_add2l (service sched j t)) addn0.

rewrite service_cat; last exact/ltnW/incomplete_implies_later_deadline.

by apply: leq_trans MET; rewrite less_service_than_cost_is_incomplete.

Qed.

End Incompletion.

Next, we look at 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 meets its deadline and is scheduled at time
t, then then 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 MET SCHED_AT.

apply: (incomplete_implies_later_deadline sched) ⇒ //.

exact: scheduled_implies_not_completed.

Qed.

End IdealProgressSchedules.

∀ j t,

job_meets_deadline sched j →

scheduled_at sched j t →

t < job_deadline j.

Proof.

move⇒ j t MET SCHED_AT.

apply: (incomplete_implies_later_deadline sched) ⇒ //.

exact: scheduled_implies_not_completed.

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.

by split; 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.

by split; rewrite /job_meets_deadline /completed_by -SERVICE.

Qed.

End EqualProgress.

End DeadlineFacts.