Library prosa.model.priority.fp

Require Export prosa.model.priority.classes.

Fixed-Priority Policy

We define what it means for an abstract job-level fixed-priority policy to behave as fixed-priority scheduling with respect to a task-level fixed-priority policy.

Section FPPolicy.

Consider any type of tasks ...

Context {Task : TaskType}.

... and jobs of these tasks.

Context {Job : JobType} `{JobTask Job Task}.

Given an underlying FP policy, a JLFP policy behaves as an FP policy if it never inverts task-level priority, and every strict task-priority relation is reflected at the job level. Jobs of equal-priority tasks may be ordered by any reflexive, transitive, and total tie-breaking rule.

  Definition policy_is_FP (FP : FP_policy Task) (JLFP : JLFP_policy Job) :=
    (∀ j1 j2,
        hep_job j1 j2 →
        hep_task (job_task j1) (job_task j2))
    ∧ (∀ j1 j2,
          hp_task (job_task j1) (job_task j2) →
          hep_job j1 j2 )
    ∧ reflexive_job_priorities JLFP
    ∧ transitive_job_priorities JLFP
    ∧ total_job_priorities JLFP.

End FPPolicy.