Library prosa.analysis.facts.behavior.deadlines

Deadlines

In this file, we observe basic properties of the behavioral job model w.r.t. deadlines.
Section DeadlineFacts.

Consider any given type of jobs with costs and deadlines...
  Context {Job : JobType} `{JobCost Job} `{JobDeadline Job}.

... any given type of processor states.
  Context {PState: ProcessorState Job}.

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

Consider any given schedule.
    Variable sched: schedule PState.

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.
      movej t MET INCOMP; apply: contraT; rewrite -leqNgtPAST_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.
      movej 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.
  Section IdealProgressSchedules.

Consider a given reference schedule...
    Variable sched: schedule PState.

...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.
      movej 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.
  Section EqualProgress.

Consider any two schedules sched and sched'.
    Variable sched sched': schedule PState.

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.
      movej SERVICE.
      by split; rewrite /job_meets_deadline /completed_by -SERVICE.
    Qed.

  End EqualProgress.

End DeadlineFacts.