Library prosa.classic.implementation.uni.basic.tdma_rta_example

Require Import prosa.classic.util.all prosa.classic.util.find_seq
Require Import prosa.classic.model.arrival.basic.job
               prosa.classic.model.arrival.basic.task prosa.classic.model.policy_tdma.
Require Import prosa.classic.model.schedule.uni.schedule prosa.classic.model.schedule.uni.schedulability.
Require Import prosa.classic.model.priority
Require Import prosa.classic.implementation.job prosa.classic.implementation.task

From mathcomp Require Import ssreflect ssrbool ssrnat eqtype seq bigop div.

Set Bullet Behavior "Strict Subproofs".
Module ResponseTimeAnalysisExemple.

  Import Job ArrivalSequence UniprocessorSchedule SporadicTaskset Schedulability Priority
         ResponseTimeAnalysisTDMA PolicyTDMA Platform_TDMA.
  Import ConcreteJob ConcreteTask ConcreteArrivalSequence BigOp
         ConcreteSchedulerTDMA WCRT_OneJobTDMA.

  Section ExampleTDMA.

    Context {Job: eqType}.

    Let tsk1 := {| task_id := 1; task_cost := 1; task_period := 16; task_deadline := 15|}.
    Let tsk2 := {| task_id := 2; task_cost := 1; task_period := 8; task_deadline := 5|}.
    Let tsk3 := {| task_id := 3; task_cost := 1; task_period := 9; task_deadline := 6|}.

    Let time_slot1 := 1.
    Let time_slot2 := 4.
    Let time_slot3 := 3.

    Program Let ts := Build_set [:: tsk1; tsk2; tsk3] _.

    Let slot_seq := [::(tsk1,time_slot1);(tsk2,time_slot2);(tsk3,time_slot3)].

    Fact ts_has_valid_parameters:
      valid_sporadic_taskset task_cost task_period task_deadline ts.
      intros tsk tskIN.
      repeat (move: tskIN ⇒ /orP [/eqP EQ | tskIN]; subst; compute); by done.

    Let arr_seq := periodic_arrival_sequence ts.

    Fact job_arrival_times_are_consistent:
      arrival_times_are_consistent job_arrival arr_seq.
    apply periodic_arrivals_are_consistent.

    Definition time_slot task:=
      if task \in (map fst slot_seq) then
      let n:= find (fun tsktsk==task)(map fst slot_seq) in
       nth n (map snd slot_seq) n else 0.

    Fact valid_time_slots:
       tsk, tsk \in ts
        is_valid_time_slot tsk time_slot.
    apply/allP. by cbn.

    Definition slot_order task1 task2:=
      task_id task1 task_id task2.

    Let sched:=
      scheduler_tdma job_arrival job_cost job_task arr_seq ts time_slot slot_order.

    Let job_in_time_slot t j:=
      Task_in_time_slot ts slot_order (job_task j) time_slot t.

    Fact slot_order_total:
      slot_order_is_total_over_task_set ts slot_order.
    intros t1 t2 IN1 IN2. rewrite /slot_order.
    case LEQ: (_ _);first by left.
    right;move/negP /negP in LEQ;rewrite -ltnNge in LEQ;auto.

    Fact slot_order_transitive:
      slot_order_is_transitive slot_order.
    rewrite /slot_order.
    intros t1 t2 t3 IN1 IN2. lia.

    Fact slot_order_antisymmetric:
      slot_order_is_antisymmetric_over_task_set ts slot_order.
    intros x y IN1 IN2. rewrite /slot_order. intros O1 O2.
    have EQ: task_id x = task_id y by lia.
    case (x==y)eqn:XY;move/eqP in XY;auto.
    repeat (move:IN2⇒ /orP [/eqP TSK2 |IN2]); repeat (move:IN1=>/orP [/eqP TSK1|IN1];subst);compute ;try done.

    Fact respects_TDMA_policy:
      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts time_slot slot_order.
    intros j t ARRJ.
    - rewrite /sched_implies_in_slot /scheduled_at /sched scheduler_uses_construction_function /job_to_schedule.
      move ⇒ /eqP FUN. unfold job_in_time_slot.
      apply findP_in_seq in FUN.
      by destruct FUN as [ TskInSlot _].
      apply job_arrival_times_are_consistent.
    - rewrite /backlogged_implies_not_in_slot_or_other_job_sched /backlogged /scheduled_at /sched scheduler_uses_construction_function /job_to_schedule.
      move ⇒ /andP [PEN NOSCHED]. have NSJ:= NOSCHED.
      apply findP_notSome_in_seq in NOSCHED.
      destruct NOSCHED as [NOIN |EXIST].
      + by left.
      + case (Task_in_time_slot ts slot_order (job_task j) time_slot t) eqn:INSLOT;last by left.
        right. destruct EXIST as [y SOMEY]. y. have FIND:=SOMEY. apply findP_in_seq in SOMEY.
        move:SOMEY ⇒ [SLOTY YIN]. have ARRY: arrives_in arr_seq y
        by apply pendinglist_jobs_in_arr_seq in YIN.
        have SAMETSK: job_task j = job_task y.
        have EQ:Task_in_time_slot ts slot_order (job_task y) time_slot t =
                  Task_in_time_slot ts slot_order (job_task j) time_slot t by rewrite INSLOT.
        try ( apply task_in_time_slot_uniq with (ts0:= ts) (t0:=t) (slot_order:=slot_order) (task_time_slot:=time_slot);auto ) ||
        apply task_in_time_slot_uniq with (ts:= ts) (t:=t) (slot_order:=slot_order) (task_time_slot:=time_slot);auto.
        intros;by apply slot_order_total.
        by apply slot_order_antisymmetric.
        by apply slot_order_transitive.
        by apply periodic_arrivals_all_jobs_from_taskset.
        by apply valid_time_slots,periodic_arrivals_all_jobs_from_taskset.
        by apply periodic_arrivals_all_jobs_from_taskset.
        by apply valid_time_slots ,periodic_arrivals_all_jobs_from_taskset.
        × split;case (y==j)eqn:YJ;move/eqP in YJ;try by rewrite FIND YJ in NSJ;move/eqP in NSJ;auto.
          ( try ( apply pending_job_in_penging_list with (arr_seq0:=arr_seq) in PEN ) ||
          apply pending_job_in_penging_list with (arr_seq:=arr_seq) in PEN);auto
          ;last apply job_arrival_times_are_consistent.
          ( try ( apply findP_FIFO with (y0:=j) in FIND ) ||
          apply findP_FIFO with (y:=j) in FIND);auto. fold sched in FIND.
          apply (respects_FIFO ) in FIND;auto.
          apply periodic_arrivals_are_sporadic with (ts:=ts) in FIND;auto.
          have PERIODY:task_period (job_task y)>0 by
          apply ts_has_valid_parameters,periodic_arrivals_all_jobs_from_taskset. lia.
          apply job_arrival_times_are_consistent.
          apply periodic_arrivals_is_a_set,ts_has_valid_parameters.
          by apply/eqP.
      + apply pending_job_in_penging_list;trivial.
        × by apply job_arrival_times_are_consistent.
      + by apply job_arrival_times_are_consistent.

    Fact job_cost_le_task_cost:
       j : concrete_job_eqType,
      arrives_in arr_seq j
      job_cost_le_task_cost task_cost job_cost job_task j.
    intros JOB ARR.
    apply periodic_arrivals_valid_job_parameters in ARR.
    apply ARR. by apply ts_has_valid_parameters.

    Let tdma_claimed_bound task:=
      WCRT task_cost time_slot ts task.
    Let tdma_valid_bound task := is_valid_tdma_bound task_deadline task (tdma_claimed_bound task).

    Fact valid_tdma_bounds:
       tsk, tsk \in ts
        tdma_valid_bound tsk = true.
    rewrite /tdma_valid_bound /tdma_claimed_bound /WCRT /TDMA_cycle.
    rewrite bigopE. by compute.

    Fact WCRT_le_period:
       tsk, tsk \in ts
      WCRT task_cost time_slot ts tsk task_period tsk.
    rewrite /tdma_valid_bound /tdma_claimed_bound /WCRT /TDMA_cycle.
    rewrite bigopE. by compute.

    Let no_deadline_missed_by :=
      task_misses_no_deadline job_arrival job_cost job_deadline job_task arr_seq sched.

    Theorem ts_is_schedulable_by_tdma :
       tsk, tsk \in ts
        no_deadline_missed_by tsk.
    intros tsk tskIN.
    have VALID_JOB := periodic_arrivals_valid_job_parameters ts ts_has_valid_parameters.
    try ( apply taskset_schedulable_by_tdma with (task_deadline:=task_deadline)(task_period:=task_period)
    (task_time_slot:=time_slot) (slot_order:= slot_order)
    (arr_seq0:=arr_seq) ) ||
    apply taskset_schedulable_by_tdma with (task_deadline:=task_deadline)(task_period:=task_period)
    (task_time_slot:=time_slot) (slot_order:= slot_order)
    - apply job_arrival_times_are_consistent.
    - apply periodic_arrivals_are_sporadic.
    - apply scheduler_jobs_must_arrive_to_execute.
      apply job_arrival_times_are_consistent.
    - apply scheduler_completed_jobs_dont_execute.
      apply job_arrival_times_are_consistent.
    - assumption.
    - by apply WCRT_le_period.
    - by apply respects_TDMA_policy.
    - by apply valid_time_slots.
    - assumption.
    - by apply job_cost_le_task_cost.
    - apply valid_tdma_bounds;auto.

  End ExampleTDMA.

End ResponseTimeAnalysisExemple.