Library prosa.classic.implementation.uni.susp.dynamic.oblivious.fp_rta_example

Require Import prosa.classic.util.all.
Require Import prosa.classic.model.arrival.basic.job prosa.classic.model.arrival.basic.task prosa.classic.model.priority.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.schedule.uni.susp.suspension_intervals.
Require Import prosa.classic.analysis.uni.basic.workload_bound_fp.
Require Import prosa.classic.analysis.uni.susp.dynamic.oblivious.fp_rta.
Require Import prosa.classic.implementation.uni.susp.dynamic.job
Require Import prosa.classic.implementation.uni.susp.schedule.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

Module ResponseTimeAnalysisFP.

  Import Job UniprocessorSchedule SporadicTaskset Priority Schedulability
         SuspensionIntervals SuspensionObliviousFP WorkloadBoundFP.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence ConcreteScheduler.

  (* In this section, we run the suspension-oblivious FP RTA on a simple task set
     to show that the theorems contain no contradictory assumptions. *)

  Section ExampleRTA.

    Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 5;
                                 task_deadline := 5; task_suspension_bound := 1 |}.
    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 5;
                                 task_deadline := 5; task_suspension_bound := 0|}.
    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 6;
                                 task_deadline := 6; task_suspension_bound := 1|}.

    (* Let ts be a task set containing these three tasks, ... *)
    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    (* ...which can be shown to have valid parameters. *)
    Fact ts_has_valid_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Now let's inflate the task costs with the suspension-bounds. *)
    Let inflated_cost := inflated_task_cost task_cost task_suspension_bound.

    (* After the inflation, note that the task costs are no larger than deadlines and periods. *)
    Fact inflated_cost_le_deadline_and_period:
        tsk \in ts
          inflated_cost tsk task_deadline tsk
          inflated_cost tsk task_period tsk.

    (* Next, recall the FP RTA schedulability test using RM as the FP policy
       and the inflated task costs. *)

    Let RTA_claimed_bounds :=
      fp_claimed_bounds inflated_cost task_period task_deadline (RM task_period).
    Let schedulability_test :=
      fp_schedulable inflated_cost task_period task_deadline (RM task_period).

    (* First, we show that the schedulability test returns the following bounds, ... *)
    Fact RTA_yields_these_bounds :
      RTA_claimed_bounds ts = Some [:: (tsk1, 3); (tsk2, 3); (tsk3, 5)].

    (* the schedulability test indeed returns true. *)
    Fact schedulability_test_succeeds :
      schedulability_test ts = true.

    (* Now, let's show that the task set is schedulable. *)

    (* Let arr_seq be the periodic arrival sequence from ts... *)
    Let arr_seq := periodic_arrival_sequence ts.

    (* ...where jobs have total suspension times that are no larger than
       the suspension bound of their tasks. *)

     Variable next_suspension: job_suspension concrete_job_eqType.
     Hypothesis H_dynamic_suspensions:
       dynamic_suspension_model job_cost job_task next_suspension task_suspension_bound.

    (* Also assume rate-monotonic priorities. *)
    Let higher_eq_priority := FP_to_JLDP job_task (RM task_period).

    (* Next, let sched be the suspension-aware RM schedule with those job suspension times. *)
    Let sched := scheduler job_arrival job_cost arr_seq next_suspension higher_eq_priority.

    (* To conclude, based on the definition of deadline miss,... *)
    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

    (* ...we use the result of the suspension-oblivious FP RTA to conclude that
       no task misses its deadline. *)

    Corollary ts_is_schedulable:
        tsk \in ts
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisFP.