Library prosa.analysis.definitions.overheads.priority_bump

Require Export prosa.model.processor.overheads.
Require Export prosa.model.priority.classes.

In this section, we define the notion of a priority bump.

Section PriorityBump.

Consider any type of jobs.

Context {Job : JobType}.

Consider a JLFP-policy.

Context {JLFP : JLFP_policy Job}.

Consider any explicit-overhead uni-processor schedule.

Variable sched : schedule (overheads.processor_state Job).

Time t is a priority bump if the job scheduled at time t has strictly higher priority than the job scheduled at time t−1. A priority bump also occurs if the processor was idle at time t−1 and starts executing a job at time t.

  Definition priority_bump (t : instant) :=
    match scheduled_job sched t .-1, scheduled_job sched t with
    | None, None ⇒ false
    | None, Some _ ⇒ true
    | Some _, None ⇒ false
    | Some j1, Some j2 ⇒ ~~ hep_job j1 j2
    end.

End PriorityBump.