Library prosa.classic.analysis.uni.jitter.fp_rta_theory

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.priority.
Require Import prosa.classic.model.arrival.basic.task.
Require Import prosa.classic.model.arrival.jitter.job prosa.classic.model.arrival.jitter.task_arrival
               prosa.classic.model.arrival.jitter.arrival_sequence prosa.classic.model.arrival.jitter.arrival_bounds.
Require Import prosa.classic.model.schedule.uni.schedule_of_task prosa.classic.model.schedule.uni.service
               prosa.classic.model.schedule.uni.schedulability prosa.classic.model.schedule.uni.response_time.
Require Import prosa.classic.model.schedule.uni.jitter.schedule
               prosa.classic.model.schedule.uni.jitter.busy_interval
               prosa.classic.model.schedule.uni.jitter.platform.
Require Import prosa.classic.analysis.uni.jitter.workload_bound_fp.
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

Module ResponseTimeAnalysisFP.

  Import ArrivalSequenceWithJitter JobWithJitter TaskArrivalWithJitter ArrivalBounds
         UniprocessorScheduleWithJitter ScheduleOfTask SporadicTaskset Priority
         ResponseTime WorkloadBoundFP Platform Schedulability BusyInterval.

  Section ResponseTimeBound.

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

    Context {Job: eqType}.
    Variable job_arrival: Job → time.
    Variable job_cost: Job → time.
    Variable job_jitter: Job → time.
    Variable job_task: Job → SporadicTask.

    Variable ts: seq SporadicTask.

    Hypothesis H_positive_periods: ∀ tsk, tsk \in ts → task_period tsk > 0.

    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.

    Hypothesis H_sporadic_tasks:
      sporadic_task_model task_period job_arrival job_task arr_seq.

    Hypothesis H_job_cost_le_task_cost:
      ∀ j,
        arrives_in arr_seq j →
        job_cost j ≤ task_cost (job_task j).

    Hypothesis H_job_jitter_le_task_jitter:
      ∀ j,
        arrives_in arr_seq j →
        job_jitter j ≤ task_jitter (job_task j).

    Hypothesis H_all_jobs_from_taskset:
      ∀ j, arrives_in arr_seq j → job_task j \in ts.

    Variable sched: schedule Job.
    Hypothesis H_jobs_come_from_arrival_sequence:
      jobs_come_from_arrival_sequence sched arr_seq.

    Hypothesis H_jobs_execute_after_jitter: jobs_execute_after_jitter job_arrival job_jitter sched.
    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.

    Variable higher_eq_priority: FP_policy SporadicTask.
    Hypothesis H_priority_is_reflexive: FP_is_reflexive higher_eq_priority.
    Hypothesis H_priority_is_transitive: FP_is_transitive higher_eq_priority.

    Hypothesis H_work_conserving: work_conserving job_arrival job_cost job_jitter arr_seq sched.
    Hypothesis H_respects_fp_policy:
      respects_FP_policy job_arrival job_cost job_jitter job_task arr_seq sched higher_eq_priority.

    Variable tsk: SporadicTask.
    Hypothesis H_tsk_in_ts: tsk \in ts.

    Let response_time_bounded_by :=
      is_response_time_bound_of_task job_arrival job_cost job_task arr_seq sched.
    Let W := total_workload_bound_fp task_cost task_period task_jitter higher_eq_priority ts tsk.

    Variable R: time.
    Hypothesis H_R_positive: R > 0.
    Hypothesis H_response_time_is_fixed_point: R = W R.

    Theorem uniprocessor_response_time_bound_fp:
      response_time_bounded_by tsk (task_jitter tsk + R).

  End ResponseTimeBound.

End ResponseTimeAnalysisFP.