Library prosa.analysis.facts.priority.classes

Require Export prosa.model.priority.classes.

In this section, we prove some basic properties about priority relations.
Section BasicLemmas.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any type of jobs associated with these tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

Consider a JLFP policy that indicates a higher-or-equal priority relation.
  Context `{JLFP_policy Job}.

First, we prove that another_hep_job relation is anti-reflexive.
  Lemma another_hep_job_antireflexive :
    ∀ j, ¬ another_hep_job j j.

Second, we relate another_hep_job to same_task.
  Lemma another_hep_job_diff_task :
    ∀ j j',
      ~~ same_task j j' →
      another_hep_job j j' = hep_job j j'.

We show that another_task_hep_job is "task-wise" anti-reflexive; that is, given two jobs j and j' from the same task, another_task_hep_job j' j is false.
  Lemma another_task_hep_job_taskwise_antireflexive :
    ∀ tsk j j',
      job_of_task tsk j →
      job_of_task tsk j' →
      ¬ another_task_hep_job j' j.

Alternative definition of another_task_hep_job using another_hep_job instead of hep_job.
  Lemma another_task_hep_job_another_hep_job :
    ∀ j1 j2,
      another_task_hep_job j1 j2
      = another_hep_job j1 j2 && (job_task j1 != job_task j2).

another_hep_job can either come from another or the same task...
  Lemma another_hep_job_split_task :
    ∀ j1 j2,
      another_hep_job j1 j2
      = another_task_hep_job j1 j2 || another_hep_job_of_same_task j1 j2.

...but not both.
  Lemma another_hep_job_exclusive :
    ∀ j1 j2,
      ~~ (another_task_hep_job j1 j2 && another_hep_job_of_same_task j1 j2).

End BasicLemmas.

In this section, we prove a basic consequence of total job-level fixed-priority relations.
Section TotalJLFPProperties.

Consider any type of jobs ...
  Context {Job : JobType}.

... and any JLFP policy.
  Context {JLFP : JLFP_policy Job}.

If a job does not have higher-or-equal priority than another job, then totality gives the priority relation in the opposite direction.
  Lemma total_priority_not_hep_job :
    total_job_priorities JLFP →
    ∀ j j',
      ~~ hep_job j j' → hep_job j' j.

End TotalJLFPProperties.

In the following section, we establish properties of hp_task and ep_task auxiliary priority relations defined for FP policies. They are useful in proving properties of the ELF scheduling policy.
Section FPRelationsProperties.

Consider any type of tasks and an FP policy that indicates a higher-or-equal priority relation on the tasks.
  Context {Task : TaskType} {FP_policy : FP_policy Task}.

First, we prove some trivial lemmas about the hep_task and ep_task relations.
hp_task is irreflexive.
  Lemma hp_task_irrefl : irreflexive hp_task.

If a task tsk1 has higher priority than task tsk2, then task tsk1 has higher-or-equal priority than task tsk2.
  Lemma hp_hep_task :
    ∀ tsk1 tsk2,
      hp_task tsk1 tsk2 →
      hep_task tsk1 tsk2.

If a task tsk1 has equal priority as task tsk2, then task tsk1 has higher-or-equal priority than task tsk2.
  Lemma ep_hep_task :
    ∀ tsk1 tsk2,
      ep_task tsk1 tsk2 →
      hep_task tsk1 tsk2.

If a task has higher priority than another task, then the two do not have equal priority.
  Lemma ep_not_hp_task :
    ∀ tsk1 tsk2,
      ep_task tsk1 tsk2 →
      ~~ hp_task tsk1 tsk2.

Task tsk1 having equal priority as task tsk2 is equivalent to task tsk2 having equal priority as task tsk1.
  Lemma ep_task_sym :
    ∀ tsk1 tsk2,
      ep_task tsk1 tsk2 = ep_task tsk2 tsk1.

If a task tsk1 has higher-or-equal priority than a task tsk2, then tsk1 either has strictly higher priority than tsk2 or the two have equal priority.
  Lemma hep_hp_ep_task :
    ∀ tsk1 tsk2,
      hep_task tsk1 tsk2 = hp_task tsk1 tsk2 || ep_task tsk1 tsk2.

In the following section, we establish a useful property about the equal priority relation, which follows when the FP policy is reflexive.
  Section ReflexiveProperties.

Assuming that the FP policy is reflexive ...
    Hypothesis H_reflexive : reflexive hep_task.

... it follows that the equal priority relation is reflexive.
    Lemma eq_reflexive : reflexive ep_task.

  End ReflexiveProperties.

Now we establish useful properties about the higher priority relation, which follow when the FP policy is transitive.
  Section TransitiveProperties.

Assuming that the FP policy is transitive ...
    Hypothesis H_transitive : transitive hep_task.

... it follows that the higher priority relation is also transitive.
    Lemma hp_trans : transitive hp_task.
If task tsk1 has higher priority than task tsk2, and task tsk2 has higher-or-equal priority than task tsk3, then task tsk1 has higher priority than task tsk3.
    Lemma hp_hep_trans :
      ∀ tsk1 tsk2 tsk3,
        hp_task tsk1 tsk2 →
        hep_task tsk2 tsk3 →
        hp_task tsk1 tsk3.
If task tsk1 has higher-or-equal priority than task tsk2, and task tsk2 has strictly higher priority than task tsk3, then task tsk1 has higher priority than task tsk3.
    Lemma hep_hp_trans :
      ∀ tsk1 tsk2 tsk3,
        hep_task tsk1 tsk2 →
        hp_task tsk2 tsk3 →
        hp_task tsk1 tsk3.
  End TransitiveProperties.

Finally, we establish a useful property about the higher priority relation, which follows when the FP policy is total.
  Section TotalProperties.

We assume that the FP policy is total.
    Hypothesis H_total : total hep_task.

If a task tsk1 does not have higher-or-equal priority than task tsk2, then task tsk2 has higher priority than task tsk1.
    Lemma not_hep_hp_task :
      ∀ tsk1 tsk2, ~~ hep_task tsk1 tsk2 = hp_task tsk2 tsk1.

The converse also holds.
    Lemma not_hp_hep_task :
      ∀ tsk1 tsk2, ~~ hp_task tsk1 tsk2 = hep_task tsk2 tsk1.

If a task tsk1 does not have higher priority than a task tsk2, then tsk1 either has lesser priority than tsk2 or the two have equal priority.
    Lemma nhp_ep_nhep_task :
      ∀ tsk1 tsk2,
        ~~hp_task tsk1 tsk2 = ~~hep_task tsk1 tsk2 || ep_task tsk1 tsk2.

  End TotalProperties.

End FPRelationsProperties.

In the following section, we show that FP policies respect the sequential tasks hypothesis. It means that later-arrived jobs of a task don't have higher priority than earlier-arrived jobs of the same task (assuming that task priorities are reflexive).
Section FPRemarks.

Consider any type of tasks ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.

... and any type of jobs associated with these tasks, ...
  Context {Job : JobType}.
  Context `{JobTask Job Task}.

.. and assume that jobs have a cost and an arrival time.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

Under any FP policy, ...
  Context {FP : FP_policy Task}.

... later-arriving jobs do not have higher priority than earlier-arriving ones.
  Remark respects_sequential_tasks :
    reflexive_task_priorities FP →
    policy_respects_sequential_tasks (fp_to_jlfp FP).

End FPRemarks.

We add some lemmas into the "Hint Database" basic_rt_facts, so Coq will be able to apply it automatically.
Global Hint Resolve
  respects_sequential_tasks
  total_priority_not_hep_job
  : basic_rt_facts.