Library prosa.analysis.facts.priority.fifo_ahep_bound

Require Export prosa.analysis.facts.interference.
Require Export prosa.analysis.facts.model.restricted_supply.schedule.
Require Import prosa.analysis.facts.priority.fifo.
Require Import prosa.analysis.facts.model.rbf.

Higher-or-Equal-Priority Interference Bound under FIFO

In this file, we introduce a bound on the cumulative interference from higher- and equal-priority under FIFO scheduling.
Section RTAforFullyPreemptiveFIFOModelwithArrivalCurves.

Consider any type of tasks, each characterized by a WCET task_cost and an arrival curve max_arrivals ...
  Context {Task : TaskType}.
  Context `{TaskCost Task}.
  Context `{MaxArrivals Task}.

... and any type of jobs associated with these tasks, where each job has a task job_task, a cost job_cost, and an arrival time job_arrival.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobCost Job}.
  Context `{JobArrival Job}.

Consider any kind of unit-supply uniprocessor model.
  Context `{PState : ProcessorState Job}.
  Hypothesis H_uniprocessor_proc_model : uniprocessor_model PState.
  Hypothesis H_unit_supply_proc_model : unit_supply_proc_model PState.

Consider any arrival sequence arr_seq with consistent, non-duplicate arrivals.
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_valid_arrival_sequence : valid_arrival_sequence arr_seq.

We further require that a job's cost cannot exceed its task's stated WCET.
  Hypothesis H_valid_job_cost : arrivals_have_valid_job_costs arr_seq.

We consider an arbitrary task set ts ...
  Variable ts : seq Task.

... and assume that all jobs stem from tasks in this task set.
  Hypothesis H_all_jobs_from_taskset : all_jobs_from_taskset arr_seq ts.

We assume that max_arrivals is a family of valid arrival curves that constrains the arrival sequence arr_seq, i.e., for any task tsk in ts, max_arrival tsk is (1) an arrival bound of tsk, and ...
  Hypothesis H_is_arrival_curve : taskset_respects_max_arrivals arr_seq ts.

... (2) a monotonic function that equals 0 for the empty interval delta = 0.
  Hypothesis H_valid_arrival_curve : valid_taskset_arrival_curve ts max_arrivals.

Let tsk be any task in ts that is to be analyzed.
  Variable tsk : Task.
  Hypothesis H_tsk_in_ts : tsk \in ts.

Consider any schedule ...
  Variable sched : schedule PState.

... where jobs do not execute before their arrival nor after completion.
  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.

Next, we establish a bound on the interference produced by higher- and equal-priority jobs.
Consider a job j of the task under analysis tsk with a positive cost.
  Variable j : Job.
  Hypothesis H_job_of_task : job_of_task tsk j.
  Hypothesis H_j_in_arrivals : arrives_in arr_seq j.
  Hypothesis H_job_cost_positive : job_cost_positive j.

Consider the busy window of j and denote it as [t1, t2).
  Variable t1 t2 : instant.
  Hypothesis H_busy_window : classical.busy_interval arr_seq sched j t1 t2.

Consider any arbitrary sub-interval [t1, Δ) within the busy window of j.
  Variable Δ : instant.
  Hypothesis H_in_busy : t1 + Δ < t2.

The cumulative interference from higher- and equal-priority jobs during [t1, Δ) is bounded as follows.
  Lemma bound_on_hep_workload :
    cumulative_another_hep_job_interference arr_seq sched j t1 (t1 + Δ) ≤
      \sum_(tsko <- ts) task_request_bound_function tsko (job_arrival j - t1 + ε) - task_cost tsk.

End RTAforFullyPreemptiveFIFOModelwithArrivalCurves.