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: eqType}.
  Context `{ProcessorState Job PState}.

We begin with 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 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.
      movej t.
      rewrite /job_meets_deadlineCOMP SCHED.
      case: (boolP (t < job_deadline j)) ⇒ //.
      rewrite -leqNgtAFTER_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.
  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.
      split;
        by rewrite /job_meets_deadline /completed_by -SERVICE.
    Qed.

  End EqualProgress.

End DeadlineFacts.