Library prosa.implementation.priority.tiebreaking_elf

Require Export prosa.implementation.priority.elf.
Require Export prosa.implementation.priority.tiebreaks_by_id.
Require Export prosa.analysis.facts.priority.elf.

ELF Priority Policy with Tie-Breaking

This implementation refines ELF over any task-level FP policy by favoring lower task IDs, and then lower job IDs, among equal priorities.
Section TiebreakingELF.

Consider tasks with relative priority points and numeric identifiers ...
  Context {Task : TaskType} `{PriorityPoint Task} `{TaskId Task}.

... and their jobs, with arrival times and numeric identifiers.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobId Job}.

The supplied task-level policy determines the primary priority order.
  Variable FP : FP_policy Task.

We resolve ties in ELF's task and priority-point orders by identifier.
  #[local] Instance tiebreaking_elf : JLFP_policy Job :=
    tiebreaks_by_id (ELF FP).

We expose the comparison rule for use in proofs about this policy.
  Fact tiebreaking_elf_hep_job :
    ∀ j1 j2,
      @hep_job Job tiebreaking_elf j1 j2
      = (hp_task (job_task j1) (job_task j2)
         || (ep_task (job_task j1) (job_task j2)
             && ((job_priority_point j1 < job_priority_point j2)%R
                 || ((job_priority_point j1 == job_priority_point j2)
                     && ((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))))))).

Valid job identifiers make the final tie-breaking step unambiguous for arriving jobs.
  Fact tiebreaking_elf_is_antisymmetric :
    ∀ arr_seq,
      valid_job_ids arr_seq →
      antisymmetric_job_priorities tiebreaking_elf arr_seq.

Assume each task has at least its own priority.
  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.

The refinement preserves reflexivity at the job level.
  Fact tiebreaking_elf_is_reflexive : reflexive_job_priorities tiebreaking_elf.

Assume task comparisons remain consistent across chains of tasks.
  Hypothesis H_transitive_priorities : transitive_task_priorities FP.

The refinement preserves transitivity at the job level.
  Fact tiebreaking_elf_is_transitive : transitive_job_priorities tiebreaking_elf.

Assume every pair of tasks can be compared.
  Hypothesis H_total_priorities : total_task_priorities FP.

The refinement lets the scheduler compare every pair of jobs.
  Fact tiebreaking_elf_is_total : total_job_priorities tiebreaking_elf.

Preserving task priorities and priority-point order makes the refinement an ELF policy with respect to the supplied task order.
  Fact tiebreaking_elf_is_elf_policy : policy_is_ELF FP tiebreaking_elf.

End TiebreakingELF.

The identifier tie-breaks repeat together with ELF's task and priority-point orders.
Section HyperperiodPriorities.

Consider periodic tasks with relative priority points and numeric identifiers ...
  Context {Task : TaskType} `{PeriodicModel Task} `{PriorityPoint Task} `{TaskId Task}.

... and jobs with task-derived absolute priority points and numeric identifiers.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job} `{JobId Job}.

The primary task-priority order is arbitrary.
  Variable FP : FP_policy Task.

Consider a task set with valid periods and unique task identifiers ...
  Variable ts : TaskSet Task.
  Hypothesis H_valid_periods : valid_periods ts.
  Hypothesis H_valid_task_ids : valid_task_ids ts.

... generating a valid arrival sequence of these tasks ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

... with periodic releases continuing indefinitely.
  Hypothesis H_periodic_arrivals : taskset_respects_periodic_task_model arr_seq ts.
  Hypothesis H_infinite_jobs : tasks_have_infinite_arrivals arr_seq ts.

Unique task IDs preserve ties between tasks. Within a task, equal priority points identify the same release, whose job-ID comparison is reflexive.
  Fact tiebreaking_elf_priorities_consistent_across_hyperperiods :
    priorities_consistent_across_hyperperiods ts arr_seq (tiebreaking_elf FP).

End HyperperiodPriorities.

We register the policy facts so Rocq can apply them automatically.
Global Hint Resolve
  tiebreaking_elf_is_elf_policy
  tiebreaking_elf_is_reflexive
  tiebreaking_elf_is_transitive
  tiebreaking_elf_is_total
  tiebreaking_elf_is_antisymmetric
  tiebreaking_elf_priorities_consistent_across_hyperperiods
  : basic_rt_facts.