Library prosa.implementation.priority.tiebreaks_by_id

Require Export prosa.model.priority.classes.
Require Export prosa.implementation.definitions.parameters.

Breaking JLFP Priority Ties by Identifier

This adapter refines a given job-level fixed-priority policy by favoring lower task IDs, and then lower job IDs, among jobs of equal priority.

Section TiebreaksById.

Consider tasks with numeric identifiers ...

Context {Task : TaskType} `{TaskId Task}.

... and their jobs, also with numeric identifiers.

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

The supplied policy determines the primary priority order.

Variable JLFP : JLFP_policy Job.

We give its comparison rule a local name to distinguish primary priorities from those produced by the adapter.

Let primary_hep_job := @hep_job Job JLFP.

Strict primary priorities take precedence. When the primary policy grants priority in both directions, identifiers determine the order.

  #[local] Instance tiebreaks_by_id : JLFP_policy Job :=
  {
    hep_job (j1 j2 : Job) :=
      primary_hep_job j1 j2
      && (~~ primary_hep_job j2 j1
          || (task_id (job_task j1) < task_id (job_task j2))
          || ((task_id (job_task j1) == task_id (job_task j2))
              && (job_id j1 ≤ job_id j2 )))
  }.

We expose the adapter's comparison rule for use in scheduling proofs.

  Fact tiebreaks_by_id_hep_job :
    ∀ j1 j2,
      @hep_job Job tiebreaks_by_id j1 j2
      = (primary_hep_job j1 j2
         && (~~ primary_hep_job j2 j1
             || (task_id (job_task j1) < task_id (job_task j2))
             || ((task_id (job_task j1) == task_id (job_task j2))
                 && (job_id j1 ≤ job_id j2 )))).

Every priority granted by the adapter respects the supplied policy.

  Fact tiebreaks_by_id_respects_primary_priority :
    ∀ j1 j2,
      @hep_job Job tiebreaks_by_id j1 j2 → primary_hep_job j1 j2.

Strict priorities established by the supplied policy carry over.

  Fact tiebreaks_by_id_preserves_strict_priority :
    ∀ j1 j2,
      primary_hep_job j1 j2 →
      ~~ primary_hep_job j2 j1 →
      @hep_job Job tiebreaks_by_id j1 j2.

Valid job identifiers turn the adapter's priority order into an unambiguous choice among arriving jobs.

  Fact tiebreaks_by_id_is_antisymmetric :
    ∀ arr_seq,
      valid_job_ids arr_seq →
      antisymmetric_job_priorities tiebreaks_by_id arr_seq.

Assume the supplied policy gives every job at least its own priority.

Hypothesis H_reflexive_priorities : reflexive_job_priorities JLFP.

The adapter preserves reflexivity.

Fact tiebreaks_by_id_is_reflexive : reflexive_job_priorities tiebreaks_by_id.

Assume primary comparisons remain consistent across chains of jobs.

Hypothesis H_transitive_priorities : transitive_job_priorities JLFP.

The adapter preserves transitivity.

Fact tiebreaks_by_id_is_transitive : transitive_job_priorities tiebreaks_by_id.

Assume the supplied policy can compare every pair of jobs.

Hypothesis H_total_priorities : total_job_priorities JLFP.

The adapter preserves totality.

Fact tiebreaks_by_id_is_total : total_job_priorities tiebreaks_by_id.

End TiebreaksById.

We register the priority properties for automatic use in proofs.

Global Hint Resolve
  tiebreaks_by_id_is_reflexive
  tiebreaks_by_id_is_transitive
  tiebreaks_by_id_is_total
  tiebreaks_by_id_is_antisymmetric
  : basic_rt_facts.