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
Require Import prosa.classic.implementation.job prosa.classic.implementation.task
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)].

    (* 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 \in ts
        no_deadline_missed_by tsk.

  End ExampleRTA.

End ResponseTimeAnalysisFP.