# Library prosa.analysis.definitions.progress

# Job Progress (or Lack Thereof)

Consider any type of jobs with a known cost...

... and any kind of schedule.

For a given job and a given schedule...

...and two ordered points in time...

... we say that the job has progressed between the two points iff its
total received service has increased.

Conversely, if the accumulated service does not change, there is no
progress.

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.

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.

End Progress.