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.

    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).

    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.

    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.

    Lemma completes_at_end_time:
          job_completes_at (job_arrival j + job_response_time_tdma_in_at_most_one_job_is_pending).

    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.

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