Library prosa.implementation.priority.elf

Require Import prosa.util.int.
Require Export prosa.model.priority.elf.
Require Export prosa.analysis.facts.hyperperiod.
Require Import prosa.implementation.priority.gel.
Require Import prosa.analysis.facts.priority.classes.

ELF Priority Policy

We introduce the canonical ELF priority policy, under which jobs are ordered by the underlying FP policy and ties are broken by absolute priority points. The ELF policy belongs to the class of JLFP policies. In order to define the policy, we introduce the required context.
Section ELF.

Consider any type of tasks with relative priority points ...
  Context {Task : TaskType} `{PriorityPoint Task}.

... and jobs of these tasks.
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.

We parameterize the ELF priority policy based on a fixed-priority policy. Job j1 is assigned a higher priority than job j2 if either the task associated with j1 has a strictly higher priority than the task associated with j2, or if their tasks have equal priorities and j1 has an earlier absolute priority point.
  #[local] Instance ELF (fp : FP_policy Task) : JLFP_policy Job :=
  {
    hep_job (j1 j2 : Job) :=
      let gel_hep_job := @hep_job _ (GEL Job) in
      hp_task (job_task j1) (job_task j2)
      || (hep_task (job_task j1) (job_task j2)
          && gel_hep_job j1 j2)
  }.

End ELF.

In this section, we prove that the concrete ELF policy satisfies the corresponding model-level predicate.
Section PropertiesOfELF.

Consider any type of tasks with relative priority points ...
  Context {Task : TaskType} `{PriorityPoint Task}.

... and jobs of these tasks.
  Context {Job : JobType} `{JobArrival Job} `{JobTask Job Task}.

Consider any fixed-priority policy.
  Variable FP : FP_policy Task.

Under the concrete ELF implementation, hep_job reduces exactly to fixed-priority order, and priority-point order for jobs of equal-priority tasks.
  Fact ELF_hep_job :
    ∀ j1 j2,
      @hep_job _ (ELF FP) j1 j2
      = (hp_task (job_task j1) (job_task j2)
         || (hep_task (job_task j1) (job_task j2)
             && (job_priority_point j1 ≤ job_priority_point j2)%R)).

By construction, ELF reduces to GEL when the two tasks have equal priority under the underlying FP policy.
  Fact hep_job_elf_gel :
    ∀ j j',
      ep_task (job_task j) (job_task j') →
      (@hep_job _ (ELF FP) j j') = (@hep_job _ (GEL Job) j j').

Assume the underlying task priorities are reflexive, transitive, and total.
  Hypothesis H_reflexive_priorities : reflexive_task_priorities FP.
  Hypothesis H_transitive_priorities : transitive_task_priorities FP.
  Hypothesis H_total_priorities : total_task_priorities FP.

ELF is reflexive.
  Fact ELF_is_reflexive : reflexive_job_priorities (ELF FP).

ELF is transitive.
  Fact ELF_is_transitive : transitive_job_priorities (ELF FP).

ELF is total.
  Fact ELF_is_total : total_job_priorities (ELF FP).
The concrete ELF implementation is indeed an ELF policy.
  Fact ELF_is_ELF_policy :
    policy_is_ELF FP (ELF FP).

End PropertiesOfELF.

ELF's task and priority-point orders repeat with a periodic workload.
Section ELFHyperperiodPriorities.

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

... and jobs whose absolute priority points are derived from their tasks.
  Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.

The primary task-priority order can be any FP instance.
  Variable FP : FP_policy Task.

Consider a task set with valid periods ...
  Variable ts : TaskSet Task.
  Hypothesis H_valid_periods : valid_periods 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.

Shifting two jobs by one hyperperiod preserves both priority orders.
  Fact ELF_priorities_consistent_across_hyperperiods :
    priorities_consistent_across_hyperperiods ts arr_seq (ELF FP).

End ELFHyperperiodPriorities.

We add the concrete-policy witness to the basic_rt_facts hint database so Rocq can apply it automatically where needed.
Global Hint Resolve
  ELF_is_ELF_policy
  ELF_is_reflexive
  ELF_is_transitive
  ELF_is_total
  ELF_priorities_consistent_across_hyperperiods
  : basic_rt_facts.