Project Page Index Table of Contents

# Library prosa.analysis.definitions.schedule_prefix

Require Export prosa.behavior.ready.
Require Export prosa.util.nat.
We define the notion of prefix-equivalence of schedules.
Section PrefixDefinition.
For any type of jobs...
Context {Job : JobType}.
... and any kind of processor model, ...
Context {PState : ProcessorState Job}.
... two schedules share an identical prefix if they are pointwise identical (at least) up to a fixed horizon.
Definition identical_prefix (sched sched' : schedule PState) (horizon : instant) :=
∀ t,
t < horizon →
sched t = sched' t.
In other words, two schedules with a shared prefix are completely interchangeable w.r.t. whether a job is scheduled (in the prefix).
Fact identical_prefix_scheduled_at :
∀ sched sched' h,
identical_prefix sched sched' h →
∀ j t,
t < h →
scheduled_at sched j t = scheduled_at sched' j t.
Proof.
move⇒ sched sched' h IDENT j t LT_h.
now rewrite /scheduled_at (IDENT t LT_h).
Qed.
Trivially, any prefix of an identical prefix is also an identical prefix.
Fact identical_prefix_inclusion :
∀ sched sched' h h',
h' ≤ h →
identical_prefix sched sched' h → identical_prefix sched sched' h'.
Proof. by move⇒ sched sched' h h' h'_le_h + t t_lt_h'; apply; apply: leq_trans h'_le_h. Qed.
End PrefixDefinition.