Library prosa.analysis.definitions.progress

Require Export prosa.analysis.facts.behavior.service.

Job Progress (or Lack Thereof)

In the following section, we define a notion of "job progress", and conversely a notion of a lack of progress.

Section Progress.

Consider any type of jobs with a known cost...
  Context {Job : JobType}.
  Context `{JobCost Job}.

... and any kind of schedule.
  Context {PState : ProcessorState Job}.

For a given job and a given schedule...
  Variable sched : schedule PState.
  Variable j : Job.

  Section NotionsOfProgress.

...and two ordered points in time...
    Variable t1 t2 : nat.
    Hypothesis H_t1_before_t2: t1 ≤ t2.

... we say that the job has progressed between the two points iff its total received service has increased.
    Definition job_has_progressed := service sched j t1 < service sched j t2.

Conversely, if the accumulated service does not change, there is no progress.
    Definition no_progress := service sched j t1 == service sched j t2.

We note that the negation of the former is equivalent to the latter definition.
    Lemma no_progress_equiv: ~~ job_has_progressed ↔ no_progress.
    Proof.
      rewrite /job_has_progressed /no_progress.
      split.
      { rewrite -leqNgt leq_eqVlt ⇒ /orP [EQ|LT]; first by rewrite eq_sym.
        exfalso.
        have MONO: service sched j t1 ≤ service sched j t2
          by apply service_monotonic.
        have NOT_MONO: ~~ (service sched j t1 ≤ service sched j t2)
          by apply /negPf; apply ltn_geF.
        move: NOT_MONO ⇒ /negP NOT_MONO.
        contradiction. }
      { move ⇒ /eqP →.
        rewrite -leqNgt.
        by apply service_monotonic. }
    Qed.

  End NotionsOfProgress.

For convenience, we define a lack of progress also in terms of given reference point t and the length of the preceding interval of inactivity delta, meaning that no progress has been made for at least delta time units.
  Definition no_progress_for (t : instant) (delta : duration) := no_progress (t - delta) t.

End Progress.