Library prosa.analysis.facts.priority.jlfp_with_fp

In this file, we prove lemmas that are useful when both an FP policy and a JLFP policy are present in context.
In this section, we prove a lemma about workload partitioning which is useful for reasoning about the interference bound function for the ELF scheduling policy.
Section WorkloadTaskSum.

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} `{JobCost Job} .

Let us consider an FP policy and a compatible JLFP policy present in context.
  Context {FP : FP_policy Task}.
  Context {JLFP : JLFP_policy Job}.
  Hypothesis JLFP_FP_is_compatible : JLFP_FP_compatible JLFP FP.

Consider any valid arrival sequence arr_seq.
We consider an arbitrary task set ts...
  Variable ts : seq Task.
  Hypothesis H_task_set : uniq ts.

... and assume that all jobs stem from tasks in this task set.
Let tsk be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

We define a predicate to identify others tasks which have equal priority as tsk.
  Definition other_ep_task := fun tsk_o(ep_task tsk tsk_o) && (tsk_o != tsk).

We consider a job j belonging to this task ...
  Variable j : Job.
  Hypothesis H_job_of_task : job_of_task tsk j.

... and focus on the jobs arriving in an arbitrary interval [t1, t2).
  Variable t1 t2 : duration.
  Let jobs_arrived := arrivals_between arr_seq t1 t2.

We first consider jobs that belong to other tasks that have equal priority as tsk and have higher-or-equal priority JLFP than j.
  Definition hep_job_of_ep_other_task :=
    fun j' : Job
      hep_job j' j
      && ep_task (job_task j') (job_task j)
      && (job_task j' != job_task j).

We then establish that the cumulative workload of these jobs can be partitioned task-wise.
Now we focus on jobs belonging to tasks which have higher priority than tsk.
  Definition from_hp_task (j' : Job) :=
    hp_task (job_task j') (job_task j).

We also identify higher-or-equal-priority jobs JLFP that belong to (1) tasks having higher priority than tsk ...
  Definition hep_from_hp_task (j' : Job) :=
    hep_job j' j && hp_task (job_task j') (job_task j).

... (2) tasks having equal priority as tsk.
  Definition hep_from_ep_task (j' : Job) :=
    hep_job j' j && ep_task (job_task j') (job_task j).

First, we establish that the cumulative workload of higher-or-equal-priority jobs belonging to tasks having higher priority than tsk is equal to the cumulative workload of jobs belonging to higher-priority tasks.
We then establish that the cumulative workload of higher-or-equal priority jobs is equal to the sum of cumulative workload of higher-or-equal priority jobs belonging to higher-priority tasks and the cumulative workload of higher-or-equal-priority jobs belonging to equal-priority tasks.