Library prosa.analysis.facts.behavior.deadlines

Require Export prosa.analysis.facts.behavior.completion.

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

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

Hypothesis H_completed_jobs: completed_jobs_dont_execute sched.

...and scheduled jobs always receive service.

Hypothesis H_scheduled_implies_serviced: ideal_progress_proc_model PState.

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.

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

  End EqualProgress.

End DeadlineFacts.