Library prosa.analysis.facts.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.
  Proof.
    by movej /andP [_ /negP NEQ]; apply: NEQ.
  Qed.


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'.
  Proof.
    movej j' DIFF; rewrite /another_hep_job.
    case: (hep_job j j'); [rewrite andTb|rewrite andFb //].
    apply: (contra _ DIFF) ⇒ /eqP → {DIFF}.
    by apply/eqP.
  Qed.


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.
  Proof.
    movetsko j j' /eqP /eqP /andP [_ AA].
    by move: AA; rewrite ⇒ /negP A; apply: A.
  Qed.


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
      = another_hep_job && (job_task != job_task ).
  Proof.
    move .
    by rewrite -andbA [X in _ && X]andb_idl//; apply: contraNN ⇒ /eqP→.
  Qed.


another_hep_job can either come from another or the same task...
  Lemma another_hep_job_split_task :
     j1 j2,
      another_hep_job
      = another_task_hep_job || another_hep_job_of_same_task .
  Proof.
    move .
    by rewrite another_task_hep_job_another_hep_job -andb_orr orNb andbT.
  Qed.


...but not both.
  Lemma another_hep_job_exclusive :
     j1 j2,
      ~~ (another_task_hep_job && another_hep_job_of_same_task ).
  Proof.
    by move ; rewrite !negb_and negbK; case: eqP; rewrite /= !orbT.
  Qed.


End BasicLemmas.

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.
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.
  Section BasicProperties.

hp_task is irreflexive.
    Lemma hp_task_irrefl : irreflexive hp_task.
    Proof. by movetsk; rewrite /hp_task; case: hep_task. Qed.

If a task has higher priority than task , then task has higher-or-equal priority than task .
    Lemma hp_hep_task :
       tsk1 tsk2,
        hp_task
        hep_task .
    Proof. by move⇒ ? ? /andP[]. Qed.

If a task has equal priority as task , then task has higher-or-equal priority than task .
    Lemma ep_hep_task :
       tsk1 tsk2,
        ep_task
        hep_task .
    Proof. by move⇒ ? ? /andP[]. Qed.

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
        ~~ hp_task .
    Proof.
      move⇒ ? ? /andP[_ ?].
      by rewrite negb_and; apply/orP; right; apply/negPn.
    Qed.


Task having equal priority as task is equivalent to task having equal priority as task .
    Lemma ep_task_sym :
       tsk1 tsk2,
        ep_task = ep_task .
    Proof. by movex y; rewrite /ep_task andbC. Qed.

If a task has higher-or-equal priority than a task , then either has strictly higher priority than or the two have equal priority.
    Lemma hep_hp_ep_task :
       tsk1 tsk2,
        hep_task = hp_task || ep_task .
    Proof. by move⇒ ? ?; rewrite /hp_task /ep_task -andb_orr orNb andbT. Qed.

  End BasicProperties.

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.
    Proof. by move⇒ ?; apply /andP; split. Qed.

  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.
    Proof.
      movey x z /andP[hepxy Nhepyx] /andP[hepyz Nhepyz]; apply/andP; split.
      { exact: H_transitive hepyz. }
      { by apply: contraNN Nhepyx; exact: H_transitive. }
    Qed.


If task has higher priority than task , and task has higher-or-equal priority than task , then task has higher priority than task .
    Lemma hp_hep_trans :
       tsk1 tsk2 tsk3,
        hp_task
        hep_task
        hp_task .
    Proof.
      movex y z /andP[hepxy Nhepyx] hepyz; apply/andP; split.
      { exact: H_transitive hepyz. }
      { by apply: contraNN Nhepyx; exact: H_transitive. }
    Qed.


If task has higher-or-equal priority than task , and task has strictly higher priority than task , then task has higher priority than task .
    Lemma hep_hp_trans :
       tsk1 tsk2 tsk3,
        hep_task
        hp_task
        hp_task .
    Proof.
      movex y z hepxy /andP[hepyz Nhepzy]; apply/andP; split.
      { exact: H_transitive hepyz. }
      { apply: contraNN Nhepzyhepzy; exact: H_transitive hepxy. }
    Qed.


  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 does not have higher-or-equal priority than task , then task has higher priority than task .
    Lemma not_hep_hp_task :
       tsk1 tsk2, ~~ hep_task = hp_task .
    Proof.
      movex y; apply /idP/idP ⇒ [| /andP[//]].
      moveNhepxy; apply /andP; split⇒ [|//].
      have /orP[h | //] := H_total x y.
      by exfalso; move/negP: Nhepxy.
    Qed.


The converse also holds.
    Lemma not_hp_hep_task :
       tsk1 tsk2, ~~ hp_task = hep_task .
    Proof. by movex y; rewrite -not_hep_hp_task negbK. Qed.

If a task does not have higher priority than a task , then either has lesser priority than or the two have equal priority.
    Lemma nhp_ep_nhep_task :
       tsk1 tsk2,
        ~~hp_task = ~~hep_task || ep_task .
    Proof.
      move ; rewrite not_hp_hep_task not_hep_hp_task.
      by rewrite hep_hp_ep_task ep_task_sym.
    Qed.


  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}.

Consider any FP policy.
  Context {FP : FP_policy Task}.

  Remark respects_sequential_tasks :
    reflexive_task_priorities FP
    policy_respects_sequential_tasks (FP_to_JLFP FP).
  Proof.
    moveREFL /eqP EQ LT.
    by rewrite /hep_job /FP_to_JLFP EQ.
  Qed.


End FPRemarks.

Section JLFPFP.
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 any pair of JLFP and FP policies that are compatible.
  Context (JLFP : JLFP_policy Job) (FP : FP_policy Task).
  Hypothesis H_compatible : JLFP_FP_compatible JLFP FP.

We restate JLFP_FP_compatible to make it easier to discover with Search. Here is the first part...
  Lemma hep_job_implies_hep_task :
     j1 j2,
      hep_job
      hep_task (job_task ) (job_task ).
  Proof. exact: H_compatible.1. Qed.

...and second part.
  Lemma hp_task_implies_hep_job :
     j1 j2,
      hp_task (job_task ) (job_task )
      hep_job .
  Proof. exact: H_compatible.2. Qed.

End JLFPFP.

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