Library prosa.classic.analysis.apa.interference_bound_fp

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.global.workload.
Require Import prosa.classic.model.schedule.global.basic.schedule.
Require Import prosa.classic.model.schedule.apa.interference prosa.classic.model.schedule.apa.affinity.
Require Import prosa.classic.analysis.apa.workload_bound prosa.classic.analysis.apa.interference_bound.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module InterferenceBoundFP.

  Import Schedule WorkloadBound Priority Interference Affinity.
  Export InterferenceBoundGeneric.

    Section Definitions.

    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task → time.
    Variable task_period: sporadic_task → time.
    Variable task_deadline: sporadic_task → time.

    Context {num_cpus: nat}.
    Variable alpha: task_affinity sporadic_task num_cpus.

    Variable tsk: sporadic_task.

    Variable alpha': affinity num_cpus.

    Let task_with_response_time := (sporadic_task × time)%type.

    Variable R_prev: seq task_with_response_time.

    Variable delta: time.

    Variable higher_eq_priority: FP_policy sporadic_task.

    Let total_interference_bound := interference_bound_generic task_cost task_period tsk delta.

    Let hp_task_in alpha' := higher_priority_task_in alpha higher_eq_priority tsk alpha'.

    Definition total_interference_bound_fp :=
      \sum_((tsk_other, R_other) <- R_prev | hp_task_in alpha' tsk_other)
         total_interference_bound (tsk_other, R_other).

  End Definitions.

End InterferenceBoundFP.