Library rt.analysis.uni.basic.tdma_wcrt_analysis

Require Import Arith Omega Nat.
Require Import rt.util.all.
Require Import rt.model.arrival.basic.job
               rt.model.arrival.basic.task_arrival
               rt.model.schedule.uni.schedulability
               rt.model.schedule.uni.schedule_of_task
               rt.model.schedule.uni.response_time.
Require Import rt.model.schedule.uni.basic.platform_tdma
               rt.model.schedule.uni.end_time.


Module WCRT_OneJobTDMA.

Import Job TaskArrival ScheduleOfTask ResponseTime Platform_TDMA end_time Schedulability.

  (* In this section, we prove that any job j of task tsk will be completed by
     the computed value WCRT of the exact response-time analysis under TDMA scheduling policy
     on an uniprocessor, assuming that all its previous jobs have been completed by its arrival time. *)

  Section WCRT_analysis.

System model
    Context {sporadic_task: eqType}.
    Variable task_cost: sporadic_task time.
    Variable task_period: sporadic_task time.
    Variable task_deadline: sporadic_task time.

    Context {Job: eqType}.
    Variable job_arrival: Job time.
    Variable job_cost: Job time.
    Variable job_deadline: Job time.
    Variable job_task: Job sporadic_task.

    (* Consider any arrival sequence... *)
    Variable arr_seq: arrival_sequence Job.
    Hypothesis H_sporadic_tasks:
    sporadic_task_model task_period job_arrival job_task arr_seq.

    (* ..., any uniprocessor... *)
    Variable sched: schedule Job.
    (* ... where jobs do not execute before their arrival times nor after completion. *)
    Hypothesis H_jobs_must_arrive_to_execute:
      jobs_must_arrive_to_execute job_arrival sched.
    Hypothesis H_completed_jobs_dont_execute:
      completed_jobs_dont_execute job_cost sched.

    (* Consider any TDMA slot assignment... *)
    Variable task_time_slot: TDMA_slot sporadic_task.
    (* ... and any slot order. *)
    Variable slot_order: TDMA_slot_order sporadic_task.

    (* ... and any sporadic task set. *)
    Variable ts: {set sporadic_task}.
    Hypothesis H_valid_task_parameters:
    valid_sporadic_taskset task_cost task_period task_deadline ts.

    (* Consider any task in task set... *)
    Variable tsk:sporadic_task.
    Hypothesis H_task_in_task_set: tsk \in ts.

    (* ... and any job belongs to it. *)
    Variable j:Job.
    Hypothesis H_job_task: job_task j =tsk.
    Hypothesis job_in_arr_seq: arrives_in arr_seq j.
    Hypothesis H_valid_job:
      valid_sporadic_job task_cost task_deadline job_cost job_deadline job_task j.

    (* For simplicity, let us use local names for some definitions and refer them to local variables. *)
    Let time_slot:= task_time_slot tsk.
    Let slot_offset:= Task_slot_offset ts slot_order tsk task_time_slot.
    Let tdma_cycle:= TDMA_cycle ts task_time_slot.
    Let is_scheduled_at t:=
      scheduled_at sched j t.
    Let in_time_slot_at t:=
        Task_in_time_slot ts slot_order tsk task_time_slot t.
    Let pending_at:=
      pending job_arrival job_cost sched j.

    (* Recall definitions of end time predicate... *)
    Let job_end_time_predicate:= end_time_predicate sched j.
    (* ... and completes_at *)
    Let job_completes_at:=
    completes_at job_arrival job_cost sched j.

    (* Then, let's give some local definition for clarity. *)
    (* We define a formula that allows to calculate the distance 
      between time t and the previous start of tsk's time slot *)

    Let from_start_of_slot t:=
      ( t + tdma_cycle- slot_offset %% tdma_cycle) %% tdma_cycle.

    (* ... and a formula that allows to calculate the distance 
      between time t and the next start of its time slot *)

    Let to_next_slot t:=
      tdma_cycle - from_start_of_slot t.

    (* and a formula that allows to calculate the duration to finish
      a job if it is right at the start of its time slot and has 
      an execution cost c *)

    Let duration_to_finish_from_start_of_slot_with c:duration :=
      (div_ceil c time_slot -1) × (tdma_cycle - time_slot) + c.

    (* a formula that allows to calculate the duration between time t and the end of slot
       in case of time t in time slot *)

    Let to_end_of_slot t:=
      time_slot - from_start_of_slot t.

    (* Given the arrival time arr and job cost c, we define a formula for calculating the response time.
       This formula will be shown to be correct w.r.t. end_time_predicate *)

    Definition formula_rt (arr:instant) (c:duration):=
      if c ==0 then 0 else
      if in_time_slot_at arr then
              if c to_end_of_slot arr then
                   c
              else to_next_slot arr +
                    duration_to_finish_from_start_of_slot_with (c - to_end_of_slot arr)
        else
            to_next_slot arr + duration_to_finish_from_start_of_slot_with c.

    (* and the response time formula for job *)
    Definition job_response_time_tdma_in_at_most_one_job_is_pending:=
      formula_rt (job_arrival j) (job_cost j).

    (* Now, let's assume that task time slot is valid, and... *)
    Hypothesis H_valid_time_slot: is_valid_time_slot tsk task_time_slot.

    (* ... the schedule respects TDMA scheduling policy. *)
    Hypothesis TDMA_policy:
      Respects_TDMA_policy job_arrival job_cost job_task arr_seq sched ts task_time_slot slot_order.

    (* Assume that all previous jobs of same task have completed 
        before the arrive of this job of this task *)

    Hypothesis all_previous_jobs_of_same_task_completed :
       j_other,
        arrives_in arr_seq j_other
        job_task j = job_task j_other
        job_arrival j_other < job_arrival j
        completed_by job_cost sched j_other (job_arrival j).

First, we prove some basic lemmas about pending.
    Section BasicLemmas.
      (* We can prove that there is at most one job of a task is pending at
        any instant t *)

      Lemma at_most_one_job_is_pending:
         j_other (t : time),
          arrives_in arr_seq j_other
          job_arrival j_other < job_arrival j
          pending job_arrival job_cost sched j t
          pending job_arrival job_cost sched j_other t
          job_task j = job_task j_other j = j_other.

      (*Lemma: it respects TDMA policy for a particular case (job must be 
        finished before the next job's arrival), that is, the job can be always 
        scheduled at time t iff it is in its time slot at time t *)

      Lemma TDMA_policy_case_RT_le_Period:
         t,
          pending_at t
          reflect (in_time_slot_at t) (is_scheduled_at t).

      (* Job is pending at its arrival *)
      Lemma pendingArrival: pending_at (job_arrival j).

      (* Job is pending at t.+1 if 
          it is pending but isn't scheduled at t *)

      Lemma pendingSt:
         t,
          pending_at t
          is_scheduled_at t = false
          pending_at t.+1.

      (* Job is pending at t.+1 if
         it is both pending and scheduled at instant t 
         but there are 2 cost left at instant t *)

      Lemma pendingSt_Sched:
         t c,
          pending_at t
          service sched j t + c.+2 =job_cost j
          is_scheduled_at t = true
          pending_at t.+1.

    End BasicLemmas.

Next, we prove some generic lemmas about the response time formula and the end time predicate.
    Section formula_predicate_eq.

      (* Lemma: duration to next start of time slot is always positive *)
      Lemma to_next_slot_pos:
         t, to_next_slot t>0.

      (* Lemma: if the duration to next start of slot is a+1 at instant t
              imply the duration to next start of slot is a at instant t+1 *)

      Lemma lt_to_next_slot_1LR:
         a t,
          a.+1 < to_next_slot t
          a < to_next_slot t.+1.

      (* Lemma: if the duration to next start of slot is a+b at instant t
              imply the duration to next start of slot is a at instant t+b *)

      Lemma lt_to_next_slot_LR:
         b a t,
          a+b < to_next_slot t
          a < to_next_slot (t+b).

      (* Lemma: if the job cannot be scheduled at instant t and the duration to 
              next start is at least 1, thus the job cannot be scheduled at instant
              t+1 *)

      Lemma S_t_not_sched:
         t, pending_at t
         is_scheduled_at t = false
         1 < to_next_slot t
         is_scheduled_at t.+1 = false.

      (* Lemma: if the job cannot be scheduled at instant t and the duration to 
              next start is at least d, thus the job cannot be scheduled at instant
              t+d and is pending at t+d *)

      Lemma duration_not_sched:
         t,
          pending_at t
          is_scheduled_at t = false
           d, d < to_next_slot t
                    is_scheduled_at (t+d) = false pending_at (t+d).

      (* Lemma: if the job is pending but cannot be scheduled at instant t
        thus that the job is pending at t+ to_next_slot t *)

      Lemma pending_Nsched_sched:
         t,
          pending_at t
          is_scheduled_at t = false
          pending_at (t+ to_next_slot t).

      (* Lemma: It must be schedulable at next start of its time slot *)
      Lemma at_next_start_of_slot_schedulabe:
         t,
          pending_at t
          is_scheduled_at t = false
          is_scheduled_at (t+to_next_slot t) = true.

      (* Lemma: if the job cannot be scheduled at instant t and its residue cost is not
              0, so it has the same residue cost at instant t+1.
              the end time of this job is fixed whenever we calculate it *)

      Lemma formula_not_sched_St: t c, pending_at t
            is_scheduled_at t = false
            t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.+1.

      (* Lemma: if the job can be scheduled at instant t and its residue cost is not
              0 (c+1), so its residue cost will be consume 1 unit and remain c at
              instant t+1.
              the end time of this job is fixed whenever we calculate it *)


      Lemma formula_sched_St:
         t c,
          is_scheduled_at t = true
          t + formula_rt t c.+1 = t.+1 + formula_rt t.+1 c.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where 
                d < the duration to the start of the next slot from t *)

      Lemma formula_not_sched_interval:
         t c,
          pending_at t
          is_scheduled_at t = false
           d, d < to_next_slot t
                    t + formula_rt t c.+1 = t + d + formula_rt (t + d) c.+1.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, then its cost will be the same at the start of the next slot *)

      Lemma formula_not_sched_to_next_slot:
         t c, pending_at t
          is_scheduled_at t = false
          t + formula_rt t c.+1 = t + to_next_slot t + formula_rt (t + to_next_slot t) c.+1.

      (* Lemma: if the job cannot be scheduled at instant t and its residue cost is not
                null, and it will remain the same at the next start of slot + 1 *)

      Lemma job_not_sched_to_cunsume_1unit:
         t c, pending_at t
          is_scheduled_at t = false
          t + formula_rt t c.+1 = (t + to_next_slot t).+1 + formula_rt (t + to_next_slot t).+1 c.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where 
                d < the duration to the start of the next slot from t.
                lemma on end time predicate with forward direction *)

      Lemma end_time_predicate_not_sched_eq:
         d c t e ,
          pending_at t
          is_scheduled_at t = false
          job_end_time_predicate t c.+1 e
          d < to_next_slot t
          job_end_time_predicate (t+d) c.+1 e.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where 
                d < the duration to the start of the next slot from t.
                lemma on end time predicate with reverse direction *)

      Lemma end_time_predicate_not_sched_eq_rev:
         d c t e ,
          pending_at t
          is_scheduled_at t = false
          job_end_time_predicate (t+d) (S c) e
          d < to_next_slot t
          job_end_time_predicate t (S c) e.

      (* Lemma: if the job cannot be scheduled at instant t and its cost is not
                null, it will have the same cost at instant t+d, where 
                d < the duration to the start of the next slot from t.
               lemma on end time predicate *)

      Lemma end_time_predicate_eq:
         t c e,
          pending_at t
          is_scheduled_at t = false
            job_end_time_predicate t c.+1 e
            job_end_time_predicate ((t+to_next_slot t).+1) c e.

      (* Lemma: service received dont change if the job isn't scheduled *)
      Lemma service_is_zero_in_Nsched_duration:
         d t,
          pending_at t
          scheduled_at sched j t = false
          d to_next_slot t
          service sched j ( t + d) = service sched j t.

      (* Lemma: job completes at end time
        this lemma allows to valide the response time formula defined above *)

      Lemma completes_at_end_time_pre:
         c t , pending_at t service sched j t + c = job_cost j
        end_time_predicate sched j t c (t + formula_rt t c).

    End formula_predicate_eq.

Then we prove that job j completes at instant (arrival + response time) by (1) assuming that all its previous jobs have been completed by its arrival time and (2) basing on the basic and generic lemmas above.
Finally, we prove that job can be finished within the formula WCRT.
    Section ValidWCRT.

      (* Recall the definition of task_cost is exactly WCET, which is the worst-case execution time
          with respect to a job *)

      Let WCET := task_cost tsk.

      (* We define a formula for calculating the worst-case response time, which means
        job arrives at the end of its time slot with WCET *)

      Definition WCRT_formula cycle s wcet:=
        (div_ceil wcet s)*(cycle - s) + wcet.
      Definition WCRT:=
        WCRT_formula tdma_cycle time_slot WCET.

      (* Assume that job cost is always less than or equal to its task cost *)
      Hypothesis H_job_cost_le_task_cost: job_cost_le_task_cost task_cost job_cost job_task j.

      (* We prove that response time is always less than or equal to WCRT *)
      Lemma response_time_le_WCRT:
        job_response_time_tdma_in_at_most_one_job_is_pending WCRT.

      (* We show that this analysis is exact: job j's response time is equal to WCRT when
         (1) the job cost is equal to WCER; and
         (2) the job arrives right at the end of its time slot. *)

      Lemma exists_WCRT:
        job_cost j = WCET from_start_of_slot (job_arrival j)=time_slot
        job_response_time_tdma_in_at_most_one_job_is_pending = WCRT.

Main Theorem
      (* We prove that any job j of task tsk will be completed by the computed value WCRT,
         assuming that all its previous jobs have been completed by its arrival time. *)

      Theorem job_completed_by_WCRT:
        completed_by job_cost sched j (job_arrival j + WCRT).

    End ValidWCRT.

  End WCRT_analysis.

End WCRT_OneJobTDMA.