interference_bound.v 1.27 KB
Newer Older
Felipe Cerqueira's avatar
Felipe Cerqueira committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44
Add LoadPath "../../" as rt.
Require Import rt.util.Vbase rt.util.lemmas.
Require Import rt.model.basic.schedule.
Require Import rt.analysis.parallel.workload_bound.
Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module InterferenceBoundGeneric.

  Section Definitions.

    Import Schedule WorkloadBound.
    
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task -> nat.
    Variable task_period: sporadic_task -> nat.
    Variable task_deadline: sporadic_task -> nat.
    
    (* Let tsk be the task to be analyzed. *)
    Variable tsk: sporadic_task.

    Let task_with_response_time := (sporadic_task * time)%type.
    
    (* Assume a known response-time bound for each interfering task ... *)
    Variable R_prev: seq task_with_response_time.

    (* ... and an interval length delta. *)
    Variable delta: time.

    Section PerTask.

      Variable tsk_R: task_with_response_time.
      Let tsk_other := fst tsk_R.
      Let R_other := snd tsk_R.
    
      (* Based on the workload bound, Bertogna and Cirinei define the
         following interference bound for a task. *)
      Definition interference_bound_generic :=
        W task_cost task_period tsk_other R_other delta.

    End PerTask.

  End Definitions.

End InterferenceBoundGeneric.