Library prosa.implementation.priority.tiebreaking_fp

Require Export prosa.model.priority.fp.
Require Export prosa.implementation.priority.tiebreaks_by_id.
Require Export prosa.analysis.facts.hyperperiod.

Fixed-Priority Policy with Tie-Breaking

This implementation refines any task-level fixed-priority policy by favoring lower task IDs, and then lower job IDs, among equal priorities.

Section TiebreakingFP.

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 task-level policy determines the primary priority order.

Variable FP : FP_policy Task.

We lift task priorities to jobs and resolve ties through the ID adapter.

#[local] Instance tiebreaking_fp : JLFP_policy Job :=
tiebreaks_by_id (fp_to_jlfp FP).

We expose the comparison rule for use in proofs about this policy.

  Fact tiebreaking_fp_hep_job :
    ∀ j1 j2,
      @hep_job Job tiebreaking_fp j1 j2
      = (hep_task (job_task j1) (job_task j2)
         && (~~ hep_task (job_task j2) (job_task 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 )))).

Valid job identifiers make the final tie-breaking step unambiguous for arriving jobs.

  Fact tiebreaking_fp_is_antisymmetric :
    ∀ arr_seq,
      valid_job_ids arr_seq →
      antisymmetric_job_priorities tiebreaking_fp 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_fp_is_reflexive : reflexive_job_priorities tiebreaking_fp.

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_fp_is_transitive : transitive_job_priorities tiebreaking_fp.

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_fp_is_total : total_job_priorities tiebreaking_fp.

Preserving task priorities and their strict comparisons makes the refined job order an FP policy with respect to the supplied task order.

Fact tiebreaking_fp_is_fp_policy : policy_is_FP FP tiebreaking_fp.

End TiebreakingFP.

Monotonic job IDs make tie-breaking repeat with the periodic workload.

Section HyperperiodPriorities.

Consider periodic tasks with numeric identifiers ...

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

... and their jobs, with arrival times 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 jobs 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.

Suppose that, w.r.t. each task, later arrivals have larger job IDs.

Hypothesis H_monotonic_job_ids : monotonic_job_ids arr_seq.

For jobs sharing a task ID, monotonic identifiers recover arrival order since periodic tasks release a single job at each release instant.

  Local Lemma job_id_order_matches_arrival_order :
    ∀ j1 j2,
      arrives_in arr_seq j1 →
      arrives_in arr_seq j2 →
      task_id (job_task j1) = task_id (job_task j2) →
      (job_id j1 ≤ job_id j2 ) = (job_arrival j1 ≤ job_arrival j2 ).

A hyperperiod shift preserves task priorities, task IDs, and the arrival order used by the final job-ID tie-break.

Fact tiebreaking_fp_priorities_consistent_across_hyperperiods :
priorities_consistent_across_hyperperiods ts arr_seq (tiebreaking_fp FP).

End HyperperiodPriorities.

We register the policy facts so Rocq can apply them automatically.

Global Hint Resolve
  tiebreaking_fp_is_fp_policy
  tiebreaking_fp_is_reflexive
  tiebreaking_fp_is_transitive
  tiebreaking_fp_is_total
  tiebreaking_fp_is_antisymmetric
  tiebreaking_fp_priorities_consistent_across_hyperperiods
  : basic_rt_facts.