Commit eba1805a authored by Björn Brandenburg's avatar Björn Brandenburg

additional minor lemmas on job arrivals

parent 5aee1165
......@@ -3,6 +3,37 @@ Require Export prosa.util.all.
(** * Arrival Sequence *)
(** First, we relate the stronger to the weaker arrival predicates. *)
Section ArrivalPredicates.
(** Consider any kinds of jobs with arrival times. *)
Context {Job : JobType} `{JobArrival Job}.
(** A job that arrives in some interval [[t1, t2)] certainly arrives before
time [t2]. *)
Lemma arrived_between_before:
forall j t1 t2,
arrived_between j t1 t2 ->
arrived_before j t2.
move=> j t1 t2.
now rewrite /arrived_before /arrived_between => /andP [_ CLAIM].
(** A job that arrives before a time [t] certainly has arrived by time
[t]. *)
Lemma arrived_before_has_arrived:
forall j t,
arrived_before j t ->
has_arrived j t.
move=> j t.
rewrite /arrived_before /has_arrived.
now apply ltnW.
End ArrivalPredicates.
(** In this section, we relate job readiness to [has_arrived]. *)
Section Arrived.
......@@ -51,6 +82,16 @@ Section Arrived.
by apply ready_implies_arrived.
(** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
Corollary backlogged_implies_arrived:
forall j t,
backlogged sched j t -> has_arrived j t.
rewrite /backlogged.
move=> j t /andP [READY _].
now apply ready_implies_arrived.
End Arrived.
(** In this section, we establish useful facts about arrival sequence prefixes. *)
......@@ -199,4 +240,4 @@ Section ArrivalSequencePrefix.
End ArrivalTimes.
End ArrivalSequencePrefix.
\ No newline at end of file
End ArrivalSequencePrefix.
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment