Library prosa.classic.implementation.uni.basic.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.analysis.uni.basic.workload_bound_fp
               prosa.classic.analysis.uni.basic.fp_rta_comp.
Require Import prosa.classic.implementation.job prosa.classic.implementation.task
               prosa.classic.implementation.arrival_sequence.
Require Import prosa.classic.implementation.uni.basic.schedule.
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

Module ResponseTimeAnalysisFP.

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

  (* In this section, we run the 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 := 4; task_deadline := 5|}.
    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 6; task_deadline := 5|}.
    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 6; task_deadline := 6|}.

    (* Let ts be a task set containing these three tasks.
       (Note that periods are not unique and one of the tasks has an arbitrary deadline.) *)
    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    (* Also note that the task set has valid parameters. *)
    Fact ts_has_valid_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Next, recall the FP RTA schedulability test using RM as the FP policy. *)
    Let RTA_claimed_bounds :=
      fp_claimed_bounds task_cost task_period task_deadline (RM task_period).
    Let schedulability_test :=
      fp_schedulable task_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, 1); (tsk2, 3); (tsk3, 3)].

    (* ...so 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.

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

    (* ... and recall that this priority assignment is total. *)
    Fact priority_is_total:
      ∀ t, total (higher_eq_priority t).

    (* Let sched be the work-conserving RM scheduler. *)
    Let sched := scheduler job_arrival job_cost arr_seq higher_eq_priority.

    (* Recall 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.

    (* Next, by using the result of the RTA, we prove that the task set is schedulable. *)
    Corollary ts_is_schedulable:
      ∀ tsk,
        tsk \in ts →
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisFP.